{-# OPTIONS --postfix-projections --without-K #-} module index where {- Agda formalization for some of the details of the construction of - path and reflexive-loop models of HoTT. -} {- - The module HoTT is a basic HoTT library (identity types, - contractibility, equivalences, W-types). -} import HoTT {- The only postulates are function extensionality and the univalence - axiom. -} funext = HoTT.funext ua = HoTT.ua {- The only inductive types used are the identity types and - W-types. -} Id = HoTT.Id W = HoTT.W {- Indexed W-types are used in the construction of W-Equiv and - W-IsRefl, but they can be derived from Id and W -} IW₀ = HoTT.IW₀ {- The module RelEquiv contains definitions of relational equivalences - and reflexivity structures for Σ, Π, W and universes. -} import RelEquiv Σ-Equiv = RelEquiv.Σ-Equiv Σ-IsRefl = RelEquiv.Σ-IsRefl {- The contractibility witnesses for Σ-Equiv and Σ-IsRefl are - constructed using the lemma is-contr-ΣΣ. -} is-contr-ΣΣ = HoTT.is-contr-ΣΣ Π-Equiv = RelEquiv.Π-Equiv Π-IsRefl = RelEquiv.Π-IsRefl {- The contractibility witnesses for Π-Equiv and Π-IsRefl are - constructed using the lemma is-contr-ΣΠ. -} is-contr-ΣΠ = HoTT.is-contr-ΣΠ W-Equiv = RelEquiv.W-Equiv W-IsRefl = RelEquiv.W-IsRefl {- Due to the isomorphism - W A B ≅ (a : A) × (B a → W A B), - the contractibility witnesses for W-Equiv and W-IsRefl are - constructed using both is-contr-ΣΣ and is-contr-ΣΠ, recursively. -} Univ-Equiv = RelEquiv.Univ-Equiv Univ-IsRefl = RelEquiv.Univ-IsRefl {- The constructions of Univ-Equiv and Univ-IsRefl rely on univalence - and on equivalences - Equiv A B ≃ equiv A B, - IsRefl E ≃ (∀ a → E .equiv-rel a a) -} Equiv↔equiv = RelEquiv.Equiv↔equiv IsRefl↔refl = RelEquiv.IsRefl↔refl