{-# OPTIONS --safe #-}
module Cubical.HITs.SequentialColimit.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat

private
  variable
    ℓ : Level

record Sequence (ℓ : Level) : Type (ℓ-suc ℓ) where
  field
    obj : ℕ → Type ℓ
    map : {n : ℕ} → obj n → obj ( + n)

open Sequence

data SeqColim (X : Sequence ℓ) : Type ℓ where
  incl : {n : ℕ} → X .obj n → SeqColim X
  push : {n : ℕ} (x : X .obj n) → incl x ≡ incl (X .map x)