{-# OPTIONS --without-K #-}
module Truncation_Level_Criteria where

open import lib.Basics
open import lib.NType2

open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Unit
open import lib.types.Empty
open import lib.types.TLevel

open import Preliminaries
open import Pointed

-- Chapter 3: Truncation Level Criteria

-- Chapter 3.1: Hedberg's Theorem Revisited


-- Proposition 3.1.1 is below.

-- Definition 3.1.2
const : ∀{i j} {X : Type i} {Y : Type j} → (f : X → Y) → Type (i ⊔ j)
const {X = X} f = (x₁ x₂ : X) → (f x₁) == (f x₂)

coll : ∀{i} → Type i → Type i
coll X = Σ (X → X) const

pathColl : ∀ {i} → Type i → Type i
pathColl X = (x₁ x₂ : X) → coll (x₁ == x₂)

-- Lemma 3.1.3
discr→pathColl : ∀ {i} {X : Type i} → has-dec-eq X → pathColl X
discr→pathColl dec x₁ x₂ with (dec x₁ x₂) 
discr→pathColl dec x₁ x₂ | inl p  = (λ _ → p) , (λ _ _ → idp)
discr→pathColl dec x₁ x₂ | inr np = idf _ , λ p → Empty-elim (np p)

-- Lemma 3.1.4
pathColl→isSet : ∀ {i} {X : Type i} → pathColl X → is-set X
pathColl→isSet {X = X} pc x₁ x₂ = all-paths-is-prop paths-equal where
  claim : (y₁ y₂ : X) → (p : y₁ == y₂) → p == ! (fst (pc _ _) idp) ∙ fst (pc _ _) p 
  claim x₁ .x₁ idp = ! (!-inv-l (fst (pc x₁ x₁) idp))
  paths-equal : (p₁ p₂ : x₁ == x₂) → p₁ == p₂
  paths-equal p₁ p₂ = 
    p₁                                      =⟨ claim _ _ p₁ ⟩
    ! (fst (pc _ _) idp) ∙ fst (pc _ _) p₁  =⟨ ap (λ q → (! (fst (pc x₁ x₁) idp)) ∙ q) (snd (pc _ _) p₁ p₂) ⟩ -- whiskering
    ! (fst (pc _ _) idp) ∙ fst (pc _ _) p₂  =⟨ ! (claim _ _ p₂) ⟩
    p₂                                      ∎  

-- Proposition 3.1.1
hedberg : ∀ {i} {X : Type i} → has-dec-eq X → is-set X
hedberg = pathColl→isSet ∘ discr→pathColl 

-- Definition 3.1.5
stable : ∀ {i} → Type i → Type i
stable X = ¬ (¬ X) → X

separated : ∀ {i} → Type i → Type i
separated X = (x₁ x₂ : X) → stable (x₁ == x₂)

-- Proposition 3.1.6
sep→set : ∀ {i} {X : Type i} → (separated X) → is-set X
sep→set {X = X} sep = pathColl→isSet isPc where
  isPc : pathColl X  
  isPc x₁ x₂ = f , c where 
    f : x₁ == x₂ → x₁ == x₂
    f = (sep x₁ x₂) ∘ (λ p np → np p)
    c : const f 
    c p₁ p₂ = 
      f p₁                        =⟨ idp ⟩
      (sep x₁ x₂) (λ np → np p₁)  =⟨ ap (sep x₁ x₂) 
                                     (λ= λ np → Empty-elim {A = λ _ → np p₁ == np p₂} (np p₁)) ⟩
      (sep x₁ x₂) (λ np → np p₂)  =⟨ idp ⟩
      f p₂                        ∎ 

-- Lemma 3.1.7
-- first: definition of 'reflexive propositional relation that implies identity'
rel-ref-id : ∀ {i} → Type i → Type (lsucc i)
rel-ref-id {i} X = Σ (X → X → Type i)
                     λ R → 
                           ((x : X) → R x x)
                         × ((x₁ x₂ : X) → (R x₁ x₂) → x₁ == x₂)
                         × ((x₁ x₂ : X) → is-prop (R x₁ x₂))

-- the actual Lemma 3.1.7
module lem317 {i : _} (X : Type i) (Rrip : rel-ref-id X) where

  R : X → X → Type i
  R = fst Rrip
  ref : (x : X) → R x x
  ref = fst (snd (Rrip)) -- fst (fst (snd Rrip))
  ii : (x₁ x₂ : X) → (R x₁ x₂) → x₁ == x₂
  ii = fst (snd (snd (Rrip))) -- snd (fst (snd Rrip))
  pr : (x₁ x₂ : X) → is-prop (R x₁ x₂)
  pr = snd (snd (snd Rrip))

  f : (x₁ x₂ : X) → x₁ == x₂ → R x₁ x₂
  f x₁ .x₁ idp = ref x₁

  id↔R : (x₁ x₂ : X) → (x₁ == x₂) ↔ R x₁ x₂
  id↔R x₁ x₂ = f _ _ , ii _ _

  pc : pathColl X
  pc x₁ x₂ = ii _ _ ∘ f _ _ , λ p₁ p₂ → ap (ii x₁ x₂) (prop-has-all-paths (pr x₁ x₂) _ _)

  isSet : is-set X
  isSet = pathColl→isSet pc


open wtrunc

-- Definition 3.1.9
splitSup : ∀ {i} → (X : Type i) → Type i
splitSup X = ∣∣ X ∣∣ → X

hSeparated : ∀ {i} → (X : Type i) → Type i
hSeparated X = (x₁ x₂ : X) → splitSup (x₁ == x₂)

-- Proposition 3.1.10
-- we show "2->1", "1->3", "3->2" as in the thesis.
-- for the last part, we show "1->4" and "4->3
set-characterisations : ∀ {i} → (X : Type i) → 
      (pathColl X → is-set X)
    × (is-set X → rel-ref-id X)
    × (rel-ref-id X → pathColl X)
    × (is-set X → hSeparated X)
    × (hSeparated X → rel-ref-id X)
set-characterisations X = 
  pathColl→isSet , 
  (λ ss → _==_ , (λ _ → idp) , (λ _ _ p → p) , ss) ,
  (lem317.pc X) ,
  (λ ss x₁ x₂ → tr-rec (ss x₁ x₂) (λ p → p)) ,
  (λ hsep → ((λ x₁ x₂ → ∣∣ x₁ == x₂ ∣∣) , (λ _ → ∣ idp ∣) , hsep , λ _ _ → tr-is-prop))

-- The rest of this section is only a replication of the arguments that we have given so far (for that reason, the proofs are not given in the article).
-- They do not directly follow from the propositions that we have proved before, but they directly imply them.
-- Of course, replication of arguments is not a good style for a formalization -
-- we chose this "disadvantageous" order purely as we believe it led to a better presentation in the article.

-- Lemma 3.1.11
pathColl→isSet-local : ∀ {i} {X : Type i} → {x₀ : X} → ((y : X) → coll (x₀ == y)) → (y : X) → is-prop (x₀ == y)
pathColl→isSet-local {X = X} {x₀} pc y = all-paths-is-prop paths-equal  where
  claim : (y : X) → (p : x₀ == y) → p == ! (fst (pc _) idp) ∙ fst (pc _) p 
  claim .x₀ idp = ! (!-inv-l (fst (pc _) idp))
  paths-equal : (p₁ p₂ : x₀ == y) → p₁ == p₂
  paths-equal p₁ p₂ = 
    p₁                                  =⟨ claim _ p₁ ⟩
    ! (fst (pc _) idp) ∙ fst (pc _) p₁  =⟨ ap (λ q → (! (fst (pc x₀) idp)) ∙ q) (snd (pc y) p₁ p₂) ⟩ -- whiskering
    ! (fst (pc _) idp) ∙ fst (pc _) p₂  =⟨ ! (claim _ p₂) ⟩
    p₂                                  ∎  

-- Proposition 3.11.12
hedberg-local : ∀ {i} {X : Type i} → {x₀ : X} → ((y : X) → Coprod (x₀ == y) (¬(x₀ == y))) → (y : X) → is-prop (x₀ == y)
hedberg-local {X = X} {x₀ = x₀} dec = pathColl→isSet-local local-pathColl where
  local-pathColl : (y : X) → coll (x₀ == y)
  local-pathColl y with (dec y)
  local-pathColl y₁ | inl p  = (λ _ → p) , (λ _ _ → idp)
  local-pathColl y₁ | inr np = idf _ , (λ p → Empty-elim (np p))

-- Lemma 3.1.13. This needs function extensionality.
sep→set-local : ∀ {i} {X : Type i} {x₀ : X} → ((y : X) → stable (x₀ == y)) → (y : X) → is-prop (x₀ == y)
sep→set-local {X = X} {x₀ = x₀} sep = pathColl→isSet-local is-pathColl where
  is-pathColl : (y : X) → coll (x₀ == y)
  is-pathColl y = f , c where
    f : x₀ == y → x₀ == y
    f = (sep y) ∘ (λ p np → np p)
    c : const f 
    c p₁ p₂ = 
      f p₁                    =⟨ idp ⟩
      (sep _) (λ np → np p₁) =⟨ ap (sep y) 
                                    (λ= (λ np → prop-has-all-paths Empty-is-prop _ _)) ⟩
      (sep _) (λ np → np p₂) =⟨ idp ⟩
      f p₂ ∎ 



-- Chapter 3.2: Generalisations to Higher Levels

-- first: some lemmata.

-- If A -> B -> A is the identity, then
-- a₁ == a₂ → s a₁ == s a₂ → r(s a₁) == r(s a₂) 
-- is also the identity in an appropriate sense
retract-path-retract : ∀ {i j} {A : Type i} {B : Type j}
  → (s : A → B) → (r : B → A) → (s-r : (a : A) → r (s a) == a)
  → (a₁ a₂ : A)
  → (p : a₁ == a₂) → ! (s-r a₁) ∙ (ap r (ap s p)) ∙ (s-r a₂) == p
retract-path-retract s r s-r a₁ .a₁ idp = !-inv-l (s-r a₁)

-- retracts of n-types are n-truncated
retract-is-truncated : ∀ {n : ℕ₋₂} {i j} {A : Type i} {B : Type j} 
  → (has-level n B) → (s : A → B) → (r : B → A) → ((a : A) → r (s a) == a) → has-level n A
retract-is-truncated {⟨-2⟩} h s r s-r = inhab-prop-is-contr (r (fst h)) (all-paths-is-prop (λ a₁ a₂ →
                       a₁       =⟨ ! (s-r a₁) ⟩
                       r(s(a₁)) =⟨ ap r (contr-has-all-paths h _ _) ⟩ 
                       r(s(a₂)) =⟨ s-r a₂ ⟩ 
                       a₂ ∎  
                       ))
retract-is-truncated {S n} h s r s-r a₁ a₂ = 
  retract-is-truncated {n} {A = a₁ == a₂} {B = s a₁ == s a₂} 
                       (h (s a₁) (s a₂)) 
                       (ap s) 
                       (λ p → ! (s-r a₁) ∙ (ap r p) ∙ (s-r a₂)) 
                       (retract-path-retract s r s-r a₁ a₂)

-- this is essentially one direction of a local version of the lemma which says that
-- a type is n-truncated iff its loop spaces are (n-1)-truncated 
trunclevel-aux₁ : ∀ {i} {X : Type i} {x₀ : X} → (n : ℕ) → ((x : X) → has-level (n -2) (x₀ == x)) 
                   → is-contr (fst ((Ω ^ n) (X , x₀)))
trunclevel-aux₁ {x₀ = x₀} O h = x₀ , λ x → fst (h x)
trunclevel-aux₁ {X = X} {x₀ = x₀} (S n) h = trunclevel-aux₁ n (h x₀ idp)

-- the other direction...
trunclevel-aux₂ : ∀ {i} {X : Type i} {x₀ : X} → (n : ℕ) → is-contr (fst ((Ω ^ n) (X , x₀)))
                   → ((x : X) → has-level (n -2) (x₀ == x)) 
trunclevel-aux₂ {X = X} {x₀ = x₀} O h = λ x → inhab-prop-is-contr (contr-has-all-paths h x₀ x) (contr-is-prop (contr-is-prop h x₀ x))
trunclevel-aux₂ {X = X} {x₀ = x₀} (S n) h .x₀ idp = trunclevel-aux₂ n h


-- Theorem 3.2.1

-- in the thesis, we write "let n ≥ -1 be a number". 
-- As we do not want to introduce a type of number that are at least -1,
-- we use ℕ.
-- To make up for this, we reduce n everywhere by 1.
module GLHA {i : ULevel} {X : Type i} {x₀ : X} {n : ℕ} where

  Ω-contr : Type i
--  loop-contr = is-contr (fst ((Ω ^ (n + 1)) (X , x₀)))
  Ω-contr = is-contr (fst ((Ω ^ n) (X , x₀)))

  locally-truncated : Type i
--  locally-truncated = (x : X) → has-level (n -1) (x₀ == x)
  locally-truncated = (x : X) → has-level (n -2) (x₀ == x)

  tr-rel-id : Type (lsucc i)
  tr-rel-id = Σ (X → Type i) λ Q → 
--                ((x : X) → has-level (n -1) (Q x))
                ((x : X) → has-level (n -2) (Q x))
                × (Q x₀)
                × ((x : X) → Q x → x₀ == x)


  tr-rel-id→locally-truncated : tr-rel-id → locally-truncated
  tr-rel-id→locally-truncated (Q , h , q₀ , ii) = λ x → retract-is-truncated {n = n -2} {A = x₀ == x} {B = Q x} (h x) s r r-s where 

    r : {x : X} → (Q x) → (x₀ == x)
    r {x} q = ! (ii x₀ q₀) ∙ (ii x q)

    s : {x : X} → (x₀ == x) → Q x
    s idp = q₀

    r-s : {x : X} → (p : x₀ == x) → r (s p) == p
    r-s idp = !-inv-l (ii x₀ q₀)


  locally-truncated→Ω-contr : locally-truncated → Ω-contr
  locally-truncated→Ω-contr loctr = trunclevel-aux₁ n loctr -- trunclevel-aux n loctr

  Ω-contr→tr-rel-id : Ω-contr → tr-rel-id
  Ω-contr→tr-rel-id h = (λ x → x₀ == x) , (trunclevel-aux₂ n h) , idp , (λ x p → p)

  module with-higher-truncs where
    -- for convenience, we import truncations from the library.
    open import lib.types.Truncation

    -- fourth item in Theorem 3.2.1
    id-stable : Type i
    id-stable = (x : X) → Trunc (n -2) (x₀ == x) → x₀ == x

    -- it is very easy to see that (4) and (2) are logically equivalent.
    -- 2 ⇒ 4
    tr-rel-id→id-stable : tr-rel-id → id-stable
    tr-rel-id→id-stable (Q , h , q₀ , ii) = λ x → (ii x) ∘ (Trunc-rec (h x) (λ p → transport _ p q₀)) 

    -- 4 ⇒ 2
    id-stable→tr-rel-id : id-stable → tr-rel-id
    id-stable→tr-rel-id idst = (λ x → Trunc (n -2) (x₀ == x)) , (λ _ → Trunc-level) , [ idp ] , idst