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

{- This module serves to develop some basic theory about pointed types.
   After defining the usual notions of pointed types, pointed equivalences,
   and loop spaces, we derive a version of univalence for pointed equivalences
   and observe that univalence between identical types is a pointed equivalence.

   We define pointed versions of dependent sums and products using the usual
   notion of pointed predicates and observe that they commute in a certain sense
   with taking loop spaces.

   We finish by deriving a generalization to n-truncation and n-th loop spaces
   of the fact allowing us to 'forget' contractible components in a dependent
   sum type that will be needed in the Hierarchy module. -}
module Universe.Utility.Pointed 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.TLevel

open import Universe.Utility.General
open import Universe.Utility.TruncUniverse


{- Pointed types.
   A pointed type is a type (base) together with a chosen element (pt).
   The loop space construction Ω takes a pointed type and returns the type
   of all loops at the given basepoint. The trivial loop is taken as
   canonical element, thus forming a new pointed type. -}
Type• : (i : ULevel)  Type (lsucc i)
Type• i = Σ (Type i) (idf _)

module _ {i} (X : Type• i) where
  base = fst X
  pt   = snd X

-- Alternate definition: Σ (n -Type i) ⟦_⟧
_-Type•_ : (n : ℕ₋₂) (i : ULevel)  Type (lsucc i)
n -Type• i = Σ (Type• i) (has-level n  base)

-- For alternate definition: Σ-≤ (n -Type-≤ i) raise
_-Type•-≤_ : (n : ℕ₋₂) (i : ULevel)  S n -Type lsucc i
n -Type•-≤ i = (n -Type• i
              , equiv-preserves-level Σ-comm-snd
                                      (snd (Σ-≤ (n -Type-≤ i) raise)))

{- Pointed equivalences.
   An equivalence of pointed types is an equivalences of the bases
   that preserves the points -}
_≃•_ :  {i j}  Type• i  Type• j  Set (i  j)
A ≃• B = Σ (base A  base B)  f  –> f (pt A) == pt B)

ide• :  {i} (X : Type• i)  X ≃• X
ide• _ = ide _ , idp

_∘e•_ :  {i j k} {X : Type• i} {Y : Type• j} {Z : Type• k}
        Y ≃• Z  X ≃• Y  X ≃• Z
(u , p) ∘e• (v , q) = (u ∘e v , ap (–> u) q  p)

_⁻¹• :  {i j} {X : Type• i} {Y : Type• j}  X ≃• Y  Y ≃• X
(u , p) ⁻¹• = (u ⁻¹ , ap (<– u) (! p) <–-inv-l u _)

-- Equational reasoning for pointed equivalences.
infix  2 _≃•∎
infixr 2 _≃•⟨_⟩_

_≃•⟨_⟩_ :  {i j k} (X : Type• i) {Y : Type• j} {Z : Type• k}
           X ≃• Y  Y ≃• Z  X ≃• Z
_ ≃•⟨ u  v = v ∘e• u

_≃•∎ :  {i} (X : Type• i)  X ≃• X
_≃•∎ = ide•


-- The loop space construction.
Ω :  {i}  Type• i  Type• i
Ω (A , a) = (a == a , idp)

Ω-≤ :  {i} {n : ℕ₋₂}  (S n) -Type• i  n -Type• i
Ω-≤ ((A , a) , t) = (Ω (A , a) , t a a)

-- Loop spaces are preserved by pointed equivalences.
equiv-Ω :  {i j} {X : Type• i} {Y : Type• j}  X ≃• Y  Ω X ≃• Ω Y
equiv-Ω (u , p) = split u p where
  split :  u {a} {b}  –> u a == b  Ω (_ , a) ≃• Ω (_ , b)
  split u idp = (equiv-ap u _ _ , idp)

equiv-Ω^ :  {i j} {X : Type• i} {Y : Type• j} (n : )
            X ≃• Y  (Ω ^ n) X ≃• (Ω ^ n) Y
equiv-Ω^ 0     e = e
equiv-Ω^ (S n) e = equiv-Ω^ n (equiv-Ω e)


