Exercise 6.18 (Scott 1981, PRG-19, §6) — 𝒟^∞ as an initial algebra

EXERCISE 6.18. With reference back to Exercise 3.16 discuss the construction of 𝒟^∞ as an initial algebra and as a solution to the domain equation 𝒟^∞ ≅ 𝒟 × 𝒟^∞.

Exercise 3.16 already constructs the infinite iterate 𝒟^∞ (iterSys, over ℕ × Δ) and proves the domain-equation half, 𝒟^∞ ≅ 𝒟 × 𝒟^∞ (iter_isomorphic, with the explicit element iso iterProdIso). This module supplies the initial-algebra half.

For a fixed ∅-free domain 𝒟 consider the (product) endofunctor T(X) = 𝒟 × X. The domain equation 𝒟^∞ ≅ T(𝒟^∞) makes 𝒟^∞ a T-algebra, with structure map i : 𝒟 × 𝒟^∞ → 𝒟^∞ the "cons" isomorphism (Exercise 3.16's iterProdIso⁻¹). We prove 𝒟^∞ is the initial T-algebra: for every T-algebra (E, k) there is a unique (strict) homomorphism 𝒟^∞ → E, namely h(⟨x₀,x₁,…⟩) = k(x₀, k(x₁, k(x₂, …))), the least fixed point of λh. k ∘ T(h) ∘ j.

Architecture

The genuine analysis is done at the level of plain approximable maps (over iterSys V, prod V (iterSys V), and a target E), then packaged into the bespoke category StrictDomainObj of ∅-free domains and strict maps (Exercise 6.17), where IsInitial directly expresses Scott's universal property among strict algebras (cf. Theorem 6.14, which is initiality among strict algebras — the product functor grows the token set, so Theorem 6.14's same-carrier colimit tower does not apply, and 𝒟^∞ must be built directly as in Exercise 3.16).

• Existence. descMap = ⋃ₙ hₙ, h₀ = ⊥, hₙ₊₁ = k ∘ T(hₙ) ∘ j. It is strict and satisfies the fixed-point equation descMap = k ∘ T(descMap) ∘ j, hence the homomorphism square descMap ∘ i = k ∘ T(descMap) (since j ∘ i = I).
• Uniqueness. The truncation chain ρₙ : 𝒟^∞ → 𝒟^∞, ρ₀ = ⊥, ρₙ₊₁ = i ∘ T(ρₙ) ∘ j, computes to ρₙ(⟨xᵢ⟩) = ⟨x₀,…,x_{n-1},⊥,⊥,…⟩ (rho_apply) and satisfies ⋃ₙ ρₙ = I (iSupRho_eq_id, the cofinite-Δ structure of iterSys). For any strict homomorphism g, the sequence g ∘ ρₙ is g-independent (the recursion g∘ρₙ₊₁ = k∘T(g∘ρₙ)∘j), so g = ⋃ₙ g∘ρₙ is forced.

Everything is choice-free where it is data.

∅-freeness is preserved by prod and iterSys

theorem Domain.Neighborhood.Exercise618.prod_nonempty {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty) (_h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty) (W : Set (α ⊕ β)) : (prod V₀ V₁).mem W → W.Nonempty

The product of two ∅-free systems is ∅-free.

theorem Domain.Neighborhood.Exercise618.iterSys_nonempty {α : Type u_1} {V : NeighborhoodSystem α} (h : ∀ (X : Set α), V.mem X → X.Nonempty) (W : Set (ℕ × α)) : (iterSys V).mem W → W.Nonempty

The infinite iterate of an ∅-free system is ∅-free (each fibre is a non-empty neighbourhood).

The "cons" description of the Exercise 3.16 isomorphism

theorem Domain.Neighborhood.Exercise618.iterProdIso_apply {α : Type u_1} {V : NeighborhoodSystem α} (z : (iterSys V).Element) : (iterProdIso V) z = pair (component z 0) (ofSeq fun (n : ℕ) => component z (n + 1))

The forward iso reads off head and tail. iterProdIso z = ⟨z₀, ⟨z₁,z₂,…⟩⟩: the first component is the 0-coordinate component z 0, the second is the shifted sequence.

def Domain.Neighborhood.Exercise618.consSeq {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) (b : (iterSys V).Element) : ℕ → V.Element

The "cons" of a head a : |𝒟| and a tail b : |𝒟^∞|, as a sequence ⟨a, b₀, b₁, …⟩.

Equations

