Contractible Maps are Bi-invertible

1. Contractible maps are bi-invertible

1 Contractible maps are bi-invertible

module Lib.ContrMap where

This file shows that maps are contractible iff they are bi-invertible. The proof is not the usual one found in the HoTT book or Rijke's introduction to HoTT, but is the one found by Christian Sattler and David Wärn (source).

1.1 Packages imports

The imported packages can be accessed via the following links:

import Lib.FunExt
import Lib.IsoToEquiv
import Lib.QInv
import Lib.Prop.BiInv
import Lib.Prop.Contr
import Lib.Prop.Paths
import Lib.Prop.Σ

1.2 Any equivalence is bi-invertible

1.2.1 Technical details

Let f : A → B an equivalence – that is – a contractible map. As for all y : B, fib f y is contractible, it has a center of contraction (x, y = f x). We build g : B → A as follows: for y ∈ B, g(x) is the first element of the center of fib f y. With the second element of the center, we get a homotopy α : y = f (g y) for all y ∈ B: g is a section of f. In fact, we will see that g is an inverse of f.

is-equiv/is-bi-inv-inv-map (A B : U) (f : A → B) (e : is-equiv A B f) : B → A =
  λy. let c : Fib A B f y = (e y).1 in c.1

is-equiv/is-bi-inv-inv-right-htpy (A B : U) (f : A → B) (e : is-equiv A B f) (y : B)
                                       : Path B (f (is-equiv/is-bi-inv-inv-map A B f e y)) y =
  let c : Fib A B f y = (e y).1
      gx : A = (is-equiv/is-bi-inv-inv-map A B f e y)
  in (inv B y (f (gx)) c.2)

We now have to show that g is also a retraction of f, that is, there is a homotopy (g (f x)) = x. Note that we have p : (f (g (f x))) = (f x) by the previous lemma, therefore (g (f x), p) : fib f (f x). Since it is contractible by assumption, we get q : (g (f x), p) = (x, refl), that is, ap pr1 q is of type g (f x) = x.

is-equiv/is-bi-inv-inv-left-htpy (A B : U) (f : A → B) (e : is-equiv A B f) (x : A)
                                      : Path A ((is-equiv/is-bi-inv-inv-map A B f e) (f x)) x =
  let c : is-contr (Fib A B f (f x)) = (e (f x))
      g : B → A = is-equiv/is-bi-inv-inv-map A B f e
      P : A → U = λx'. Path B (f (g (f x'))) (f x')
      p : Path B (f x) (f (g (f x))) = inv B (f (g (f x))) (f x) (is-equiv/is-bi-inv-inv-right-htpy A B f e (f x))
      fib : Fib A B f (f x) = (g (f x), p)
      fib' : Fib A B f (f x) = (x, refl B (f x))
      r : Path (Fib A B f (f x)) fib c.1 = (inv (Fib A B f (f x)) c.1 fib (c.2 fib))
      s : Path (Fib A B f (f x)) c.1 fib' = c.2 fib'
      q : Path (Fib A B f (f x)) fib fib' = (comp (Fib A B f (f x)) fib c.1 r fib' s)
  in ap (Fib A B f (f x)) A (λu. u.1) fib fib' q

1.2.2 Result

Thus, an equivalence is bi-invertible.

is-equiv/is-bi-inv (A B : U) (f : A → B) (e : is-equiv A B f) : is-bi-inv A B f =
  has-inverse-is-bi-inv A B f
    (is-equiv/is-bi-inv-inv-map A B f e,
      (is-equiv/is-bi-inv-inv-right-htpy A B f e,
       is-equiv/is-bi-inv-inv-left-htpy A B f e))

Equiv/is-bi-inv (A B : U) (e : Equiv A B) : is-bi-inv A B e.1 =
  is-equiv/is-bi-inv A B e.1 e.2

1.3 Any bi-invertible map is an equivalence

