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

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

open import Sec2preliminaries 
open import Sec3hedberg
open import Sec4collapsibility
open import Sec5factorConst
open import Sec6collImplDecEq
open import Sec7populatedness


module Sec8taboos where


-- Subsection 8.1

all-coll : Type₁
all-coll = (X : Type)  coll X

-- Theorem 8.1
module functional-subrelation (ac : all-coll) (X : Type) (R : X × X  Type) where

  all-sets : (Y : Type)  is-set Y
  all-sets Y = pathColl→isSet  y₁ y₂  ac _)

  R₋ : (x : X)  Type
  R₋ x = Σ X λ y  R(x , y)

  k : (x : X)  (R₋ x)  (R₋ x)
  k x = fst (ac _)

  kc : (x : X)  const (k x)
  kc x = snd (ac _)

  S : X × X  Type
  S (x , y) = Σ (R(x , y)) λ a  
                (y , a) == k x (y , a)

  -- the relation S
  S₋ : (x : X)  Type
  S₋ x = Σ X λ y  S(x , y)

  -- fix kₓ is equivalent to Sₓ
  -- This is just Σ-assoc. We try to make it more readable by adding some (trivial) steps.
  fixk-S : (x : X)  (fix (k x))  S₋ x
  fixk-S x = 
      (fix (k x))                                           ≃⟨ ide _ 
      (Σ (Σ X λ y  R(x , y)) λ a  a == k x a)             ≃⟨ Σ-assoc 
      (Σ X λ y  Σ (R(x , y)) λ r  (y , r) == k x (y , r)) ≃⟨ ide _ 
      (S₋ x)                                                ≃∎

  -- claim (0)
  subrelation : (x y : X)  S(x , y)   R(x , y)
  subrelation x y (r , _) = r

   -- claim (1)
  prop-Sx : (x : X)  is-prop (S₋ x)
  prop-Sx x = equiv-preserves-level {A = fix (k x)} {B = (S₋ x)} (fixk-S x) (fixed-point _ (kc x)) 

  -- claim (2)
  same-domain : (x : X)  (R₋ x)  (S₋ x)
  same-domain x = rs , sr where
    rs : (R₋ x)  (S₋ x)
    rs a = –> (fixk-S x) (to-fix (k x) (kc x) a)
    sr : (S₋ x)  (R₋ x)
    sr (y , r , _) = y , r

  -- claim (3) 
  prop-S : (x y : X)  is-prop (S (x , y))
  prop-S x y = all-paths-is-prop all-paths where
    all-paths : (s₁ s₂ : S(x , y))  s₁ == s₂
    all-paths s₁ s₂ = ss where

      yss : (y , s₁) == (y , s₂)
      yss = prop-has-all-paths (prop-Sx x) _ _

      ss : s₁ == s₂
      ss = set-lemma (all-sets _) y s₁ s₂ yss


-- intermediate definition
-- see the caveat about the notion 'epimorphism' in the article
is-split-epimorphism : {U V : Type}  (U  V)  Type
is-split-epimorphism {U} {V} e = Σ (V  U) λ s  (v : V)  e (s v) == v

is-epimorphism : {U V : Type}  (U  V)  Type₁
is-epimorphism {U} {V} e = (W : Type)  (f g : V  W)  ((u : U)  f (e u) == g (e u))  (v : V)  f v == g v

-- Lemma 8.2
path-trunc-epi→set : {Y : Type}  ((y₁ y₂ : Y)  is-epimorphism (∣_∣ {X = y₁ == y₂}))  is-set Y
path-trunc-epi→set {Y} path-epi = reminder special-case where

  f : (y₁ y₂ : Y)  Trunc (y₁ == y₂)  Y
  f y₁ _ _ = y₁

  g : (y₁ y₂ : Y)  Trunc (y₁ == y₂)  Y
  g _ y₂ _ = y₂

  special-case : (y₁ y₂ : Y)  Trunc (y₁ == y₂)  y₁ == y₂
  special-case y₁ y₂ = path-epi y₁ y₂ Y (f y₁ y₂) (g y₁ y₂) (idf _)

  reminder : hseparated Y  is-set Y
  reminder = fst set-characterizations  snd (snd set-characterizations)

-- Theorem 8.3 (1)
all-split→all-deceq : ((X : Type)  is-split-epimorphism (∣_∣ {X = X}))  (X : Type)  has-dec-eq X
all-split→all-deceq all-split = all-coll→dec-eq ac where
  ac : (X : Type)  coll X
  ac X = snd coll↔hstable (fst (all-split X))

-- Theorem 8.3 (2)
all-epi→all-set : ((X : Type)  is-epimorphism (∣_∣ {X = X}))  (X : Type)  is-set X
all-epi→all-set all-epi X = path-trunc-epi→set  y₁ y₂  all-epi (y₁ == y₂))


-- Subsection 8.2

