# Invertible maps

Content created by Fredrik Bakke, Egbert Rijke and maybemabeline.

Created on 2023-09-11.

module foundation.invertible-maps where

open import foundation-core.invertible-maps public

Imports
open import foundation.action-on-identifications-functions
open import foundation.commuting-triangles-of-homotopies
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.full-subtypes
open import foundation.function-extensionality
open import foundation.functoriality-cartesian-product-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-algebra
open import foundation.homotopy-induction
open import foundation.postcomposition-functions
open import foundation.retractions
open import foundation.sections
open import foundation.structure-identity-principle
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.cartesian-product-types
open import foundation-core.coherently-invertible-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.torsorial-type-families
open import foundation-core.truncated-types
open import foundation-core.truncation-levels

open import synthetic-homotopy-theory.free-loops


## Properties

### Characterizing equality of invertible maps

#### Characterizing equality of is-inverse

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

htpy-is-inverse : (s t : is-inverse f g) → UU (l1 ⊔ l2)
htpy-is-inverse s t = (pr1 s ~ pr1 t) × (pr2 s ~ pr2 t)

extensionality-is-inverse :
{s t : is-inverse f g} → (s ＝ t) ≃ htpy-is-inverse s t
extensionality-is-inverse {s} {t} =
equiv-product equiv-funext equiv-funext ∘e equiv-pair-eq s t

htpy-eq-is-inverse : {s t : is-inverse f g} → s ＝ t → htpy-is-inverse s t
htpy-eq-is-inverse = map-equiv extensionality-is-inverse

eq-htpy-is-inverse : {s t : is-inverse f g} → htpy-is-inverse s t → s ＝ t
eq-htpy-is-inverse = map-inv-equiv extensionality-is-inverse


#### Characterizing equality of is-invertible

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

coherence-htpy-is-invertible :
(s t : is-invertible f) →
map-inv-is-invertible s ~ map-inv-is-invertible t → UU (l1 ⊔ l2)
coherence-htpy-is-invertible s t H =
( coherence-htpy-section {f = f}
( section-is-invertible s)
( section-is-invertible t)
( H)) ×
( coherence-htpy-retraction
( retraction-is-invertible s)
( retraction-is-invertible t)
( H))

htpy-is-invertible : (s t : is-invertible f) → UU (l1 ⊔ l2)
htpy-is-invertible s t =
Σ ( map-inv-is-invertible s ~ map-inv-is-invertible t)
( coherence-htpy-is-invertible s t)

refl-htpy-is-invertible : (s : is-invertible f) → htpy-is-invertible s s
pr1 (refl-htpy-is-invertible s) = refl-htpy
pr1 (pr2 (refl-htpy-is-invertible s)) = refl-htpy
pr2 (pr2 (refl-htpy-is-invertible s)) = refl-htpy

htpy-eq-is-invertible :
(s t : is-invertible f) → s ＝ t → htpy-is-invertible s t
htpy-eq-is-invertible s .s refl = refl-htpy-is-invertible s

is-torsorial-htpy-is-invertible :
(s : is-invertible f) → is-torsorial (htpy-is-invertible s)
is-torsorial-htpy-is-invertible s =
is-torsorial-Eq-structure
( is-torsorial-htpy (map-inv-is-invertible s))
( map-inv-is-invertible s , refl-htpy)
( is-torsorial-Eq-structure
( is-torsorial-htpy (is-section-map-inv-is-invertible s))
( is-section-map-inv-is-invertible s , refl-htpy)
(is-torsorial-htpy (is-retraction-map-inv-is-invertible s)))

is-equiv-htpy-eq-is-invertible :
(s t : is-invertible f) → is-equiv (htpy-eq-is-invertible s t)
is-equiv-htpy-eq-is-invertible s =
fundamental-theorem-id
( is-torsorial-htpy-is-invertible s)
( htpy-eq-is-invertible s)

extensionality-is-invertible :
(s t : is-invertible f) → (s ＝ t) ≃ (htpy-is-invertible s t)
pr1 (extensionality-is-invertible s t) = htpy-eq-is-invertible s t
pr2 (extensionality-is-invertible s t) = is-equiv-htpy-eq-is-invertible s t

eq-htpy-is-invertible :
(s t : is-invertible f) → htpy-is-invertible s t → s ＝ t
eq-htpy-is-invertible s t = map-inv-equiv (extensionality-is-invertible s t)


#### Characterizing equality of invertible-map

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

coherence-htpy-invertible-map :
(s t : invertible-map A B) →
map-invertible-map s ~ map-invertible-map t →
map-inv-invertible-map s ~ map-inv-invertible-map t → UU (l1 ⊔ l2)
coherence-htpy-invertible-map s t H I =
( coherence-triangle-homotopies
( is-section-map-inv-invertible-map s)
( is-section-map-inv-invertible-map t)
( horizontal-concat-htpy H I)) ×
( coherence-triangle-homotopies
( is-retraction-map-inv-invertible-map s)
( is-retraction-map-inv-invertible-map t)
( horizontal-concat-htpy I H))

