{-# OPTIONS --without-K --rewriting --overlapping-instances #-}

open import lib.Basics
open import lib.NConnected
open import lib.NType2
open import lib.cubical.Square
open import lib.types.Lift
open import lib.types.Nat
open import lib.types.Sigma
open import lib.types.TLevel
open import lib.types.Truncation
open import lib.types.Unit

{- Sequential colimits -}

module lib.types.NatColim where

module _ {i} {D :   Type i} (d : (n : )  D n  D (S n)) where

  postulate  -- HIT
    ℕColim : Type i
    ncin' : (n : )  D n  ℕColim
    ncglue' : (n : )  (x : D n)  ncin' n x == ncin' (S n) (d n x)

module _ {i} {D :   Type i} {d : (n : )  D n  D (S n)} where

  ncin = ncin' d
  ncglue = ncglue' d

module _ {i} {D :   Ptd i} where

  ⊙ℕColim : (d : (n : )  (D n ⊙→ D (S n)))  Ptd i
  ⊙ℕColim d = ⊙[ ℕColim (fst  d) , ncin 0 (pt (D 0)) ]

module _ {i} {D :   Type i} (d : (n : )  D n  D (S n)) where

  module ℕColimElim {j} {P : ℕColim d  Type j}
    (ncin* : (n : ) (x : D n)  P (ncin n x))
    (ncglue* : (n : ) (x : D n)
       ncin* n x == ncin* (S n) (d n x) [ P  ncglue n x ])
    where

    postulate  -- HIT
      f : Π (ℕColim d) P
      ncin-β :  n x  f (ncin n x)  ncin* n x
    {-# REWRITE ncin-β #-}

    postulate  -- HIT
      ncglue-β : (n : ) (x : D n)  apd f (ncglue n x) == ncglue* n x

  open ℕColimElim public using () renaming (f to ℕColim-elim)

  module ℕColimRec {j} {A : Type j}
    (ncin* : (n : )  D n  A)
    (ncglue* : (n : )  (x : D n)  ncin* n x == ncin* (S n) (d n x))
    where

    private
      module M = ℕColimElim ncin*  n x  ↓-cst-in (ncglue* n x))

    f : ℕColim d  A
    f = M.f

    ncglue-β : (n : ) (x : D n)  ap f (ncglue n x) == ncglue* n x
    ncglue-β n x = apd=cst-in {f = f} (M.ncglue-β n x)

{- Raising and lifting -}
module _ {i} {D :   Type i} (d : (n : )  D n  D (S n)) where

  {- Can define a function [nc-raise d : ℕColim d → ℕColim d]
     so that [inn (S n) ∘ d = nc-raise d ∘ inn n] -}

  module ℕCRaise = ℕColimRec d {A = ℕColim d}
     n x  ncin (S n) (d n x))
     n x  ncglue (S n) (d n x))

  nc-raise : ℕColim d  ℕColim d
  nc-raise = ℕCRaise.f

  nc-raise-= : (c : ℕColim d)  c == nc-raise c
  nc-raise-= = ℕColimElim.f d
     n x  ncglue n x)
     n x  ↓-='-from-square $
      ap-idf (ncglue n x) ∙v⊡ (connection2 ⊡v∙ (! (ℕCRaise.ncglue-β n x))))

  {- Lift an element of D₀ to any level -}

  nc-lift : (n : )  D O  D n
  nc-lift O x = x
  nc-lift (S n) x = d n (nc-lift n x)

  nc-lift-= : (n : ) (x : D O)
     ncin' d O x == ncin n (nc-lift n x)
  nc-lift-= O x = idp
  nc-lift-= (S n) x = nc-lift-= n x  ncglue n (nc-lift n x)

  {- Lift an element of D₀ to the 'same level' as some element of ℕColim d -}

  module ℕCMatch (x : D O) = ℕColimRec d {A = ℕColim d}
     n _  ncin n (nc-lift n x))
     n _  ncglue n (nc-lift n x))

  nc-match = ℕCMatch.f

  nc-match-=-base : (x : D O) (c : ℕColim d)  ncin O x == nc-match x c
  nc-match-=-base x = ℕColimElim.f d
     n _  nc-lift-= n x)
     n y  ↓-cst=app-from-square $
      disc-to-square idp ⊡v∙ ! (ℕCMatch.ncglue-β x n y))

{- If all Dₙ are m-connected, then the colim is m-connected -}

ncolim-conn :  {i} {D :   Type i} (d : (n : )  D n  D (S n)) (m : ℕ₋₂)
  {{_ : {n : }  is-connected m (D n)}}
   is-connected m (ℕColim d)
