Kubus

8. Equivalences, Glue and univalence

The univalence principle says that equivalent types are equal: an equivalence e : Equiv A B gives a path ua e : Path U A B, and every path between types arises this way. In Kubus, ua is a definition, and transport along ua e computes to e.

Equivalences

A type is contractible if it has an element to which every element is connected by a path. A function is an equivalence if each of its fibers is contractible:

lib/equiv.ktt
✓def isContr (A : U) : U := (x : A) × ((y : A) -> Path A x y)
✓def fiber {A B : U} (f : A -> B) (y : B) : U := (x : A) × Path B (f x) y
✓def isEquiv {A B : U} (f : A -> B) : U := (y : B) -> isContr (fiber f y)
✓def Equiv (A B : U) : U := (f : A -> B) × isEquiv f

The identity is an equivalence, and so is every function with an inverse up to paths (an isomorphism); the library proves the latter in lemIso:

import bool
#check isoToEquiv
isoToEquiv : {A B : U} → (f : A → B) → (g : B → A) → section f g → retract f g → Equiv A B
✓def notEquiv : Equiv Bool Bool := isoToEquiv not not notnot notnot

Glue types

To turn an equivalence into a path of types, we need a line of types that is A at one end and B at the other. Glue types build such lines. Glue B [φ -> (T, e)] is a type that

  • is T on the faces φ,
  • and elsewhere is B, with the elements of T glued on along the equivalence e : Equiv T B.

With φ = (i = 0 \/ i = 1), gluing A along e at i = 0 and B along the identity at i = 1 gives exactly the line we want:

lib/equiv.ktt
✓def ua {A B : U} (e : Equiv A B) : Path U A B :=
\i -> Glue B [i = 0 -> (A, e), i = 1 -> (B, idEquiv B)]

On the faces, the Glue type reduces to the glued type, so the endpoints are right by computation:

✓def G (i : I) : U := Glue Bool [i = 0 -> (Bool, notEquiv), i = 1 -> (Bool, idEquiv Bool)]
✓def g0 (b : Bool) : G 0 := b
✓def g1 (b : Bool) : G 1 := b

Elements of Glue types are introduced with glue and eliminated with unglue, which maps a glued element to the base B:

✓def toBase (i : I) (x : G i) : Bool := unglue x

Transport along ua computes

Composition in a Glue type is defined in terms of composition in the base and the equivalence (it is the most intricate case of the evaluator). The upshot: transporting along ua e applies e.

#eval transport (ua notEquiv) true
false
  : Bool
#eval transport (ua notEquiv) false
true
  : Bool
#eval transport (sym^1 (ua notEquiv)) true
false
  : Bool

Transporting backwards (along the reversed path; the ^1 is explained in chapter 10) applies the inverse. In general, transport along ua e agrees with e up to a path, by unglueing the filler of the transport:

lib/equiv.ktt
✓def uaβ {A B : U} (e : Equiv A B) (x : A) : Path B (e.1 x) (transport (ua e) x) :=
\i -> unglue (fill j (ua e j) [] x i)

The univalence axiom, as a theorem

ua gives one direction of univalence. The full statement says that ua is an equivalence, or equivalently that for each type A the type of types T with an equivalence T ≃ A is contractible: there is essentially only one such pair, (A, idEquiv A). The proof glues A along the given equivalence and shows that unglue is an equivalence:

import univalence
#check EquivContr
EquivContr : (A : U) → isContr^1 ((T : U) × Equiv T A)

The proof is in lib/univalence.ktt. Like everything else in the library, it is certified by the kernel.