Bi-invertible Maps are Quasi-Inverses

1. Logical equivalence between quasi-inverses and bi-invertible maps

1 Logical equivalence between quasi-inverses and bi-invertible maps

module Lib.QInv where

In univalent mathematics, a map f is an equivalence (is-equiv f) if it has a left and right inverse (or, equivalently, if its fibers are contractible). This definition makes sense as in this case, is-equiv f is a proposition, that is, being an equivalence is a property of a map rather than a structure on the map. However, in practice, it is easier to use the natural notion of equivalence: bijection. In HoTT, bijections are called quasi-inverses. This file proves that a map is a quasi-inverse iff it is bi-invertible.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Lib.Data.BiInv
import Lib.Data.QInv

1.2 Logical equivalence between quasi-inverses and bi-invertible maps

In this section, we focus on showing that has-inverse f is logically equivalent to is-bi-inv f (that is, there is a map back and forth between the two types).

1.2.1 Map between quasi-inverse and bi-invertible

The map between has-inverse f and is-bi-inv f is trivial ; indeed, the map of a quasi-inverse is both the left and right inverse of f.

has-inverse-is-bi-inv (A B : U) (f : A → B) (i : has-inverse A B f) : is-bi-inv A B f =
  let g : B → A = QInv/map A B f i in
  ( (g, QInv/right-htpy A B f i),
    (g, QInv/left-htpy A B f i))

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

1.2.2 Map between bi-invertible and quasi-inverse

It is not obvious as to why bi-invertible maps are quasi-inverses, but actually, the right inverse is also a left inverse: we can build a homotopy K : g ~ h as follows:

g(y) = h(f(g(y))) as H : h ˆ f ~ id = h(y) as G : f ˆ g ~ id

Thus, we have that:

g(f(x)) = h(f(x)) as K : g ~ h = x as H : h ˆ f ~ id

is-bi-inv-has-inverse (A B : U) (f : A → B) (b : is-bi-inv A B f) : has-inverse A B f =
  let g : B → A = is-bi-inv/right-inv A B f b in
  let h : B → A = is-bi-inv/left-inv A B f b in
  let G : Htpy B (λ_. B) (map/comp B A B f g) (id B) = is-bi-inv/right-htpy A B f b in
  let H : Htpy A (λ_. A) (map/comp A B A h f) (id A) = is-bi-inv/left-htpy A B f b in
  let K : Htpy B (λ_. A) g h = λy. comp A (g y) (h (f (g y)))
                                          (inv A (h (f (g y))) (g y) (H (g y)))
                                          (h y)
                                          (ap B A h (f (g y)) y (G y)) in
  (g, G,
    λx. comp A (g (f x)) (h (f x))
              (K (f x))
              x (H x))

1.3 Inverse of a bi-invertible map

This result allows us to give (i) an inverse to a bi-invertible map that is (ii) also a bi-invertible map.

1.3.1 Inverse map

is-bi-inv/inv-map (A B : U) (f : A → B) (b : is-bi-inv A B f) : B → A =
  QInv/map A B f (is-bi-inv-has-inverse A B f b)

1.3.2 Homotopies of inverse map

is-bi-inv/inv-right-htpy (A B : U) (f : A → B) (b : is-bi-inv A B f) : Htpy B (λ_. B) (map/comp B A B f (is-bi-inv/inv-map A B f b)) (id B) =
  QInv/right-htpy A B f (is-bi-inv-has-inverse A B f b)

is-bi-inv/inv-left-htpy (A B : U) (f : A → B) (b : is-bi-inv A B f) : Htpy A (λ_. A) (map/comp A B A (is-bi-inv/inv-map A B f b) f) (id A) =
  QInv/left-htpy A B f (is-bi-inv-has-inverse A B f b)

1.3.3 Bi-invertibility of inverse map

is-bi-inv/inv-is-bi-inv (A B : U) (f : A → B) (b : is-bi-inv A B f) : is-bi-inv B A (is-bi-inv/inv-map A B f b) =
  let g : B → A = is-bi-inv/inv-map A B f b in
  let left-htpy : Htpy A (λ_. A) (map/comp A B A g f) (id A) = QInv/left-htpy A B f (is-bi-inv-has-inverse A B f b) in
  has-inverse-is-bi-inv B A g
    (f, (left-htpy, is-bi-inv/right-htpy A B f b))