Sequential colimits

DirectedColim is the quotient of a sequence of types by its transition maps. The local Skolem tower uses this generic construction for its function and relation symbols.

Sequential colimit of types

def FirstOrder.Language.DirectedColim (F : ℕ → Type) (φ : (k : ℕ) → F k → F (k + 1)) : Type

The sequential colimit of a tower of types F 0 → F 1 → … along maps φ, as the quotient of Σ k, F k identifying ⟨k, x⟩ with ⟨k+1, φ k x⟩.

Equations

• FirstOrder.Language.DirectedColim F φ = Quot fun (a b : (k : ℕ) × F k) => b = ⟨a.fst + 1, φ a.fst a.snd⟩

def FirstOrder.Language.DirectedColim.incl {F : ℕ → Type} {φ : (k : ℕ) → F k → F (k + 1)} (k : ℕ) (x : F k) : DirectedColim F φ

The canonical inclusion of stage k into the colimit.

Equations

• FirstOrder.Language.DirectedColim.incl k x = Quot.mk (fun (a b : (k : ℕ) × F k) => b = ⟨a.fst + 1, φ a.fst a.snd⟩) ⟨k, x⟩

theorem FirstOrder.Language.DirectedColim.incl_step {F : ℕ → Type} {φ : (k : ℕ) → F k → F (k + 1)} (k : ℕ) (x : F k) : incl (k + 1) (φ k x) = incl k x

Inclusions commute with the tower maps: a stage-k element and its image at stage k+1 have the same colimit class.