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-04-17.
module foundation-core.coherently-invertible-maps where
Imports
open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.homotopy-algebra open import foundation.universe-levels open import foundation.whiskering-higher-homotopies-composition open import foundation.whiskering-homotopies-composition open import foundation-core.commuting-squares-of-homotopies open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.invertible-maps open import foundation-core.retractions open import foundation-core.sections open import foundation-core.whiskering-homotopies-concatenation
Idea
A (two-sided) inverse for a map
f : A → B is a map g : B → A equipped with
homotopies S : f ∘ g ~ id and
R : g ∘ f ~ id. Such data, however is structure on
the map f, and not generally a property.
One way to make the type of inverses into a property is by adding a single
coherence condition between the homotopies of the inverse, asking that the
following diagram commmutes
S ·r f
--------->
f ∘ g ∘ f f.
--------->
f ·l R
We call such data a
coherently invertible map¶. I.e., a
coherently invertible map f : A → B is a map equipped with a two-sided inverse
and this additional coherence.
There is also the alternative coherence condition we could add
R ·r g
--------->
g ∘ f ∘ g g.
--------->
g ·l S
We will colloquially refer to invertible maps equipped with this coherence as transpose coherently invertible maps.
Note. Coherently invertible maps are referred to as half adjoint equivalences¶ in [UF13].
On this page we will prove that every two-sided inverse g of f can be
promoted to a coherent two-sided inverse. Thus, for most properties of
coherently invertible maps, it suffices to consider the data of a two-sided
inverse. However, this coherence construction requires us to replace the section
homotopy (or retraction homotopy). For this reason we also give direct
constructions showing
- 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 [Rij22].
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-invertible f) where is-retraction-map-inv-is-coherently-invertible-is-invertible : map-inv-is-invertible H ∘ f ~ id is-retraction-map-inv-is-coherently-invertible-is-invertible = is-retraction-map-inv-is-invertible H abstract is-section-map-inv-is-coherently-invertible-is-invertible : f ∘ map-inv-is-invertible H ~ id is-section-map-inv-is-coherently-invertible-is-invertible = ( ( inv-htpy (is-section-map-inv-is-invertible H)) ·r ( f ∘ map-inv-is-invertible H)) ∙h ( ( ( f) ·l ( is-retraction-map-inv-is-invertible H) ·r ( map-inv-is-invertible H)) ∙h ( is-section-map-inv-is-invertible H)) abstract inv-coh-is-coherently-invertible-is-invertible : f ·l is-retraction-map-inv-is-coherently-invertible-is-invertible ~ is-section-map-inv-is-coherently-invertible-is-invertible ·r f inv-coh-is-coherently-invertible-is-invertible = left-transpose-htpy-concat ( ( is-section-map-inv-is-invertible H) ·r ( f ∘ map-inv-is-invertible H ∘ f)) ( f ·l is-retraction-map-inv-is-invertible H) ( ( ( f) ·l ( is-retraction-map-inv-is-invertible H) ·r ( map-inv-is-invertible H ∘ f)) ∙h ( is-section-map-inv-is-invertible H ·r f)) ( ( ( nat-htpy (is-section-map-inv-is-invertible H ·r f)) ·r ( is-retraction-map-inv-is-invertible H)) ∙h ( right-whisker-concat-htpy ( ( inv-preserves-comp-left-whisker-comp ( f) ( map-inv-is-invertible H ∘ f) ( is-retraction-map-inv-is-invertible H)) ∙h ( left-whisker-comp² ( f) ( inv-coh-htpy-id (is-retraction-map-inv-is-invertible H)))) ( is-section-map-inv-is-invertible H ·r f))) abstract coh-is-coherently-invertible-is-invertible : coherence-is-coherently-invertible ( f) ( map-inv-is-invertible H) ( is-section-map-inv-is-coherently-invertible-is-invertible) ( is-retraction-map-inv-is-coherently-invertible-is-invertible) coh-is-coherently-invertible-is-invertible = inv-htpy inv-coh-is-coherently-invertible-is-invertible is-coherently-invertible-is-invertible : is-coherently-invertible f is-coherently-invertible-is-invertible = ( map-inv-is-invertible H , is-section-map-inv-is-coherently-invertible-is-invertible , is-retraction-map-inv-is-coherently-invertible-is-invertible , coh-is-coherently-invertible-is-invertible)
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 [UF13].
Proof. By naturality of homotopies we have
gfRg
gfgfg --------------------> gfg
| |
Rgfg | nat-htpy R ·r (R ·r g) | Rg
∨ ∨
gfg ----------------------> g.
Rg
We can paste the homotopy
g (inv-coh-htpy-id S) ∙ gHg : Sgfg ~ gfSg ~ gfRg
along the top edge of this naturality square obtaining the coherence square
gfgS
gfgfg -------> gfg
| |
Rgfg | | Rg
∨ ∨
gfg ---------> g.
Rg
There is also the naturality square
gfgS
gfgfg --------------------> gfg
| |
Rgfg | nat-htpy (R ·r g) ·r S | Rg
∨ ∨
gfg ----------------------> g.
gS
Now, by pasting these along the common edge Rgfg, we obtain
gfgS gfgS
gfg <------- gfgfg -------> gfg
| | |
Rg | | Rgfg | Rg
∨ ∨ ∨
g <--------- gfg --------> gm
Rg gS
After cancelling gfgS and Rg with themselves, we are left with Rg ~ gS as
desired.
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) (S : is-section f g) (R : is-retraction f g) (H : coherence-is-coherently-invertible f g S R) where abstract coh-transposition-coherence-is-coherently-invertible : (g ∘ f ∘ g) ·l S ~ (g ∘ f) ·l R ·r g coh-transposition-coherence-is-coherently-invertible = ( inv-preserves-comp-left-whisker-comp g (f ∘ g) S) ∙h ( left-whisker-comp² g (inv-coh-htpy-id S)) ∙h ( double-whisker-comp² g H g) ∙h ( preserves-comp-left-whisker-comp g f (R ·r g)) abstract naturality-square-transposition-coherence-is-coherently-invertible : coherence-square-homotopies ( R ·r (g ∘ f ∘ g)) ( (g ∘ f ∘ g) ·l S) ( R ·r g) ( R ·r g) naturality-square-transposition-coherence-is-coherently-invertible = ( ap-concat-htpy' ( R ·r g) ( coh-transposition-coherence-is-coherently-invertible)) ∙h ( inv-htpy (nat-htpy R ·r (R ·r g))) ∙h ( ap-concat-htpy ( R ·r (g ∘ f ∘ g)) ( left-unit-law-left-whisker-comp (R ·r g))) abstract coherence-transposition-coherence-is-coherently-invertible : coherence-is-transpose-coherently-invertible f g S R coherence-transposition-coherence-is-coherently-invertible = ( ap-concat-htpy' ( R ·r g) ( inv-htpy (left-inv-htpy ((g ∘ f ∘ g) ·l S)))) ∙h ( assoc-htpy (inv-htpy ((g ∘ f ∘ g) ·l S)) ((g ∘ f ∘ g) ·l S) (R ·r g)) ∙h ( ap-concat-htpy ( inv-htpy ((g ∘ f ∘ g) ·l S)) ( inv-htpy (nat-htpy (R ·r g) ·r S))) ∙h ( inv-htpy ( assoc-htpy ( inv-htpy ((g ∘ f ∘ g) ·l S)) ( R ·r (g ∘ f ∘ g)) ( g ·l S))) ∙h ( ap-concat-htpy' ( g ·l S) ( ( vertical-inv-coherence-square-homotopies ( R ·r (g ∘ f ∘ g)) ((g ∘ f ∘ g) ·l S) (R ·r g) (R ·r g) ( naturality-square-transposition-coherence-is-coherently-invertible)) ∙h ( right-inv-htpy (R ·r g))))
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where coherence-transposition-is-coherently-invertible : (H : is-coherently-invertible f) → coherence-is-transpose-coherently-invertible ( f) ( map-inv-is-coherently-invertible H) ( is-section-map-inv-is-coherently-invertible H) ( is-retraction-map-inv-is-coherently-invertible H) coherence-transposition-is-coherently-invertible ( g , S , R , H) = coherence-transposition-coherence-is-coherently-invertible f g S R H transposition-is-coherently-invertible : is-coherently-invertible f → is-transpose-coherently-invertible f transposition-is-coherently-invertible H = is-transpose-coherently-invertible-transpose-coherence-is-invertible ( is-invertible-is-coherently-invertible H) ( coherence-transposition-is-coherently-invertible H)
Transpose coherently invertible maps are coherently invertible
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where coherence-transposition-is-transpose-coherently-invertible : (H : is-transpose-coherently-invertible f) → coherence-is-coherently-invertible ( f) ( map-inv-is-transpose-coherently-invertible H) ( is-section-map-inv-is-transpose-coherently-invertible H) ( is-retraction-map-inv-is-transpose-coherently-invertible H) coherence-transposition-is-transpose-coherently-invertible H = coherence-transposition-is-coherently-invertible ( is-coherently-invertible-map-inv-is-transpose-coherently-invertible H) transposition-is-transpose-coherently-invertible : is-transpose-coherently-invertible f → is-coherently-invertible f transposition-is-transpose-coherently-invertible H = is-coherently-invertible-coherence-is-invertible ( is-invertible-is-transpose-coherently-invertible H) ( coherence-transposition-is-transpose-coherently-invertible H) module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where transposition-coherently-invertible-map : coherently-invertible-map A B → transpose-coherently-invertible-map A B transposition-coherently-invertible-map (f , H) = ( f , transposition-is-coherently-invertible H) transposition-transpose-coherently-invertible-map : transpose-coherently-invertible-map A B → coherently-invertible-map A B transposition-transpose-coherently-invertible-map (f , H) = ( f , transposition-is-transpose-coherently-invertible H)
Coherently invertible maps are closed under homotopies
Proof. Assume given a coherently invertible map f with inverse g,
homotopies S : f ∘ g ~ id, R : g ∘ f ~ id and coherence C : Sf ~ fR.
Moreover, assume the map f' is homotopic to f with homotopy H : f' ~ f.
Then g is also a two-sided inverse to f' via the homotopies
S' := Hg ∙ S : f' ∘ g ~ id and R' := gH ∙ R : g ∘ f' ~ id.
Moreover, these witnesses are part of a coherent inverse to f'. To show this,
we must construct a coherence C' of the square
Hgf'
f'gf' -----> f'gf
| |
f'gH | | Sf'
∨ ∨
f'gf -------> f'.
f'R
We begin by observing that C fits somewhere along the diagonal of this square
via the composite
Sf
HgH ------> H⁻¹
f'gf' ------> fgf C f ------> f'.
------>
fR
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f f' : A → B} (H : f' ~ f) (g : B → A) (S : f ∘ g ~ id) (R : g ∘ f ~ id) (C : S ·r f ~ f ·l R) where coh-coh-is-coherently-invertible-htpy : horizontal-concat-htpy' (H ·r g) H ∙h (S ·r f ∙h inv-htpy H) ~ horizontal-concat-htpy' (H ·r g) H ∙h (f ·l R ∙h inv-htpy H) coh-coh-is-coherently-invertible-htpy = left-whisker-concat-htpy ( horizontal-concat-htpy' (H ·r g) H) ( right-whisker-concat-htpy C (inv-htpy H))
Now the problem is reduced to constructing two homotopies
Hgf' ∙ Sf' ~ HgH ∙ Sf ∙ H⁻¹ and f'gH ∙ f'R ~ HgH ∙ fR ∙ H⁻¹.
By the two equivalent constructions of the horizontal composite HgH
Hgf' ∙ fgH ~ HgH ~ f'gH ∙ Hgf
constructing the two homotopies is equivalent to constructing coherences of the squares
fgH Hgf
fgf' -------> fgf f'gf -------> fgf
| | | |
Sf' | | Sf f'R | | fR
∨ ∨ ∨ ∨
f' ---------> f f' ---------> f.
H H
However, these squares are naturality squares, so we are done.
coh-section-is-coherently-invertible-htpy : (H ·r g ∙h S) ·r f' ~ horizontal-concat-htpy' (H ·r g) H ∙h ((S ·r f) ∙h inv-htpy H) coh-section-is-coherently-invertible-htpy = ( left-whisker-concat-htpy ( H ·r (g ∘ f')) ( right-transpose-htpy-concat (S ·r f') H ((f ∘ g) ·l H ∙h S ·r f) ( ( ap-concat-htpy ( S ·r f') ( inv-htpy (left-unit-law-left-whisker-comp H))) ∙h ( nat-htpy S ·r H)))) ∙h ( ( ap-concat-htpy ( H ·r (g ∘ f')) ( assoc-htpy ((f ∘ g) ·l H) (S ·r f) (inv-htpy H))) ∙h ( inv-htpy ( assoc-htpy (H ·r (g ∘ f')) ((f ∘ g) ·l H) ((S ·r f) ∙h inv-htpy H)))) coh-retraction-is-coherently-invertible-htpy : horizontal-concat-htpy' (H ·r g) H ∙h ((f ·l R) ∙h inv-htpy H) ~ f' ·l ((g ·l H) ∙h R) coh-retraction-is-coherently-invertible-htpy = ( ap-concat-htpy' ( f ·l R ∙h inv-htpy H) ( coh-horizontal-concat-htpy (H ·r g) H)) ∙h ( assoc-htpy ((f' ∘ g) ·l H) (H ·r (g ∘ f)) (f ·l R ∙h inv-htpy H)) ∙h ( ap-concat-htpy ( (f' ∘ g) ·l H) ( inv-htpy (assoc-htpy (H ·r (g ∘ f)) (f ·l R) (inv-htpy H)))) ∙h ( left-whisker-concat-htpy ( (f' ∘ g) ·l H) ( inv-htpy ( right-transpose-htpy-concat (f' ·l R) H ((H ·r (g ∘ f) ∙h f ·l R)) ( inv-htpy (nat-htpy H ·r R))))) ∙h ( ap-concat-htpy' ( f' ·l R) ( inv-preserves-comp-left-whisker-comp f' g H)) ∙h ( inv-htpy (distributive-left-whisker-comp-concat f' (g ·l H) R))
Finally, we concatenate the three coherences to obtain our desired result.
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f f' : A → B} where abstract coh-is-coherently-invertible-htpy : (H : f' ~ f) (F : is-coherently-invertible f) → coherence-is-coherently-invertible ( f') ( map-inv-is-coherently-invertible F) ( is-section-map-inv-is-invertible-htpy ( H) ( is-invertible-is-coherently-invertible F)) ( is-retraction-map-inv-is-invertible-htpy ( H) ( is-invertible-is-coherently-invertible F)) coh-is-coherently-invertible-htpy H F = ( coh-section-is-coherently-invertible-htpy H ( map-inv-is-coherently-invertible F) ( is-section-map-inv-is-coherently-invertible F) ( is-retraction-map-inv-is-coherently-invertible F) ( coh-is-coherently-invertible F)) ∙h ( coh-coh-is-coherently-invertible-htpy H ( map-inv-is-coherently-invertible F) ( is-section-map-inv-is-coherently-invertible F) ( is-retraction-map-inv-is-coherently-invertible F) ( coh-is-coherently-invertible F)) ∙h ( coh-retraction-is-coherently-invertible-htpy H ( map-inv-is-coherently-invertible F) ( is-section-map-inv-is-coherently-invertible F) ( is-retraction-map-inv-is-coherently-invertible F) ( coh-is-coherently-invertible F)) is-coherently-invertible-htpy : f' ~ f → is-coherently-invertible f → is-coherently-invertible f' is-coherently-invertible-htpy H F = is-coherently-invertible-coherence-is-invertible ( is-invertible-htpy H (is-invertible-is-coherently-invertible F)) ( coh-is-coherently-invertible-htpy H F) is-coherently-invertible-inv-htpy : f ~ f' → is-coherently-invertible f → is-coherently-invertible f' is-coherently-invertible-inv-htpy H = is-coherently-invertible-htpy (inv-htpy H) module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where is-coherently-invertible-htpy-coherently-invertible-map : (e : coherently-invertible-map A B) → f ~ map-coherently-invertible-map e → is-coherently-invertible f is-coherently-invertible-htpy-coherently-invertible-map (e , E) H = is-coherently-invertible-htpy H E is-coherently-invertible-inv-htpy-coherently-invertible-map : (e : coherently-invertible-map A B) → map-coherently-invertible-map e ~ f → is-coherently-invertible f is-coherently-invertible-inv-htpy-coherently-invertible-map (e , E) H = is-coherently-invertible-inv-htpy H E
The identity map is coherently invertible
module _ {l : Level} {A : UU l} where is-coherently-invertible-id : is-coherently-invertible (id {A = A}) is-coherently-invertible-id = is-coherently-invertible-coherence-is-invertible is-invertible-id refl-htpy id-coherently-invertible-map : coherently-invertible-map A A id-coherently-invertible-map = ( id , is-coherently-invertible-id) is-transpose-coherently-invertible-id : is-transpose-coherently-invertible (id {A = A}) is-transpose-coherently-invertible-id = is-transpose-coherently-invertible-map-inv-is-coherently-invertible ( is-coherently-invertible-id) id-transpose-coherently-invertible-map : transpose-coherently-invertible-map A A id-transpose-coherently-invertible-map = ( id , is-transpose-coherently-invertible-id)
Inversion of coherently invertible maps
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where is-coherently-invertible-map-inv-is-coherently-invertible : {f : A → B} (H : is-coherently-invertible f) → is-coherently-invertible (map-inv-is-coherently-invertible H) is-coherently-invertible-map-inv-is-coherently-invertible H = is-coherently-invertible-map-inv-is-transpose-coherently-invertible ( transposition-is-coherently-invertible H) is-transpose-coherently-invertible-map-inv-is-transpose-coherently-invertible : {f : A → B} (H : is-transpose-coherently-invertible f) → is-transpose-coherently-invertible ( map-inv-is-transpose-coherently-invertible H) is-transpose-coherently-invertible-map-inv-is-transpose-coherently-invertible H = transposition-is-coherently-invertible ( is-coherently-invertible-map-inv-is-transpose-coherently-invertible H) inv-coherently-invertible-map : coherently-invertible-map A B → coherently-invertible-map B A inv-coherently-invertible-map (f , H) = ( map-inv-is-coherently-invertible H , is-coherently-invertible-map-inv-is-coherently-invertible H) inv-transpose-coherently-invertible-map : transpose-coherently-invertible-map A B → transpose-coherently-invertible-map B A inv-transpose-coherently-invertible-map (f , H) = ( map-inv-is-transpose-coherently-invertible H , is-transpose-coherently-invertible-map-inv-is-transpose-coherently-invertible ( H))
Composition of coherently invertible maps
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (g : B → C) (f : A → B) (G : is-coherently-invertible g) (F : is-coherently-invertible f) where coh-is-coherently-invertible-comp : coherence-is-coherently-invertible ( g ∘ f) ( map-inv-is-invertible-comp g f ( is-invertible-is-coherently-invertible G) ( is-invertible-is-coherently-invertible F)) ( is-section-map-inv-is-invertible-comp g f ( is-invertible-is-coherently-invertible G) ( is-invertible-is-coherently-invertible F)) ( is-retraction-map-inv-is-invertible-comp g f ( is-invertible-is-coherently-invertible G) ( is-invertible-is-coherently-invertible F)) coh-is-coherently-invertible-comp = ( ap-concat-htpy ( ( g) ·l ( is-section-map-inv-is-coherently-invertible F) ·r ( map-inv-is-coherently-invertible G ∘ g ∘ f)) ( coh-is-coherently-invertible G ·r f)) ∙h ( right-whisker-comp² ( ( nat-htpy (g ·l is-section-map-inv-is-coherently-invertible F)) ·r ( is-retraction-map-inv-is-coherently-invertible G)) ( f)) ∙h ( ap-binary-concat-htpy ( inv-preserves-comp-left-whisker-comp ( g ∘ f) ( map-inv-is-coherently-invertible F) ( is-retraction-map-inv-is-coherently-invertible G ·r f)) ( ( left-whisker-comp² g (coh-is-coherently-invertible F)) ∙h ( preserves-comp-left-whisker-comp g f ( is-retraction-map-inv-is-coherently-invertible F)))) ∙h ( inv-htpy ( distributive-left-whisker-comp-concat ( g ∘ f) ( ( map-inv-is-coherently-invertible F) ·l ( is-retraction-map-inv-is-coherently-invertible G ·r f)) ( is-retraction-map-inv-is-coherently-invertible F))) is-coherently-invertible-comp : is-coherently-invertible (g ∘ f) is-coherently-invertible-comp = is-coherently-invertible-coherence-is-invertible ( is-invertible-comp g f ( is-invertible-is-coherently-invertible G) ( is-invertible-is-coherently-invertible F)) ( coh-is-coherently-invertible-comp) module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (g : B → C) (f : A → B) (G : is-transpose-coherently-invertible g) (F : is-transpose-coherently-invertible f) where coh-is-transpose-coherently-invertible-comp : coherence-is-transpose-coherently-invertible ( g ∘ f) ( map-inv-is-invertible-comp g f ( is-invertible-is-transpose-coherently-invertible G) ( is-invertible-is-transpose-coherently-invertible F)) ( is-section-map-inv-is-invertible-comp g f ( is-invertible-is-transpose-coherently-invertible G) ( is-invertible-is-transpose-coherently-invertible F)) ( is-retraction-map-inv-is-invertible-comp g f ( is-invertible-is-transpose-coherently-invertible G) ( is-invertible-is-transpose-coherently-invertible F)) coh-is-transpose-coherently-invertible-comp = coh-is-coherently-invertible-comp ( map-inv-is-transpose-coherently-invertible F) ( map-inv-is-transpose-coherently-invertible G) ( is-coherently-invertible-map-inv-is-transpose-coherently-invertible F) ( is-coherently-invertible-map-inv-is-transpose-coherently-invertible G) is-transpose-coherently-invertible-comp : is-transpose-coherently-invertible (g ∘ f) is-transpose-coherently-invertible-comp = is-transpose-coherently-invertible-transpose-coherence-is-invertible ( is-invertible-comp g f ( is-invertible-is-transpose-coherently-invertible G) ( is-invertible-is-transpose-coherently-invertible F)) ( coh-is-transpose-coherently-invertible-comp) module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} where comp-coherently-invertible-map : coherently-invertible-map B C → coherently-invertible-map A B → coherently-invertible-map A C comp-coherently-invertible-map (g , G) (f , F) = ( g ∘ f , is-coherently-invertible-comp g f G F) comp-transpose-coherently-invertible-map : transpose-coherently-invertible-map B C → transpose-coherently-invertible-map A B → transpose-coherently-invertible-map A C comp-transpose-coherently-invertible-map (g , G) (f , F) = ( g ∘ f , is-transpose-coherently-invertible-comp g f G F)
The 3-for-2 property of coherently invertible maps
The 3-for-2 property¶ of coherently invertible maps asserts that for any commuting triangle of maps
h
A ------> B
\ /
f\ /g
\ /
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
- [Rij22]
- Egbert Rijke. Introduction to Homotopy Type Theory. 12 2022. arXiv:2212.11082.
- [UF13]
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.
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 Lab
Recent changes
- 2024-04-17. Fredrik Bakke. Splitting idempotents (#1105).
- 2024-03-20. Fredrik Bakke. chore: Janitorial work in foundation (#1086).
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 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).