Coherently invertible maps
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Elisabeth Bonnevier.
Created on 2022-01-26.
Last modified on 2023-09-12.
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.dependent-pair-types open import foundation.equivalences open import foundation.identity-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-theoretic-principle-of-choice 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.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.propositions open import foundation-core.sections open import foundation-core.whiskering-homotopies
Properties
Being coherently invertible is a property
abstract is-prop-is-coherently-invertible : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-prop (is-coherently-invertible f) is-prop-is-coherently-invertible {A = A} {B} f = is-prop-is-proof-irrelevant ( λ H → is-contr-equiv' ( Σ ( section f) ( λ s → Σ ( ( map-section f s ∘ f) ~ id) ( λ H → ( htpy-right-whisk (is-section-map-section f s) f) ~ ( htpy-left-whisk f H)))) ( associative-Σ ( B → A) ( λ g → (f ∘ g) ~ id) ( λ s → Σ ( ( map-section f s ∘ f) ~ id) ( λ H → ( htpy-right-whisk (is-section-map-section f s) f) ~ ( htpy-left-whisk f H)))) ( is-contr-Σ ( is-contr-section-is-equiv (is-equiv-is-coherently-invertible H)) ( section-is-coherently-invertible H) ( is-contr-equiv' ( (x : A) → Σ ( map-inv-is-coherently-invertible H (f x) = x) ( λ p → is-retraction-is-coherently-invertible H (f x) = ap f p)) ( distributive-Π-Σ) ( is-contr-Π ( λ x → is-contr-equiv' ( fiber ( ap f) ( is-retraction-is-coherently-invertible H (f x))) ( equiv-tot ( λ p → equiv-inv ( ap f p) ( is-retraction-is-coherently-invertible H (f x)))) ( is-contr-map-is-equiv ( is-emb-is-equiv ( is-equiv-is-coherently-invertible H) ( map-inv-is-coherently-invertible H (f x)) x) ( is-retraction-is-coherently-invertible H (f x)))))))) abstract is-equiv-is-coherently-invertible-is-equiv : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-equiv (is-coherently-invertible-is-equiv {f = f}) is-equiv-is-coherently-invertible-is-equiv f = is-equiv-is-prop ( is-property-is-equiv f) ( is-prop-is-coherently-invertible f) ( is-equiv-is-coherently-invertible)
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
.
Recent changes
- 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-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).