Path-split maps

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

Created on 2022-02-07.
Last modified on 2024-03-12.

module foundation-core.path-split-maps where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.coherently-invertible-maps
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.sections

Idea

A map f : A → B is said to be path split if it has a section and its action on identifications x ＝ y → f x ＝ f y has a section for each x y : A. By the fundamental theorem of identity types, it follows that a map is path-split if and only if it is an equivalence.

Definition

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

  is-path-split : UU (l1 ⊔ l2)
  is-path-split = section f × ((x y : A) → section (ap f {x = x} {y = y}))

Properties

A map is path-split if and only if it is an equivalence

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

  abstract
    is-path-split-is-equiv : is-equiv f → is-path-split f
    pr1 (is-path-split-is-equiv is-equiv-f) = pr1 is-equiv-f
    pr2 (is-path-split-is-equiv is-equiv-f) x y =
      pr1 (is-emb-is-equiv is-equiv-f x y)

  abstract
    is-coherently-invertible-is-path-split :
      is-path-split f → is-coherently-invertible f
    pr1 (is-coherently-invertible-is-path-split ((g , G) , s)) =
      g
    pr1 (pr2 (is-coherently-invertible-is-path-split ((g , G) , s))) =
      G
    pr1 (pr2 (pr2 (is-coherently-invertible-is-path-split ((g , G) , s)))) x =
      pr1 (s (g (f x)) x) (G (f x))
    pr2 (pr2 (pr2 (is-coherently-invertible-is-path-split ((g , G) , s)))) x =
      inv (pr2 (s (g (f x)) x) (G (f x)))

  abstract
    is-equiv-is-path-split : is-path-split f → is-equiv f
    is-equiv-is-path-split =
      is-equiv-is-coherently-invertible ∘
      is-coherently-invertible-is-path-split

See also

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.

Recent changes