# Coherently invertible maps

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, Raymond Baker, fernabnor and louismntnu.

Created on 2022-02-07.

module foundation-core.coherently-invertible-maps where

Imports
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.homotopy-algebra
open import foundation.universe-levels
open import foundation.whiskering-higher-homotopies-composition
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-homotopies
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.invertible-maps
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.whiskering-homotopies-concatenation


## Idea

A (two-sided) inverse for a map f : A → B is a map g : B → A equipped with homotopies S : f ∘ g ~ id and R : g ∘ f ~ id. Such data, however is structure on the map f, and not generally a property. One way to make the type of inverses into a property is by adding a single coherence condition between the homotopies of the inverse, asking that the following diagram commmutes

              S ·r f
--------->
f ∘ g ∘ f            f.
--------->
f ·l R


We call such data a coherently invertible map. I.e., a coherently invertible map f : A → B is a map equipped with a two-sided inverse and this additional coherence.

There is also the alternative coherence condition we could add

              R ·r g
--------->
g ∘ f ∘ g            g.
--------->
g ·l S


We will colloquially refer to invertible maps equipped with this coherence as transpose coherently invertible maps.

Note. Coherently invertible maps are referred to as half adjoint equivalences in [UF13].

On this page we will prove that every two-sided inverse g of f can be promoted to a coherent two-sided inverse. Thus, for most properties of coherently invertible maps, it suffices to consider the data of a two-sided inverse. However, this coherence construction requires us to replace the section homotopy (or retraction homotopy). For this reason we also give direct constructions showing

1. The identity map is coherently invertible.
2. The composite of two coherently invertible maps is coherently invertible.
3. The inverse of a coherently invertible map is coherently invertible.
4. Every map homotopic to a coherently invertible map is coherently invertible.
5. The 3-for-2 property of coherently invertible maps.

Each of these constructions appropriately preserve the data of the underlying two-sided inverse.

## Definition

### The predicate of being a coherently invertible map

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

coherence-is-coherently-invertible :
(f : A → B) (g : B → A) (G : f ∘ g ~ id) (H : g ∘ f ~ id) → UU (l1 ⊔ l2)
coherence-is-coherently-invertible f g G H = G ·r f ~ f ·l H

is-coherently-invertible : (A → B) → UU (l1 ⊔ l2)
is-coherently-invertible f =
Σ ( B → A)
( λ g →
Σ ( f ∘ g ~ id)
( λ G →
Σ ( g ∘ f ~ id)
( λ H → coherence-is-coherently-invertible f g G H)))

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
(H : is-coherently-invertible f)
where

map-inv-is-coherently-invertible : B → A
map-inv-is-coherently-invertible = pr1 H

is-section-map-inv-is-coherently-invertible :
is-section f map-inv-is-coherently-invertible
is-section-map-inv-is-coherently-invertible = pr1 (pr2 H)

is-retraction-map-inv-is-coherently-invertible :
is-retraction f map-inv-is-coherently-invertible
is-retraction-map-inv-is-coherently-invertible = pr1 (pr2 (pr2 H))

coh-is-coherently-invertible :
coherence-is-coherently-invertible f
( map-inv-is-coherently-invertible)
( is-section-map-inv-is-coherently-invertible)
( is-retraction-map-inv-is-coherently-invertible)
coh-is-coherently-invertible = pr2 (pr2 (pr2 H))

is-invertible-is-coherently-invertible : is-invertible f
pr1 is-invertible-is-coherently-invertible =
map-inv-is-coherently-invertible
pr1 (pr2 is-invertible-is-coherently-invertible) =
is-section-map-inv-is-coherently-invertible
pr2 (pr2 is-invertible-is-coherently-invertible) =
is-retraction-map-inv-is-coherently-invertible

section-is-coherently-invertible : section f
pr1 section-is-coherently-invertible =
map-inv-is-coherently-invertible
pr2 section-is-coherently-invertible =
is-section-map-inv-is-coherently-invertible

retraction-is-coherently-invertible : retraction f
pr1 retraction-is-coherently-invertible =
map-inv-is-coherently-invertible
pr2 retraction-is-coherently-invertible =
is-retraction-map-inv-is-coherently-invertible


We will show that is-coherently-invertible is a proposition in foundation.coherently-invertible-maps.

### The type of coherently invertible maps

coherently-invertible-map : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
coherently-invertible-map A B = Σ (A → B) (is-coherently-invertible)

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (e : coherently-invertible-map A B)
where

map-coherently-invertible-map : A → B
map-coherently-invertible-map = pr1 e

is-coherently-invertible-map-coherently-invertible-map :
is-coherently-invertible map-coherently-invertible-map
is-coherently-invertible-map-coherently-invertible-map = pr2 e

map-inv-coherently-invertible-map : B → A
map-inv-coherently-invertible-map =
map-inv-is-coherently-invertible
( is-coherently-invertible-map-coherently-invertible-map)

is-section-map-inv-coherently-invertible-map :
map-coherently-invertible-map ∘ map-inv-coherently-invertible-map ~ id
is-section-map-inv-coherently-invertible-map =
is-section-map-inv-is-coherently-invertible
( is-coherently-invertible-map-coherently-invertible-map)

is-retraction-map-inv-coherently-invertible-map :
map-inv-coherently-invertible-map ∘ map-coherently-invertible-map ~ id
is-retraction-map-inv-coherently-invertible-map =
is-retraction-map-inv-is-coherently-invertible
( is-coherently-invertible-map-coherently-invertible-map)

coh-coherently-invertible-map :
coherence-is-coherently-invertible
( map-coherently-invertible-map)
( map-inv-coherently-invertible-map)
( is-section-map-inv-coherently-invertible-map)
( is-retraction-map-inv-coherently-invertible-map)
coh-coherently-invertible-map =
coh-is-coherently-invertible
( is-coherently-invertible-map-coherently-invertible-map)

section-coherently-invertible-map :
section map-coherently-invertible-map
section-coherently-invertible-map =
section-is-coherently-invertible
( is-coherently-invertible-map-coherently-invertible-map)

