Foundations README
- Preamble: Basics of the UniMath type theory: universes, type constructors, some base types, notation
- PartA: Path algebra, contractibility, homotopy fibers, weak equivalences, sums
- PartB: Homotopy levels
- UnivalenceAxiom: Univalence Axiom (UA), proof of function extensionality from UA
- PartC: Decidability
- PartD: Spaces of weak equivalences
- Propositions: Intuitionistic logic on propositions, propositional truncation
- Sets: Constructions of set-level quotients
MoreFoundations README
Mirrors the file structure of Foundations, contains convenient variants of results in Foundations