Chuangjie Xu 2014

We recall the proof of the fact that

  If a type A has a constant endo-function, then ∥ A ∥ → A

whose original proof is from

  http://www.cs.bham.ac.uk/~mhe/GeneralizedHedberg/html/GeneralizedHedberg.html

to make our Agda formalization self-contained.

\begin{code}

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

module Continuity.TheoremKECA where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber hiding (_+_)
open import Continuity.PropositionalTruncation

\end{code}

Some lemmas of identity types

\begin{code}

infix   finally
infixr  _≡⟨_⟩_

_≡⟨_⟩_ : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ p ⟩ q = p · q

finally : {A : Set} (x y : A) → x ≡ y → x ≡ y
finally _ _ p = p

syntax finally x y p = x ≡⟨ p ⟩∎ y ∎

refl-is-left-id : {X : Set} {x y : X} (p : x ≡ y) → p ≡ refl · p
refl-is-left-id refl = refl

refl-is-right-id : {X : Set} {x y : X} (p : x ≡ y) → p ≡ p · refl
refl-is-right-id refl = refl

sym-trans : {X : Set} {x y z : X} (p : x ≡ y) (q : y ≡ z) → (q ⁻¹) · (p ⁻¹) ≡ (p · q)⁻¹
sym-trans {X} {x} {.x} {.x} refl refl = refl

sym-sym-trivial : {X : Set} {x y : X} (p : x ≡ y) → p ≡ (p ⁻¹)⁻¹
sym-sym-trivial refl = refl

trans₀ : {X : Set}{x₀ x₁ x₂ : X} → (p : x₁ ≡ x₂) → p ≡ refl · p
trans₀ refl = refl

trans₁ : {X : Set}{x₀ x₁ x₂ : X} → (p : x₀ ≡ x₁) → p ≡ p · refl
trans₁ refl = refl

trans-assoc : {X : Set} {x y z w : X} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) →
              (p · q) · r ≡ p · (q · r)
trans-assoc refl refl refl = refl

ap-id-is-id : {X : Set} {x y : X} (p : x ≡ y) → ap id p ≡ p
ap-id-is-id refl = refl

\end{code}

The fix point lemma:

\begin{code}

Kraus-Lemma₀ : {X Y : Set} (f : X → Y) (cf : constant f) {x y : X} (p : x ≡ y)
             → ap f p ≡ (cf x x)⁻¹ · (cf x y) 
Kraus-Lemma₀ {X} {Y} f cf {x} {.x} refl = sym-is-inverse (cf x x)

Kraus-Lemma₁ : {X Y : Set} (f : X → Y) → constant f → {x : X} (p : x ≡ x)
             → ap f p ≡ refl
Kraus-Lemma₁ {X} {Y} f cf {x} p = (Kraus-Lemma₀ f cf p) · (sym-is-inverse (cf x x))⁻¹

transport-paths-along-paths : {X Y : Set} {x y : X} (p : x ≡ y) (h k : X → Y) (q : h x ≡ k x) 
                            → transport (λ z → h z ≡ k z) p q ≡ (ap h p)⁻¹ · q · (ap k p)
transport-paths-along-paths {X} {Y} {x} {.x} refl h k q = claim₀ · claim₁
 where
  claim₀ : q ≡ q · refl
  claim₀ = trans₁ {Y} {h x} {k x} {k x} q
  claim₁ : q · refl ≡ refl · q · refl
  claim₁ = trans₀ {Y} {h x} {h x} {k x} (q · refl)

transport-paths-along-paths' : {X : Set} {x : X} (p : x ≡ x) (f : X → X) (q : x ≡ f x) 
                             → transport (λ z → z ≡ f z) p q ≡ p ⁻¹ · q · (ap f p)
transport-paths-along-paths' {X} {x} p f q = claim₀ · claim₁
 where
  claim₀ : transport (λ z → z ≡ f z) p q ≡ (ap id p) ⁻¹ · q · (ap f p)
  claim₀ = transport-paths-along-paths p (λ z → z) f q
  claim₁ : (ap id p) ⁻¹ · q · (ap f p) ≡ p ⁻¹ · q · (ap f p)
  claim₁ = ap (λ r → r ⁻¹ · q · (ap f p)) (ap-id-is-id p)

fix : {X : Set} → (X → X) → Set
fix {X} f = Σ \(x : X) → x ≡ f x

Kraus-Lemma : {X : Set} → (f : X → X) → constant f → hprop(fix f)
Kraus-Lemma {X} f g (x , p) (y , q) =
  -- p : x ≡ f x
  -- q : y ≡ f y
  (x , p)        ≡⟨ pair⁼ r refl ⟩
  (y , p')       ≡⟨ pair⁼ s t ⟩∎           
  (y , q) ∎
    where
     r : x ≡ y
     r = x ≡⟨ p ⟩
       f x ≡⟨ g x y ⟩
       f y ≡⟨ q ⁻¹ ⟩∎
         y ∎
     p' : y ≡ f y
     p' = transport (λ z → z ≡ f z) r p
     s : y ≡ y
     s = y   ≡⟨ p' ⟩
         f y ≡⟨ q ⁻¹ ⟩∎
         y   ∎
     q' : y ≡ f y
     q' = transport (λ z → z ≡ f z) s p'
     t : q' ≡ q
     t = q'                         ≡⟨ transport-paths-along-paths' s f p' ⟩
         s ⁻¹ · (p' · ap f s)       ≡⟨ ap (λ pr → s ⁻¹ · (p' · pr)) (Kraus-Lemma₁ f g s) ⟩
         s ⁻¹ · (p' · refl)         ≡⟨ ap (λ pr → s ⁻¹ · pr) ((refl-is-right-id p')⁻¹)  ⟩
         s ⁻¹ · p'                  ≡⟨ refl  ⟩
         (p' · (q ⁻¹))⁻¹ · p'       ≡⟨ ap (λ pr → pr · p') ((sym-trans p' (q ⁻¹))⁻¹)  ⟩
         ((q ⁻¹)⁻¹ · (p' ⁻¹)) · p'  ≡⟨ ap (λ pr → (pr · (p' ⁻¹)) · p') ((sym-sym-trivial q)⁻¹) ⟩
         (q · (p' ⁻¹)) · p'         ≡⟨ trans-assoc q (p' ⁻¹) p'  ⟩
         q · ((p' ⁻¹) · p')         ≡⟨ ap (λ pr → q · pr) ((sym-is-inverse p')⁻¹) ⟩
         q · refl                   ≡⟨ (refl-is-right-id q)⁻¹  ⟩∎
         q  ∎

\end{code}

If a type A has a constant endo-function, then ∥ A ∥ → A.

\begin{code}

Theorem[KECA-TLCA'2013] : ∀{A : Set} → (f : A → A) → constant f → ∥ A ∥ → A
Theorem[KECA-TLCA'2013] {A} f cf = F2A ∘ hA2F
 where
  F : Set
  F = fix f
  hF : hprop F
  hF = Kraus-Lemma f cf
  A2F : A → F
  A2F a = f a , cf a (f a)
  hA2F : ∥ A ∥ → F
  hA2F = ∥-∥-elim hF A2F
  F2A : F → A
  F2A = pr₁

\end{code}