retraction-coherently-invertible-map :
retraction map-coherently-invertible-map
retraction-coherently-invertible-map =
retraction-is-coherently-invertible
( is-coherently-invertible-map-coherently-invertible-map)

is-invertible-coherently-invertible-map :
is-invertible map-coherently-invertible-map
is-invertible-coherently-invertible-map =
is-invertible-is-coherently-invertible
( is-coherently-invertible-map-coherently-invertible-map)

invertible-map-coherently-invertible-map : invertible-map A B
pr1 invertible-map-coherently-invertible-map =
map-coherently-invertible-map
pr2 invertible-map-coherently-invertible-map =
is-invertible-coherently-invertible-map


### The predicate of being a transpose coherently invertible map

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

coherence-is-transpose-coherently-invertible :
(f : A → B) (g : B → A) (G : f ∘ g ~ id) (H : g ∘ f ~ id) → UU (l1 ⊔ l2)
coherence-is-transpose-coherently-invertible f g G H = H ·r g ~ g ·l G

is-transpose-coherently-invertible : (A → B) → UU (l1 ⊔ l2)
is-transpose-coherently-invertible f =
Σ ( B → A)
( λ g →
Σ ( f ∘ g ~ id)
( λ G →
Σ ( g ∘ f ~ id)
( λ H → coherence-is-transpose-coherently-invertible f g G H)))

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
(H : is-transpose-coherently-invertible f)
where

map-inv-is-transpose-coherently-invertible : B → A
map-inv-is-transpose-coherently-invertible = pr1 H

is-section-map-inv-is-transpose-coherently-invertible :
f ∘ map-inv-is-transpose-coherently-invertible ~ id
is-section-map-inv-is-transpose-coherently-invertible = pr1 (pr2 H)

is-retraction-map-inv-is-transpose-coherently-invertible :
map-inv-is-transpose-coherently-invertible ∘ f ~ id
is-retraction-map-inv-is-transpose-coherently-invertible = pr1 (pr2 (pr2 H))

coh-is-transpose-coherently-invertible :
coherence-is-transpose-coherently-invertible f
( map-inv-is-transpose-coherently-invertible)
( is-section-map-inv-is-transpose-coherently-invertible)
( is-retraction-map-inv-is-transpose-coherently-invertible)
coh-is-transpose-coherently-invertible = pr2 (pr2 (pr2 H))

is-invertible-is-transpose-coherently-invertible : is-invertible f
pr1 is-invertible-is-transpose-coherently-invertible =
map-inv-is-transpose-coherently-invertible
pr1 (pr2 is-invertible-is-transpose-coherently-invertible) =
is-section-map-inv-is-transpose-coherently-invertible
pr2 (pr2 is-invertible-is-transpose-coherently-invertible) =
is-retraction-map-inv-is-transpose-coherently-invertible

section-is-transpose-coherently-invertible : section f
pr1 section-is-transpose-coherently-invertible =
map-inv-is-transpose-coherently-invertible
pr2 section-is-transpose-coherently-invertible =
is-section-map-inv-is-transpose-coherently-invertible

retraction-is-transpose-coherently-invertible : retraction f
pr1 retraction-is-transpose-coherently-invertible =
map-inv-is-transpose-coherently-invertible
pr2 retraction-is-transpose-coherently-invertible =
is-retraction-map-inv-is-transpose-coherently-invertible


We will show that is-transpose-coherently-invertible is a proposition in foundation.coherently-invertible-maps.

### The type of transpose coherently invertible maps