htpy-invertible-map : (s t : invertible-map A B) → UU (l1 ⊔ l2)
htpy-invertible-map s t =
Σ ( map-invertible-map s ~ map-invertible-map t)
( λ H →
Σ ( map-inv-invertible-map s ~ map-inv-invertible-map t)
( coherence-htpy-invertible-map s t H))

refl-htpy-invertible-map : (s : invertible-map A B) → htpy-invertible-map s s
pr1 (refl-htpy-invertible-map s) = refl-htpy
pr1 (pr2 (refl-htpy-invertible-map s)) = refl-htpy
pr1 (pr2 (pr2 (refl-htpy-invertible-map s))) = refl-htpy
pr2 (pr2 (pr2 (refl-htpy-invertible-map s))) = refl-htpy

htpy-eq-invertible-map :
(s t : invertible-map A B) → s ＝ t → htpy-invertible-map s t
htpy-eq-invertible-map s .s refl = refl-htpy-invertible-map s

is-torsorial-htpy-invertible-map :
(s : invertible-map A B) → is-torsorial (htpy-invertible-map s)
is-torsorial-htpy-invertible-map s =
is-torsorial-Eq-structure
( is-torsorial-htpy (map-invertible-map s))
( map-invertible-map s , refl-htpy)
( is-torsorial-Eq-structure
( is-torsorial-htpy (map-inv-invertible-map s))
( map-inv-invertible-map s , refl-htpy)
( is-torsorial-Eq-structure
( is-torsorial-htpy (is-section-map-inv-invertible-map s))
( is-section-map-inv-invertible-map s , refl-htpy)
( is-torsorial-htpy (is-retraction-map-inv-invertible-map s))))

is-equiv-htpy-eq-invertible-map :
(s t : invertible-map A B) → is-equiv (htpy-eq-invertible-map s t)
is-equiv-htpy-eq-invertible-map s =
fundamental-theorem-id
( is-torsorial-htpy-invertible-map s)
( htpy-eq-invertible-map s)

extensionality-invertible-map :
(s t : invertible-map A B) → (s ＝ t) ≃ (htpy-invertible-map s t)
pr1 (extensionality-invertible-map s t) = htpy-eq-invertible-map s t
pr2 (extensionality-invertible-map s t) = is-equiv-htpy-eq-invertible-map s t

eq-htpy-invertible-map :
(s t : invertible-map A B) → htpy-invertible-map s t → s ＝ t
eq-htpy-invertible-map s t = map-inv-equiv (extensionality-invertible-map s t)


### If the domains are k-truncated, then the type of inverses is k-truncated

