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

open import lib.Basics
open import lib.types.Sigma
open import lib.types.Bool
open import lib.types.Empty

open import Preliminaries
open import Truncation_Level_Criteria
open import Anonymous_Existence_CollSplit
open import Anonymous_Existence_Populatedness

module Anonymous_Existence_Comparison where

-- Chapter 4.3: Comparison of Notions of Existence

-- Section 4.3.1: Inhabited and Merely Inhabited

-- Lemma 4.3.1
coll-family-dec : ∀ {i} {X : Type i} → (x₁ x₂ : X) → ((x : X) → coll (Coprod (x₁ == x) (x₂ == x))) → Coprod (x₁ == x₂) (¬(x₁ == x₂))
coll-family-dec {i} {X} x₁ x₂ coll-fam = solution where
f₋ : (x : X) → Coprod (x₁ == x) (x₂ == x) → Coprod (x₁ == x) (x₂ == x)
f₋ x = fst (coll-fam x)

E₋ : X → Type i
E₋ x = fix (f₋ x)

E : Type i
E = Σ X λ x → (E₋ x)

E-fst-determines-eq : (e₁ e₂ : E) → (fst e₁ == fst e₂) → e₁ == e₂
E-fst-determines-eq e₁ e₂ p = second-comp-triv (λ x → fixed-point (f₋ x) (snd (coll-fam x))) _ _ p

r : Bool {i} → E
r true = x₁ , to-fix (f₋ x₁) (snd (coll-fam x₁)) (inl idp)
r false = x₂ , to-fix (f₋ x₂) (snd (coll-fam x₂)) (inr idp)

about-r : (r true == r false) ↔ (x₁ == x₂)
about-r = (λ p → ap fst p) , (λ p → E-fst-determines-eq _ _ p)

s : E → Bool
s (_ , inl _ , _) = true
s (_ , inr _ , _) = false

s-section-of-r : (e : E) → r(s e) == e
s-section-of-r (x , inl p , q) = E-fst-determines-eq _ _ p
s-section-of-r (x , inr p , q) = E-fst-determines-eq _ _ p

about-s : (e₁ e₂ : E) → (s e₁ == s e₂) ↔ (e₁ == e₂)
about-s e₁ e₂ = one , two where
one : (s e₁ == s e₂) → (e₁ == e₂)
one p =
e₁       =⟨ ! (s-section-of-r e₁) ⟩
r(s(e₁)) =⟨ ap r p ⟩
r(s(e₂)) =⟨ s-section-of-r e₂ ⟩
e₂       ∎
two : (e₁ == e₂) → (s e₁ == s e₂)
two p = ap s p

combine : (s (r true) == s (r false)) ↔ (x₁ == x₂)

check-bool : Coprod (s (r true) == s (r false)) (¬(s (r true) == s (r false)))
check-bool = Bool-has-dec-eq _ _

solution : Coprod (x₁ == x₂) (¬(x₁ == x₂))
solution with check-bool
solution | inl p = inl (fst combine p)
solution | inr np = inr (λ p → np (snd combine p))

-- definition: "all types have a weakly constant endofunction".
-- this assumption is, if we have ∣∣_∣∣, logically equivalent to saying that
-- every type has split support.
all-coll : ∀ {i} → Type (lsucc i)
all-coll {i} = (X : Type i) → coll X

-- Proposition 4.3.2
all-coll→dec-eq : ∀ {i} → all-coll {i} → (X : Type i) → has-dec-eq X
all-coll→dec-eq all-coll X x₁ x₂ = coll-family-dec x₁ x₂ (λ x → all-coll _)

open with-weak-trunc
open wtrunc

--  Proposition 4.3.3
module functional-subrelation {i : ULevel} (ac : all-coll {i}) (X : Type i) (R : X × X → Type i) where

all-sets : (Y : Type i) → is-set Y
all-sets Y = pathColl→isSet (λ y₁ y₂ → ac _)

R₋ : (x : X) → Type i
R₋ x = Σ X λ y → R(x , y)

k : (x : X) → (R₋ x) → (R₋ x)
k x = fst (ac _)

kc : (x : X) → const (k x)
kc x = snd (ac _)

SS : X × X → Type i
SS (x , y) = Σ (R(x , y)) λ a →
(y , a) == k x (y , a)

-- the relation S
SS₋ : (x : X) → Type i
SS₋ x = Σ X λ y → SS(x , y)

-- fix kₓ is equivalent to Sₓ
-- This is just Σ-assoc. We try to make it more readable by adding some (trivial) steps.
fixk-SS : (x : X) → (fix (k x)) ≃ SS₋ x
fixk-SS x =
(fix (k x))                                           ≃⟨ ide _ ⟩
(Σ (Σ X λ y → R(x , y)) λ a → a == k x a)             ≃⟨ Σ-assoc ⟩
(Σ X λ y → Σ (R(x , y)) λ r → (y , r) == k x (y , r)) ≃⟨ ide _ ⟩
(SS₋ x)                                                ≃∎