transpose-coherently-invertible-map :
{l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
transpose-coherently-invertible-map A B =
Σ (A → B) (is-transpose-coherently-invertible)

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
(e : transpose-coherently-invertible-map A B)
where

map-transpose-coherently-invertible-map : A → B
map-transpose-coherently-invertible-map = pr1 e

is-transpose-coherently-invertible-map-transpose-coherently-invertible-map :
is-transpose-coherently-invertible map-transpose-coherently-invertible-map
is-transpose-coherently-invertible-map-transpose-coherently-invertible-map =
pr2 e

map-inv-transpose-coherently-invertible-map : B → A
map-inv-transpose-coherently-invertible-map =
map-inv-is-transpose-coherently-invertible
( is-transpose-coherently-invertible-map-transpose-coherently-invertible-map)

is-section-map-inv-transpose-coherently-invertible-map :
( map-transpose-coherently-invertible-map ∘
map-inv-transpose-coherently-invertible-map) ~
( id)
is-section-map-inv-transpose-coherently-invertible-map =
is-section-map-inv-is-transpose-coherently-invertible
( is-transpose-coherently-invertible-map-transpose-coherently-invertible-map)

is-retraction-map-inv-transpose-coherently-invertible-map :
( map-inv-transpose-coherently-invertible-map ∘
map-transpose-coherently-invertible-map) ~
( id)
is-retraction-map-inv-transpose-coherently-invertible-map =
is-retraction-map-inv-is-transpose-coherently-invertible
( is-transpose-coherently-invertible-map-transpose-coherently-invertible-map)

coh-transpose-coherently-invertible-map :
coherence-is-transpose-coherently-invertible
( map-transpose-coherently-invertible-map)
( map-inv-transpose-coherently-invertible-map)
( is-section-map-inv-transpose-coherently-invertible-map)
( is-retraction-map-inv-transpose-coherently-invertible-map)
coh-transpose-coherently-invertible-map =
coh-is-transpose-coherently-invertible
( is-transpose-coherently-invertible-map-transpose-coherently-invertible-map)

section-transpose-coherently-invertible-map :
section map-transpose-coherently-invertible-map
section-transpose-coherently-invertible-map =
section-is-transpose-coherently-invertible
( is-transpose-coherently-invertible-map-transpose-coherently-invertible-map)

retraction-transpose-coherently-invertible-map :
retraction map-transpose-coherently-invertible-map
retraction-transpose-coherently-invertible-map =
retraction-is-transpose-coherently-invertible
( is-transpose-coherently-invertible-map-transpose-coherently-invertible-map)

is-invertible-transpose-coherently-invertible-map :
is-invertible map-transpose-coherently-invertible-map
is-invertible-transpose-coherently-invertible-map =
is-invertible-is-transpose-coherently-invertible
( is-transpose-coherently-invertible-map-transpose-coherently-invertible-map)

invertible-map-transpose-coherently-invertible-map : invertible-map A B
pr1 invertible-map-transpose-coherently-invertible-map =
map-transpose-coherently-invertible-map
pr2 invertible-map-transpose-coherently-invertible-map =
is-invertible-transpose-coherently-invertible-map


### Invertible maps that are coherent are coherently invertible maps

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
(H : is-invertible f)
where

coherence-is-invertible : UU (l1 ⊔ l2)
coherence-is-invertible =
coherence-is-coherently-invertible
( f)
( map-inv-is-invertible H)
( is-section-map-inv-is-invertible H)
( is-retraction-map-inv-is-invertible H)

transpose-coherence-is-invertible : UU (l1 ⊔ l2)
transpose-coherence-is-invertible =
coherence-is-transpose-coherently-invertible
( f)
( map-inv-is-invertible H)
( is-section-map-inv-is-invertible H)
( is-retraction-map-inv-is-invertible H)

is-coherently-invertible-coherence-is-invertible :
coherence-is-invertible → is-coherently-invertible f
is-coherently-invertible-coherence-is-invertible coh =
( map-inv-is-invertible H ,
is-section-map-inv-is-invertible H ,
is-retraction-map-inv-is-invertible H ,
coh)

is-transpose-coherently-invertible-transpose-coherence-is-invertible :
transpose-coherence-is-invertible → is-transpose-coherently-invertible f
is-transpose-coherently-invertible-transpose-coherence-is-invertible coh =
( map-inv-is-invertible H ,
is-section-map-inv-is-invertible H ,
is-retraction-map-inv-is-invertible H ,
coh)


## Properties

### The inverse of a coherently invertible map is transpose coherently invertible and vice versa

The inverse of a coherently invertible map is transpose coherently invertible. Conversely, the inverse of a transpose coherently invertible map is coherently invertible. Since these are defined by simply moving data around, they are strict inverses to one another.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

is-transpose-coherently-invertible-map-inv-is-coherently-invertible :
{f : A → B} (H : is-coherently-invertible f) →
is-transpose-coherently-invertible (map-inv-is-coherently-invertible H)
is-transpose-coherently-invertible-map-inv-is-coherently-invertible {f} H =
( f ,
is-retraction-map-inv-is-coherently-invertible H ,
is-section-map-inv-is-coherently-invertible H ,
coh-is-coherently-invertible H)

is-coherently-invertible-map-inv-is-transpose-coherently-invertible :
{f : A → B} (H : is-transpose-coherently-invertible f) →
is-coherently-invertible (map-inv-is-transpose-coherently-invertible H)
is-coherently-invertible-map-inv-is-transpose-coherently-invertible {f} H =
( f ,
is-retraction-map-inv-is-transpose-coherently-invertible H ,
is-section-map-inv-is-transpose-coherently-invertible H ,
coh-is-transpose-coherently-invertible H)

transpose-coherently-invertible-map-inv-coherently-invertible-map :
coherently-invertible-map A B → transpose-coherently-invertible-map B A
transpose-coherently-invertible-map-inv-coherently-invertible-map e =
( map-inv-coherently-invertible-map e ,
is-transpose-coherently-invertible-map-inv-is-coherently-invertible
( is-coherently-invertible-map-coherently-invertible-map e))

coherently-invertible-map-inv-transpose-coherently-invertible-map :
transpose-coherently-invertible-map A B → coherently-invertible-map B A
coherently-invertible-map-inv-transpose-coherently-invertible-map e =
( map-inv-transpose-coherently-invertible-map e ,
is-coherently-invertible-map-inv-is-transpose-coherently-invertible
( is-transpose-coherently-invertible-map-transpose-coherently-invertible-map
( e)))


### Invertible maps are coherently invertible

This result is known as Vogt's lemma in point-set topology. The construction follows Lemma 10.4.5 in [Rij22].

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-invertible f)
where

is-retraction-map-inv-is-coherently-invertible-is-invertible :
map-inv-is-invertible H ∘ f ~ id
is-retraction-map-inv-is-coherently-invertible-is-invertible =
is-retraction-map-inv-is-invertible H

abstract
is-section-map-inv-is-coherently-invertible-is-invertible :
f ∘ map-inv-is-invertible H ~ id
is-section-map-inv-is-coherently-invertible-is-invertible =
( ( inv-htpy (is-section-map-inv-is-invertible H)) ·r
( f ∘ map-inv-is-invertible H)) ∙h
( ( ( f) ·l
( is-retraction-map-inv-is-invertible H) ·r
( map-inv-is-invertible H)) ∙h
( is-section-map-inv-is-invertible H))

abstract
inv-coh-is-coherently-invertible-is-invertible :
f ·l is-retraction-map-inv-is-coherently-invertible-is-invertible ~
is-section-map-inv-is-coherently-invertible-is-invertible ·r f
inv-coh-is-coherently-invertible-is-invertible =
left-transpose-htpy-concat
( ( is-section-map-inv-is-invertible H) ·r
( f ∘ map-inv-is-invertible H ∘ f))
( f ·l is-retraction-map-inv-is-invertible H)
( ( ( f) ·l
( is-retraction-map-inv-is-invertible H) ·r
( map-inv-is-invertible H ∘ f)) ∙h
( is-section-map-inv-is-invertible H ·r f))
( ( ( nat-htpy (is-section-map-inv-is-invertible H ·r f)) ·r
( is-retraction-map-inv-is-invertible H)) ∙h
( right-whisker-concat-htpy
( ( inv-preserves-comp-left-whisker-comp
( f)
( map-inv-is-invertible H ∘ f)
( is-retraction-map-inv-is-invertible H)) ∙h
( left-whisker-comp²
( f)
( inv-coh-htpy-id (is-retraction-map-inv-is-invertible H))))
( is-section-map-inv-is-invertible H ·r f)))

