\import Equiv
\import Equiv.Univalence
\import HLevel
\import Homotopy.Fibration
\import Logic
\import Paths

\record Seq (A : Nat -> \Type) (f : \Pi {n : Nat} -> A n -> A (suc n))

\data SeqColimit (s : Seq)
  | inSC {n : Nat} (s.A n)
  | quotSC {n : Nat} (x : s.A n) : inSC x = inSC (s.f x)
  \where {
    -- | The total space of a fibration over a sequential colimit is equivalent to a sequential colimit of fibers of this fibration.
    \func flattening {s : Seq} (P : SeqColimit s -> \Type) : total = (\Sigma (w : SeqColimit s) (P w))
      => Equiv-to-= totalSeqColimitLeft *> path TotalSeqColimit *> Equiv-to-= totalSeqColimitRight
      \where {
        \func total => SeqColimit seq
          \where
            \func seq : Seq \cowith
              | A n => \Sigma (x : s.A n) (P (inSC x))
              | f p => (s.f p., transport P (path (quotSC p.)) p.)

        \data TotalSeqColimit (j : I)
          | tinSC {n : Nat} (x : s.A n) (P (inSC x))
          | tquotSC {n : Nat} (x : s.A n) (i : I) (w : P (quotSC x (I.squeeze i j))) \elim i {
            | left => tinSC x w
            | right => tinSC (s.f x) (coe2 (\lam i => P (quotSC x i)) j w right)
          }

        \func totalSeqColimitLeft : QEquiv {total} {TotalSeqColimit left} \cowith
          | f => LR
          | ret => RL
          | ret_f t => \case \elim t \with {
            | inSC (x,p) => idp
            | quotSC (x,p) i => idp
          }
          | f_sec t => \case \elim t \with {
            | tinSC x p => idp
            | tquotSC x i p => idp
          }
          \where {
            \func LR (t : total) : TotalSeqColimit left \elim t
              | inSC (x,p) => tinSC x p
              | quotSC (x,p) i => tquotSC x i p

            \func RL (t : TotalSeqColimit left) : total \elim t
              | tinSC x p => inSC (x,p)
              | tquotSC x i p => quotSC (x,p) i
          }

        \func totalSeqColimitRight : QEquiv {TotalSeqColimit right} {\Sigma (w : SeqColimit s) (P w)} \cowith
          | f => LR
          | ret => RL
          | ret_f t => \case \elim t \with {
            | tinSC _ _ => idp
            | tquotSC _ _ _ => idp
          }
          | f_sec t => \case \elim t \with {
            | (inSC x, p) => idp
            | (quotSC x i, p) => idp
          }
          \where {
            \func LR (t : TotalSeqColimit right) : \Sigma (w : SeqColimit s) (P w) \elim t
              | tinSC x p => (inSC x, p)
              | tquotSC x i p => (quotSC x i, p)

            \func RL (p : \Sigma (w : SeqColimit s) (P w)) : TotalSeqColimit right \elim p
              | (inSC x, p) => tinSC x p
              | (quotSC x i, p) => tquotSC x i p
          }
      }
  }

-- | The colimit of a sequence of surjections is a surjection.
\lemma seqColimit-surj (s : Seq) (p : \Pi (n : Nat) -> Surjection (s.f {n})) : Surjection (inSC {s} {}) \cowith
  | isSurjMap (inSC x) => helper x
  \where {
    \lemma helper {n : Nat} (x : s.A n) : TruncP (Fib (inSC {s} {}) (inSC x)) \elim n
      |  => inP (x,idp)
      | suc n =>
        \let | (inP r) => isSurjMap {p n} x
             | (inP t) => helper r.
        \in inP (t., t. *> path (quotSC r.) *> pmap inSC r.)
  }

-- | The colimit of a sequence of constant maps is contractible.
\lemma constantMaps (s : Seq) (p : \Pi (n : Nat) -> \Sigma (x : s.A (suc n)) (\Pi (a : s.A n) -> s.f a = x)) : Contr (SeqColimit s)
  => Contr.make (inSC (p ).) (\lam x => inv (contraction x))
  \where {
    \func points (n : Nat) : inSC (p n). = inSC (p ). \elim n
      |  => idp
      | suc n => inv (path (quotSC (p n).) *> pmap inSC ((p (suc n)). (p n).)) *> points n

    \func contraction (x : SeqColimit s) : x = inSC (p ). \elim x
      | inSC {n} x => path (quotSC x) *> pmap inSC ((p n). x) *> points n
      | quotSC {n} x =>
        \let | t => path (quotSC x) *> pmap inSC ((p n). x) *> points n
             | h a => path (quotSC a) *> pmap inSC ((p (suc n)). a)
             | q =>
               coe (quotSC x __ = inSC (p ).) t right                                        ==< coe_path (path (quotSC x)) t idp >==
               inv (path (quotSC x)) *> t                                                      ==< inv (*>-assoc _ _ _) >==
               (inv (path (quotSC x)) *> path (quotSC x)) *> pmap inSC ((p n). x) *> points n ==< pmap (`*> pmap inSC ((p n). x) *> points n) (inv_*> (path (quotSC x))) >==
               idp *> pmap inSC ((p n). x) *> points n                                        ==< idp_*> _ >==
               pmap inSC ((p n). x) *> points n                                               ==< pmap (`*> points n) (inv (Jl (\lam y q => h (s.f x) *> inv (h y) = pmap inSC q) (*>_inv _) ((p n). x))) >==
               (h (s.f x) *> inv (h (p n).)) *> points n                                      ==< *>-assoc _ _ _ >==
               h (s.f x) *> points (suc n)                                                     ==< *>-assoc _ _ _ >==
               path (quotSC (s.f x)) *> pmap inSC ((p (suc n)). (s.f x)) *> points (suc n)    `qed
        \in pathOver q
  }