ncolim-conn {D = D} d ⟨-2⟩ = -2-conn (ℕColim d)
ncolim-conn {D = D} d (S m) {{cD}} =
  Trunc-rec
     x  has-level-in ([ ncin O x ] ,
            (Trunc-elim $
              λ c  ap [_] (nc-match-=-base d x c)  nc-match-=-point x c)))
    (contr-center cD)
  where

  nc-match-=-point : (x : D O) (c : ℕColim d)
     [_] {n = S m} (nc-match d x c) == [ c ]
  nc-match-=-point x = ℕColimElim.f d
     n y  ap (Trunc-fmap (ncin n))
                (contr-has-all-paths [ nc-lift d n x ] [ y ]))
       n y  ↓-='-from-square $
        (ap-∘ [_] (nc-match d x) (ncglue n y)
          ap (ap [_]) (ℕCMatch.ncglue-β d x n y))
        ∙v⊡
        ! (ap-idf _)
        ∙h⊡
        square-symmetry
          (natural-square
            (Trunc-elim
                c  ap [_] (nc-raise-= d c)))
            (ap (Trunc-fmap (ncin n))
                (contr-has-all-paths [ nc-lift d n x ] [ y ])))
        ⊡h∙
        ∘-ap (Trunc-fmap (nc-raise d)) (Trunc-fmap (ncin n))
          (contr-has-all-paths [ nc-lift d n x ] [ y ])
        ⊡h∙
        vert-degen-path
          (natural-square
             t  Trunc-fmap-∘ (nc-raise d) (ncin n) t
                    ! (Trunc-fmap-∘ (ncin (S n)) (d n) t))
            (contr-has-all-paths [ nc-lift d n x ] [ y ]))
        ⊡h∙
        ap-∘ (Trunc-fmap (ncin (S n))) (Trunc-fmap (d n))
             (contr-has-all-paths [ nc-lift d n x ] [ y ])
        ⊡h∙
        ap (ap (Trunc-fmap (ncin (S n))))
           (contr-has-all-paths _ _))

{- Type of finite tuples -}

⊙FinTuplesType :  {i}  (  Ptd i)    Ptd i
⊙FinTuplesType F O = ⊙Lift ⊙Unit
⊙FinTuplesType F (S n) = F O ⊙× ⊙FinTuplesType (F  S) n

FinTuplesType :  {i}  (  Ptd i)    Type i
FinTuplesType F n = de⊙ (⊙FinTuplesType F n)

fin-tuples-map :  {i} (F :   Ptd i) (n : )
   (⊙FinTuplesType F n ⊙→ ⊙FinTuplesType F (S n))
fin-tuples-map F O = (_ , idp)
fin-tuples-map F (S n) =
  ((λ {(x , r)  (x , fst (fin-tuples-map (F  S) n) r)}) ,
   pair×= idp (snd (fin-tuples-map (F  S) n)))

⊙FinTuples :  {i}  (  Ptd i)  Ptd i
⊙FinTuples {i} F = ⊙ℕColim (fin-tuples-map F)

FinTuples :  {i}  (  Ptd i)  Type i
FinTuples = de⊙  ⊙FinTuples

fin-tuples-cons :  {i} (F :   Ptd i)
   de⊙ (F O) × FinTuples (F  S)  FinTuples F
fin-tuples-cons {i} F = equiv into out into-out out-into
  where
    module Into (x : de⊙ (F O)) =
      ℕColimRec (fst  fin-tuples-map (F  S)) {A = FinTuples F}
         n r  ncin (S n) (x , r))
         n r  ncglue (S n) (x , r))

    into = uncurry Into.f

    out-ncin : (n : )
       FinTuplesType F n  de⊙ (F O) × FinTuples (F  S)
    out-ncin O x = (pt (F O) , ncin O _)
    out-ncin (S n) (x , r) = (x , ncin n r)

    out-ncglue : (n : ) (r : FinTuplesType F n)
       out-ncin n r == out-ncin (S n) (fst (fin-tuples-map F n) r)
    out-ncglue O x = idp
    out-ncglue (S n) (x , r) = pair= idp (ncglue n r)

    module Out = ℕColimRec _ out-ncin out-ncglue
    out = Out.f

    abstract
      into-out-ncin : (n : ) (r : FinTuplesType F n)
         into (out-ncin n r) == ncin n r
      into-out-ncin O x = ! (ncglue O x)
      into-out-ncin (S n) (x , r) = idp

      into-out-ncglue : (n : ) (r : FinTuplesType F n)
         into-out-ncin n r == into-out-ncin (S n) (fst (fin-tuples-map F n) r)
          [  s  into (out s) == s)  ncglue n r ]
      into-out-ncglue O x =
        ↓-∘=idf-from-square into out $
          ap (ap into) (Out.ncglue-β O x)
          ∙v⊡ bl-square (ncglue O x)
      into-out-ncglue (S n) (x , r) =
        ↓-∘=idf-from-square into out $
          (ap (ap into) (Out.ncglue-β (S n) (x , r))
            ∘-ap into (_,_ x) (ncglue n r)
            Into.ncglue-β x n r)
          ∙v⊡ vid-square

      into-out : (r : FinTuples F)  into (out r) == r
      into-out = ℕColimElim.f _
        into-out-ncin
        into-out-ncglue

      out-into : (t : de⊙ (F O) × FinTuples (F  S))  out (into t) == t
      out-into = uncurry $ λ x  ℕColimElim.f _
         n r  idp)
         n r  ↓-='-from-square $
          (ap-∘ out (Into.f x) (ncglue n r)
            ap (ap out) (Into.ncglue-β x n r)
            Out.ncglue-β (S n) (x , r))
          ∙v⊡ vid-square)

⊙fin-tuples-cons :  {i} (F :   Ptd i)
   (F O ⊙× ⊙FinTuples (F  S)) ⊙≃ ⊙FinTuples F
⊙fin-tuples-cons F = ≃-to-⊙≃ (fin-tuples-cons F) (! (ncglue O _))