abstract
coh-is-coherently-invertible-is-invertible :
coherence-is-coherently-invertible
( f)
( map-inv-is-invertible H)
( is-section-map-inv-is-coherently-invertible-is-invertible)
( is-retraction-map-inv-is-coherently-invertible-is-invertible)
coh-is-coherently-invertible-is-invertible =
inv-htpy inv-coh-is-coherently-invertible-is-invertible

is-coherently-invertible-is-invertible : is-coherently-invertible f
is-coherently-invertible-is-invertible =
( map-inv-is-invertible H ,
is-section-map-inv-is-coherently-invertible-is-invertible ,
is-retraction-map-inv-is-coherently-invertible-is-invertible ,
coh-is-coherently-invertible-is-invertible)


module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-invertible f)
where

is-transpose-coherently-invertible-is-invertible :
is-transpose-coherently-invertible f
is-transpose-coherently-invertible-is-invertible =
is-transpose-coherently-invertible-map-inv-is-coherently-invertible
( is-coherently-invertible-is-invertible
( is-invertible-map-inv-is-invertible H))


### Coherently invertible maps are injective

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
where

is-injective-is-coherently-invertible :
(H : is-coherently-invertible f) {x y : A} → f x ＝ f y → x ＝ y
is-injective-is-coherently-invertible H =
is-injective-is-invertible
( is-invertible-is-coherently-invertible H)

is-injective-is-transpose-coherently-invertible :
(H : is-transpose-coherently-invertible f) {x y : A} → f x ＝ f y → x ＝ y
is-injective-is-transpose-coherently-invertible H =
is-injective-is-invertible
( is-invertible-is-transpose-coherently-invertible H)


### Coherently invertible maps are embeddings

We show that is-injective-is-coherently-invertible is a section and retraction of ap f.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
(H : is-coherently-invertible f) {x y : A}
where

abstract
is-section-is-injective-is-coherently-invertible :
ap f {x} {y} ∘ is-injective-is-coherently-invertible H ~ id
is-section-is-injective-is-coherently-invertible p =
( ap-concat f
( inv (is-retraction-map-inv-is-coherently-invertible H x))
( ( ap (map-inv-is-coherently-invertible H) p) ∙
( is-retraction-map-inv-is-coherently-invertible H y))) ∙
( ap-binary
( _∙_)
( ap-inv f (is-retraction-map-inv-is-coherently-invertible H x))
( ( ap-concat f
( ap (map-inv-is-coherently-invertible H) p)
( is-retraction-map-inv-is-coherently-invertible H y)) ∙
( ap-binary
( _∙_)
( inv (ap-comp f (map-inv-is-coherently-invertible H) p))
( inv (coh-is-coherently-invertible H y))))) ∙
( inv
( left-transpose-eq-concat
( ap f (is-retraction-map-inv-is-coherently-invertible H x))
( p)
( ( ap (f ∘ map-inv-is-coherently-invertible H) p) ∙
( is-section-map-inv-is-coherently-invertible H (f y)))
( ( ap-binary
( _∙_)
( inv (coh-is-coherently-invertible H x))
( inv (ap-id p))) ∙
( nat-htpy (is-section-map-inv-is-coherently-invertible H) p))))

abstract
is-retraction-is-injective-is-coherently-invertible :
is-injective-is-coherently-invertible H ∘ ap f {x} {y} ~ id
is-retraction-is-injective-is-coherently-invertible refl =
left-inv (is-retraction-map-inv-is-coherently-invertible H x)

is-invertible-ap-is-coherently-invertible : is-invertible (ap f {x} {y})
is-invertible-ap-is-coherently-invertible =
( is-injective-is-coherently-invertible H ,
is-section-is-injective-is-coherently-invertible ,
is-retraction-is-injective-is-coherently-invertible)

is-coherently-invertible-ap-is-coherently-invertible :
is-coherently-invertible (ap f {x} {y})
is-coherently-invertible-ap-is-coherently-invertible =
is-coherently-invertible-is-invertible
( is-invertible-ap-is-coherently-invertible)


### Coherently invertible maps are transpose coherently invertible

The proof follows Lemma 4.2.2 in [UF13].

Proof. By naturality of homotopies we have

                   gfRg
gfgfg --------------------> gfg
|                          |
Rgfg |  nat-htpy R ·r (R ·r g)  | Rg
∨                          ∨
gfg ----------------------> g.
Rg


We can paste the homotopy

  g (inv-coh-htpy-id S) ∙ gHg : Sgfg ~ gfSg ~ gfRg


along the top edge of this naturality square obtaining the coherence square

             gfgS
gfgfg -------> gfg
|             |
Rgfg |             | Rg
∨             ∨
gfg ---------> g.
Rg


There is also the naturality square

                   gfgS
gfgfg --------------------> gfg
|                          |
Rgfg |  nat-htpy (R ·r g) ·r S  | Rg
∨                          ∨
gfg ----------------------> g.
gS


Now, by pasting these along the common edge Rgfg, we obtain

            gfgS           gfgS
gfg <------- gfgfg -------> gfg
|             |             |
Rg |             | Rgfg        | Rg
∨             ∨             ∨
g <--------- gfg --------> gm
Rg             gS


After cancelling gfgS and Rg with themselves, we are left with Rg ~ gS as desired.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
(f : A → B)
(g : B → A)
(S : is-section f g)
(R : is-retraction f g)
(H : coherence-is-coherently-invertible f g S R)
where

abstract
coh-transposition-coherence-is-coherently-invertible :
(g ∘ f ∘ g) ·l S ~ (g ∘ f) ·l R ·r g
coh-transposition-coherence-is-coherently-invertible =
( inv-preserves-comp-left-whisker-comp g (f ∘ g) S) ∙h
( left-whisker-comp² g (inv-coh-htpy-id S)) ∙h
( double-whisker-comp² g H g) ∙h
( preserves-comp-left-whisker-comp g f (R ·r g))

