# Path-split maps

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

Created on 2022-01-26.
Last modified on 2024-06-05.

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.iterated-dependent-product-types
open import foundation.logical-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-product
( is-contr-section-is-equiv
( is-equiv-is-path-split f is-path-split-f))
( is-contr-iterated-Π 2
( λ x 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-has-converse-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-has-converse-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 =
( is-equiv-is-path-split f , is-equiv-is-equiv-is-path-split f)


## References

[Shu14]
Mike Shulman. Universal properties without function extensionality. Blog post, 11 2014. URL: https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/.
[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.