-- Lemma 8.4, first proof
pop-hstable-1 : {X : Type}  Pop (hstable X)
pop-hstable-1 {X} f c = to-fix f c (coll→hstable (g , gc)) where

  g : X  X
  g x = f  _  x)  x 

  gc : const g
  gc x₁ x₂ = 
    g x₁               =⟨ idp 
    f  _  x₁)  x₁  =⟨ ap  k  k  x₁ ) (c  _  x₁)  _  x₂)) 
    f  _  x₂)  x₁  =⟨ ap (f  _  x₂)) (prop-has-all-paths (h-tr X)  x₁   x₂ ) 
    f  _  x₂)  x₂  =⟨ idp 
    g x₂                 

-- Lemma 8.4, second proof
pop-hstable-2 : {X : Type}  Pop (hstable X)
pop-hstable-2 {X} = snd (pop-alt₂ {hstable X}) get-P where
  get-P : (P : Type)  is-prop P  hstable X  P  P
  get-P P pp (hstp , phst) = hstp free-hst where

    xp : X  P
    xp x = hstp  _  x)

    zp : Trunc X  P
    zp = rec pp xp

    free-hst : hstable X
    free-hst z = phst (zp z) z

-- Lemma 8.5, third proof
pop-hstable-3 : {X : Type}  Pop (hstable X)
pop-hstable-3 {X} = snd pop-alt translation where

  translation-aux : hstable (hstable X)  hstable X
  translation-aux = λ hsthst z  hsthst (trunc-functorial {X = X} {Y = hstable X}  x _  x) z) z

  translation : Trunc (hstable (hstable X))  Trunc (hstable X)
  translation = trunc-functorial translation-aux

-- Theorem 8.5
module thm85 where

  One = (X : Type)  Pop X  Trunc X

  Two = (X : Type)  Trunc (hstable X)

  Three = (P : Type)  is-prop P  (Y : P  Type)  ((p : P)  Trunc (Y p))  Trunc ((p : P)  Y p)

  Four = (X Y : Type)  (X  Y)  (Pop X  Pop Y)


  One→Two : One  Two
  One→Two poptr X = poptr (hstable X) pop-hstable-1 

  Two→One : Two  One
  Two→One trhst X pop = fst pop-alt pop (trhst X)

  One→Four : One  Four
  One→Four poptr X Y f = Trunc→Pop  (trunc-functorial f)  (poptr X)

  Four→One : Four  One
  Four→One funct X px = prop-pop (h-tr _) pz where
    pz : Pop (Trunc X)
    pz  =  funct X (Trunc X) ∣_∣ px

  -- only very slightly different to the proof in the article
  One→Three : One  Three
  One→Three poptr P pp Y = λ py  poptr _ (snd pop-alt'  hst p₀  hst (contr-trick p₀ py) p₀)) where
    contr-trick : (p₀ : P)  ((p : P)  Trunc (Y p))  Trunc ((p : P)  Y p)
    contr-trick p₀ py = rec {X = Y p₀} 
                            {P = Trunc ((p : P)  Y p)} 
                            (h-tr _) 
                             y₀   <– (thm55aux.neutral-contr-exp {P = P} {Y = Y} pp p₀) y₀ ) (py p₀)

  Three→Two : Three  Two
  Three→Two proj X = proj (Trunc X) (h-tr _)  _  X) (idf _)


-- Subsection 8.3

-- Some very simple lemmata

-- If P is a proposition, so is P + ¬ P
dec-is-prop : {P : Type}  (Funext {X = P} {Y = Empty})  is-prop P  is-prop (P + ¬ P)
dec-is-prop {P} fext pp = all-paths-is-prop  { (inl p₁) (inl p₂)  ap inl (prop-has-all-paths pp _ _) ; 
                                (inl p₁) (inr np₂)  Empty-elim {A = λ _  inl p₁ == inr np₂} (np₂ p₁) ; 
                                (inr np₁) (inl p₂)  Empty-elim {A = λ _  inr np₁ == inl p₂} (np₁ p₂) ; 
                                (inr np₁) (inr np₂)  ap inr (fext np₁ np₂  p  prop-has-all-paths  ()) _ _)) })


-- Theorem 8.7
nonempty-pop→lem : ((X : Type)  Funext {X} {Empty}) 
                          ((X : Type)  (¬(¬ X)  Pop X))  LEM
nonempty-pop→lem fext nn-pop P pp = from-fix {X = dec} (idf _) (nn-pop dec nndec (idf _) idc) where
  dec : Type
  dec = P + ¬ P

  idc : const (idf dec)
  idc = λ _ _  prop-has-all-paths (dec-is-prop {P} (fext P) pp) _ _

  nndec : ¬(¬ dec)
  nndec ndec =  np  ndec (inr np)) λ p  ndec (inl p)

-- Corollary 8.8
nonempty-pop↔lem : ((X : Type)  Funext {X} {Empty}) 
                          ((X : Type)  (¬(¬ X)  Pop X)) ↔₁₁ LEM
nonempty-pop↔lem fext = nonempty-pop→lem fext , other where
  other : LEM  ((X : Type)  (¬(¬ X)  Pop X))
  other lem X nnX = p where
    pnp : Pop X + ¬ (Pop X)
    pnp = lem (Pop X) pop-property₂

    p : Pop X
    p = match pnp withl idf _ withr  np  Empty-elim {A = λ _  Pop X} (nnX  x  np (pop-property₁ x))))