• Domain.Neighborhood.Exercise618.consSeq a b i = Nat.casesOn i a fun (k : ℕ) => Domain.Neighborhood.component b k

@[simp]

theorem Domain.Neighborhood.Exercise618.consSeq_zero {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) (b : (iterSys V).Element) : consSeq a b 0 = a

@[simp]

theorem Domain.Neighborhood.Exercise618.consSeq_succ {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) (b : (iterSys V).Element) (k : ℕ) : consSeq a b (k + 1) = component b k

theorem Domain.Neighborhood.Exercise618.iterProdIso_symm_pair {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) (b : (iterSys V).Element) : (iterProdIso V).symm (pair a b) = ofSeq (consSeq a b)

The inverse iso is "cons". iterProdIso⁻¹ ⟨a, b⟩ = ⟨a, b₀, b₁, …⟩.

Bottom-element computations

theorem Domain.Neighborhood.Exercise618.iterBot_eq {α : Type u_1} {V : NeighborhoodSystem α} : (iterSys V).bot = ofSeq fun (x : ℕ) => V.bot

⊥ of 𝒟^∞ is the all-⊥ sequence.

@[simp]

theorem Domain.Neighborhood.Exercise618.component_bot {α : Type u_1} {V : NeighborhoodSystem α} (n : ℕ) : component (iterSys V).bot n = V.bot

The n-th coordinate of ⊥ is ⊥.

