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

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][>>][..]