{-# OPTIONS --without-K #-}
open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
open import Sec2preliminaries
open import Sec3hedberg
open import Sec4collapsibility
module Sec7populatedness where
Pop : Type → Type
Pop X = (f : X → X) → const f → fix f
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
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 _))
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) ∣)
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
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
pop-property₁ : {X : Type} → X → Pop X
pop-property₁ = Trunc→Pop ∘ ∣_∣
pop-property₂ : {X : Type} → is-prop (Pop X)
pop-property₂ = Π-is-prop (λ f → Π-is-prop (λ c → fixed-point f c))