Introduction to Intuitionistic Type Theory
summary
Claims a workable type theory that drops sets and the law of excluded middle and uses Topos Theory and category constructions to get dependent types and logic; builds products, exponentials, Omega and subtypes as monomorphisms, derives equality and singletons from the diagonal, and defines conjunction disjunction implication quantifiers and a maybe monad; demonstrates on Set^2 (two moments in time) that double negation fails so negation is intuitionistic, and shows these constructions actually compose and classify as advertised.
AI-written summary · about
chapters (23)
- 0:00Intro
- 2:20Motivation
- 5:06Types in "Before/After"
- 7:15Start from Ground Zero
- 11:11Terminal Type T
- 12:34Applying Function to Instance
- 14:14Product Type, aka Forming Pairs
- 16:41Diagonal Function
- 18:58Currying (Exponential Type)
- 22:06Eval Function
- 26:28Power Type Type of all subtypes of iso
- 27:40Equality, Singleton, Membership
- 31:23Equalizer Type
- 32:44Pullback Type
- 33:22Empty Type Empty type: Nothing, Unique for each a We can build it
- 34:42Meet False It classifies the inclusion of Empty type into Unit type
- 36:18More Logic Conjunction
- 38:25Even More Logic Partial order on Logical type tabla bwa
- 40:37Quantifiers. V
- 43:01Bonus: Maybe Monad Given a partial map..
- 44:33"Before/After" Logic Modeled Set is trivial four old Boolean stull
- 47:15Alternative Representation
- 51:16References
related talks
56mCalculating Intuitionistic Logic in Scala
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
19mIll-Typed Programs Don't Evaluate
51mA Gentle Introduction to Modern Model Theory
51mCategory Theory for the Working Hacker
19mType Inference Logics
25mShallowly embedding type theories
18mA modal deconstruction of Löb induction