Univalence

#lang rzk-1

Given two functions f : A → B and g : A → B, we define a homotopy from f to g as point-wise equality:

#define homotopy
  ( A B : U)
  ( f g : A → B)
  : U
  := (x : A) → f x = g x

Following HoTT Book, we say that a function f : A → B is an equivalence if it has both a retraction (left inverse) and a section (right inverse):

#define is-equiv
  ( A B : U)
  ( f : A → B)
  : U
  := prod
      ( Σ (r : B → A), homotopy A A (\ a → r (f a)) (identity A))
      ( Σ (s : B → A), homotopy B B (\ b → f (s b)) (identity B))

Two types A and B are equivalent if there exists an equivalence f : A → B:

#define Equiv
  ( A B : U)
  : U
  := Σ (f : A → B), is-equiv A B f

An example of an equivalence is an identity function:

#define is-equiv-identity
  ( A : U)
  : is-equiv A A (identity A)
  := ((identity A , \ _ → refl)
     , (identity A , \ _ → refl))

We can show that Equiv is an equivalence relation:

-- Equiv is reflexive
#define Equiv-identity
  ( A : U)
  : Equiv A A
  := (identity A, is-equiv-identity A)

-- #define Equiv-sym
--   (A B : U)
--   : Equiv A B → Equiv B A
--   := \ (f , ((r, rf-eq), (s, fs-eq))) →
--        (s , ((f, fs-eq), (f, _exercise)) )

Univalence axiom (HoTT Book Axiom 2.10.3) states that equality of types is equivalence to equivalence of types¹:

#define UnivalenceAxiom
  : U
  :=
    ( A : U)
  → (B : U)
  → Equiv (A = B) (Equiv A B)

#postulate ua : UnivalenceAxiom

#define inv
  ( A B : U)
  : Equiv A B → (B → A)
  := \ (f, ((r, er), (s, es))) → r

#define eq-from-Equiv
  ( A B : U)
  : Equiv A B → (A = B)
  := inv (A = B) (Equiv A B)
        ( ua A B)

---

1. Here we postulate the equivalence, although, it is sufficient to say that a function idtoequiv : (A = B) → (Equiv A B) is an equivalence. ↩