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 --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-}

module UF.Section-Embedding where

open import MLTT.Spartan

open import UF.Base
open import UF.Subsingletons renaming (⊤Ω to ⊤ ; ⊥Ω to ⊥)
open import UF.Equiv
open import UF.Retracts
open import UF.Embeddings
open import UF.EquivalenceExamples
open import UF.KrausLemma
open import UF.PropTrunc

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}