Quasi-inverses Properties

1. Quasi-inverses properties
- 1.1. Packages imports
- 1.2. 3-for-2 property for composition

1 Quasi-inverses properties

module Lib.Prop.QInv where

This file provides some useful properties for quasi-inverses.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Lib.Data.Nat  
import Lib.Data.QInv

1.2 3-for-2 property for composition

An important property of quasi-inverses is that, for two maps f : A \to B and g : B \to C, then if any two of

f has a quasi-inverse ;
g has a quasi-inverse ;
g \circ f has a quasi-inverse

hold, then the third also hold.

1.2.1 Composition

We start by the case where f and g have a quasi-inverse. The quasi-inverse of g \circ f is (inv f) \circ (inv g). It is easy to show that this is the case:

for the right inverse, it suffices to remark that: f ˆ f^-1 ˆ g^-1 ~ g^-1, and thus g ˆ f ˆ f^-1 ˆ g^-1 ~ g ˆ g^-1, that gives us the property using the right homotopy of g ;
for the left inverse, it goes the same way: g^-1 ˆ g ˆ f ~ f, hence f^-1 ˆ g^-1 ˆ g ˆ f ~ f^-1 ˆ f which suffices to conclude given the left homotopy of f.

has-inverse/comp-has-inverse (A B C : U) (f : A → B) (g : B → C) (i : has-inverse A B f) (i' : has-inverse B C g) : has-inverse A C (map/comp A B C g f) =
  let h : C → A = map/comp C B A (QInv/map A B f i) (QInv/map B C g i')
      H : Htpy C (λ_. C) (map/comp C A C (map/comp A B C g f) h) (id C) =
          λx. comp C (g (f (h x))) (g (QInv/map B C g i' x))
                   (ap B C g (f (h x)) (QInv/map B C g i' x) (QInv/right-htpy A B f i (QInv/map B C g i' x))) 
                   x
                   (QInv/right-htpy B C g i' x)
      K : Htpy A (λ_. A) (map/comp A C A h (map/comp A B C g f)) (id A) =
          λx. comp A (h (g (f x))) ((QInv/map A B f i) (f x))
                     (ap B A (QInv/map A B f i) ((QInv/map B C g i') (g (f x))) (f x) (QInv/left-htpy B C g i' (f x)))
                     x
                     (QInv/left-htpy A B f i x)                   
  in
  (h, (H, K))

1.2.2 Left map

We continue with the case where g and g \circ f have an inverse. In this case, the inverse of f is (g ˆ f)^-1 ˆ g. Indeed:

g ˆ f ˆ (g ˆ f)^-1 ˆ g ~ g, hence g^-1 ˆ g ˆ f ˆ (g ˆ f)^-1 ˆ g ~ g^-1 ˆ g and we can conclude ;
(g ˆ f)^-1 ˆ g ˆ f ~ id by hypothesis.

has-inverse/has-inverse-comp-left (A B C : U) (f : A → B) (g : B → C) (i : has-inverse B C g)
                                                                      (i' : has-inverse A C (map/comp A B C g f)) : has-inverse A B f =
  let ig : C → B = QInv/map B C g i
      h : B → A = map/comp B C A (QInv/map A C (map/comp A B C g f) i') g
      H : Htpy B (λ_. B) (map/comp B A B f h) (id B) =
          λx. comp-n B three-Nat
                (f (h x)) (ig (g (f (h x)))) (inv B (ig (g (f (h x)))) (f (h x)) (QInv/left-htpy B C g i (f (h x))))
                (ig (g x)) (ap C B ig (g (f (h x))) (g x)
                              (QInv/right-htpy A C (map/comp A B C g f) i' (g x)))
                x (QInv/left-htpy B C g i x)
      K : Htpy A (λ_. A) (map/comp A B A h f) (id A) = QInv/left-htpy A C (map/comp A B C g f) i'
  in
  (h, (H, K))

1.2.3 Right map

Finally, we conclude with the case where f and g \circ f have an inverse. As before, the inverse of g is f ˆ (g ˆ f)^-1. Indeed:

g ˆ f ˆ (g ˆ f)^-1 ~ id by hypothesis ;
f ˆ (g ˆ f)^-1 ˆ g ˆ f ~ f, hence f ˆ (g ˆ f)^-1 ˆ g ˆ f ˆ f^-1 ~ f ˆ f^-1 and we can conclude.

Note that it is totally symmetric to the previous case.

has-inverse/has-inverse-comp-right (A B C : U) (f : A → B) (g : B → C) (i : has-inverse A B f)
                                   (i' : has-inverse A C (map/comp A B C g f)) : has-inverse B C g =
  let if : B → A = QInv/map A B f i
      igf : C → A = (QInv/map A C (map/comp A B C g f) i')
      h : C → B  = map/comp C A B f igf
      H : Htpy C (λ_. C) (map/comp C B C g h) (id C) = QInv/right-htpy A C (map/comp A B C g f) i'
      K : Htpy B (λ_. B) (map/comp B C B h g) (id B) =
          λx. comp-n B three-Nat
                        (h (g x)) (h (g (f (if x))))
                        (ap B B (map/comp B C B h g) x (f (if x)) (inv B (f (if x)) x
                                                       (QInv/right-htpy A B f i x)))
                        (f (if x)) (ap A B f (igf (g (f (if x)))) (if x)
                                             (QInv/left-htpy A C (map/comp A B C g f) i' (if x)))
                        x (QInv/right-htpy A B f i x)                    
  in
  (h, (H, K))