Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}

module foundations.UnivalenceAxiom where

open import foundations.TransportLemmas
open import foundations.EquivalenceType

open import foundations.HomotopyType
open import foundations.QuasiinverseType
open import foundations.QuasiinverseLemmas

Voevodsky’s Univalence axiom is postulated. It induces an equality between any two equivalent types. Some (β) and (η) rules are provided.

module _ {ℓ : Level} {A B : Type ℓ} where

  idtoeqv
    : A ≡ B
    --------
    → A ≃ B

  idtoeqv p =
    qinv-≃
      (coe p)
      ((!coe p) ,
        (coe-inv-l p , coe-inv-r p))

  ≡-to-≃ = idtoeqv
  ite     = idtoeqv
  cast    = idtoeqv  -- Used in the Symmetry Book.

The induces an equivalence between equalities and equivalences.

  postulate axiomUnivalence : isEquivalence idtoeqv

In Slide 20 from an , base on what we saw, we give the following no standard definition of Univalence axiom (without transport).

  open import foundations.HLevelTypes

  UA
    : ∀ {ℓ : Level}
    → (Type (lsuc ℓ))

  UA {ℓ = ℓ}  = (X : Type ℓ) → isContr (∑ (Type ℓ) (λ Y → (X ≃ Y)))

About this Univalence axiom version:

  eqvUnivalence
    : (A ≡ B) ≃ (A ≃ B)

  eqvUnivalence = idtoeqv , axiomUnivalence
  ≡-equiv-≃ = eqvUnivalence
  ≡-≃-≃     = eqvUnivalence

Introduction rule for equalities:

  ua
    : A ≃ B
    -------
    → A ≡ B

  ua = remap eqvUnivalence
  ≃-to-≡   = ua
  eqv-to-eq = ua

Computation rules

  ua-β idtoeqv-ua-β
    : (α : A ≃ B)
    ----------------------
    → idtoeqv (ua α) ≡ α

  ua-β eqv = lrmap-inverse eqvUnivalence
  idtoeqv-ua-β = ua-β

  ua-η
    : (p : A ≡ B)
    ---------------------
    → ua (idtoeqv p) ≡ p

  ua-η p = rlmap-inverse eqvUnivalence

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides