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

{- This module defines our notion of connectedness not requiring HITs.
   We define the generic n-connected version of a type, show that it is
   n-connected, and that it behaves like the original type above level n.
   We conclude by shoing this notion coincides with the usual notion.
   of connectedness in the presence of HITs. -}
module Trunc.Connection where

open import lib.Basics
open import lib.NType2
open import lib.Equivalences2
open import lib.types.Unit
open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Paths
open import lib.types.TLevel

open import Preliminaries
open import Pointed
open import UniverseOfNTypes

open import Trunc.Universal
open import Trunc.Basics
open import Trunc.TypeConstructors

open import HHHUU-ComplicatedTypes

-- Definition 7.6.1 is in the library:
-- lib.NConnected.is-connected

-- In this file, our own notion of connectedness is discussed.

open trunc-ty
open trunc-props

-- Definition 7.6.13
{- Our plain MLTT connectedness predicate.
   Because of predicativity issues, it has to live in one universe higher
   than its argument type C. Internally, we really want to quantify over
   truncation operators not only at the level of C, but also at levels below C.
   This would be the same in a theory with cumulative universes, but we are
   working in Agda. Since we are only going to actually use the truncation
   operator at one level lower than C, we restrict ourselves to this specific
   assumption in this particular development for no particular reason other
   than brevity of presentation. The reason for this difference of one level
   will become apparent in the definition of 'connection'. -}
module _ {i} (n : ℕ₋₂) (C : Type (lsucc i)) where
  is-connected⋆ : Type (lsucc (lsucc i))
  is-connected⋆ = (Tr : (X : Type i) → trunc-ty n X (lsucc i))
                  (TrC : trunc-ty n C (lsucc i))
                → is-contr ⟦ type TrC ⟧

{- The (n+1)-connected version, or n-connection of some pointed type A.
   Since we internally quantify over the type of truncations of a path space
   from a before being able to require an element in the truncation,
   predicativity issues force 'connection' to live in a universe one level
   higher than A.
   
   Take particular care in noting that the parameter n is in fact one-off,
   for example, The type 'connection (-2)' denotes the (-1)-connection. -}
module _ {i} (A : Type• i) where
  module con (n : ℕ₋₂) where
    -- Definition 7.6.11
    connection• : Type• (lsucc i)
    connection• =
      Σ• (A
        , ((λ b → (TrP : trunc-ty n (pt A == b) i) → ⟦ type TrP ⟧)
         , (λ TrP → cons TrP idp)))

    {- The base type of the (n+1)-connection:
      Σ A (λ b → (TrP : trunc-ty n (a == b) i) → ⟦ type TrP ⟧. -}
    connection : Type (lsucc i)
    connection = base connection•

    -- Lemma 7.6.14
    connection-is-connected : is-connected⋆ (S n) connection
    connection-is-connected Tr TrC = equiv-preserves-level (e ⁻¹) h where

      -- The supplied generic truncation operator is used only to truncate A.
      TrA : trunc-ty (S n) (base A) (lsucc i)
      TrA = Tr (base A)

      TrP : (b : base A) → trunc-ty n (pt A == b) i
      TrP = trunc-path.trunc {j = i} TrA (pt A)

      {- This definition typechecks since
              Σ A (λ b → ⟦ type (TrP b) ⟧
           ≡  Σ A (λ a → cons TrA (pt A) == cons TrA b)
         by construction of trunc-path.trunc. -}
      TrD : trunc-ty (S n) (Σ (base A) (λ b → ⟦ type (TrP b) ⟧)) (lsucc i)
      TrD = trunc-Σ.trunc {j = lsucc i} TrA
              (λ b → trunc-self.trunc (Path-≤ (type TrA) (cons TrA (pt A)) b))

      u : connection ≃ Σ (base A) (λ b → ⟦ type (TrP b) ⟧)
      u = equiv-Σ-snd {B = λ _ → Π _ _}  -- No idea why Agda wants this.
                      (λ b → Π₁-contr (trunc-inhab-contr {j = i} (TrP b)))

      e : ⟦ type TrC ⟧ ≃ ⟦ type TrD ⟧
      e = trunc-functor.fmap-equiv {j = lsucc i} TrC TrD u

      {- Note that
           ⟦ type TrD ⟧  ≡  Σ ⟦ type TrA ⟧ (λ tb → cons TrA (pt A) == tb)
         by construction of trunc-Σ.trunc. -}
      h : is-contr ⟦ type TrD ⟧
      h = pathfrom-is-contr (cons TrA (pt A))

  module con2 (n : ℕ) where
    open con (n -2)

    -- Lemma 7.6.12
    -- The (n+1)-connection of A coincides with A on dimension n+2 and above.
    connection-higher-dim : (Ω ^ n) connection• ≃• (Ω ^ n) A
    connection-higher-dim =
      forget-Ω^-Σ•₂ _ n (λ _ → Π-level (λ Tr → snd (type Tr)))

  open con public
  open con2 public

-- For the first time in the dependency chain, we assume HITs.
module with-hits where
  open import lib.types.Truncation
  open import lib.NConnected
  
  {- With the truncations of the HoTT community's library,
     our truncation types are always inhabited, and hence contractible. -}
  module _ {i j} where
    trunc : (n : ℕ₋₂) (A : Type i) → trunc-ty n A (i ⊔ j)
    trunc n A = record
      { type = (Trunc n A , Trunc-level)
      ; cons = [_]
      ; univ = λ U → is-eq
        (λ f → f ∘ [_]) (Trunc-rec (snd U)) (λ f → idp)
        (λ f → λ= (Trunc-elim (λ _ → =-preserves-level _ (snd U))
                              (λ a → idp)))}
      
    trunc-contr : {n : ℕ₋₂} {A : Type i} → is-contr (trunc-ty n A (i ⊔ j))
    trunc-contr = trunc-inhab-contr {j = j} (trunc _ _)

  -- Lemma 7.6.15
  -- Our connectedness⋆ is equivalent to HIT connectedness.
  module _ {i} {n : ℕ₋₂} {A : Type (lsucc i)} where
    conn⋆-conn : is-connected⋆ n A ≃ is-connected n A
    conn⋆-conn = Π₁-contr (trunc-contr {j = lsucc i})
              ∘e Π₁-contr (Π-level (λ _ → trunc-contr {j = lsucc i}))


-- Theorem 7.7.1
module _ (n : ℕ) where
  M• : Type• ｢ n +  ｣
  M• = connection• (_ , Loop n) (n -1)

  assertion-0 : has-level ⟨ n +  ⟩ (base M•)
  assertion-0 = snd (Σ-≤ (⟨ n ⟩ -Type-≤ ｢ n ｣)
                    (λ b → Π-≤ (trunc-ty _ (_ == b) _)
                               (λ tr → raise (raise (type tr)))))

  assertion-1 : ¬ (has-level ⟨ n ⟩ (base M•))
  assertion-1 =
      main' n
    ∘ –> (equiv-is-contr• (connection-higher-dim _ (n + )))
    ∘ (λ z → z (pt M•))
    ∘ –> has-level-equiv-contr-loops

  assertion-2 : is-connected⋆ ⟨ n ⟩ (base M•)
  assertion-2 = connection-is-connected _ _