Univalence

1. Univalence

1 Univalence

module Lib.Univalence where

This file shows the univalence and applies the fundamental theorem of identity to univalence.

1.1 Packages imports

The imported packages can be accessed via the following links:

Lib/FundamentalTheorem

import Stdlib.Prelude
import Lib.FundamentalTheorem

1.2 Fundamental theorem of univalence

We state the fundamental theorem of univalence, that is: the fundamental theorem of identity for equivalences.

ua/is-contr-total-equiv (A : U) : is-contr (Σ U (Equiv A)) =
  let i : (B : U) → has-inverse (Path U A B) (Equiv A B) (path-to-equiv A B) = λB. (equiv-to-path A B, (equiv-to-path/comp A B, equiv-to-path/unique A B)) in
  fundamental-theorem-id' U
    ( Equiv A) A
    ( path-to-equiv A)
    ( λB. has-inverse/is-equiv
            ( Path U A B)
            ( Equiv A B)
            ( path-to-equiv A B)
            ( i B))

1.3 Equivalence between paths and equivalence

Path between types is equivalent to equivalence between types.

univalence (A B : U) : Equiv (Equiv A B) (Path U A B) =
  has-inverse/Equiv
    ( Equiv A B)
    ( Path U A B)
    ( equiv-to-path A B)
    ( path-to-equiv A B,
      ( equiv-to-path/unique A B,
        equiv-to-path/comp A B))

univalence' (A B : U) : Equiv (Path U A B) (Equiv A B) =
  has-inverse/Equiv
    ( Path U A B)
    ( Equiv A B)
    ( path-to-equiv A B)
    ( equiv-to-path A B,
      ( equiv-to-path/comp A B,
        equiv-to-path/unique A B))

Univalence

Table of Contents

1 Univalence

1.1 Packages imports

1.2 Fundamental theorem of univalence

1.3 Equivalence between paths and equivalence