Univalence—Ⅰ

Contents

1. More about the identity principle in types
2. Function extensionality
3. Application: Universal Properties
4. The Univalence Axiom

---

{-# OPTIONS --without-K --safe #-}

module univalence-base where

open import mltt
open import twocatconstructions
open import negation hiding (Id-to-Fun; Id-to-Fun') --redefine them here
open import basichomotopy

open ≡-Reasoning
open ◾-lemmas
open ap-lemmas

More about the identity principle in types

An underlying (minor) theme is the identity principle in types: how to prove that a b : A ⊢ a ≡ b based on some more elementary construction possibly available about A. For example, in Σ-types, we often reduce the task of proving u ≡ v to that of proving π₁ u ≡ π₁ v and u ╝ v. This is a form of identity principle. Note that, in the simpler case of a Cartesian product, it will reduce an equality of two pairs to a pair of equalities amongst the components. It is actually convenient to state it here in this form, in order to not appeal to PathPair in these simpler situations:

apₚₐᵢᵣ : ∀{ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y : A × B} → 
      x ≡ y → ((π₁ x) ≡ (π₁ y)) × ( (π₂ x) ≡ (π₂ y) )
apₚₐᵢᵣ p = (ap π₁ p) , (ap π₂ p)

ap' = apₚₐᵢᵣ -- more practical


pair⁼ : ∀{ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y : A × B} → 
        ((π₁ x) ≡ (π₁ y)) × ( (π₂ x) ≡ (π₂ y) ) → x ≡ y
pair⁼ {x = x1 , x2} {y = .x1 , .x2} (refl , refl) = refl

The idea is straightforward: ap' sends an identification to the pair of its projections (via ap π₁ and ap π₂). A function in the opposite direction is defined by path induction and we prove that it is an equivalence:

ap'-iseq : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y : A × B} →
          x ≡ y ≃ ((π₁ x) ≡ (π₁ y)) × ( (π₂ x) ≡ (π₂ y) )
Σ.fst ap'-iseq = ap'
Σ.fst (Σ.fst (Σ.snd ap'-iseq)) = pair⁼
Σ.snd (Σ.fst (Σ.snd ap'-iseq)) = λ u → ap'-pair⁼ u
  where
      ap'-pair⁼ : ∀{ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y : A × B}
                (u :  (π₁ x ≡ π₁ y) × (π₂ x ≡ π₂ y)) → 
                (ap' ∘′ pair⁼) u ≡ u
      ap'-pair⁼ {x = x1 , x2} {.x1 , .x2} (refl , refl) = refl
Σ.fst (Σ.snd (Σ.snd ap'-iseq)) = pair⁼
Σ.snd (Σ.snd (Σ.snd ap'-iseq)) = λ u → pair⁼ap' u
  where
      pair⁼ap' : ∀{ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y : A × B} 
                (u : x ≡ y) → (pair⁼ ∘′ ap') u ≡ u
      pair⁼ap' {x = x} {.x} refl = refl

Such a principle can be established for other types: let us look at 𝟙, the unit type.

We know that 𝟙 is contractible, and that anything contractible is weakly equivalent to it. The question is, what about its “path space,” namely what about the type x ≡ y when x y : 𝟙? In fact we can already prove that up to equivalence 𝟙 has only one term. We do this as follows:

x=y:𝟙-is-𝟙 : {x y : 𝟙} → (x ≡ y) ≃ 𝟙
Σ.fst x=y:𝟙-is-𝟙 = λ _ → *
Σ.fst (Σ.snd x=y:𝟙-is-𝟙) = (λ _ → refl) , (λ _ → refl)
Σ.fst (Σ.snd (Σ.snd x=y:𝟙-is-𝟙)) = λ _ → refl
Σ.snd (Σ.snd (Σ.snd x=y:𝟙-is-𝟙)) = λ {refl → refl}

Incidentally, we can produce an alternative proof based on our previous analysis of contractibility:

x=y:𝟙-is-𝟙' : {x y : 𝟙} → 𝟙 ≃ (x ≡ y)
x=y:𝟙-is-𝟙' {x} {y} = contr-is-we-to-𝟙 is
                        where
                           is : iscontr (x ≡ y)
                           is = refl , λ { refl → refl}

Above we used the extended λ-syntax: λ{ x → ?}. It allows case-splitting within the lambda abstraction.

However, we may not be able to prove something analogous in other types. Case in point is that of Π-types: here having (=proving) an identity principle f ≡ g for two function terms f g : Π A P amounts to the following: assuming P : A → 𝓤, a dependent type, we must prove the equivalence:

f ≡ g ≃ Π[ x ∈ A ] (f x ≡ g x)

in other words,

f ≡ g ≃ f ~ g

This is known as function extensionality, which says that two function terms are equal if and only if they have the same values, where “same” means equal in the sense of propositional equality.

This cannot be done within the Type Theory we have so far developed. All we can say is that

happly : ∀ {ℓ ℓ'} {A : Set ℓ} {P : A → Set ℓ'} (f g : Π[ x ∈ A ] P x) →
         f ≡ g → f ~ g
happly f g p = λ x → ap (ev' x) p

where we have applied the evaluation function at x : A. It can of course be proved by path induction

happly' : ∀ {ℓ ℓ'} {A : Set ℓ} {P : A → Set ℓ'} (f g : Π[ x ∈ A ] P x) →
          f ≡ g → f ~ g
happly' f .f refl x = refl

but the first version is more elegant (due to MHE).

top ⇑

---

Function extensionality

Function extensionality can be assumed as an “axiom,” without compromising the integrity of the theory, by defining its type, and then assuming it in a module. One way to state it is to claim that happly is in fact a weak equivalence:

hfunext : (ℓ ℓ' : Level) → Set (lsuc (ℓ ⊔ ℓ'))
hfunext ℓ ℓ' = {A : Set ℓ} {P : A → Set ℓ'} (f g : Π A P) → iseq (happly f g) 

There are variants of the same postulate. For example, we can simply require that there exists a function in the opposite direction:

dfunext : (ℓ ℓ' : Level) → Set (lsuc (ℓ ⊔ ℓ'))
dfunext ℓ ℓ' = {A : Set ℓ} {P : A → Set ℓ'} (f g : Π A P) → f ~ g → f ≡ g

Of course, Voevodsky proposed an alternative: function extensionality is equivalent to saying that products of contractible types are themselves contractible:

vfunext : (ℓ ℓ' : Level) → Set (lsuc (ℓ ⊔ ℓ'))
vfunext ℓ ℓ' = {A : Set ℓ} {P : A → Set ℓ'} → (Π A (λ x →  iscontr (P x))) → iscontr (Π A P)

Here is how to use these axioms. We do not include the code, say:

postulate
  funext : dfunext

This would hold unconditionally in our development and it would also be incompatible with the clause --safe we are including at the top of each of our files (precisely to ensure that we do not accidentally render things inconsistent by being to trigger-happy with the postulate clause). Instead, we could declare something like:

hfunext→funext : ∀ {ℓ ℓ'} (hfe : hfunext ℓ ℓ') {A : Set ℓ} {P : A → Set ℓ'}
                 (f g : Π A P) → f ~ g → f ≡ g 
hfunext→funext hfe f g = π₁ (iseq→qinv (happly f g) (hfe f g))

This assumes that function extensionality holds and then extracts the inverse. Better yet, we put everything inside a module. Let us demonstrate how to do this to prove, under the assumption that function extensionality holds, a few properties of Π-types:

module Π-lemmas {ℓ ℓ' : Level} {A : Set ℓ} {P : A → Set ℓ'} 
                (hfe : hfunext ℓ ℓ') -- here the postulate holds
                where

  open ~-lemmas

  funext : (f g : Π A P) → f ~ g → f ≡ g
  funext f g = π₁ (iseq→qinv (happly f g) (hfe _ _))

  Π-id : {f : Π A P} → f ≡ f
  Π-id {f} = funext f f ~-refl

  Π-inv : {f g : Π A P} → f ≡ g → g ≡ f
  Π-inv {f} {g} α = funext g f ((happly f g α) ~⁻¹)

  Π-◾ : {f g h : Π A P} → f ≡ g → g ≡ h → f ≡ h
  Π-◾ {f} {g} {h} α β = funext f h ((happly f g α) ~◾~ (happly g h β))

top ⇑

---

Application: Universal Properties

As a small application to illustrate how to use function extensionality, let us look at some familiar universal properties. For a simple example, we consider the Cartesian Product.

-- private

By uncommenting the above line we make the whole module private, so it will not be in scope in any module that imports univalence-base.

module Univ-Cart-Prod where

We prove, using function extensionality, that the function

Σ[ g ∈ (Π A P) ] (Π[ x ∈ A ] (Q x (g x)))  → Π[ x ∈ A ] ( Σ[ u ∈ P x ] (Q x u) )

we showed to be the section of a retraction is actually an equivalence.

    ΣΠ-univ-is-equiv : ∀ {ℓ ℓ' ℓ''} {A : Set ℓ} {P : (x : A) → Set ℓ'} {Q : (x : A) (u : P x) → Set ℓ''} →
                       (dfe : dfunext ℓ (ℓ' ⊔ ℓ'')) → 
                       (Σ[ g ∈ (Π A P) ] (Π[ x ∈ A ] (Q x (g x))))  ≃ (Π[ x ∈ A ] ( Σ[ u ∈ P x ] (Q x u) ))
    ΣΠ-univ-is-equiv {A = A} {P} {Q} dfe = s , qinv→iseq s isinv-s
      where
        s : Σ (Π A P) (λ g → Π A (λ x → Q x (g x))) → Π A (λ x → Σ (P x) (Q x))
        s (g , h) = λ x → (g x) , (h x)

        r : Π A (λ x → Σ (P x) (Q x)) → Σ (Π A P) (λ g → Π A (λ x → Q x (g x)))
        r f = (λ x → π₁ (f x)) , (λ x → π₂ (f x))

        isinv-s : qinv s
        Σ.fst isinv-s = r
        Σ.snd isinv-s = ε , η
          where
            ε : s ∘′ r ~ id
            ε f = dfe (s (r f)) f H
              where
                H : s (r f) ~ f
                H x =  PathPair→PathΣ pp
                  where
                    pp : s (r f) x ╝ f x
                    pp = refl , refl

            η : r ∘′ s ~ id
            η = λ { (g , h) → refl}

top ⇑

---

The Univalence Axiom

For two types A and B in the given universe, we have previously defined a function Id-to-Fun : A ≡ B → (A → B). We do the same here (with slightly different names), which is why they are hidden in the import. Like before, we define two versions: the first by transporting with respect to the identity function of the universe id : 𝓤 → 𝓤, if 𝓤 = Set ℓ, along an identification p : A ≡ B; the second, by path induction.

Id→Fun : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
Id→Fun {ℓ}  =  transport (id {A = Set ℓ})

Id→Fun' : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
Id→Fun' {ℓ} {A} {.A} refl = id

Id→Funs-agree : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → Id→Fun p ≡ Id→Fun' p
Id→Funs-agree {ℓ} {A} {.A} refl = idp (id {A = A})

By path induction, any equality (i.e. homotopy in a higher universe) between types gives an equivalence

Id→Eq' : ∀ {ℓ} (A B : Set ℓ) → A ≡ B → A ≃ B
Id→Eq' A .A refl = ≃id {A = A}
  where
    open ≃-lemmas

Id→Eq : ∀ {ℓ} (A B : Set ℓ) → A ≡ B → A ≃ B
Id→Eq {ℓ} A B p = (Id→Fun p) , transport-is-≃ (id {A = Set ℓ}) p

therefore we naturally get a function from the idenity type A ≡ B to that of weak equivalences A ≃ B.

Voevodsky’s Univalence Axiom posits that Id→Eq is itself an equivalence. As for function extensionality, it is formulated to be used whenever required by simply providing the predicate (=type) that for any pair of types Id→Eq is a weak equivalence. Alternatively, we can give the type of weak equivalences between A ≡ B and A ≃ B.

is-univalent : ∀ ℓ → Set (lsuc ℓ)
is-univalent ℓ = (A B : Set ℓ) → iseq (Id→Eq A B)

univalence-≃ : ∀ {ℓ} → is-univalent ℓ → (A B : Set ℓ) → (A ≡ B) ≃ (A ≃ B)
univalence-≃ ua A B = (Id→Eq A B) , (ua A B)

Note that both isunivalent ℓ and univalence-≃ are predicates on the Universe 𝓤 = Set ℓ. So we say that “𝓤 is univalent.”

As a first example, let us check that under univalence certain simple elimination and computation rules hold for Id→Eq, as well as simple algebraic properties.

module U-Rules {ℓ : Level}
               (ua : is-univalent ℓ) -- univalence holds
               where

Extract the inverse to Id→Eq and the right and left homotopies:

       
  Eq→Id : (A B : Set ℓ) → A ≃ B → A ≡ B
  Eq→Id A B = π₁ (iseq→qinv (Id→Eq A B) (ua _ _) )

  Eq→Id-is-rinv : {A B : Set ℓ} (φ : A ≃ B) → (Id→Eq A B) (Eq→Id _ _ φ) ≡ φ
  Eq→Id-is-rinv {A} {B} φ = π₁ (π₂ (iseq→qinv (Id→Eq A B) (ua _ _) )) φ

  Eq→Id-is-linv : {A B : Set ℓ} (p : A ≡ B) → Eq→Id A B (Id→Eq _ _ p) ≡ p
  Eq→Id-is-linv {A} {B} p = π₂ (π₂ (iseq→qinv (Id→Eq A B) (ua _ _) )) p

Here some elemmentary rules from the HoTT book: the first is that the identity function gives the reflexivity, while the others establish some relationships with path concatenation:

  open ≃-lemmas
  id→refl : (A : Set ℓ) → Eq→Id A A ≃id ≡ idp A
  id→refl A = Eq→Id-is-linv {A} {A} (idp A)

  Id→Eq◾ : {A B C : Set ℓ} (p : A ≡ B) (q : B ≡ C) →
            (Id→Eq A B p) ≃◾≃ (Id→Eq B C q) ≡ Id→Eq A C (p ◾ q)
  Id→Eq◾ {A} {.A} {.A} refl refl = refl

  Id→Eq⁻¹ : {A B : Set ℓ} (p : A ≡ B) →
            ((Id→Eq A B p) ≃⁻¹) ≡ (Id→Eq B A (p ⁻¹))
  Id→Eq⁻¹ {A} {.A} refl = refl

  ua◾ : {A B C : Set ℓ} (φ : A ≃ B) (ψ : B ≃ C) →
         (Eq→Id A B φ) ◾ (Eq→Id B C ψ) ≡ Eq→Id A C (φ ≃◾≃ ψ)
  ua◾ {A} {B} {C} φ ψ = lemma ⁻¹
          where
            p = Eq→Id A B φ
            q = Eq→Id B C ψ

            φφ = Id→Eq A B p ≡⟨ Eq→Id-is-rinv φ ⟩
                  φ ∎
            φφ⁻¹ = φ ≡⟨ (Eq→Id-is-rinv φ) ⁻¹ ⟩
                    Id→Eq A B p ∎

            ψψ = Id→Eq B C q ≡⟨ Eq→Id-is-rinv ψ ⟩
                  ψ ∎
            ψψ⁻¹ = ψ ≡⟨ (Eq→Id-is-rinv ψ) ⁻¹ ⟩
                    Id→Eq B C q ∎

            lemma = Eq→Id A C (φ ≃◾≃ ψ)                          ≡⟨  ap (Eq→Id A C) (ap (λ α → α ≃◾≃ ψ ) φφ⁻¹) ⟩
                    Eq→Id A C ( (Id→Eq A B p) ≃◾≃ ψ)             ≡⟨  ap (Eq→Id A C) (ap (λ α → (Id→Eq A B p) ≃◾≃ α) ψψ⁻¹) ⟩
                    Eq→Id A C ( (Id→Eq A B p) ≃◾≃ (Id→Eq B C q)) ≡⟨  ap (Eq→Id A C) (Id→Eq◾ p q) ⟩
                    Eq→Id A C ( Id→Eq A C (p ◾ q))               ≡⟨ Eq→Id-is-linv (p ◾ q) ⟩
                    (Eq→Id A B φ) ◾ (Eq→Id B C ψ) ∎

  ua⁻¹ : {A B : Set ℓ} (φ : A ≃ B) → (Eq→Id A B φ) ⁻¹ ≡ Eq→Id B A (φ ≃⁻¹ )
  ua⁻¹ {A} {B} φ = lemma ⁻¹
    where
      p = Eq→Id A B φ

      φφ = Id→Eq A B p ≡⟨ Eq→Id-is-rinv φ ⟩
            φ ∎
      φφ⁻¹ = φ ≡⟨ (Eq→Id-is-rinv φ) ⁻¹ ⟩
              Id→Eq A B p ∎

      lemma = Eq→Id B A (φ ≃⁻¹ )             ≡⟨ ap (Eq→Id B A) (ap (λ α → α ≃⁻¹) φφ⁻¹) ⟩
              Eq→Id B A ((Id→Eq A B p) ≃⁻¹ ) ≡⟨ ap (Eq→Id B A) (Id→Eq⁻¹ p) ⟩
              Eq→Id B A (Id→Eq B A (p ⁻¹))   ≡⟨ Eq→Id-is-linv (p ⁻¹) ⟩
              (Eq→Id A B φ) ⁻¹ ∎

top ⇑

---