theorem Domain.Neighborhood.Exercise618.pair_bot {α : Type u_2} {β : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : pair V₀.bot V₁.bot = (prod V₀ V₁).bot

⊥ of a product is the pair of ⊥s.

The structure isomorphism i, j as approximable maps

def Domain.Neighborhood.Exercise618.jmap {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (iterSys V) (prod V (iterSys V))

j : 𝒟^∞ → 𝒟 × 𝒟^∞, the splitting iso (iterProdIso).

Equations

• Domain.Neighborhood.Exercise618.jmap V = Domain.Neighborhood.ApproximableMap.ofIso (Domain.Neighborhood.iterProdIso V)

def Domain.Neighborhood.Exercise618.imap {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (prod V (iterSys V)) (iterSys V)

i : 𝒟 × 𝒟^∞ → 𝒟^∞, the "cons" iso (iterProdIso⁻¹); the T-algebra structure map.

Equations

• Domain.Neighborhood.Exercise618.imap V = Domain.Neighborhood.ApproximableMap.ofIso (Domain.Neighborhood.iterProdIso V).symm

theorem Domain.Neighborhood.Exercise618.isStrict_imap {α : Type u_1} {V : NeighborhoodSystem α} : Exercise510.IsStrict (imap V)

theorem Domain.Neighborhood.Exercise618.jmap_comp_imap {α : Type u_1} {V : NeighborhoodSystem α} : (jmap V).comp (imap V) = ApproximableMap.idMap (prod V (iterSys V))

j ∘ i = I on 𝒟 × 𝒟^∞.

Monotonicity of the product action

theorem Domain.Neighborhood.Exercise618.prodMap_idMap_mono {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} {f f' : ApproximableMap (iterSys V) E} (h : f ≤ f') : prodMap (ApproximableMap.idMap V) f ≤ prodMap (ApproximableMap.idMap V) f'

T(·) = (id_𝒟 × ·) is monotone.

theorem Domain.Neighborhood.Exercise618.toElementMap_le_of_le {β₀ : Type u_2} {β₁ : Type u_3} {W₀ : NeighborhoodSystem β₀} {W₁ : NeighborhoodSystem β₁} {f g : ApproximableMap W₀ W₁} (h : f ≤ g) (x : W₀.Element) : f.toElementMap x ≤ g.toElementMap x

Approximable maps are monotone in the map argument: f ≤ g ⟹ f(x) ≤ g(x).

The homomorphism operator and the descent chain

def Domain.Neighborhood.Exercise618.descOp {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (f : ApproximableMap (iterSys V) E) : ApproximableMap (iterSys V) E

The homomorphism operator Op(f) = k ∘ T(f) ∘ j.

Equations

• Domain.Neighborhood.Exercise618.descOp k f = k.comp ((Domain.Neighborhood.prodMap (Domain.Neighborhood.ApproximableMap.idMap V) f).comp (Domain.Neighborhood.Exercise618.jmap V))

theorem Domain.Neighborhood.Exercise618.descOp_apply {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (f : ApproximableMap (iterSys V) E) (z : (iterSys V).Element) : (descOp k f).toElementMap z = k.toElementMap (pair (component z 0) (f.toElementMap (ofSeq fun (n : ℕ) => component z (n + 1))))

The defining action of the operator: Op(f)(z) = k(z₀, f(⟨z₁,z₂,…⟩)).

theorem Domain.Neighborhood.Exercise618.descOp_mono {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) {f f' : ApproximableMap (iterSys V) E} (h : f ≤ f') : descOp k f ≤ descOp k f'

def Domain.Neighborhood.Exercise618.descSeq {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) : ℕ → ApproximableMap (iterSys V) E

The descent chain h₀ = ⊥, hₙ₊₁ = Op(hₙ).

Equations

• Domain.Neighborhood.Exercise618.descSeq k 0 = Domain.Neighborhood.constMap (Domain.Neighborhood.iterSys V) E.bot
• Domain.Neighborhood.Exercise618.descSeq k n.succ = Domain.Neighborhood.Exercise618.descOp k (Domain.Neighborhood.Exercise618.descSeq k n)

theorem Domain.Neighborhood.Exercise618.constBot_le {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (f : ApproximableMap (iterSys V) E) : constMap (iterSys V) E.bot ≤ f

The bottom map is below everything.

theorem Domain.Neighborhood.Exercise618.descSeq_mono_succ {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (n : ℕ) : descSeq k n ≤ descSeq k (n + 1)

theorem Domain.Neighborhood.Exercise618.descSeq_mono {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) {n m : ℕ} (h : n ≤ m) : descSeq k n ≤ descSeq k m

theorem Domain.Neighborhood.Exercise618.descSeq_dir {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (i j : ℕ) : ∃ (l : ℕ), (∀ (X : Set (ℕ × α)) (Y : Set γ), (descSeq k i).rel X Y → (descSeq k l).rel X Y) ∧ ∀ (X : Set (ℕ × α)) (Y : Set γ), (descSeq k j).rel X Y → (descSeq k l).rel X Y

def Domain.Neighborhood.Exercise618.descMap {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) : ApproximableMap (iterSys V) E

The descent map h = ⋃ₙ hₙ : 𝒟^∞ → E.

Equations

• Domain.Neighborhood.Exercise618.descMap k = Domain.Neighborhood.ApproximableMap.iSupMap (Domain.Neighborhood.Exercise618.descSeq k) ⋯

theorem Domain.Neighborhood.Exercise618.descMap_toElementMap {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (z : (iterSys V).Element) {Y : Set γ} : ((descMap k).toElementMap z).mem Y ↔ ∃ (n : ℕ), ((descSeq k n).toElementMap z).mem Y

Generic chain helpers

theorem Domain.Neighborhood.Exercise618.chain_le_of_succ {β : Type u_2} {W : NeighborhoodSystem β} {a : ℕ → W.Element} (h : ∀ (n : ℕ), a n ≤ a (n + 1)) {i j : ℕ} (hij : i ≤ j) : a i ≤ a j

A successor-increasing chain is increasing.

theorem Domain.Neighborhood.Exercise618.succChainDir {β : Type u_2} {W : NeighborhoodSystem β} (a : ℕ → W.Element) (h : ∀ (n : ℕ), a n ≤ a (n + 1)) (i j : ℕ) : ∃ (l : ℕ), a i ≤ a l ∧ a j ≤ a l

Directedness of a successor-increasing chain.

theorem Domain.Neighborhood.Exercise618.descSeqEltMono {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (x : (iterSys V).Element) (n : ℕ) : (descSeq k n).toElementMap x ≤ (descSeq k (n + 1)).toElementMap x

The descent chain is increasing element-wise.

theorem Domain.Neighborhood.Exercise618.descMap_eq {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (x : (iterSys V).Element) : (descMap k).toElementMap x = NeighborhoodSystem.iSupDirected (fun (n : ℕ) => (descSeq k n).toElementMap x) ⋯

The descent map as a directed union. h(x) = ⋃ₙ hₙ(x).

def Domain.Neighborhood.Exercise618.kHead {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (a : V.Element) : ApproximableMap E E

The continuity helper k(a, ·) : E → E as an approximable map.

Equations

• Domain.Neighborhood.Exercise618.kHead k a = k.comp (Domain.Neighborhood.paired (Domain.Neighborhood.constMap E a) (Domain.Neighborhood.ApproximableMap.idMap E))

theorem Domain.Neighborhood.Exercise618.kHead_apply {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (a : V.Element) (u : E.Element) : (kHead k a).toElementMap u = k.toElementMap (pair a u)

The fixed-point equation h = k ∘ T(h) ∘ j

theorem Domain.Neighborhood.Exercise618.descMap_fix {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) : descMap k = descOp k (descMap k)

The descent map is a fixed point of Op = k ∘ T(·) ∘ j.

Strictness of the descent map

theorem Domain.Neighborhood.Exercise618.descSeq_strict {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (hk : Exercise510.IsStrict k) (n : ℕ) : Exercise510.IsStrict (descSeq k n)

theorem Domain.Neighborhood.Exercise618.descMap_strict {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (hk : Exercise510.IsStrict k) : Exercise510.IsStrict (descMap k)

The homomorphism square h ∘ i = k ∘ T(h)

theorem Domain.Neighborhood.Exercise618.descMap_comm {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) : (descMap k).comp (imap V) = k.comp (prodMap (ApproximableMap.idMap V) (descMap k))

Existence of the algebra homomorphism. The descent map makes the square commute: descMap ∘ i = k ∘ T(descMap) (using j ∘ i = I and the fixed-point equation).

The truncation chain ρₙ and ⋃ₙ ρₙ = I

The descent chain for the structure map i itself, ρₙ = (descSeq i)ₙ : 𝒟^∞ → 𝒟^∞, truncates a sequence to its first n coordinates. Its supremum is the identity (iSupRho_eq_id), the key fact behind uniqueness: every strict homomorphism is determined on the finite truncations.

theorem Domain.Neighborhood.Exercise618.rho_apply {α : Type u_1} {V : NeighborhoodSystem α} (n : ℕ) (z : (iterSys V).Element) : (descSeq (imap V) n).toElementMap z = ofSeq fun (i : ℕ) => if i < n then component z i else V.bot

The truncation formula ρₙ(⟨x₀,x₁,…⟩) = ⟨x₀,…,x_{n-1},⊥,⊥,…⟩.

theorem Domain.Neighborhood.Exercise618.iSupRho_eq_id {α : Type u_1} {V : NeighborhoodSystem α} : descMap (imap V) = ApproximableMap.idMap (iterSys V)

⋃ₙ ρₙ = I. Every z is the directed union of its truncations: the cofinite-Δ structure of 𝒟^∞ means each neighbourhood of z is already realised by a finite truncation.

Uniqueness of strict homomorphisms

theorem Domain.Neighborhood.Exercise618.gcomp_rho_zero {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (g : ApproximableMap (iterSys V) E) (hg : Exercise510.IsStrict g) : g.comp (descSeq (imap V) 0) = constMap (iterSys V) E.bot

The descent chain for any strict g starts at the constant ⊥: g ∘ ρ₀ = ⊥.

theorem Domain.Neighborhood.Exercise618.gcomp_rho_succ {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) (g : ApproximableMap (iterSys V) E) (hc : g.comp (imap V) = k.comp (prodMap (ApproximableMap.idMap V) g)) (n : ℕ) : g.comp (descSeq (imap V) (n + 1)) = descOp k (g.comp (descSeq (imap V) n))

g-independence step. If g is a homomorphism (g ∘ i = k ∘ T(g)) then g ∘ ρₙ₊₁ = k ∘ T(g ∘ ρₙ) ∘ j = Op_k(g ∘ ρₙ): the composite depends only on g ∘ ρₙ.

theorem Domain.Neighborhood.Exercise618.comm_unique {α : Type u_1} {V : NeighborhoodSystem α} {γ : Type u_2} {E : NeighborhoodSystem γ} (k : ApproximableMap (prod V E) E) {g g' : ApproximableMap (iterSys V) E} (hg : Exercise510.IsStrict g) (hg' : Exercise510.IsStrict g') (hc : g.comp (imap V) = k.comp (prodMap (ApproximableMap.idMap V) g)) (hc' : g'.comp (imap V) = k.comp (prodMap (ApproximableMap.idMap V) g')) : g = g'

Uniqueness. Any two strict homomorphisms g, g' : 𝒟^∞ → E into a T-algebra (E,k) are equal. By g-independence they agree on every truncation (g ∘ ρₙ = g' ∘ ρₙ), and ⋃ₙ ρₙ = I forces g = g'.

The endofunctor T(X) = 𝒟 × X and 𝒟^∞ as its initial algebra

We package the analysis into the bespoke category StrictDomainObj of ∅-free domains and strict maps (Exercise 6.17), exactly the setting in which IsInitial expresses Scott's universal property. The fixed domain 𝒟 is an arbitrary StrictDomainObj.

theorem Domain.Neighborhood.Exercise618.isStrict_prodMap {α : Type u_2} {β : Type u_3} {α' : Type u_4} {β' : Type u_5} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {f₀ : ApproximableMap V₀ V₀'} {f₁ : ApproximableMap V₁ V₁'} (hf₀ : Exercise510.IsStrict f₀) (hf₁ : Exercise510.IsStrict f₁) : Exercise510.IsStrict (prodMap f₀ f₁)

T(f₀ × f₁) is strict when both factors are: (f₀ × f₁)(⊥,⊥) = (f₀ ⊥, f₁ ⊥) = (⊥,⊥).

def Domain.Neighborhood.Exercise618.prodObj (Dom X : StrictDomainObj) : StrictDomainObj

The fixed domain 𝒟 times an object X, again an ∅-free domain.

Equations

• Domain.Neighborhood.Exercise618.prodObj Dom X = { carrier := Dom.carrier ⊕ X.carrier, sys := Domain.Neighborhood.prod Dom.sys X.sys, nonempty := ⋯ }

def Domain.Neighborhood.Exercise618.prodMapHom (Dom : StrictDomainObj) {X Y : StrictDomainObj} (f : Category.Hom X Y) : Category.Hom (prodObj Dom X) (prodObj Dom Y)

The morphism action T(f) = id_𝒟 × f, strict by isStrict_prodMap.

Equations

• Domain.Neighborhood.Exercise618.prodMapHom Dom f = ⟨Domain.Neighborhood.prodMap (Domain.Neighborhood.ApproximableMap.idMap Dom.sys) ↑f, ⋯⟩

def Domain.Neighborhood.Exercise618.prodFunctor (Dom : StrictDomainObj) : Endofunctor StrictDomainObj

The product endofunctor T(X) = 𝒟 × X on ∅-free domains and strict maps, for a fixed domain 𝒟. On objects T(X) = 𝒟 × X; on maps T(f) = id_𝒟 × f.

Equations

• One or more equations did not get rendered due to their size.

def Domain.Neighborhood.Exercise618.iterObj (Dom : StrictDomainObj) : StrictDomainObj

𝒟^∞ (Exercise 3.16's iterSys) as an ∅-free object.

Equations

• Domain.Neighborhood.Exercise618.iterObj Dom = { carrier := ℕ × Dom.carrier, sys := Domain.Neighborhood.iterSys Dom.sys, nonempty := ⋯ }

def Domain.Neighborhood.Exercise618.iterAlg (Dom : StrictDomainObj) : TAlgebra (prodFunctor Dom)

𝒟^∞ as a T-algebra, (𝒟^∞, i) with i : 𝒟 × 𝒟^∞ → 𝒟^∞ the "cons" iso (imap, Exercise 3.16's iterProdIso⁻¹), strict by isStrict_imap.

Equations

• Domain.Neighborhood.Exercise618.iterAlg Dom = { carrier := Domain.Neighborhood.Exercise618.iterObj Dom, str := ⟨Domain.Neighborhood.Exercise618.imap Dom.sys, ⋯⟩ }

def Domain.Neighborhood.Exercise618.descAlgHom (Dom : StrictDomainObj) (B : TAlgebra (prodFunctor Dom)) : AlgHom (iterAlg Dom) B

The descent homomorphism (𝒟^∞, i) → (E, k): the strict map descMap k (existence half), with the homomorphism square supplied by descMap_comm.

Equations

• Domain.Neighborhood.Exercise618.descAlgHom Dom B = { hom := ⟨Domain.Neighborhood.Exercise618.descMap ↑B.str, ⋯⟩, comm := ⋯ }

def Domain.Neighborhood.Exercise618.iterIsInitial (Dom : StrictDomainObj) : IsInitial (iterAlg Dom)

Exercise 6.18 (initial-algebra half) — 𝒟^∞ is the initial T-algebra for T(X) = 𝒟 × X. For every T-algebra (E, k) the descent map h(⟨x₀,x₁,…⟩) = k(x₀, k(x₁, …)) is the unique strict homomorphism 𝒟^∞ → E. Together with Exercise 3.16's 𝒟^∞ ≅ 𝒟 × 𝒟^∞ (the domain-equation half), this exhibits 𝒟^∞ both as the canonical solution of the domain equation and as the initial algebra (determined up to iso by Proposition 6.6).

Equations

• Domain.Neighborhood.Exercise618.iterIsInitial Dom = { desc := Domain.Neighborhood.Exercise618.descAlgHom Dom, uniq := ⋯ }