abstract
naturality-square-transposition-coherence-is-coherently-invertible :
coherence-square-homotopies
( R ·r (g ∘ f ∘ g))
( (g ∘ f ∘ g) ·l S)
( R ·r g)
( R ·r g)
naturality-square-transposition-coherence-is-coherently-invertible =
( ap-concat-htpy'
( R ·r g)
( coh-transposition-coherence-is-coherently-invertible)) ∙h
( inv-htpy (nat-htpy R ·r (R ·r g))) ∙h
( ap-concat-htpy
( R ·r (g ∘ f ∘ g))
( left-unit-law-left-whisker-comp (R ·r g)))

abstract
coherence-transposition-coherence-is-coherently-invertible :
coherence-is-transpose-coherently-invertible f g S R
coherence-transposition-coherence-is-coherently-invertible =
( ap-concat-htpy'
( R ·r g)
( inv-htpy (left-inv-htpy ((g ∘ f ∘ g) ·l S)))) ∙h
( assoc-htpy (inv-htpy ((g ∘ f ∘ g) ·l S)) ((g ∘ f ∘ g) ·l S) (R ·r g)) ∙h
( ap-concat-htpy
( inv-htpy ((g ∘ f ∘ g) ·l S))
( inv-htpy (nat-htpy (R ·r g) ·r S))) ∙h
( inv-htpy
( assoc-htpy
( inv-htpy ((g ∘ f ∘ g) ·l S))
( R ·r (g ∘ f ∘ g))
( g ·l S))) ∙h
( ap-concat-htpy'
( g ·l S)
( ( vertical-inv-coherence-square-homotopies
( R ·r (g ∘ f ∘ g)) ((g ∘ f ∘ g) ·l S) (R ·r g) (R ·r g)
( naturality-square-transposition-coherence-is-coherently-invertible)) ∙h
( right-inv-htpy (R ·r g))))

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
where

coherence-transposition-is-coherently-invertible :
(H : is-coherently-invertible f) →
coherence-is-transpose-coherently-invertible
( f)
( map-inv-is-coherently-invertible H)
( is-section-map-inv-is-coherently-invertible H)
( is-retraction-map-inv-is-coherently-invertible H)
coherence-transposition-is-coherently-invertible
( g , S , R , H) =
coherence-transposition-coherence-is-coherently-invertible f g S R H

transposition-is-coherently-invertible :
is-coherently-invertible f → is-transpose-coherently-invertible f
transposition-is-coherently-invertible H =
is-transpose-coherently-invertible-transpose-coherence-is-invertible
( is-invertible-is-coherently-invertible H)
( coherence-transposition-is-coherently-invertible H)


### Transpose coherently invertible maps are coherently invertible

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
where

coherence-transposition-is-transpose-coherently-invertible :
(H : is-transpose-coherently-invertible f) →
coherence-is-coherently-invertible
( f)
( map-inv-is-transpose-coherently-invertible H)
( is-section-map-inv-is-transpose-coherently-invertible H)
( is-retraction-map-inv-is-transpose-coherently-invertible H)
coherence-transposition-is-transpose-coherently-invertible H =
coherence-transposition-is-coherently-invertible
( is-coherently-invertible-map-inv-is-transpose-coherently-invertible H)

transposition-is-transpose-coherently-invertible :
is-transpose-coherently-invertible f → is-coherently-invertible f
transposition-is-transpose-coherently-invertible H =
is-coherently-invertible-coherence-is-invertible
( is-invertible-is-transpose-coherently-invertible H)
( coherence-transposition-is-transpose-coherently-invertible H)

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

transposition-coherently-invertible-map :
coherently-invertible-map A B → transpose-coherently-invertible-map A B
transposition-coherently-invertible-map (f , H) =
( f , transposition-is-coherently-invertible H)

transposition-transpose-coherently-invertible-map :
transpose-coherently-invertible-map A B → coherently-invertible-map A B
transposition-transpose-coherently-invertible-map (f , H) =
( f , transposition-is-transpose-coherently-invertible H)


### Coherently invertible maps are closed under homotopies

Proof. Assume given a coherently invertible map f with inverse g, homotopies S : f ∘ g ~ id, R : g ∘ f ~ id and coherence C : Sf ~ fR. Moreover, assume the map f' is homotopic to f with homotopy H : f' ~ f. Then g is also a two-sided inverse to f' via the homotopies

  S' := Hg ∙ S : f' ∘ g ~ id    and    R' := gH ∙ R : g ∘ f' ~ id.


Moreover, these witnesses are part of a coherent inverse to f'. To show this, we must construct a coherence C' of the square

           Hgf'
f'gf' -----> f'gf
|           |
f'gH |           | Sf'
∨           ∨
f'gf -------> f'.
f'R


We begin by observing that C fits somewhere along the diagonal of this square via the composite

                        Sf
HgH       ------>     H⁻¹
f'gf' ------> fgf    C    f ------> f'.
------>
fR

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f f' : A → B} (H : f' ~ f)
(g : B → A) (S : f ∘ g ~ id) (R : g ∘ f ~ id) (C : S ·r f ~ f ·l R)
where

coh-coh-is-coherently-invertible-htpy :
horizontal-concat-htpy' (H ·r g) H ∙h (S ·r f ∙h inv-htpy H) ~
horizontal-concat-htpy' (H ·r g) H ∙h (f ·l R ∙h inv-htpy H)
coh-coh-is-coherently-invertible-htpy =
left-whisker-concat-htpy
( horizontal-concat-htpy' (H ·r g) H)
( right-whisker-concat-htpy C (inv-htpy H))


Now the problem is reduced to constructing two homotopies

  Hgf' ∙ Sf' ~ HgH ∙ Sf ∙ H⁻¹    and    f'gH ∙ f'R ~ HgH ∙ fR ∙ H⁻¹.


By the two equivalent constructions of the horizontal composite HgH

    Hgf' ∙ fgH ~ HgH ~ f'gH ∙ Hgf


constructing the two homotopies is equivalent to constructing coherences of the squares

            fgH                        Hgf
fgf' -------> fgf          f'gf -------> fgf
|             |            |             |
Sf' |             | Sf     f'R |             | fR
∨             ∨            ∨             ∨
f' ---------> f            f' ---------> f.
H                          H


However, these squares are naturality squares, so we are done.

  coh-section-is-coherently-invertible-htpy :
(H ·r g ∙h S) ·r f' ~
horizontal-concat-htpy' (H ·r g) H ∙h ((S ·r f) ∙h inv-htpy H)
coh-section-is-coherently-invertible-htpy =
( left-whisker-concat-htpy
( H ·r (g ∘ f'))
( right-transpose-htpy-concat (S ·r f') H ((f ∘ g) ·l H ∙h S ·r f)
( ( ap-concat-htpy
( S ·r f')
( inv-htpy (left-unit-law-left-whisker-comp H))) ∙h
( nat-htpy S ·r H)))) ∙h
( ( ap-concat-htpy
( H ·r (g ∘ f'))
( assoc-htpy ((f ∘ g) ·l H) (S ·r f) (inv-htpy H))) ∙h
( inv-htpy
( assoc-htpy (H ·r (g ∘ f')) ((f ∘ g) ·l H) ((S ·r f) ∙h inv-htpy H))))

coh-retraction-is-coherently-invertible-htpy :
horizontal-concat-htpy' (H ·r g) H ∙h ((f ·l R) ∙h inv-htpy H) ~
f' ·l ((g ·l H) ∙h R)
coh-retraction-is-coherently-invertible-htpy =
( ap-concat-htpy'
( f ·l R ∙h inv-htpy H)
( coh-horizontal-concat-htpy (H ·r g) H)) ∙h
( assoc-htpy ((f' ∘ g) ·l H) (H ·r (g ∘ f)) (f ·l R ∙h inv-htpy H)) ∙h
( ap-concat-htpy
( (f' ∘ g) ·l H)
( inv-htpy (assoc-htpy (H ·r (g ∘ f)) (f ·l R) (inv-htpy H)))) ∙h
( left-whisker-concat-htpy
( (f' ∘ g) ·l H)
( inv-htpy
( right-transpose-htpy-concat (f' ·l R) H ((H ·r (g ∘ f) ∙h f ·l R))
( inv-htpy (nat-htpy H ·r R))))) ∙h
( ap-concat-htpy'
( f' ·l R)
( inv-preserves-comp-left-whisker-comp f' g H)) ∙h
( inv-htpy (distributive-left-whisker-comp-concat f' (g ·l H) R))


Finally, we concatenate the three coherences to obtain our desired result.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f f' : A → B}
where

abstract
coh-is-coherently-invertible-htpy :
(H : f' ~ f) (F : is-coherently-invertible f) →
coherence-is-coherently-invertible
( f')
( map-inv-is-coherently-invertible F)
( is-section-map-inv-is-invertible-htpy
( H)
( is-invertible-is-coherently-invertible F))
( is-retraction-map-inv-is-invertible-htpy
( H)
( is-invertible-is-coherently-invertible F))
coh-is-coherently-invertible-htpy H F =
( coh-section-is-coherently-invertible-htpy H
( map-inv-is-coherently-invertible F)
( is-section-map-inv-is-coherently-invertible F)
( is-retraction-map-inv-is-coherently-invertible F)
( coh-is-coherently-invertible F)) ∙h
( coh-coh-is-coherently-invertible-htpy H
( map-inv-is-coherently-invertible F)
( is-section-map-inv-is-coherently-invertible F)
( is-retraction-map-inv-is-coherently-invertible F)
( coh-is-coherently-invertible F)) ∙h
( coh-retraction-is-coherently-invertible-htpy H
( map-inv-is-coherently-invertible F)
( is-section-map-inv-is-coherently-invertible F)
( is-retraction-map-inv-is-coherently-invertible F)
( coh-is-coherently-invertible F))

is-coherently-invertible-htpy :
f' ~ f → is-coherently-invertible f → is-coherently-invertible f'
is-coherently-invertible-htpy H F =
is-coherently-invertible-coherence-is-invertible
( is-invertible-htpy H (is-invertible-is-coherently-invertible F))
( coh-is-coherently-invertible-htpy H F)

is-coherently-invertible-inv-htpy :
f ~ f' → is-coherently-invertible f → is-coherently-invertible f'
is-coherently-invertible-inv-htpy H =
is-coherently-invertible-htpy (inv-htpy H)

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
where

is-coherently-invertible-htpy-coherently-invertible-map :
(e : coherently-invertible-map A B) →
f ~ map-coherently-invertible-map e →
is-coherently-invertible f
is-coherently-invertible-htpy-coherently-invertible-map (e , E) H =
is-coherently-invertible-htpy H E

is-coherently-invertible-inv-htpy-coherently-invertible-map :
(e : coherently-invertible-map A B) →
map-coherently-invertible-map e ~ f →
is-coherently-invertible f
is-coherently-invertible-inv-htpy-coherently-invertible-map (e , E) H =
is-coherently-invertible-inv-htpy H E


### The identity map is coherently invertible

module _
{l : Level} {A : UU l}
where

is-coherently-invertible-id :
is-coherently-invertible (id {A = A})
is-coherently-invertible-id =
is-coherently-invertible-coherence-is-invertible is-invertible-id refl-htpy

id-coherently-invertible-map : coherently-invertible-map A A
id-coherently-invertible-map =
( id , is-coherently-invertible-id)

is-transpose-coherently-invertible-id :
is-transpose-coherently-invertible (id {A = A})
is-transpose-coherently-invertible-id =
is-transpose-coherently-invertible-map-inv-is-coherently-invertible
( is-coherently-invertible-id)

id-transpose-coherently-invertible-map :
transpose-coherently-invertible-map A A
id-transpose-coherently-invertible-map =
( id , is-transpose-coherently-invertible-id)


### Inversion of coherently invertible maps

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

is-coherently-invertible-map-inv-is-coherently-invertible :
{f : A → B} (H : is-coherently-invertible f) →
is-coherently-invertible (map-inv-is-coherently-invertible H)
is-coherently-invertible-map-inv-is-coherently-invertible H =
is-coherently-invertible-map-inv-is-transpose-coherently-invertible
( transposition-is-coherently-invertible H)

is-transpose-coherently-invertible-map-inv-is-transpose-coherently-invertible :
{f : A → B} (H : is-transpose-coherently-invertible f) →
is-transpose-coherently-invertible
( map-inv-is-transpose-coherently-invertible H)
is-transpose-coherently-invertible-map-inv-is-transpose-coherently-invertible
H =
transposition-is-coherently-invertible
( is-coherently-invertible-map-inv-is-transpose-coherently-invertible H)

inv-coherently-invertible-map :
coherently-invertible-map A B → coherently-invertible-map B A
inv-coherently-invertible-map (f , H) =
( map-inv-is-coherently-invertible H ,
is-coherently-invertible-map-inv-is-coherently-invertible H)

inv-transpose-coherently-invertible-map :
transpose-coherently-invertible-map A B →
transpose-coherently-invertible-map B A
inv-transpose-coherently-invertible-map (f , H) =
( map-inv-is-transpose-coherently-invertible H ,
is-transpose-coherently-invertible-map-inv-is-transpose-coherently-invertible
( H))


### Composition of coherently invertible maps

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
(g : B → C) (f : A → B)
(G : is-coherently-invertible g)
(F : is-coherently-invertible f)
where

coh-is-coherently-invertible-comp :
coherence-is-coherently-invertible
( g ∘ f)
( map-inv-is-invertible-comp g f
( is-invertible-is-coherently-invertible G)
( is-invertible-is-coherently-invertible F))
( is-section-map-inv-is-invertible-comp g f
( is-invertible-is-coherently-invertible G)
( is-invertible-is-coherently-invertible F))
( is-retraction-map-inv-is-invertible-comp g f
( is-invertible-is-coherently-invertible G)
( is-invertible-is-coherently-invertible F))
coh-is-coherently-invertible-comp =
( ap-concat-htpy
( ( g) ·l
( is-section-map-inv-is-coherently-invertible F) ·r
( map-inv-is-coherently-invertible G ∘ g ∘ f))
( coh-is-coherently-invertible G ·r f)) ∙h
( right-whisker-comp²
( ( nat-htpy (g ·l is-section-map-inv-is-coherently-invertible F)) ·r
( is-retraction-map-inv-is-coherently-invertible G))
( f)) ∙h
( ap-binary-concat-htpy
( inv-preserves-comp-left-whisker-comp
( g ∘ f)
( map-inv-is-coherently-invertible F)
( is-retraction-map-inv-is-coherently-invertible G ·r f))
( ( left-whisker-comp² g (coh-is-coherently-invertible F)) ∙h
( preserves-comp-left-whisker-comp g f
( is-retraction-map-inv-is-coherently-invertible F)))) ∙h
( inv-htpy
( distributive-left-whisker-comp-concat
( g ∘ f)
( ( map-inv-is-coherently-invertible F) ·l
( is-retraction-map-inv-is-coherently-invertible G ·r f))
( is-retraction-map-inv-is-coherently-invertible F)))

is-coherently-invertible-comp : is-coherently-invertible (g ∘ f)
is-coherently-invertible-comp =
is-coherently-invertible-coherence-is-invertible
( is-invertible-comp g f
( is-invertible-is-coherently-invertible G)
( is-invertible-is-coherently-invertible F))
( coh-is-coherently-invertible-comp)

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
(g : B → C) (f : A → B)
(G : is-transpose-coherently-invertible g)
(F : is-transpose-coherently-invertible f)
where

coh-is-transpose-coherently-invertible-comp :
coherence-is-transpose-coherently-invertible
( g ∘ f)
( map-inv-is-invertible-comp g f
( is-invertible-is-transpose-coherently-invertible G)
( is-invertible-is-transpose-coherently-invertible F))
( is-section-map-inv-is-invertible-comp g f
( is-invertible-is-transpose-coherently-invertible G)
( is-invertible-is-transpose-coherently-invertible F))
( is-retraction-map-inv-is-invertible-comp g f
( is-invertible-is-transpose-coherently-invertible G)
( is-invertible-is-transpose-coherently-invertible F))
coh-is-transpose-coherently-invertible-comp =
coh-is-coherently-invertible-comp
( map-inv-is-transpose-coherently-invertible F)
( map-inv-is-transpose-coherently-invertible G)
( is-coherently-invertible-map-inv-is-transpose-coherently-invertible F)
( is-coherently-invertible-map-inv-is-transpose-coherently-invertible G)

is-transpose-coherently-invertible-comp :
is-transpose-coherently-invertible (g ∘ f)
is-transpose-coherently-invertible-comp =
is-transpose-coherently-invertible-transpose-coherence-is-invertible
( is-invertible-comp g f
( is-invertible-is-transpose-coherently-invertible G)
( is-invertible-is-transpose-coherently-invertible F))
( coh-is-transpose-coherently-invertible-comp)

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
where

comp-coherently-invertible-map :
coherently-invertible-map B C →
coherently-invertible-map A B →
coherently-invertible-map A C
comp-coherently-invertible-map (g , G) (f , F) =
( g ∘ f , is-coherently-invertible-comp g f G F)

comp-transpose-coherently-invertible-map :
transpose-coherently-invertible-map B C →
transpose-coherently-invertible-map A B →
transpose-coherently-invertible-map A C
comp-transpose-coherently-invertible-map (g , G) (f , F) =
( g ∘ f , is-transpose-coherently-invertible-comp g f G F)


### The 3-for-2 property of coherently invertible maps

The 3-for-2 property of coherently invertible maps asserts that for any commuting triangle of maps

       h
A ------> B
\       /
f\     /g
\   /
∨ ∨
X,


if two of the three maps are coherently invertible, then so is the third.

We also record special cases of the 3-for-2 property of coherently invertible maps, where we only assume maps g : B → X and h : A → B. In this special case, we set f := g ∘ h and the triangle commutes by refl-htpy.

André Joyal proposed calling this property the 3-for-2 property, despite most mathematicians calling it the 2-out-of-3 property. The story goes that on the produce market is is common to advertise a discount as "3-for-2". If you buy two apples, then you get the third for free. Similarly, if you prove that two maps in a commuting triangle are coherently invertible, then you get the third proof for free.

#### The left map in a commuting triangle is coherently invertible if the other two maps are

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) (h : A → B) (T : f ~ g ∘ h)
where

is-coherently-invertible-left-map-triangle :
is-coherently-invertible h →
is-coherently-invertible g →
is-coherently-invertible f
is-coherently-invertible-left-map-triangle H G =
is-coherently-invertible-htpy T (is-coherently-invertible-comp g h G H)


#### The right map in a commuting triangle is coherently invertible if the other two maps are

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) (h : A → B) (T : f ~ g ∘ h)
where

is-coherently-invertible-right-map-triangle :
is-coherently-invertible f →
is-coherently-invertible h →
is-coherently-invertible g
is-coherently-invertible-right-map-triangle F H =
is-coherently-invertible-htpy
( ( g ·l inv-htpy (is-section-map-inv-is-coherently-invertible H)) ∙h
( inv-htpy T ·r map-inv-is-coherently-invertible H))
( is-coherently-invertible-comp
( f)
( map-inv-is-coherently-invertible H)
( F)
( is-coherently-invertible-map-inv-is-coherently-invertible H))


#### The top map in a commuting triangle is coherently invertible if the other two maps are

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) (h : A → B) (T : f ~ g ∘ h)
where

is-coherently-invertible-top-map-triangle :
is-coherently-invertible g →
is-coherently-invertible f →
is-coherently-invertible h
is-coherently-invertible-top-map-triangle G F =
is-coherently-invertible-htpy
( ( inv-htpy (is-retraction-map-inv-is-coherently-invertible G) ·r h) ∙h
( map-inv-is-coherently-invertible G ·l inv-htpy T))
( is-coherently-invertible-comp
( map-inv-is-coherently-invertible G)
( f)
( is-coherently-invertible-map-inv-is-coherently-invertible G)
( F))


#### If a composite and its right factor are coherently invertible, then so is its left factor

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
where

is-coherently-invertible-left-factor :
(g : B → X) (h : A → B) →
is-coherently-invertible (g ∘ h) →
is-coherently-invertible h →
is-coherently-invertible g
is-coherently-invertible-left-factor g h GH H =
is-coherently-invertible-right-map-triangle (g ∘ h) g h refl-htpy GH H


#### If a composite and its left factor are coherently invertible, then so is its right factor

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
where

is-coherently-invertible-right-factor :
(g : B → X) (h : A → B) →
is-coherently-invertible g →
is-coherently-invertible (g ∘ h) →
is-coherently-invertible h
is-coherently-invertible-right-factor g h G GH =
is-coherently-invertible-top-map-triangle (g ∘ h) g h refl-htpy G GH


### Any section of a coherently invertible map is coherently invertible

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

is-coherently-invertible-is-section :
{f : A → B} {g : B → A} →
is-coherently-invertible f → f ∘ g ~ id → is-coherently-invertible g
is-coherently-invertible-is-section {f = f} {g} F H =
is-coherently-invertible-top-map-triangle id f g
( inv-htpy H)
( F)
( is-coherently-invertible-id)


### Any retraction of a coherently invertible map is coherently invertible

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

is-coherently-invertible-is-retraction :
{f : A → B} {g : B → A} →
is-coherently-invertible f → (g ∘ f) ~ id → is-coherently-invertible g
is-coherently-invertible-is-retraction {f = f} {g} F H =
is-coherently-invertible-right-map-triangle id g f
( inv-htpy H)
( is-coherently-invertible-id)
( F)


### If a section of f is coherently invertible, then f is coherently invertible

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

is-coherently-invertible-is-coherently-invertible-section :
(s : section f) →
is-coherently-invertible (map-section f s) → is-coherently-invertible f
is-coherently-invertible-is-coherently-invertible-section (g , G) S =
is-coherently-invertible-is-retraction S G


### If a retraction of f is coherently invertible, then f is coherently invertible

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

abstract
is-coherently-invertible-is-coherently-invertible-retraction :
(r : retraction f) →
is-coherently-invertible (map-retraction f r) → is-coherently-invertible f
is-coherently-invertible-is-coherently-invertible-retraction (g , G) R =
is-coherently-invertible-is-section R G


### Any section of a coherently invertible map is homotopic to its inverse

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (e : coherently-invertible-map A B)
where

htpy-map-inv-coherently-invertible-map-section :
(f : section (map-coherently-invertible-map e)) →
map-inv-coherently-invertible-map e ~
map-section (map-coherently-invertible-map e) f
htpy-map-inv-coherently-invertible-map-section =
htpy-map-inv-invertible-map-section
( invertible-map-coherently-invertible-map e)


### Any retraction of a coherently invertible map is homotopic to its inverse

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (e : coherently-invertible-map A B)
where

htpy-map-inv-coherently-invertible-map-retraction :
(f : retraction (map-coherently-invertible-map e)) →
map-inv-coherently-invertible-map e ~
map-retraction (map-coherently-invertible-map e) f
htpy-map-inv-coherently-invertible-map-retraction =
htpy-map-inv-invertible-map-retraction
( invertible-map-coherently-invertible-map e)


## References

[Rij22]
Egbert Rijke. Introduction to Homotopy Type Theory. 12 2022. arXiv:2212.11082.
[UF13]
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.