Martin Escardo, 27 Jan 2021.

We write down in Agda a result attributed to Martin Escardo by Shulman
(2015) https://arxiv.org/abs/1507.03634, Logical Methods in Computer
Science, April 27, 2017, Volume 12, Issue 3,
https://lmcs.episciences.org/2027

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.Section-Embedding where

open import MLTT.Spartan
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Hedberg
open import UF.KrausLemma
open import UF.ExitPropTrunc
open import UF.PropTrunc
open import UF.Subsingletons

splits : {X : 𝓤 ̇ }  (X  X)  (𝓥 : Universe)  𝓤  (𝓥 ) ̇
splits {𝓤} {X} f 𝓥 = Σ A  𝓥 ̇
                   , Σ r  (X  A)
                   , Σ s  (A  X)
                   , (r  s  id)
                   × (f  s  r)

splits-gives-idempotent : {X : 𝓤 ̇ } (f : X  X)
                         splits f 𝓥
                         idempotent-map f
splits-gives-idempotent f (A , r , s , η , h) x =
  f (f x)         =⟨ ap f (h x) 
  f (s (r x))     =⟨ h (s (r x)) 
  s (r (s (r x))) =⟨ ap s (η (r x)) 
  s (r x)         =⟨ (h x)⁻¹ 
  f x 

split-via-embedding-gives-collapsible : {X : 𝓤 ̇ } (f : X  X)
                                       ((A , r , s , η , h) : splits f 𝓥)
                                       is-embedding s
                                       (x : X)  collapsible (f x  x)
split-via-embedding-gives-collapsible {𝓤} {𝓥} {X} f (A , r , s , η , h) e x = γ
 where
  ϕ : (x : X)  f x  x  fiber s x
  ϕ x p = r x , (s (r x)         =⟨ ap (s  r) (p ⁻¹) 
                 s (r (f x))     =⟨ ap (s  r) (h x) 
                 s (r (s (r x))) =⟨ ap s (η (r x)) 
                 s (r x)         =⟨ (h x)⁻¹ 
                 f x             =⟨ p 
                 x               )

  ψ : (x : X)  fiber s x  f x  x
  ψ x (a , q) = f x         =⟨ h x 
                s (r x)     =⟨ ap (s  r) (q ⁻¹) 
                s (r (s a)) =⟨ ap s (η a) 
                s a         =⟨ q 
                x           

  κ : f x  x  f x  x
  κ = ψ x  ϕ x

  κ-constant : (p p' : f x  x)  κ p  κ p'
  κ-constant p p' = ap (ψ x) (e x (ϕ x p) (ϕ x p'))

  γ : collapsible (f x  x)
  γ = κ , κ-constant

section-embedding-gives-collapsible : {X : 𝓤 ̇ } {A : 𝓥 ̇ }
                                      (r : X  A) (s : A  X) (η : r  s  id)
                                     is-embedding s
                                     (x : X)  collapsible (s (r x)  x)
section-embedding-gives-collapsible {𝓤} {𝓥} {X} {A} r s η =
 split-via-embedding-gives-collapsible (s  r) (A , r , s , η ,  _  refl))

collapsible-gives-split-via-embedding : {X : 𝓤 ̇ } (f : X  X)
                                       idempotent-map f
                                       ((x : X)  collapsible (f x  x))
                                       Σ (A , r , s , η , h)  splits f 𝓤
                                                              , is-embedding s
collapsible-gives-split-via-embedding {𝓤} {X} f i c = γ
 where
  κ : (x : X)  f x  x  f x  x
  κ x = pr₁ (c x)

  κ-constant : (x : X)  wconstant (κ x)
  κ-constant x = pr₂ (c x)

  P : X  𝓤 ̇
  P x = fix (κ x)

  P-is-prop-valued : (x : X)  is-prop (P x)
  P-is-prop-valued x = fix-is-prop (κ x) (κ-constant x)

  A : 𝓤 ̇
  A = Σ x  X , P x

  s : A  X
  s (x , _) = x

  r : X  A
  r x = f x , to-fix (κ (f x)) (κ-constant (f x)) (i x)

  η : r  s  id
  η (x , p , _) = to-subtype-= P-is-prop-valued p

  h : f  s  r
  h x = refl

  𝕘 : (x : X)  fiber s x  P x
  𝕘 x = (Σ (x' , _)  (Σ x  X , P x) , x'  x) ≃⟨ Σ-assoc 
        (Σ x'  X , P x' × (x'  x))            ≃⟨ right-Id-equiv x 
        P x                                     

  e : (x : X)  is-prop (fiber s x)
  e x = equiv-to-prop (𝕘 x) (P-is-prop-valued x)

  γ : Σ (A , r , s , η , h)  splits f 𝓤 , is-embedding s
  γ = (A , r , s , η , h) , e

\end{code}

If we assume the existence of propositional truncations, we can
reformulate the above as follows:

\begin{code}

module _ (pe : propositional-truncations-exist) where

 open PropositionalTruncation pe
 open split-support-and-collapsibility pe

 split-via-embedding-gives-split-support : {X : 𝓤 ̇ } (f : X  X)
                                          ((A , r , s , η , h) : splits f 𝓥)
                                          is-embedding s
                                          (x : X)  has-split-support (f x  x)
 split-via-embedding-gives-split-support f σ e x =
  collapsible-gives-split-support (split-via-embedding-gives-collapsible f σ e x)


 split-support-gives-split-via-embedding : {X : 𝓤 ̇ } (f : X  X)
                                          idempotent-map f
                                          ((x : X)  has-split-support (f x  x))
                                          Σ (A , r , s , η , h)  splits f 𝓤
                                                                 , is-embedding s
 split-support-gives-split-via-embedding f i g =
  collapsible-gives-split-via-embedding f i  x  split-support-gives-collapsible (g x))

 section-embedding-gives-split-support : {X : 𝓤 ̇ } {A : 𝓥 ̇ }
                                         (r : X  A) (s : A  X) (η : r  s  id)
                                        is-embedding s
                                        (x : X)  has-split-support (s (r x)  x)
 section-embedding-gives-split-support r s η e x =
  collapsible-gives-split-support (section-embedding-gives-collapsible r s η e x)

\end{code}