HoTT & Cubical

🌀

Homotopy Type Theory, Cubical Agda, univalence axiom, higher inductive types,
synthetic homotopy theory, path induction, identity types, and all things ∞-groupoid.
Propositional equality is interpreted as homotopy — and we do it with catgirl energy. nya~

247 Threads
1,893 Posts
89 Members

📖 About This Subforum

HoTT relates Martin-Löf's system of intensional, constructive type theory with abstract homotopy theory — types as spaces, terms as points, proofs of equality as paths. Cubical Agda gives computational meaning to the univalence axiom and higher inductive types, making ua a theorem rather than an axiom. Whether you're working through the HoTT Book, formalizing in Agda, or just trying to understand why refl : Path A x x = λ i → x, you're in the right place. 🐱

Moderators: CubicalCat, UnivalenceFan, PathKitty

[ + New Thread ] 🔍 Search This Forum

Page: 1 2 3 »

	Thread	Replies	Views	Last Post
📌	ANNOUNCE Rules & Resources for HoTT & Cubical — READ BEFORE POSTING Started by CubicalCat · Links to HoTT Book, agda/cubical library, and community guidelines nya~	3	4,201	CubicalCat 2025-11-01 09:14
📌	STICKY READING GROUP [ONGOING] HoTT Book Reading Group — Weekly Chapter Discussion Thread Started by UnivalenceFan · Currently on Ch.8: Homotopy Theory. All welcome, beginners encouraged! 🐾	142	8,877	PathKitty 2026-03-26 23:41
📌	STICKY GUIDE How to Set Up Cubical Agda + agda/cubical Library (2025 Edition) Started by CubicalCat · Step-by-step setup, `--cubical` flag, common pitfalls, nya~	37	5,614	CubicalCat 2026-01-15 16:05
🔥	HOT Why does univalence have computational content in Cubical but not book HoTT? Started by FiberFeline · Great discussion on ua as theorem vs axiom, transport reduction, glue types	68	3,201	UnivalenceFan 2026-03-27 02:18
💬	NEW Path Induction (J eliminator) — an intuitive guide with cat-themed examples Started by CubicalCat · Deriving transport, ap, sym, trans from J. Includes Agda code snippets!	29	1,840	NyaTerminal 2026-03-26 21:55
💬	Higher Inductive Types — what are they and why do we need them? Started by MewMorphism · S¹, torus, suspensions, truncations, pushouts — defining spaces with path constructors	51	2,773	UnivalenceFan 2026-03-25 14:32
💬	HOT Identity Types in HoTT vs. Book HoTT vs. Cubical — what's the actual difference? Started by UnivalenceFan · Comparing Id type, Path type, PropEq... I keep confusing myself orz	84	4,150	CubicalCat 2026-03-24 19:07
💬	Synthetic homotopy theory in HoTT — computing π₁(S¹) = ℤ Started by ToposTail · The encode-decode method, universal cover, winding numbers in type theory	43	2,019	PathKitty 2026-03-23 11:44
💬	SOLVED [Cubical Agda] Defining S¹ as a HIT and proving loop ≠ refl Started by FiberFeline · `data S¹ : Set where base : S¹ ; loop : base ≡ base` — then what?	22	1,388	CubicalCat 2026-03-22 08:53
💬	Function Extensionality: why is it not provable in MLTT but holds in Cubical? Started by LambdaLynx · funExt in cubical is definable, not an axiom — it has computational content!	31	1,712	UnivalenceFan 2026-03-21 17:29
💬	NEW Struggling with transport and coercion in Cubical Agda — help me out nya~ Started by NyaTerminal · The transp primitive, `subst`, heterogeneous PathP, and when they don't reduce	17	609	CubicalCat 2026-03-27 01:03
💬	n-Truncations, h-levels, and the hierarchy of types in HoTT Started by UnivalenceFan · Propositions (-1), sets (0), groupoids (1)… when does it stop?! 😿	57	2,444	MewMorphism 2026-03-20 22:11
💬	READING GROUP HoTT Book Ch.2 Exercises — stuck on 2.17 (the torus) Started by KanComplexKitty · Cross-posting from reading group thread for more visibility	14	877	PathKitty 2026-03-19 15:38
💬	HOT Glue Types in CCHM Cubical Type Theory — a guided tour Started by CubicalCat · How Glue makes univalence work computationally. With diagrams (ASCII art edition)!	73	3,891	UnivalenceFan 2026-03-18 09:22
💬	Propositions-as-Types vs Propositions-as-(-1)-Types in HoTT Started by ToposTail · Proof-relevance, squash types, propositional truncation. When should we use which?	46	2,108	LambdaLynx 2026-03-17 20:55
💬	SOLVED The Structure Identity Principle (SIP) in Univalent Foundations — formalized in Cubical Agda Started by UnivalenceFan · Isomorphic structures are equal! Formalizing SIP for groups, rings, etc.	38	1,654	CubicalCat 2026-03-16 13:07
💬	Loop Spaces and Ω-types in HoTT — building up to homotopy groups Started by FiberFeline · ΩA = (a₀ = a₀), iterated loop spaces, πₙ as set-truncated nth loop space	26	1,290	MewMorphism 2026-03-15 18:44
💬	Quotient Types in Cubical Agda — integers as ℤ = ℕ × ℕ / ~ Started by NyaTerminal · Using HITs for quotients, setquot, effectiveQuotient. Much cleaner than setoids!	19	998	CubicalCat 2026-03-14 10:31
💬	Kan Composition — what is it and why does Cubical need it? Started by KanComplexKitty · From Kan complexes in simplicial sets to the hcomp operation in type theory	34	1,503	UnivalenceFan 2026-03-13 22:09
💬	NEW The Rezk Completion in HoTT — precategories vs. categories Started by ToposTail · Chapter 9 of the HoTT Book. Why do we need to impose univalence on categories?	11	543	ToposTail 2026-03-27 00:47
💬	PathP (heterogeneous paths) — when to use them and how to avoid universe issues Started by LambdaLynx · `PathP (λ i → A i) a0 a1` vs `subst`-ing into homogeneous paths	23	1,044	CubicalCat 2026-03-12 14:18
🔒	LOCKED [MEGATHREAD] HoTT vs. Set Theory as Foundations — the eternal debate Started by UnivalenceFan · Locked after 400+ posts. Summary pinned. Please don't restart this nya~	412	18,022	UnivalenceFan 2025-08-14 11:00

[ + New Thread ]

Page: 1 2 3 »

👥 Users browsing this subforum: CubicalCat, UnivalenceFan, FiberFeline, 7 guests · Total: 10 users