# Coherently invertible maps

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-01-26.

module foundation.coherently-invertible-maps where

open import foundation-core.coherently-invertible-maps public

Imports
open import foundation.action-on-identifications-functions
open import foundation.equivalences
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.fibers-of-maps
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.propositions
open import foundation-core.sections
open import foundation-core.type-theoretic-principle-of-choice


## Properties

### Coherently invertible maps have a contractible type of sections

Proof: Since coherently invertible maps are contractible maps, and products of contractible types are contractible, it follows that the type

  (b : B) → fiber f b


is contractible, for any coherently invertible map f. However, by the type theoretic principle of choice it follows that this type is equivalent to the type

  Σ (B → A) (λ g → (b : B) → f (g b) ＝ b),


which is the type of sections of f.

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

abstract
is-contr-section-is-coherently-invertible :
{f : A → B} → is-coherently-invertible f → is-contr (section f)
is-contr-section-is-coherently-invertible {f} F =
is-contr-equiv'
( (b : B) → fiber f b)
( distributive-Π-Σ)
( is-contr-Π (is-contr-map-is-coherently-invertible F))


### Being coherently invertible is a property

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

abstract
is-proof-irrelevant-is-coherently-invertible :
is-proof-irrelevant (is-coherently-invertible f)
is-proof-irrelevant-is-coherently-invertible H =
is-contr-equiv'
( _)
( associative-Σ _ _ _)
( is-contr-Σ
( is-contr-section-is-coherently-invertible H)
( section-is-coherently-invertible H)
( is-contr-equiv'
( _)
( distributive-Π-Σ)
( is-contr-Π
( λ x →
is-contr-equiv'
( _)
( equiv-tot
( λ p →
equiv-inv
( ap f p)
( is-section-map-inv-is-coherently-invertible H (f x))))
( is-contr-map-is-coherently-invertible
( is-coherently-invertible-ap-is-coherently-invertible H)
( is-section-map-inv-is-coherently-invertible H (f x)))))))

abstract
is-prop-is-coherently-invertible : is-prop (is-coherently-invertible f)
is-prop-is-coherently-invertible =
is-prop-is-proof-irrelevant is-proof-irrelevant-is-coherently-invertible

abstract
is-equiv-is-coherently-invertible-is-equiv :
is-equiv (is-coherently-invertible-is-equiv {f = f})
is-equiv-is-coherently-invertible-is-equiv =
is-equiv-has-converse-is-prop
( is-property-is-equiv f)
( is-prop-is-coherently-invertible)
( is-equiv-is-coherently-invertible)


### Being transpose coherently invertible is a property

This remains to be formalized.

## References

[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.