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

comments powered by Disqus