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.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Hedberg
open import UF.KrausLemma
open import UF.PropTrunc
open import UF.Retracts
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}