{-# 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

-- Addendum of Corollary 7.3
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))