The following functions are copy of Escardo’s: — title: Investigations on graph-theoretical constructions in Homotopy type theory —

{-# OPTIONS --without-K --exact-split #-}

module foundations.SectionsAndRetractions where
open import foundations.BasicTypes
open import foundations.BasicFunctions
open import foundations.HLevelTypes
open import foundations.HomotopyType
open import foundations.TypesofMorphisms

has-section : {ℓ₁ ℓ₂ : Level} {X : Type ℓ₁} {Y : Type ℓ₂} → (X → Y) → Type _
has-section r = ∑[ s ] (r ∘ s ∼ id {A = codomain r})

is-section : {ℓ₁ ℓ₂ : Level} {X : Type ℓ₁} {Y : Type ℓ₂ } → (X → Y) → Type _
is-section s = ∑[ r ] (r ∘ s ∼ id)

sections-are-lc : {ℓ₁ ℓ₂ : Level} {X : Type ℓ₁} {Y : Type ℓ₂ } (s : X → Y)
                → is-section s → s is-injective
sections-are-lc s (r , rs) {x} {x'} p = ! (rs x) · ap r p · rs x'

retract_of_ : {ℓ₁ ℓ₂ : Level} → Type ℓ₁ → Type ℓ₂ → Type _
retract Y of X = ∑[ r ∶ (X → Y) ] has-section r

retract-of-singleton
  : {ℓ₁ ℓ₂ : Level} {X : Type ℓ₁} {Y : Type ℓ₂}
  → retract Y of X
  → is-singleton X
  → is-singleton Y
retract-of-singleton (r , s , rs) (c , φ) = r c , λ y → ap r (φ (s y)) · rs y

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides