Nottingham FP Lab Blog

Isomorphisms and weak equivalences

by Paolo Capriotti on November 28, 2012.
Tagged as: Type theory meetings.

Today we discussed about isomorphisms and weak equivalences in type theory.

There are at least two ways to define the notion of equivalence between two types X and Y.

The first, which we will call isomorphism, is a tuple (f, g, H, K), with:

f : X → Y
g : Y → X

H : (x : X) → g (f x) ≡ x
K : (y : Y) → f (g y) ≡ y

i.e. essentially a pair of functions and pair of homotopies. This corresponds to the notion of homotopy equivalence in homotopy theory.

The other possible definition is the usual one by Voevodsky: a function f : X → Y is a weak equivalence if the following type is inhabited:

(y : Y) → h₀ (Σ X λ x → f x ≡ y)

i.e. every fiber is contractible.

We can show that these two notions are logically equivalent. Going from a weak equivalence to an isomorphism is quite straightforward. Given a weak equivalence f, unfolding the definition gives that, for all y : Y, we have a triple

(g y, K y, ϕ y)

with

g y : X
K y : f (g y) ≡ y
ϕ y : (x : X)(p : f x ≡ y) → (x, p) ≡ (g y, K y)

So we automatically get an inverse g and a homotopy K, and we only need to find an H. So we define:

H x = cong proj₁ (ϕ (f x))

and we're done.

The other direction is trickier. We first prove the type-theoretic equivalent of Vogt's lemma:

Given an isomorphism (f, g, H, K), we can find K', of the same type as K, and γ : (x : X) → cong f (H x) ≡ K' (f x).

The outline of the proof is as follows: we first show that the following diagram of homotopies

\[ \newcommand{\ra}[1]{\kern-1.5ex\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} \newcommand{\ras}[1]{\kern-1.5ex\xrightarrow{\ \ \smash{#1}\ \ }\phantom{}\kern-1.5ex} \newcommand{\da}[1]{\bigg\downarrow\raise.5ex\rlap{\scriptstyle#1}} \begin{array}{c} f g f g f & \ra{fHgf} & f g f \\ \da{fgKf} & & \da{K f} \\ f g f & \ra{f H} & f \\ \end{array} \]

commutes. In fact, it is quite easy to see that we can replace fHgf with fgfH in the top arrow. Similarly, we can replace fgKf with Kfgf in the left arrow. Then commutativity of the diagram follows immediately from the interchange law (i.e. the fact that horizontal composition of homotopies is well defined).

Next, we can observe that f appears on the right of every arrow except the bottom one, hence if we define:

\[ K' = K \circ f H g \circ (f g K)^{-1} \]

it's clear that

\[ K' f \equiv f H \]

\(\square\)

Now we're ready to show that any isomorphism is a weak equivalence. Given any isomorphism (f, g, H, K), Vogt's lemma implies that we can assume the existence of γ : (x : X) → cong f (H x) ≡ K (f x) (we say that the isomorphism is coherent, in this case). Again, a weak equivalence is given by a triple (g, K, ϕ), and we have g and K already, so we only need to provide ϕ.

Using the fact that equality in a \(Σ\)-type is the same as a \(Σ\) of equalities, and given x : X, y : Y and p : f x ≡ y, we define

q : x ≡ g y
q = (H x)⁻¹ ; cong g p

contr : subst (λ x → f x ≡ y) q p ≡ K y
contr = ? -- see below

ϕ x y p = q , contr

The proof contr consists simply of algebraic manipulations on paths:

  subst (λ x → f x ≡ y) q p
≡⟨ substituting on an equality is the same as composing ⟩
  cong f q⁻¹ ; p
≡⟨ definition of q ⟩
  cong f (cong g p⁻¹) ; cong f (H x) ; p
≡⟨ coherence ⟩
  cong (g ∘ f) p⁻¹ ; K (f x) ; p
≡⟨ interchange law ⟩
  K y ; p⁻¹ ; p
≡⟨ groupoid law ⟩
  K y

Questions raised:

What's an example of non-coherent isomorphism, i.e. a quadruple (f, g, H, K) for which there exists no corresponding γ?
Is the logical equivalence above (restricted to coherent isomorphisms) an isomorphism itself?
It is possible to define a dual notion of coherence by swapping f and g. Fortunately, one coherence is enough to prove the other, but it raises a question: is it possible to have non-coherent coherence proofs (and so on)?

Update:

An answer to 1 can be found in this agda file, which uses our work in progress base library for HoTT