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

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