Path-split maps

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

Created on 2022-02-07.
Last modified on 2024-01-31.

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

  1. Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013) (website, arXiv:1308.0729)
  2. Mike Shulman, Universal properties without function extensionality (November 2014) (HoTT Blog)

Recent changes