Path-split maps
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-01-26.
Last modified on 2023-06-28.
module foundation.path-split-maps where open import foundation-core.path-split-maps public
Imports
open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.propositions
Properties
Being path-split is a property
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where abstract is-prop-is-path-split : (f : A → B) → is-prop (is-path-split f) is-prop-is-path-split f = is-prop-is-proof-irrelevant ( λ is-path-split-f → ( is-contr-prod ( is-contr-section-is-equiv ( is-equiv-is-path-split f is-path-split-f)) ( is-contr-Π ( λ x → is-contr-Π ( λ y → is-contr-section-is-equiv ( is-emb-is-equiv ( is-equiv-is-path-split f is-path-split-f) x y)))))) abstract is-equiv-is-path-split-is-equiv : (f : A → B) → is-equiv (is-path-split-is-equiv f) is-equiv-is-path-split-is-equiv f = is-equiv-is-prop ( is-property-is-equiv f) ( is-prop-is-path-split f) ( is-equiv-is-path-split f) equiv-is-path-split-is-equiv : (f : A → B) → is-equiv f ≃ is-path-split f equiv-is-path-split-is-equiv f = pair (is-path-split-is-equiv f) (is-equiv-is-path-split-is-equiv f) abstract is-equiv-is-equiv-is-path-split : (f : A → B) → is-equiv (is-equiv-is-path-split f) is-equiv-is-equiv-is-path-split f = is-equiv-is-prop ( is-prop-is-path-split f) ( is-property-is-equiv f) ( is-path-split-is-equiv f) equiv-is-equiv-is-path-split : (f : A → B) → is-path-split f ≃ is-equiv f equiv-is-equiv-is-path-split f = pair (is-equiv-is-path-split f) (is-equiv-is-equiv-is-path-split f)
See also
- For the notion of biinvertible maps see
foundation.equivalences
. - For the notions of inverses and coherently invertible maps, also known as
half-adjoint equivalences, see
foundation.coherently-invertible-maps
. - For the notion of maps with contractible fibers see
foundation.contractible-maps
.
References
- Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013) (website, arXiv:1308.0729, DOI:10.48550)
- Mike Shulman, Universal properties without function extensionality (November 2014) (HoTT Blog)
Recent changes
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).