{-# 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