Isomorphisms to Equivalences

1. Isomorphisms to equivalences
- 1.1. Packages imports
- 1.2. The proof

1 Isomorphisms to equivalences

module Lib.IsoToEquiv where

This file is an alternative to the proof in Lib/ContrMap. It uses squares that are built «by hand» instead of using others fancy features like funext or closure by retraction of contractibility. The hope is that it computes better than the previous proof (i.e., that it avoids the explosion in the size of the term).

1.1 Packages imports

The imported packages can be accessed via the following links:

Lib/QInv

import Stdlib.Prelude
import Lib.Data.QInv

1.2 The proof

First, we define the notion of a square. The setting is the following:

a₀ ⟶ a₁ ↓ ↓ b₀ ⟶ b₁

and the goal is to show that we can "fill" this square.

Square (A : U) (a0 b0 a1 b1 : A)
       (p : Path A a0 a1) (q : Path A b0 b1)
       (r0 : Path A a0 b0) (r1 : Path A a1 b1) : U =
  PathP (i. (Path A (p i) (q i))) r0 r1

First, we define the center of contraction.

iso-to-equiv/center (A B : U) (f : A → B) (i : has-inverse A B f) (y : B)
                         : Fib A B f y =
  let g : B → A = QInv/map A B f i in      
  ( g y,
    inv B (f (g y)) y
    ( QInv/right-htpy A B f i y))

Then, we show that the fibers are a proposition, i.e., that all elements of fib_f(y) are equal. We start by showing that all first elements are equal to g(y).

lem-iso/rem (A B : U) (f : A → B) (g : B → A)
            (K : Htpy' A A (λx. g (f x)) (id A))
            (y : B) (x : A) (p : Path B y (f x))
               : Path A (g y) x =
  λi. hComp 0 1 A (g (p i)) [ (i=0) → _. g y, (i=1) → j. K x j ]

In particular, for any two fibers, their first element are equal.

lem-iso/p (A B : U) (f : A → B) (g : B → A)
          (K : Htpy' A A (λx. g (f x)) (id A))
          (y : B) (x0 x1 : A)
          (p0 : Path B y (f x0))
          (p1 : Path B y (f x1))
              : Path A x0 x1 =
  λi. hComp 0 1 A (g y) [ (i=0) → j. lem-iso/rem A B f g K y x0 p0 j,
                          (i=1) → j. lem-iso/rem A B f g K y x1 p1 j ]

We show that under these conditions, the following square can be filled:

g(y) ⟶ g(f(x)) ↓ ↓ g(y) ⟶ x

lem-iso/fill (A B : U) (f : A → B) (g : B → A)
             (K : Htpy' A A (λx. g (f x)) (id A))
             (y : B) (x : A) (p : Path B y (f x))
  : Square A (g y) (g y) (g (f x)) x
             (λi. g (p i))
             (lem-iso/rem A B f g K y x p)
             (λi. g y)
             (K x) =
  λi j. hComp 0 1 A (g (p i)) [ (i=0) → _. g y,
                                (i=1) → k. K x (j /λk),
                                (j=0) → _. g (p i) ]

Moreover, between two fibers (x₀,p₀), (x₁,p₁), we have that the following square can be filled:

g(y) ⟶ g(y) ↓ ↓ x₀ ⟶ x₁

lem-iso/fill' (A B : U) (f : A → B) (g : B → A)
              (K : Htpy' A A (λx. g (f x)) (id A))
              (y : B) (x0 x1 : A)
              (p0 : Path B y (f x0))
              (p1 : Path B y (f x1))
  : Square A (g y) x0 (g y) x1
             (λ_. g y)
             (lem-iso/p A B f g K y x0 x1 p0 p1)
             (lem-iso/rem A B f g K y x0 p0)
             (lem-iso/rem A B f g K y x1 p1) =
  λi j. hComp 0 1 A (g y) [ (i=0) → k. lem-iso/rem A B f g K y x0 p0 (j /λk),
                            (i=1) → k. lem-iso/rem A B f g K y x1 p1 (j /λk),
                            (j=0) → _. g y ]

Hence, the following square can be filled:

g(y) ⟶ g(y) ↓ ↓ g(f(x0) ⟶ g(f(x1))

lem-iso/sq (A B : U) (f : A → B) (g : B → A)
           (K : Htpy' A A (λx. g (f x)) (id A))
           (y : B) (x0 x1 : A)
           (p0 : Path B y (f x0))
           (p1 : Path B y (f x1))
  : Square A (g y) (g (f x0)) (g y) (g (f x1))
      (λ_. g y)
      (λi. g (f (lem-iso/p A B f g K y x0 x1 p0 p1 i)))
      (λi. g (p0 i))
      (λi. g (p1 i)) =
  λi j. hComp 1 0 A (lem-iso/fill' A B f g K y x0 x1 p0 p1 i j)
          [ (i=0) → k. lem-iso/fill A B f g K y x0 p0 j k,
            (i=1) → k. lem-iso/fill A B f g K y x1 p1 j k,
            (j=0) → _. g y,
            (j=1) → k. K (lem-iso/p A B f g K y x0 x1 p0 p1 i) k ]

Which finally implies the awaited path between p₀ and p₁:

lem-iso/sq' (A B : U) (f : A → B) (g : B → A)
            (H : Htpy' B B (λy. f (g y)) (id B))
            (K : Htpy' A A (λx. g (f x)) (id A))
            (y : B) (x0 x1 : A)
            (p0 : Path B y (f x0))
            (p1 : Path B y (f x1))
  : Square B y (f x0) y (f x1)
      (λ_. y)
      (λi. f (lem-iso/p A B f g K y x0 x1 p0 p1 i)) p0 p1 =
  λi j. hComp 0 1 B (f (lem-iso/sq A B f g K y x0 x1 p0 p1 i j))
          [ (i=0) → k. H (p0 j) k,
            (i=1) → k. H (p1 j) k,
            (j=0) → k. H y k,
            (j=1) → k. H (f (lem-iso/p A B f g K y x0 x1 p0 p1 i)) k ]

Thus, the fibers of f at y is a proposition.

lem-iso/is-prop-fib (A B : U) (f : A → B) (e : has-inverse A B f)
                    (y : B) : is-prop (Fib A B f y) =
  let g : B → A = QInv/map A B f e
      H : Htpy' B B (λy'. f (g y')) (id B) = QInv/right-htpy A B f e
      K : Htpy' A A (λx. g (f x)) (id A) = QInv/left-htpy A B f e in
  λt u i.
    ( lem-iso/p A B f g K y t.1 u.1 t.2 u.2 i,
      lem-iso/sq' A B f g H K y t.1 u.1 t.2 u.2 i)

Hence, f has contractible fibers.

iso-to-equiv (A B : U) (f : A → B) (i : has-inverse A B f)
                  : is-equiv A B f =
  λy.
  let c : Fib A B f y = iso-to-equiv/center A B f i y in
  ( c, lem-iso/is-prop-fib A B f i y c)

Isomorphisms to Equivalences

Table of Contents

1 Isomorphisms to equivalences

1.1 Packages imports

1.2 The proof