-- claim (0)
subrelation : (x y : X) → SS(x , y) →  R(x , y)
subrelation x y (r , _) = r

-- claim (1)
prop-SSx : (x : X) → is-prop (SS₋ x)
prop-SSx x = equiv-preserves-level {A = fix (k x)} {B = (SS₋ x)} (fixk-SS x) (fixed-point _ (kc x))

-- claim (2)
same-domain : (x : X) → (R₋ x) ↔ (SS₋ x)
same-domain x = rs , sr where
rs : (R₋ x) → (SS₋ x)
rs a = –> (fixk-SS x) (to-fix (k x) (kc x) a)
sr : (SS₋ x) → (R₋ x)
sr (y , r , _) = y , r

-- claim (3)
prop-SS : (x y : X) → is-prop (SS (x , y))
prop-SS x y = all-paths-is-prop all-paths where
all-paths : (s₁ s₂ : SS(x , y)) → s₁ == s₂
all-paths s₁ s₂ = ss where

yss : (y , s₁) == (y , s₂)
yss = prop-has-all-paths (prop-SSx x) _ _

ss : s₁ == s₂
ss = set-lemma (all-sets _) y s₁ s₂ yss

-- intermediate definition
-- see the caveat about the notion 'epimorphism' in the article
is-split-epimorphism : ∀ {i j} {U : Type i} {V : Type j} → (U → V) → Type (i ⊔ j)
is-split-epimorphism {U = U} {V = V} e = Σ (V → U) λ s → (v : V) → e (s v) == v

is-epimorphism : ∀ {i j} {U : Type i} {V : Type j} → (U → V) → Type (lsucc (i ⊔ j))
is-epimorphism {i} {j} {U = U} {V = V} e = (W : Type (i ⊔ j)) → (f g : V → W) → ((u : U) → f (e u) == g (e u)) → (v : V) → f v == g v

-- Lemma 4.3.4
path-trunc-epi→set : ∀ {i} {Y : Type i} → ((y₁ y₂ : Y) → is-epimorphism (∣_∣ {X = y₁ == y₂})) → is-set Y
path-trunc-epi→set {Y = Y} path-epi = reminder special-case where

f : (y₁ y₂ : Y) → ∣∣ y₁ == y₂ ∣∣ → Y
f y₁ _ _ = y₁

g : (y₁ y₂ : Y) → ∣∣ y₁ == y₂ ∣∣ → Y
g _ y₂ _ = y₂

special-case : (y₁ y₂ : Y) → ∣∣ y₁ == y₂ ∣∣ → y₁ == y₂
special-case y₁ y₂ = path-epi y₁ y₂ Y (f y₁ y₂) (g y₁ y₂) (idf _)

-- we know that hSeparated(X) implies that X is a set,
-- from the previous Proposition 3.1.9;
-- however, we have proved it in such a way which forces
-- us to combine three directions:
reminder : hSeparated Y → is-set Y
reminder = (fst (set-characterisations Y)) ∘ (fst (snd (snd (set-characterisations Y)))) ∘ (snd (snd (snd (snd (set-characterisations Y)))))

-- Proposition 4.3.5 (1)
all-split→all-deceq : ∀ {i} → ((X : Type i) → is-split-epimorphism (∣_∣ {X = X})) → (X : Type i) → has-dec-eq X
all-split→all-deceq {i} all-split = all-coll→dec-eq ac where
ac : (X : Type i) → coll X
ac X = snd coll↔splitSup (fst (all-split X))

-- Proposition 4.3.5 (2)
all-epi→all-set : ∀ {i} → ((X : Type i) → is-epimorphism (∣_∣ {X = X})) → (X : Type i) → is-set X
all-epi→all-set all-epi X = path-trunc-epi→set (λ y₁ y₂ → all-epi (y₁ == y₂))

-- Section 4.3.2: Merely Inhabited and Populated

-- Lemma 4.3.6, first proof
pop-hstable-1 : ∀ {i} {X : Type i} → ⟪ splitSup X ⟫
pop-hstable-1 {X = X} f c = to-fix f c (coll→splitSup (g , gc)) where

g : X → X
g x = f (λ _ → x) ∣ x ∣

gc : const g
gc x₁ x₂ =
g x₁               =⟨ idp ⟩
f (λ _ → x₁) ∣ x₁ ∣ =⟨ ap (λ k → k ∣ x₁ ∣) (c (λ _ → x₁) (λ _ → x₂)) ⟩
f (λ _ → x₂) ∣ x₁ ∣ =⟨ ap (f (λ _ → x₂)) (prop-has-all-paths tr-is-prop ∣ x₁ ∣ ∣ x₂ ∣) ⟩
f (λ _ → x₂) ∣ x₂ ∣ =⟨ idp ⟩
g x₂               ∎

-- Lemma 4.3.6, second proof
pop-hstable-2 : ∀ {i} {X : Type i} → ⟪ splitSup X ⟫
pop-hstable-2 {i} {X} = snd (pop-alt₂ {X = splitSup X}) get-P where
get-P : (P : Type i) → is-prop P → splitSup X ↔ P → P
get-P P pp (hstp , phst) = hstp free-hst where