In this section, we show that if f : A → B is a bi-invertible map, then it has contractible fibers.

1.3.1 Technical details

Let g : B → A be a bi-invertible map, that is, it is equipped with f, h : A → B and homotopies p : g ˆ f ∼ id, q : h ˆ g ∼ id.

Bi-invertibility of ap of composites

By function extensionality, g ˆ f = id and h ˆ g = id. Thus, as ap id is bi-invertible, ap g ˆ f and ap h ˆ g are also bi-invertible.

is-bi-inv/is-equiv-ap-comp-right-is-bi-inv (A B : U) (g : B → A) (b : is-bi-inv B A g) (x y : A)
                                                : is-bi-inv (Path A x y) (Path A (g (is-bi-inv/right-inv B A g b x)) (g (is-bi-inv/right-inv B A g b y)))
                                                            (ap A A (λz. g (is-bi-inv/right-inv B A g b z)) x y) =
  let f : A → B = is-bi-inv/right-inv B A g b
      p : Path (A → A) (λz. g (f z)) (id A) = (eq-htpy' A A (λz. g (f z)) (id A) (is-bi-inv/right-htpy B A g b))
      q : Path (A → A) (id A) (λz. g (f z)) = (inv (A → A) (λz. g (f z)) (id A) p)
  in
  is-bi-inv/ap-eq-id A (λz. g (f z)) q x y

is-bi-inv/is-equiv-ap-comp-left-is-bi-inv (A B : U) (g : B → A) (b : is-bi-inv B A g) (x y : B)
                                               : is-bi-inv (Path B x y) (Path B (is-bi-inv/left-inv B A g b (g x)) (is-bi-inv/left-inv B A g b (g y)))
                                                           (ap B B (λz. (is-bi-inv/left-inv B A g b (g z))) x y) =
  let h : A → B = is-bi-inv/left-inv B A g b
      p : Path (B → B) (λz. h (g z)) (id B) = (eq-htpy' B B (λz. h (g z)) (id B) (is-bi-inv/left-htpy B A g b))
      q : Path (B → B) (id B) (λz. h (g z)) = (inv (B → B) (λz. h (g z)) (id B) p)
  in
  is-bi-inv/ap-eq-id B (λz. h (g z)) q x y

ap g is bi-invertible

As such, ap g is also bi-invertible.

is-bi-inv/is-inj'/inv (A B : U) (g : B → A) (b : is-bi-inv B A g) (x y : A) : is-bi-inv (Path B (is-bi-inv/right-inv B A g b x) (is-bi-inv/right-inv B A g b y))
                                                                                        (Path A (g (is-bi-inv/right-inv B A g b x)) (g (is-bi-inv/right-inv B A g b y)))
                                                                                        (ap B A g (is-bi-inv/right-inv B A g b x) (is-bi-inv/right-inv B A g b y)) =
  let f : A → B = is-bi-inv/right-inv B A g b
      h : A → B = is-bi-inv/left-inv B A g b in
  is-bi-inv-comp/is-bi-inv-middle-map (Path A x y) (Path B (f x) (f y)) (Path A (g (f x)) (g (f y))) (Path B (h (g (f x))) (h (g (f y))))
    (ap A B f x y) (ap B A g (f x) (f y)) (ap A B h (g (f x)) (g (f y)))
    (is-bi-inv/is-equiv-ap-comp-right-is-bi-inv A B g b x y)
    (is-bi-inv/is-equiv-ap-comp-left-is-bi-inv A B g b (f x) (f y))

is-bi-inv/is-inj' (A B : U) (g : B → A) (b : is-bi-inv B A g) (x y : B) : is-bi-inv (Path B x y) (Path A (g x) (g y)) (ap B A g x y) =
  let f : A → B = is-bi-inv/right-inv B A g b 
      p : Path (B → B) (λz. f (g z)) (id B) = eq-htpy B (λ_. B) (λz. f (g z)) (id B) (is-bi-inv/inv-left-htpy B A g b)
  in
  tr (B → B) (λz. f (g z)) (id B) p (λh. is-bi-inv (Path B (h x) (h y)) (Path A (g (h x)) (g (h y))) (ap B A g (h x) (h y)))
    (is-bi-inv/is-inj'/inv A B g b (g x) (g y))

In a more general sense, any bi-invertible map is injective (that is, ap of this bi-invertible map is also bi-invertible).

is-bi-inv/is-inj (A B : U) (f : A → B) (b : is-bi-inv A B f) (x y : A) : is-bi-inv (Path A x y) (Path B (f x) (f y)) (ap A B f x y) =
  is-bi-inv/is-inj' B A f b x y

Any bi-invertible map is contractible

For any x : A, Σ (y : A) f x = f y is also contractible: from the previous lemma, we can deduce that this space is a retract of Σ (y : A) x = y.

is-bi-inv/is-equiv-retr-total-space (A B : U) (f : A → B) (H : (x y : A) → is-bi-inv (Path A x y) (Path B (f x) (f y)) (ap A B f x y)) (x : A)
                                         : retract-of (Σ A (λy. Path B (f x) (f y))) (Σ A (λy. Path A x y)) =
  let h-i : (y : A) → has-inverse (Path A x y) (Path B (f x) (f y)) (ap A B f x y) = λy. is-bi-inv-has-inverse (Path A x y) (Path B (f x) (f y)) (ap A B f x y) (H x y)
      h : (y : A) → Path B (f x) (f y) → Path A x y = λy. QInv/map (Path A x y) (Path B (f x) (f y)) (ap A B f x y) (h-i y)
      i : (Σ A (λy. Path B (f x) (f y))) → Σ A (λy. Path A x y) = λp. (p.1, h p.1 p.2)
      r : (Σ A (λy. Path A x y)) → Σ A (λy. Path B (f x) (f y)) = λp. (p.1, (ap A B f x p.1 p.2))
      htpy : (y : A) → Htpy' (Path B (f x) (f y)) (Path B (f x) (f y)) (λq. (ap A B f x y (h y q))) (id (Path B (f x) (f y))) =
                 λy q. QInv/right-htpy (Path A x y) (Path B (f x) (f y)) (ap A B f x y) (h-i y) q
  in (i, (r, λq. SgPathO→PathΣ A (λy. Path B (f x) (f y)) (r (i q)) q
                                   (refl A q.1, PathO/refl A q.1 (λy. Path B (f x) (f y)) (r (i q)).2 q.2 (htpy q.1 q.2))))

As Σ (y : A) x = y is contractible, the space Σ (y : A) (f x) = (f y) is then also contractible.

is-bi-inv/is-equiv-is-contr-total-space (A B : U) (f : A → B) (H : (x y : A) → is-bi-inv (Path A x y) (Path B (f x) (f y)) (ap A B f x y)) (x : A)
                                             : is-contr (Σ A (λy. Path B (f x) (f y))) =
  let A' : U = (Σ A (λy. Path B (f x) (f y)))
      B' : U = (Σ A (λy. Path A x y))
  in
  is-contr/closed-retract A' B' (is-bi-inv/is-equiv-retr-total-space A B f H x) (is-contr/Sg-path-is-contr A x)

As the contractibility of f will give a y : B, and that the right inverse of g is also the inverse of g, we have that f (g y) is y, thus the spaces Σ A (λx. Path B (f (g y)) (f x)) and Σ A (λx. Path B y (f x)) are bi-invertible.

Bi-invertibility of spaces

First, we define the maps.

is-bi-inv/is-equiv-is-bi-inv-total-space-map (A B : U) (g : B → A) (b : is-bi-inv B A g) (y : B)
                                                  : Σ A (λx. Path B (is-bi-inv/right-inv B A g b (g y)) (is-bi-inv/right-inv B A g b x)) → Σ A (λx. Path B y (is-bi-inv/right-inv B A g b x)) =
  let f : A → B = is-bi-inv/right-inv B A g b
      L : Htpy' B B (λz. f (g z)) (id B) = is-bi-inv/inv-left-htpy B A g b
  in
  λp. (p.1, comp B y (f (g y)) (inv B (f (g y)) y (L y)) (f p.1) p.2)

is-bi-inv/is-equiv-is-bi-inv-total-space-invmap (A B : U) (g : B → A) (b : is-bi-inv B A g) (y : B)
                                                     : Σ A (λx. Path B y (is-bi-inv/right-inv B A g b x)) → Σ A (λx. Path B (is-bi-inv/right-inv B A g b (g y)) (is-bi-inv/right-inv B A g b x)) =
  let f : A → B = is-bi-inv/right-inv B A g b
      L : Htpy' B B (λz. f (g z)) (id B) = is-bi-inv/inv-left-htpy B A g b
  in
  λp. (p.1, comp B (f (g y)) y (L y) (f p.1) p.2)

Then, we show that invmap is a right inverse. It is straightforward: (L y) ⋅ (inv (L y)) cancel each other out.

is-bi-inv/is-equiv-is-bi-inv-total-space-right-htpy (A B : U) (g : B → A) (b : is-bi-inv B A g) (y : B)
                                                         : Htpy' (Σ A (λx. Path B y (is-bi-inv/right-inv B A g b x)))
                                                                 (Σ A (λx. Path B y (is-bi-inv/right-inv B A g b x)))
                                                                 (λz. (is-bi-inv/is-equiv-is-bi-inv-total-space-map A B g b y) (is-bi-inv/is-equiv-is-bi-inv-total-space-invmap A B g b y z))
                                                                 (id (Σ A (λx. Path B y (is-bi-inv/right-inv B A g b x)))) =
  λpair.
    let f : A → B = is-bi-inv/right-inv B A g b
        L : Htpy' B B (λz. f (g z)) (id B) = is-bi-inv/inv-left-htpy B A g b
        h : Σ A (λx. Path B (f (g y)) (f x)) → Σ A (λx. Path B y (f x)) = is-bi-inv/is-equiv-is-bi-inv-total-space-map A B g b y                   
        i : Σ A (λx. Path B y (f x)) → Σ A (λx. Path B (f (g y)) (f x)) = is-bi-inv/is-equiv-is-bi-inv-total-space-invmap A B g b y
        x : A = pair.1
        p : Path B y (f x) = pair.2
        q : Path (Path B y (f x)) (h (i pair)).2 p
                 = comp-n (Path B y (f x)) three-Nat (h (i pair)).2
                                                     (comp B y y (comp B y (f (g y)) (inv B (f (g y)) y (L y)) y (L y)) (f x) p)
                                                     (comp/assoc' B y (f (g y)) (inv B (f (g y)) y (L y)) y (L y) (f x) p)
                                                     (comp B y y (refl B y) (f x) p)
                                                     (ap (Path B y y) (Path B y (f x)) (λr. comp B y y r (f x) p)
                                                         (comp B y (f (g y)) (inv B (f (g y)) y (L y)) y (L y)) (refl B y)
                                                         (comp/inv-l B (f (g y)) y (L y)))
                                                     p (comp/ident-l B y (f x) p)
    in SgPathO→PathΣ A (λz. Path B y (f z)) (h (i pair)) (x, p) (refl A x, PathO/refl A x (λz. Path B y (f z)) (h (i pair)).2 p q)

f is contractible.

That is, the map f is contractible: any y : B corresponds to a unique x : A.

is-bi-inv/is-equiv-is-bi-inv-ap (A B : U) (f : A → B) (b : is-bi-inv A B f) (H : (x y : A) → is-bi-inv (Path A x y) (Path B (f x) (f y)) (ap A B f x y))
                                     : is-equiv A B f =
  let g : B → A = is-bi-inv/inv-map A B f b
      b' : is-bi-inv B A g = ((f, is-bi-inv/inv-left-htpy A B f b), (f, is-bi-inv/inv-right-htpy A B f b))
  in
  λy.
    is-contr/closed-retract
      ( Fib A B f y)
      ( Fib A B f (f (g y)))
      ( is-bi-inv/is-equiv-is-bi-inv-total-space-invmap A B g b' y,
        ( is-bi-inv/is-equiv-is-bi-inv-total-space-map A B g b' y,
          is-bi-inv/is-equiv-is-bi-inv-total-space-right-htpy A B g b' y))
      ( is-bi-inv/is-equiv-is-contr-total-space A B f H (g y))

1.3.2 Bi-invertibility implies equivalence

Thus, if f : A → B is a bi-invertible map, it is also an equivalence.

-- is-bi-inv/is-equiv (A B : U) (f : A → B) (b : is-bi-inv A B f) : is-equiv A B f =
--   is-bi-inv/is-equiv-is-bi-inv-ap A B f b (is-bi-inv/is-inj A B f b)

The above version is kept because it is clearer than the following version.

is-bi-inv/is-equiv (A B : U) (f : A → B) (b : is-bi-inv A B f) : is-equiv A B f =
  iso-to-equiv A B f
    ( is-bi-inv-has-inverse A B f b)

Hence:

is-bi-inv/Equiv (A B : U) (f : A → B) (b : is-bi-inv A B f) : Equiv A B =
  (f, is-bi-inv/is-equiv A B f b)

BiInv/Equiv (A B : U) (b : BiInv A B) : Equiv A B =
  is-bi-inv/Equiv A B (BiInv/map A B b) (BiInv/is-bi-inv A B b)

1.3.3 Inverse implies equivalence

has-inverse/is-equiv : (A B : U) (f : A → B) (i : has-inverse A B f) → is-equiv A B f = iso-to-equiv 

has-inverse/Equiv (A B : U) (f : A → B) (i : has-inverse A B f) : Equiv A B =
  is-bi-inv/Equiv A B f (has-inverse-is-bi-inv A B f i)

1.4 Any equivalence is injective

Equiv/is-inj (A B : U) (f : A → B) (e : is-equiv A B f) (x y : A) : is-equiv (Path A x y) (Path B (f x) (f y)) (ap A B f x y) =
  is-bi-inv/is-equiv (Path A x y) (Path B (f x) (f y)) (ap A B f x y)
    (is-bi-inv/is-inj A B f (is-equiv/is-bi-inv A B f e) x y)

1.5 FunExt principle

htpy-eq is a family of equivalences.

htpy-eq/is-equiv (A : U) (B : A → U) (f g : (x : A) → B x) : is-equiv (Path ((x : A) → B x) f g) (Htpy A B f g) (htpy-eq A B f g) =
  has-inverse/is-equiv (Path ((x : A) → B x) f g) (Htpy A B f g) (htpy-eq A B f g) (htpy-eq/has-inverse A B f g)

htpy-eq/Equiv (A : U) (B : A → U) (f g : (x : A) → B x) : Equiv (Path ((x : A) → B x) f g) (Htpy A B f g) =
  ( htpy-eq A B f g,
    htpy-eq/is-equiv A B f g)

Same for eq-htpy.

eq-htpy/is-equiv (A : U) (B : A → U) (f g : (x : A) → B x) : is-equiv (Htpy A B f g) (Path ((x : A) → B x) f g) (eq-htpy A B f g) =
  has-inverse/is-equiv (Htpy A B f g) (Path ((x : A) → B x) f g) (eq-htpy A B f g) (eq-htpy/has-inverse A B f g)

eq-htpy/Equiv (A : U) (B : A → U) (f g : (x : A) → B x) : Equiv (Htpy A B f g) (Path ((x : A) → B x) f g) =
  ( eq-htpy A B f g,
    eq-htpy/is-equiv A B f g)