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

open import lib.Basics
open import lib.types.Sigma

open import Preliminaries
open import Truncation_Level_Criteria
open import Anonymous_Existence_CollSplit

open wtrunc
open with-weak-trunc

module Anonymous_Existence_Populatedness where

-- Definition 4.2.1
⟪_⟫ : ∀ {i} → Type i → Type i
⟪ X ⟫ = (f : X → X) → const f → fix f

-- Proposition 4.2.2
Trunc→Pop : ∀ {i} {X : Type i} → ∣∣ X ∣∣ → ⟪ X ⟫
Trunc→Pop z f c = tr-rec {P = fix f} (fixed-point f c) (to-fix f c) z

-- Corollary 4.2.3: We show pairwise logical equivalence as it is easy
-- (of course, some directions are redundant)
coll-characterizations : ∀ {i} {X : Type i}
→ (coll X ↔ splitSup X)
× ((coll X ↔ (⟪ X ⟫ → X))
× ((⟪ X ⟫ → X) ↔ splitSup X))
coll-characterizations {X = X} = coll↔splitSup ,
(coll→pop→X , reverse₁) ,
(pop→X→splitSup , reverse₂) where

coll→pop→X : coll X → ⟪ X ⟫ → X
coll→pop→X (f , c) pop = fst (pop f c)

pop→X→splitSup : (⟪ X ⟫ → X) → splitSup X
pop→X→splitSup g = g ∘ Trunc→Pop

reverse₁ = snd coll↔splitSup ∘ pop→X→splitSup
reverse₂ = coll→pop→X ∘ snd coll↔splitSup

prop-pop : ∀ {i} {P : Type i} → is-prop P → ⟪ P ⟫ → P
prop-pop {P = P} pp = snd (snd (snd coll-characterizations)) (tr-rec pp (idf _))

-- Lemma 4.2.4
module _ {i : ULevel} {X : Type i} where

pop→splitSup→X : ⟪ X ⟫ → splitSup X → X
pop→splitSup→X pop = λ hst → snd (snd (snd (coll-characterizations {X = X}))) hst pop

use-funct : (splitSup X → X) → ∣∣ splitSup X ∣∣ → ∣∣ X ∣∣
use-funct f = trunc-functorial f

tr-hst-X→pop : (∣∣ splitSup X ∣∣ → ∣∣ X ∣∣) → ⟪ X ⟫
tr-hst-X→pop g f c = tr-rec (fixed-point f c) (to-fix f c) (g ∣ coll→splitSup (f , c) ∣)

-- we formulate the two logical equivalence that we will need explicitly:
pop-alt : ⟪ X ⟫ ↔ (∣∣ splitSup X ∣∣ → ∣∣ X ∣∣)
pop-alt = use-funct ∘ pop→splitSup→X , tr-hst-X→pop

pop-alt' : ⟪ X ⟫ ↔ (splitSup X → X)
pop-alt' = pop→splitSup→X , tr-hst-X→pop ∘ use-funct

-- Proposition 4.2.5
pop-alt₂ : ∀ {i} {X : Type i} → ⟪ X ⟫ ↔ ((P : Type i) → (is-prop P) → (X ↔ P) → P)
pop-alt₂ {i} {X} = one , two where

one : ⟪ X ⟫ → (P : Type i) → is-prop P → (X ↔ P) → P
one pop P pp (xp , px) = xp (fst (pop f c)) where
f : X → X
f = px ∘ xp
c : const f
c x₁ x₂ = ap px (prop-has-all-paths pp _ _)

two : ((P : Type i) → is-prop P → (X ↔ P) → P) → ⟪ X ⟫
two rest f c = rest (fix f) (fixed-point f c) (to-fix f c , from-fix f)

-- Proposition 4.2.6, part 1
pop-property₁ : ∀ {i} {X : Type i} → X → ⟪ X ⟫
pop-property₁ = Trunc→Pop ∘ ∣_∣

-- Proposition 4.2.6, part 2: this needs function extensionality.
-- We import the library file with the consequence of funext that we need.
open import lib.types.Pi
pop-property₂ : ∀ {i} {X : Type i} → is-prop ⟪ X ⟫
pop-property₂ = Π-is-prop (λ f → Π-is-prop (λ c → fixed-point f c))
```