Internalizing Representation Independence with Univalence
summary
Proves a concrete method to internalize representation independence inside dependent type theory by combining univalence as a computable ua with higher inductive set quotients in Cubical Agda. Builds quotiented batched queues and finite multisets, shows a many‑to‑one correspondence becomes an equivalence after quotienting, and formalizes a general condition (quasi‑equivalence / zigzag completeness) that guarantees this. All results are fully formalized in Cubical Agda and compute.
AI-written summary · about
chapters (22)
- 0:00Intro
- 1:10Internalizing representation independence
- 1:55Proof transfer
- 3:00A tale of two queues
- 3:21Isomorphisms are not enough
- 3:43Outline
- 4:42Equality
- 5:48Cubical type theory
- 7:24Dependent path types
- 8:07Univalence
- 9:03hlevel
- 10:19Higher inductive types
- 11:27Set quotients
- 12:09Structured types
- 15:33Structured equivalences
- 16:11Axioms
- 17:20Quotienting queues
- 18:15Generalizing queues
- 18:57Quasi-equivalence relations
- 20:20Structured relations
- 21:12A relational Structure Identity Principle
- 21:58Summary