# 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

- The identity map is coherently invertible.
- The composite of two coherently invertible maps is coherently invertible.
- The inverse of a coherently invertible map is coherently invertible.
- Every map homotopic to a coherently invertible map is coherently invertible.
- 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

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

## See also

- For the notion of biinvertible maps see
`foundation.equivalences`

. - For the notion of maps with contractible fibers see
`foundation.contractible-maps`

. - For the notion of path-split maps see
`foundation.path-split-maps`

.

## External links

- Adjoint equivalences at 1lab
- adjoint equivalence at $n$Lab

## Recent changes

- 2024-02-19. Fredrik Bakke.
*Additions for coherently invertible maps (#1024).* - 2024-02-06. Egbert Rijke and Fredrik Bakke.
*Refactor files about identity types and homotopies (#1014).* - 2023-09-12. Egbert Rijke.
*Factoring out whiskering (#756).* - 2023-09-11. Fredrik Bakke and Egbert Rijke.
*Some computations for different notions of equivalence (#711).* - 2023-09-10. Fredrik Bakke.
*Rename*`inv-con`

and`con-inv`

to`left/right-transpose-eq-concat`

(#730).