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}