module _
{l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
where

is-trunc-is-inverse :
(f : A → B) (g : B → A) →
is-trunc (succ-𝕋 k) A → is-trunc (succ-𝕋 k) B →
is-trunc k (is-inverse f g)
is-trunc-is-inverse f g is-trunc-A is-trunc-B =
is-trunc-product k
( is-trunc-Π k (λ x → is-trunc-B (f (g x)) x))
( is-trunc-Π k (λ x → is-trunc-A (g (f x)) x))

is-trunc-is-invertible :
(f : A → B) →
is-trunc k A → is-trunc (succ-𝕋 k) B →
is-trunc k (is-invertible f)
is-trunc-is-invertible f is-trunc-A is-trunc-B =
is-trunc-Σ
( is-trunc-function-type k is-trunc-A)
( λ g →
is-trunc-is-inverse f g
( is-trunc-succ-is-trunc k is-trunc-A)
( is-trunc-B))

is-trunc-invertible-map :
is-trunc k A → is-trunc k B →
is-trunc k (invertible-map A B)
is-trunc-invertible-map is-trunc-A is-trunc-B =
is-trunc-Σ
( is-trunc-function-type k is-trunc-B)
( λ f →
is-trunc-is-invertible f
( is-trunc-A)
( is-trunc-succ-is-trunc k is-trunc-B))


### The type is-invertible id is equivalent to id ~ id

is-invertible-id-htpy-id-id :
{l : Level} (A : UU l) →
(id {A = A} ~ id {A = A}) → is-invertible (id {A = A})
pr1 (is-invertible-id-htpy-id-id A H) = id
pr1 (pr2 (is-invertible-id-htpy-id-id A H)) = refl-htpy
pr2 (pr2 (is-invertible-id-htpy-id-id A H)) = H

triangle-is-invertible-id-htpy-id-id :
{l : Level} (A : UU l) →
( is-invertible-id-htpy-id-id A) ~
( ( map-associative-Σ
( A → A)
( λ g → (id ∘ g) ~ id)
( λ s → (pr1 s ∘ id) ~ id)) ∘
( map-inv-left-unit-law-Σ-is-contr
{ B = λ s → (pr1 s ∘ id) ~ id}
( is-contr-section-is-equiv (is-equiv-id {_} {A}))
( pair id refl-htpy)))
triangle-is-invertible-id-htpy-id-id A H = refl

abstract
is-equiv-is-invertible-id-htpy-id-id :
{l : Level} (A : UU l) → is-equiv (is-invertible-id-htpy-id-id A)
is-equiv-is-invertible-id-htpy-id-id A =
is-equiv-left-map-triangle
( is-invertible-id-htpy-id-id A)
( map-associative-Σ
( A → A)
( λ g → (id ∘ g) ~ id)
( λ s → (pr1 s ∘ id) ~ id))
( map-inv-left-unit-law-Σ-is-contr
( is-contr-section-is-equiv is-equiv-id)
( pair id refl-htpy))
( triangle-is-invertible-id-htpy-id-id A)
( is-equiv-map-inv-left-unit-law-Σ-is-contr
( is-contr-section-is-equiv is-equiv-id)
( pair id refl-htpy))
( is-equiv-map-associative-Σ _ _ _)


### The type of invertible maps is equivalent to the type of free loops on equivalences

#### The type of invertible equivalences is equivalent to the type of invertible maps

Proof: Since every invertible map is an equivalence, the Σ-type of invertible maps which are equivalences forms a full subtype of the type of invertible maps. Swapping the order of Σ-types then shows that the Σ-type of invertible maps which are equivalences is equivalent to the Σ-type of equivalences which are invertible.

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

is-equiv-prop-is-invertible : (invertible-map A B) → Prop (l1 ⊔ l2)
is-equiv-prop-is-invertible = is-equiv-Prop ∘ map-invertible-map

is-full-subtype-is-equiv-prop-is-invertible :
is-full-subtype is-equiv-prop-is-invertible
is-full-subtype-is-equiv-prop-is-invertible =
is-equiv-is-invertible' ∘ is-invertible-map-invertible-map

equiv-invertible-equivalence-invertible-map :
Σ (A ≃ B) (is-invertible ∘ map-equiv) ≃ invertible-map A B
equiv-invertible-equivalence-invertible-map =
( equiv-inclusion-is-full-subtype
( is-equiv-prop-is-invertible)
( is-full-subtype-is-equiv-prop-is-invertible)) ∘e
( equiv-right-swap-Σ)


#### The type of free loops on equivalences is equivalent to the type of invertible equivalences

Proof: First, associating the order of Σ-types shows that a function being invertible is equivalent to it having a section, such that this section is also its retraction. Now, since equivalences have a contractible type of sections, a proof of invertibility of the underlying map f of an equivalence contracts to just a single homotopy g ∘ f ~ id, showing that a section g of f is also its retraction. As g is a section, composing on the left with f and canceling f ∘ g yields a loop f ~ f. By equivalence extensionality, this loop may be lifted to a loop on the entire equivalence.

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

equiv-is-retraction-section-is-invertible :
(f : A → B) →
Σ (section f) (λ g → (map-section f g) ∘ f ~ id) ≃ is-invertible f
equiv-is-retraction-section-is-invertible f =
associative-Σ
( B → A)
( λ g → f ∘ g ~ id)
( λ g → (map-section f g) ∘ f ~ id)

equiv-free-loop-equivalence-invertible-equivalence :
free-loop (A ≃ B) ≃ Σ (A ≃ B) (is-invertible ∘ map-equiv)
equiv-free-loop-equivalence-invertible-equivalence =
( equiv-tot
( equiv-is-retraction-section-is-invertible ∘ map-equiv)) ∘e
( equiv-tot
( λ f →
( inv-left-unit-law-Σ-is-contr
( is-contr-section-is-equiv (is-equiv-map-equiv f))
( section-is-equiv (is-equiv-map-equiv f))) ∘e
( inv-equiv
( equiv-htpy-postcomp-htpy
( f)
( map-section-is-equiv (is-equiv-map-equiv f) ∘ map-equiv f)
( id))) ∘e
( equiv-concat-htpy
( is-section-map-section-map-equiv f ·r map-equiv f)
( map-equiv f)))) ∘e
( equiv-tot (λ f → extensionality-equiv f f))


#### The equivalence

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

equiv-free-loop-equivalence-invertible-map :
free-loop (A ≃ B) ≃ invertible-map A B
equiv-free-loop-equivalence-invertible-map =
equiv-invertible-equivalence-invertible-map ∘e
equiv-free-loop-equivalence-invertible-equivalence


### The action of invertible maps on identifications is invertible

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

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