[<<][math][>>][..]
Fri Jun 15 02:23:15 EDT 2018

Brouwer

Homotopy Type Theory introduction lecture -- Robert Harper
https://www.youtube.com/watch?v=ISq1xi-mGk8&list=PLo61mJSqK5cXHsnYUAXNea31BCj1u-zln

Brouwer: Proofs are mathematical objects.

Different idea that just formal proofs (Goedel's theorem is about formal
proof being strictly limiting, compared to the proof "outside").

Difference between HoTT way of thinking about proofs and just proofs
in set theory encoded in Coq.

Synthetic (abstract) vs. Analytic (nuts & bolts, Bourbaki tedious).


Lecture 2: Entailment (Logical consequence)

Mapping (entailment) becomes internalized (implication).

Entailment and implication are not the same thing:
https://philosophy.stackexchange.com/questions/12816/difference-between-implication-conditional-and-logical-entailment



[Reply][About]
[<<][math][>>][..]