{- We call a pointed type n-truncated if its base is.
   Constructing the loop space decrements the truncation level. -}
has-level• :  {i}  ℕ₋₂  Type• i  Type i
has-level• n = has-level n  base

trunc-many :  {i} {X : Type• i} {k : } (n : )
              has-level• (k + n -2)          X
              has-level• (k     -2) ((Ω ^ n) X)
trunc-many 0     t = t
trunc-many (S n) t = trunc-many n (t _ _)

--Ω^-≤ : ∀ {i} {k : ℕ} (n : ℕ) → (k + n -2) -Type• i → (k -2) -Type• i
--Ω^-≤ O     X = X
--Ω^-≤ (S n) X = Ω^-≤ n (Ω-≤ X)

Ω^-≤ :  {i} {k : } (n : )  (k + n -2) -Type• i  (k -2) -Type• i
Ω^-≤ n (X , t) = ((Ω ^ n) X , trunc-many n t)

Ω^-≤' :  {i} {k : } (n : )  (n + k -2) -Type• i  (k -2) -Type• i
Ω^-≤' n (X , t) =
  ((Ω ^ n) X , trunc-many n (transport  z  has-level• (z -2) X)
                                       (+-comm _ n) t))


{- Pointedness allows for a more direct notion of contractibility.
   Since pointed types are always inhabited,
   being contractible and propositional is equivalent. -}
module _ {i} (X : Type• i) where
  is-contr• : Type i
  is-contr• =  a  a == pt X

  prop-is-contr• : has-level• ⟨-1⟩ X  is-contr•
  prop-is-contr• t _ = prop-has-all-paths t _ _

-- Pointed equivalences preserve (pointed) contractibility.
equiv-is-contr• :  {i j} {X : Type• i} {Y : Type• j}
                 X ≃• Y  is-contr• X  is-contr• Y
equiv-is-contr• (u , p) = equiv-Π u  a  (_ , post∙-is-equiv p)
                                        ∘e (_ , pre∙-is-equiv (<–-inv-r u a)) ⁻¹
                                        ∘e equiv-ap u _ _)


-- Univalence for pointed equivalences.
module _ {i} {A B : Type• i} where
  ua•-equiv : (A ≃• B)  (A == B)
  ua•-equiv = 
      A ≃• B
    ≃⟨ ide _ 
      Σ (base A  base B)  f  –> f (pt A) == pt B)
    ≃⟨ equiv-Σ-fst _ (snd (ua-equiv ⁻¹)) ⁻¹ 
      Σ (base A == base B)  q  coe q (pt A) == pt B)
    ≃⟨ equiv-Σ-snd  q  coe-equiv (ap  f  coe f (pt A) == pt B)
                                        (! (ap-idf q)))) 
      Σ (base A == base B)  q  coe (ap (idf _) q) (pt A) == pt B)
    ≃⟨ equiv-Σ-snd  q  to-transp-equiv _ q ⁻¹) 
      Σ (base A == base B)  q  pt A == pt B [ idf _  q ])
    ≃⟨ =Σ-eqv _ _ 
      A == B
    ≃∎

  ua• : A ≃• B  A == B
  ua• = –> ua•-equiv

  coe•-equiv : A == B  A ≃• B
  coe•-equiv = <– ua•-equiv

-- Normal univalence can be made pointed in the endo-setting.
module _ {i} {A : Type i} where
  ua-equiv• : (A  A , ide _) ≃• (A == A , idp)
  ua-equiv• = ((ua-equiv ⁻¹) , idp) ⁻¹•


{- Pointed predicates.
   A pointed predicate over a pointed type is a predicate over the base
   together with a inhabitant of the predicate at the point.
   Note that pointed types are equivalent to pointed predicates
   over the pointed unit type (not shown here). -}
Pred• :  {i} (X : Type• i) (j : ULevel)  Type (i  lsucc j)
Pred• X j = Σ (base X  Type j)  P  P (pt X))

-- We have fibered notions of the loop space contruction and n-truncatedness.
module _ {i} {X : Type• i} {j} where
  Ω̃ : Pred• X j  Pred• (Ω X) j
  Ω̃ (P , x) = ((λ p  x == x [ P  p ]) , idp)

  pred-has-level : ℕ₋₂  Pred• X j  Type (i  j)
  pred-has-level n Q = (a : base X)  has-level n (fst Q a)


{- == Pointed dependent sums ==
   Pointed predicates as defined above enable us to introduce a Σ-connective
   for pointed types. Because of the abstract nature of some of our lemmata, we
   give Σ• in its uncurried form and first define the type of its parameter. -}
Σ•-param :  i j  Type (lsucc (i  j))
Σ•-param i j = Σ (Type• i)  X  Pred• X j)

module _ {i j} where
  Ω-Σ•-param : Σ•-param i j  Σ•-param i j
  Ω-Σ•-param (X , W) = (Ω X , Ω̃ W)

  Σ• : Σ•-param i j  Type• (i  j)
  Σ• (X , Q) = (Σ (base X) (fst Q) , (pt X , snd Q))
  
  {- Commutativity of pointed dependent sums and the loop space construction
     will become an important technical tool, enabling us to work at a more
     abstract level later on. -}
  Ω-Σ•-comm : (R : Σ•-param i j)  Ω (Σ• R) ≃• Σ• (Ω-Σ•-param R)
  Ω-Σ•-comm _ = (=Σ-eqv _ _ , idp) ⁻¹•


{- Pointed dependent products.
   This is not quite the equivalent of Π for pointed types: the domain parameter
   is just an ordinary non-pointed type. However, to enable our goal of
   abstractly working with pointed types, defining this notion is useful. -}
Π•-param :  i j  Type (lsucc (i  j))
Π•-param i j = Σ (Type i)  A  A  Type• j)

module _ {i j} where
  Ω-Π•-param : Π•-param i j  Π•-param i j
  Ω-Π•-param (A , F) = (A , Ω  F)

  Π• : Π•-param i j  Type• (i  j)
  Π• (A , Y) = (Π A (base  Y) , pt  Y)

  {- Pointed dependent products and loop space construction on
     its codomain parameter commute as well. -}
  Ω-Π•-comm : (R : Π•-param i j)  Ω (Π• R) ≃• Π• (Ω-Π•-param R)
  Ω-Π•-comm _ = (app=-equiv , idp)

  Ω^-Π•-comm : (C : Type i) (F : C  Type• j) (n : )
              (Ω ^ n) (Π• (C , F)) ≃• Π• (C , Ω ^ n  F)
  Ω^-Π•-comm C F 0     = ide• _
  Ω^-Π•-comm C F (S n) = Ω^-Π•-comm C _ n ∘e• equiv-Ω^ n (Ω-Π•-comm _)

equiv-Π• :  {i₀ i₁ j₀ j₁} {R₀ : Π•-param i₀ j₀} {R₁ : Π•-param i₁ j₁}
            Σ (fst R₀  fst R₁)  u   a  snd R₀ (<– u a) ≃• snd R₁ a)
            Π• R₀ ≃• Π• R₁
equiv-Π• (u , v) = (equiv-Π u (fst  v) , λ= (snd  v))


-- In an n-th loop space, we can forget components of truncation level n.
forget-Ω^-Σ•₂ :  {i j} {X : Type• i} (Q : Pred• X j) (n : )
                 pred-has-level (n -2) Q  (Ω ^ n) (Σ• (X , Q)) ≃• (Ω ^ n) X
forget-Ω^-Σ•₂     {X = X} Q    O  h = (Σ₂-contr h , idp)
forget-Ω^-Σ•₂ {i} {X = X} Q (S n) h =
  (Ω ^ (S n)) (Σ• (X , Q))  ≃•⟨ equiv-Ω^ n (Ω-Σ•-comm _) 
  (Ω ^ n) (Σ• (Ω X , Ω̃ Q))  ≃•⟨ forget-Ω^-Σ•₂ {i} _ n  _  =-[-↓-]-level h) 
  (Ω ^ (S n)) X             ≃•∎