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

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma

open import Sec2preliminaries
open import Sec3hedberg
open import Sec4collapsibility

-- In this section, we require function extensionality again.

module Sec7populatedness where

-- Definition 7.1
Pop : Type → Type
Pop X = (f : X → X) → const f → fix f

-- Theorem 7.2
Trunc→Pop : {X : Type} → Trunc X → Pop X
Trunc→Pop z f c = rec {P = fix f} (fixed-point f c) (to-fix f c) z

-- Corollary 7.3
coll-characterizations : {X : Type} → (coll X ↔ hstable X) × ((coll X ↔ (Pop X → X)) × ((Pop X → X) ↔ hstable X))
coll-characterizations {X} = coll↔hstable , (coll→pop→X , reverse₁) , (pop→X→hstable , reverse₂) where

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

pop→X→hstable : (Pop X → X) → hstable X
pop→X→hstable g = g ∘ Trunc→Pop

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

prop-pop : {P : Type} → is-prop P → (Pop P) → P
prop-pop {P} pp = snd (snd (snd coll-characterizations)) (rec pp (idf _))

-- Lemma 7.4
module _ {X : Type} where

pop→hstable→X : Pop X → hstable X → X
pop→hstable→X pop = λ hst → snd (snd (snd (coll-characterizations {X}))) hst pop

use-funct : (hstable X → X) → Trunc (hstable X) → Trunc X
use-funct f = trunc-functorial f

tr-hst-X→pop : (Trunc (hstable X) → Trunc X) → Pop X
tr-hst-X→pop g f c = rec (fixed-point f c) (to-fix f c) (g ∣ coll→hstable (f , c) ∣)

-- we formulate the two logical equivalence that we will need explicitly:
pop-alt : Pop X ↔ (Trunc (hstable X) → Trunc X)
pop-alt = use-funct ∘ pop→hstable→X , tr-hst-X→pop

pop-alt' : Pop X ↔ (hstable X → X)
pop-alt' = pop→hstable→X , tr-hst-X→pop ∘ use-funct

-- Theorem 7.5
pop-alt₂ : {X : Type} → Pop X ↔₀₁ ((P : Type) → (is-prop P) → (X ↔ P) → P)
pop-alt₂ {X} = one , two where

one : Pop X → (P : Type) → 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) → is-prop P → (X ↔ P) → P) → Pop X
two rest f c = rest (fix f) (fixed-point f c) (to-fix f c , from-fix f)

open import library.types.Pi

-- Theorem 7.6
pop-property₁ : {X : Type} → X → Pop X
pop-property₁ = Trunc→Pop ∘ ∣_∣

-- this needs function extensionality
pop-property₂ : {X : Type} → is-prop (Pop X)
pop-property₂ = Π-is-prop (λ f → Π-is-prop (λ c → fixed-point f c))
```