📐

Foundations

Martin-Löf Type Theory, dependent types, universe hierarchies, Curry-Howard, constructive mathematics, and the logical bedrock of it all. nya~

This subforum is dedicated to the theoretical foundations of type theory and constructive mathematics. Discuss Martin-Löf Type Theory (MLTT), Pi-types, Sigma-types, universe hierarchies, the Curry-Howard correspondence, and the philosophy of propositions as types. All skill levels welcome — from "what is a judgement?" to Voevodsky-level shenanigans. Keep it constructive (pun intended). 🐾

📌 Before posting: Check the Foundations Reading List megathread first!
📂 Sub-categories
🧩 MLTT Deep Dives
🔮 HoTT & Univalence
🧊 Cubical Type Theory
🗂️ Type Theory vs Set Theory
⚖️ Constructive Logic
312 Threads
4,871 Posts
89 Members
Last post: universePolyNya — 14 min ago
✏️ New Thread 🕐 Latest 🔥 Most Active ❓ Unanswered
Sort by: Topic | Author | Replies | Views | Last Post Showing threads 1–20 of 312
Topic Replies Views Last Post
📌
PIN 📚 Foundations Reading List & Resource Megathread [UPDATED 2025]
megathread resources by lambdaNeko · Started 2024-03-01
203replies 18.4kviews by sigmaKitty 2 hrs ago
📌
PIN ❓ MLTT FAQ: Judgements, Formation, Introduction, Elimination — Beginner's Guide
faq mltt beginners by perMartin · Started 2024-03-15
97replies 12.1kviews by betaReducer 1 day ago
🔥
HOT Intensional vs Extensional MLTT — which is the "real" Martin-Löf?
mltt identity-types philosophy by nyaTypist · Started 2025-01-08
148replies 9,302views by extensionNya 14 min ago
✨
NEW ELI5: What even IS a Π-type (Pi-type) and why should I care?
pi-types dependent-functions beginners by flopEarNeko · Started 2025-03-26
23replies 1,204views by piFormerNya 2 hrs ago
✨
NEW Σ-types as existential statements — a worked example thread
sigma-types existentials worked-examples by sigmaKitty · Started 2025-03-25
31replies 2,019views by pairIntroNya 5 hrs ago
💬
The Curry-Howard Correspondence: Proofs as Programs, Types as Propositions
curry-howard propositions-as-types history by lambdaNeko · Started 2024-09-11
87replies 7,541views by howardCat 3 days ago
🔥
HOT Universe hierarchies and Girard's Paradox — "Type : Type" considered dangerous
universes universe-polymorphism paradoxes by girardNya · Started 2024-11-03
112replies 8,840views by universePolyNya 14 min ago
💬
Propositions as Types — deep dive into the BHK interpretation and its consequences
propositions-as-types bhk-interpretation intuitionism by brouwerPaw · Started 2024-08-20
54replies 4,412views by intuitionistCat 1 week ago
💬
Identity types and the J-eliminator — what does it compute, actually?
identity-types j-eliminator mltt by reflNeko · Started 2024-10-30
76replies 5,103views by jElimCat 4 days ago
💬
Why constructivists reject the Law of Excluded Middle — and what they use instead
constructive-math LEM intuitionism by nyaTypist · Started 2024-07-17
93replies 6,778views by classicalEvil 2 days ago
✨
NEW Function Extensionality: axiom or theorem? Does MLTT need it?
funext extensionality axioms by extNyaFun · Started 2025-03-22
19replies 843views by univalentNya 1 day ago
💬
W-types and general inductive types — the secret engine behind recursion in MLTT
w-types inductive-types recursion by wellFounded · Started 2024-12-05
41replies 2,918views by inductionCat 5 days ago
💬
Natural Deduction vs Sequent Calculus — which presentation do you prefer for type theory?
natural-deduction proof-theory sequent-calculus by gentzenNya · Started 2024-06-14
62replies 3,511views by cutElimNeko 3 days ago
💬
Predicativity: why can't we just have impredicative universes and be done with it?
predicativity universes set-theory by ramifiedNya · Started 2024-09-28
58replies 3,204views by propTypeNya 1 week ago
💬
Reading Group: Per Martin-Löf's 1984 Bibliopolis lectures — Chapter by Chapter
reading-group mltt bibliopolis classic by perMartin · Started 2024-04-01
134replies 9,971views by biblioNeko 2 days ago
✨
NEW Definitional equality is making me lose my mind — how do you actually check it?
definitional-equality beta-reduction help by confusedKitten · Started 2025-03-24
28replies 1,554views by normNya 18 hrs ago
💬
Dependent pairs (Σ-types) vs record types — when to use which?
sigma-types records agda by sigmaKitty · Started 2025-01-29
37replies 2,103views by recordNya 6 days ago
🔒
[LOCKED] Type Theory vs Set Theory — debate got too spicy nya (see rules)
locked debate by setNyaFan · Started 2024-08-05
219replies 11.2kviews by mods_nya 6 months ago
💬
Locally cartesian closed categories as models of dependent type theory — Seely's theorem explained
categorical-semantics lccc models by categoryNya · Started 2024-11-22
44replies 3,008views by seelyNeko 4 days ago
✨
NEW Universe polymorphism in Agda — how does Level work under the hood?
universe-polymorphism agda level by universePolyNya · Started 2025-03-27
7replies 318views by agdaNeko 14 min ago
✏️ Post New Thread

🐱 Online in Foundations

universePolyNya
piFormerNya
sigmaKitty
betaReducer
+ 12 guests lurking

📊 Subforum Stats

Total threads: 312
Total posts: 4,871
Newest member: axiomdNya
Most active: lambdaNeko (841 posts)

🔗 Quick Links

📚 Reading List
❓ MLTT FAQ
📖 MLTT Wiki Page
🛠️ Proof Assistants Forum
🔮 HoTT Forum

📌 Did You Know?

Σ (Sigma) types play double duty: as dependent pairs, they encode existential statements. A proof of ∃x.P(x) is literally a pair (a, proof that P(a))! nya~

Π (Pi) types encode universal statements and dependent functions. When B doesn't depend on x, Π(x:A).B is just the ordinary function type A→B.