xp : X → P
xp x = hstp (λ _ → x)

zp : ∣∣ X ∣∣ → P
zp = tr-rec pp xp

free-hst : splitSup X
free-hst z = phst (zp z) z

-- Lemma 4.3.6, third proof
pop-hstable-3 : ∀ {i} {X : Type i} → ⟪ splitSup X ⟫
pop-hstable-3 {X = X} = snd pop-alt translation where

translation-aux : splitSup (splitSup X) → splitSup X
translation-aux = λ hsthst z → hsthst (trunc-functorial {X = X} {Y = splitSup X} (λ x _ → x) z) z

translation :  ∣∣ splitSup (splitSup X) ∣∣ → ∣∣ splitSup X ∣∣
translation = trunc-functorial translation-aux

-- Lemma 4.3.7
module tlem437 {i : ULevel} where

One = (X : Type i) → ⟪ X ⟫ → ∣∣ X ∣∣

Two = (X : Type i) → ∣∣ splitSup X ∣∣

Three = (P : Type i) → is-prop P → (Y : P → Type i) → ((p : P) → ∣∣ Y p ∣∣) → ∣∣ ((p : P) → Y p) ∣∣

Four = (X Y : Type i) → (X → Y) → (⟪ X ⟫ → ⟪ Y ⟫)

One→Two : One → Two
One→Two poptr X = poptr (splitSup X) pop-hstable-1

Two→One : Two → One
Two→One trhst X pop = fst pop-alt pop (trhst X)

One→Four : One → Four
One→Four poptr X Y f = Trunc→Pop ∘ (trunc-functorial f) ∘ (poptr X)

Four→One : Four → One
Four→One funct X px = prop-pop tr-is-prop pz where -- (tr-rec _) pz where
pz : ⟪ ∣∣ X ∣∣ ⟫
pz  =  funct X (∣∣ X ∣∣) ∣_∣ px

-- only very slightly different to the proof in the article
One→Three : One → Three
One→Three poptr P pp Y = λ py → poptr _ (snd pop-alt' (λ hst p₀ → hst (contr-trick p₀ py) p₀)) where
contr-trick : (p₀ : P) → ((p : P) → ∣∣ Y p ∣∣) → ∣∣ ((p : P) → Y p) ∣∣
contr-trick p₀ py = tr-rec {X = Y p₀}
{P = ∣∣ ((p : P) → Y p) ∣∣}
tr-is-prop
(λ y₀ → ∣ (λ p → transport Y (prop-has-all-paths pp p₀ p) y₀) ∣)
(py p₀)

Three→Two : Three → Two
Three→Two proj X = proj (∣∣ X ∣∣) tr-is-prop (λ _ → X) (idf _)

-- Section 4.3.3: Populated and Non-Empty

-- We now need function extensionality. We
-- lemmata (not numbered in the thesis).

-- If P is a proposition, so is P + ¬ P
dec-is-prop : ∀ {i} {P : Type i} → is-prop P → is-prop (Coprod P (¬ P))
dec-is-prop {P = P} pp = all-paths-is-prop (λ { (inl p₁) (inl p₂) → ap inl (prop-has-all-paths pp _ _) ;
(inl p₁) (inr np₂) → Empty-elim {A = λ _ → inl p₁ == inr np₂} (np₂ p₁) ;
(inr np₁) (inl p₂) → Empty-elim {A = λ _ → inr np₁ == inl p₂} (np₁ p₂) ;
(inr np₁) (inr np₂) → ap inr (λ= (λ x → prop-has-all-paths Empty-is-prop _ _ )) })

-- Proposition 4.3.8
nonempty-pop→LEM : ∀ {i} → ((X : Type i) → (¬(¬ X) → ⟪ X ⟫)) → LEM {i}
nonempty-pop→LEM {i} nn-pop P pp = from-fix {X = dec} (idf _) (nn-pop dec nndec (idf _) idc) where
dec : Type i
dec = Coprod P (¬ P)

idc : const (idf dec)
idc = λ _ _ → prop-has-all-paths (dec-is-prop {P = P} pp) _ _

nndec : ¬(¬ dec)
nndec ndec = (λ np → ndec (inr np)) λ p → ndec (inl p)

-- Corollary 4.3.9
nonempty-pop↔lem : ∀ {i} → ((X : Type i) → (¬(¬ X) → ⟪ X ⟫)) ↔ LEM {i}
nonempty-pop↔lem {i} = nonempty-pop→LEM , other where
other : LEM {i} → ((X : Type i) → (¬(¬ X) → ⟪ X ⟫))
other lem X nnX = p where
pnp : Coprod ⟪ X ⟫ (¬ ⟪ X ⟫)
pnp = lem ⟪ X ⟫ pop-property₂

p : ⟪ X ⟫
p = match pnp withl idf _ withr (λ np → Empty-elim {A = λ _ → ⟪ X ⟫} (nnX (λ x → np (pop-property₁ x))))
```