Fri Jun 15 02:23:15 EDT 2018


Homotopy Type Theory introduction lecture -- Robert Harper

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: