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.
Last modified on 2024-02-19.

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 for transpose coherently invertible maps.

Note. Coherently invertible maps are referred to as half adjoint equivalences in Homotopy Type Theory – Univalent Foundations of Mathematics.

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 Introduction to Homotopy Type Theory.

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)

We get the transpose version for free:

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 Homotopy Type Theory – Univalent Foundations of Mathematics.

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
     \   /
      V V
       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

  1. Egbert Rijke, Introduction to Homotopy Type Theory (2022) (arXiv:2212.11082)
  2. Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013) (website, arXiv:1308.0729)

See also

Recent changes