This is like TTFV, but for the more theory-minded people.
Plan
- From ΠΣ to inductive datatypes
- Primitive Agda
- Intuitionistic Logics
- Propositional
- Simply typed λ-calculus
- First-order
- λP₁
- Second-order
- HM and λ2
- Curry’s paradox
- High-order
- λP
- Axioms and Axiom schemes
- ? Finite Sets
- ? Models
- Peano Arithmetic and Agda
- Constructive Set Theory and Agda
- Russell’ paradox
- Curry’s paradox
- Universal set
- The law of the excluded middle, extrapolation to infinite sets
- ZF
- NBG
- Axiom of choice, Zorn’s lemma, Zermelo’s theorem
- Ordinals
- Up to ω
- Constructive
- Classical
- Arithmetic
- Burali-Forti paradox
- Cardinals
- Constructive
- Classical
- Arithmetic
- High-order Type Theories
- Pure Type Systems
- Martin-Löf Type Theory and variants
- “Axiom of choice” theorem
- Girard’s/Hurken’s paradox
Was this useful? Do you want me spending more time working on similar things?
Support me via:
- Patreon,
- Bitcoin (BTC) bc1q6hlk9v2jkw86yarve67dsmny6yej7jyhgsypxl (QR),
- Monero (XMR) 838KWx98i8o459fFqRSwzQaPdm7idUyASGujJqBbmUw2eHe541AaEnCKrk8GxrcJEwQCgTFMmZdD21q5C7Qo2ifJ7ydAsoa (QR),
- or any other cryptocurrency.