Exercise 6.19 (Scott 1981, PRG-19, §6) — sum and product on the category of

strict maps

EXERCISE 6.19. For the sake of uniformity restrict attention to systems 𝒟 on sets Δ ⊆ {0,1}*, where Λ ∈ Δ and ∅ ∉ 𝒟, and to the category of strict maps. Define sum and product by 𝒟₀ + 𝒟₁ = {{Λ} ∪ 0Δ₀ ∪ 1Δ₁} ∪ {0X ∣ X ∈ 𝒟₀} ∪ {1Y ∣ Y ∈ 𝒟₁}, 𝒟₀ × 𝒟₁ = {{Λ} ∪ 0X ∪ 1Y ∣ X ∈ 𝒟₀ and Y ∈ 𝒟₁}. Are these correct up to isomorphism? …

This module formalizes Part A of the exercise: Scott's uniform token-level presentations of sum and product over {0,1}* (so that the constructions are genuine endo-operations on a single category, unlike the abstract separated sum 𝒟₀ + 𝒟₁ of Exercise 3.18 over Option (α ⊕ β) or the product 𝒟₀ × 𝒟₁ of Definition 3.1 over α ⊕ β), and the answer to "Are these correct up to isomorphism?" — yes:

• sumTok_iso_sum : sumTok D₀ D₁ h₀ h₁ ≅ᴰ sum D₀ D₁ h₀ h₁, and
• prodTok_iso_prod : prodTok D₀ D₁ ≅ᴰ prod D₀ D₁.

We reuse the single-bit prefix embBit b X = bX of Example 6.2 (so 0X = embBit false X, 1Y = embBit true Y), whose disjointness/intersection algebra (embBit_inter, embBit_inter_ne, embBit_subset, embBit_injective, embBit_nonempty) is exactly what makes the concrete sum a neighbourhood system and drives the isomorphism (a token-level analogue of Example62.bbEquiv, generalised from B to arbitrary ∅-free D₀, D₁).

The functor-algebra closure (all T(X) generated by constants/identity/sum/product are functors, continuous on maps, monotone and continuous on domains) is Part B, deferred.

Everything here is choice-free (#print axioms ⊆ {propext, Quot.sound}).

The concrete sum D₀ + D₁ over {0,1}*

D₀ + D₁ = {{Λ} ∪ 0Δ₀ ∪ 1Δ₁} ∪ {0X ∣ X ∈ 𝒟₀} ∪ {1Y ∣ Y ∈ 𝒟₁}, with Λ = [], 0X = embBit false X, 1Y = embBit true Y.

def Domain.Neighborhood.Exercise619.sumTokMaster (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : Set ExampleB.Str

The master neighbourhood {Λ} ∪ 0Δ₀ ∪ 1Δ₁ of the concrete sum.

Equations

• Domain.Neighborhood.Exercise619.sumTokMaster D₀ D₁ = insert [] (Domain.Neighborhood.Example62.embBit false D₀.master ∪ Domain.Neighborhood.Example62.embBit true D₁.master)

theorem Domain.Neighborhood.Exercise619.nil_mem_sumTokMaster {D₀ D₁ : NeighborhoodSystem ExampleB.Str} : [] ∈ sumTokMaster D₀ D₁

theorem Domain.Neighborhood.Exercise619.embF_subset_sumTokMaster {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} (hX : D₀.mem X) : Example62.embBit false X ⊆ sumTokMaster D₀ D₁

theorem Domain.Neighborhood.Exercise619.embT_subset_sumTokMaster {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {Y : Set ExampleB.Str} (hY : D₁.mem Y) : Example62.embBit true Y ⊆ sumTokMaster D₀ D₁

theorem Domain.Neighborhood.Exercise619.sumTokMaster_inter_embF {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} (hX : D₀.mem X) : sumTokMaster D₀ D₁ ∩ Example62.embBit false X = Example62.embBit false X

theorem Domain.Neighborhood.Exercise619.sumTokMaster_inter_embT {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {Y : Set ExampleB.Str} (hY : D₁.mem Y) : sumTokMaster D₀ D₁ ∩ Example62.embBit true Y = Example62.embBit true Y

theorem Domain.Neighborhood.Exercise619.embF_ne_sumTokMaster {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} : Example62.embBit false X ≠ sumTokMaster D₀ D₁

theorem Domain.Neighborhood.Exercise619.embT_ne_sumTokMaster {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {Y : Set ExampleB.Str} : Example62.embBit true Y ≠ sumTokMaster D₀ D₁

def Domain.Neighborhood.Exercise619.sumTok (D₀ D₁ : NeighborhoodSystem ExampleB.Str) (h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty) (h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty) : NeighborhoodSystem ExampleB.Str

Exercise 6.19 — the concrete sum system 𝒟₀ + 𝒟₁ over {0,1}*. A neighbourhood is the master {Λ} ∪ 0Δ₀ ∪ 1Δ₁, a left copy 0X (X ∈ 𝒟₀), or a right copy 1Y (Y ∈ 𝒟₁). The standing assumption ∅ ∉ 𝒟ᵢ (h₀, h₁) makes the two tagged copies disjoint, so the system is closed under consistent intersection.

Equations

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

theorem Domain.Neighborhood.Exercise619.sumTok_mem_master {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} : (sumTok D₀ D₁ h₀ h₁).mem (sumTokMaster D₀ D₁)

theorem Domain.Neighborhood.Exercise619.sumTok_mem_embF {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {X : Set ExampleB.Str} (hX : D₀.mem X) : (sumTok D₀ D₁ h₀ h₁).mem (Example62.embBit false X)

theorem Domain.Neighborhood.Exercise619.sumTok_mem_embT {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {Y : Set ExampleB.Str} (hY : D₁.mem Y) : (sumTok D₀ D₁ h₀ h₁).mem (Example62.embBit true Y)

theorem Domain.Neighborhood.Exercise619.sumTok_mem_embF_inv {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {W : Set ExampleB.Str} (h : (sumTok D₀ D₁ h₀ h₁).mem (Example62.embBit false W)) : D₀.mem W

theorem Domain.Neighborhood.Exercise619.sumTok_mem_embT_inv {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {W : Set ExampleB.Str} (h : (sumTok D₀ D₁ h₀ h₁).mem (Example62.embBit true W)) : D₁.mem W

theorem Domain.Neighborhood.Exercise619.sumTok_mem_nonempty {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {W : Set ExampleB.Str} (h : (sumTok D₀ D₁ h₀ h₁).mem W) : W.Nonempty

theorem Domain.Neighborhood.Exercise619.sumTok_nonempty {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} (W : Set ExampleB.Str) : (sumTok D₀ D₁ h₀ h₁).mem W → W.Nonempty

The concrete sum is again ∅-free (an object of Scott's category).

Generic inversion lemmas for the abstract separated sum sum D₀ D₁

theorem Domain.Neighborhood.Exercise619.sum_mem_nonempty {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {W : Set (Option (ExampleB.Str ⊕ ExampleB.Str))} (h : (sum D₀ D₁ h₀ h₁).mem W) : W.Nonempty

theorem Domain.Neighborhood.Exercise619.sum_mem_inj₀_inv {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {X : Set ExampleB.Str} (h : (sum D₀ D₁ h₀ h₁).mem (inj₀ X)) : D₀.mem X

theorem Domain.Neighborhood.Exercise619.sum_mem_inj₁_inv {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {Y : Set ExampleB.Str} (h : (sum D₀ D₁ h₀ h₁).mem (inj₁ Y)) : D₁.mem Y

The forward half toSum : |D₀ + D₁|ₜₒₖ → |D₀ + D₁|

def Domain.Neighborhood.Exercise619.toSum {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} (x : (sumTok D₀ D₁ h₀ h₁).Element) : (sum D₀ D₁ h₀ h₁).Element

The forward half of the isomorphism, a token-level analogue of Example62.toBB.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.toSum_mem_inj₀ {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {x : (sumTok D₀ D₁ h₀ h₁).Element} {X : Set ExampleB.Str} (hX : D₀.mem X) : (toSum x).mem (inj₀ X) ↔ x.mem (Example62.embBit false X)

@[simp]

theorem Domain.Neighborhood.Exercise619.toSum_mem_inj₁ {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {x : (sumTok D₀ D₁ h₀ h₁).Element} {Y : Set ExampleB.Str} (hY : D₁.mem Y) : (toSum x).mem (inj₁ Y) ↔ x.mem (Example62.embBit true Y)

The inverse half fromSum : |D₀ + D₁| → |D₀ + D₁|ₜₒₖ

def Domain.Neighborhood.Exercise619.fromSum {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} (s : (sum D₀ D₁ h₀ h₁).Element) : (sumTok D₀ D₁ h₀ h₁).Element

The inverse half of the isomorphism, a token-level analogue of Example62.fromBB.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.fromSum_mem_embF {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {s : (sum D₀ D₁ h₀ h₁).Element} {X : Set ExampleB.Str} (hX : D₀.mem X) : (fromSum s).mem (Example62.embBit false X) ↔ s.mem (inj₀ X)

@[simp]

theorem Domain.Neighborhood.Exercise619.fromSum_mem_embT {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {s : (sum D₀ D₁ h₀ h₁).Element} {Y : Set ExampleB.Str} (hY : D₁.mem Y) : (fromSum s).mem (Example62.embBit true Y) ↔ s.mem (inj₁ Y)

The two halves are mutually inverse, giving the isomorphism.

theorem Domain.Neighborhood.Exercise619.fromSum_toSum {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} (x : (sumTok D₀ D₁ h₀ h₁).Element) : fromSum (toSum x) = x

theorem Domain.Neighborhood.Exercise619.toSum_fromSum {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} (s : (sum D₀ D₁ h₀ h₁).Element) : toSum (fromSum s) = s

def Domain.Neighborhood.Exercise619.sumTokEquiv {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} : (sumTok D₀ D₁ h₀ h₁).Element ≃o (sum D₀ D₁ h₀ h₁).Element

Exercise 6.19 — the concrete sum is correct up to isomorphism. The order-isomorphism |D₀ + D₁|ₜₒₖ ≃o |D₀ + D₁| between Scott's {0,1}*-presentation and the abstract separated sum.

Equations

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

theorem Domain.Neighborhood.Exercise619.sumTok_iso_sum {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} : sumTok D₀ D₁ h₀ h₁ ≅ᴰ sum D₀ D₁ h₀ h₁

Exercise 6.19 — "Are these correct up to isomorphism?" (sum). Scott's uniform {0,1}*-presentation 𝒟₀ + 𝒟₁ is isomorphic, as a domain, to the abstract separated sum of Exercise 3.18.

The concrete product D₀ × D₁ over {0,1}*

D₀ × D₁ = {{Λ} ∪ 0X ∪ 1Y ∣ X ∈ 𝒟₀ and Y ∈ 𝒟₁}. Every neighbourhood carries both coordinates and the basepoint, in contrast to the sum (where a proper neighbourhood refines exactly one summand).

def Domain.Neighborhood.Exercise619.prodTokNbhd (X Y : Set ExampleB.Str) : Set ExampleB.Str

A product neighbourhood {Λ} ∪ 0X ∪ 1Y over {0,1}*.

Equations

• Domain.Neighborhood.Exercise619.prodTokNbhd X Y = insert [] (Domain.Neighborhood.Example62.embBit false X ∪ Domain.Neighborhood.Example62.embBit true Y)

@[simp]

theorem Domain.Neighborhood.Exercise619.mem_prodTokNbhd_nil {X Y : Set ExampleB.Str} : [] ∈ prodTokNbhd X Y

@[simp]

theorem Domain.Neighborhood.Exercise619.mem_prodTokNbhd_false {X Y : Set ExampleB.Str} {w' : ExampleB.Str} : false :: w' ∈ prodTokNbhd X Y ↔ w' ∈ X

@[simp]

theorem Domain.Neighborhood.Exercise619.mem_prodTokNbhd_true {X Y : Set ExampleB.Str} {w' : ExampleB.Str} : true :: w' ∈ prodTokNbhd X Y ↔ w' ∈ Y

theorem Domain.Neighborhood.Exercise619.prodTokNbhd_master_eq {D₀ D₁ : NeighborhoodSystem ExampleB.Str} : prodTokNbhd D₀.master D₁.master = sumTokMaster D₀ D₁

prodTokNbhd D₀.master D₁.master is exactly the sum master {Λ} ∪ 0Δ₀ ∪ 1Δ₁.

theorem Domain.Neighborhood.Exercise619.prodTokNbhd_inter (X X' Y Y' : Set ExampleB.Str) : prodTokNbhd X Y ∩ prodTokNbhd X' Y' = prodTokNbhd (X ∩ X') (Y ∩ Y')

Scott's (2) for the product: product neighbourhoods intersect componentwise.

theorem Domain.Neighborhood.Exercise619.prodTokNbhd_subset_iff {X X' Y Y' : Set ExampleB.Str} : prodTokNbhd X Y ⊆ prodTokNbhd X' Y' ↔ X ⊆ X' ∧ Y ⊆ Y'

Scott's (1) for the product: inclusion of product neighbourhoods is componentwise.

theorem Domain.Neighborhood.Exercise619.prodTokNbhd_injective {X X' Y Y' : Set ExampleB.Str} (h : prodTokNbhd X Y = prodTokNbhd X' Y') : X = X' ∧ Y = Y'

def Domain.Neighborhood.Exercise619.prodTok (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : NeighborhoodSystem ExampleB.Str

Exercise 6.19 — the concrete product system 𝒟₀ × 𝒟₁ over {0,1}*. Neighbourhoods are {Λ} ∪ 0X ∪ 1Y with X ∈ 𝒟₀, Y ∈ 𝒟₁. Closed under consistent intersection by Scott's (1)/(2) together with the factors' closure.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.prodTok_mem_iff {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {W : Set ExampleB.Str} : (prodTok D₀ D₁).mem W ↔ ∃ (X : Set ExampleB.Str), ∃ (Y : Set ExampleB.Str), D₀.mem X ∧ D₁.mem Y ∧ W = prodTokNbhd X Y

theorem Domain.Neighborhood.Exercise619.prodTok_mem_prodTokNbhd {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X Y : Set ExampleB.Str} (hX : D₀.mem X) (hY : D₁.mem Y) : (prodTok D₀ D₁).mem (prodTokNbhd X Y)

@[simp]

theorem Domain.Neighborhood.Exercise619.prodTok_master {D₀ D₁ : NeighborhoodSystem ExampleB.Str} : (prodTok D₀ D₁).master = prodTokNbhd D₀.master D₁.master

theorem Domain.Neighborhood.Exercise619.prodTok_nonempty {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (W : Set ExampleB.Str) : (prodTok D₀ D₁).mem W → W.Nonempty

The concrete product is again ∅-free (every neighbourhood contains Λ).

Components of a product element and the splitting lemma

def Domain.Neighborhood.Exercise619.fstTok {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (z : (prodTok D₀ D₁).Element) : D₀.Element

Scott's z₀: the first component of a prodTok-element.

Equations

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

def Domain.Neighborhood.Exercise619.sndTok {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (z : (prodTok D₀ D₁).Element) : D₁.Element

Scott's z₁: the second component of a prodTok-element.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise619.mem_fstTok {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {z : (prodTok D₀ D₁).Element} {X : Set ExampleB.Str} : (fstTok z).mem X ↔ D₀.mem X ∧ z.mem (prodTokNbhd X D₁.master)

@[simp]

theorem Domain.Neighborhood.Exercise619.mem_sndTok {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {z : (prodTok D₀ D₁).Element} {Y : Set ExampleB.Str} : (sndTok z).mem Y ↔ D₁.mem Y ∧ z.mem (prodTokNbhd D₀.master Y)

theorem Domain.Neighborhood.Exercise619.prodTok_mem_split {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {z : (prodTok D₀ D₁).Element} {X Y : Set ExampleB.Str} (hX : D₀.mem X) (hY : D₁.mem Y) : z.mem (prodTokNbhd X Y) ↔ z.mem (prodTokNbhd X D₁.master) ∧ z.mem (prodTokNbhd D₀.master Y)

Scott's (3) for the product: membership of X ∪ Y splits into its two slices.

The element pairing and the isomorphism |D₀ × D₁|ₜₒₖ ≃o |D₀| × |D₁|.

def Domain.Neighborhood.Exercise619.pairTok {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (x : D₀.Element) (y : D₁.Element) : (prodTok D₀ D₁).Element

The element pairing ⟨x, y⟩ for the concrete product.

Equations

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

theorem Domain.Neighborhood.Exercise619.mem_pairTok_prodTokNbhd {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {x : D₀.Element} {y : D₁.Element} {X Y : Set ExampleB.Str} : (pairTok x y).mem (prodTokNbhd X Y) ↔ x.mem X ∧ y.mem Y

theorem Domain.Neighborhood.Exercise619.pairTok_fstTok_sndTok {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (z : (prodTok D₀ D₁).Element) : pairTok (fstTok z) (sndTok z) = z

@[simp]

theorem Domain.Neighborhood.Exercise619.fstTok_pairTok {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (x : D₀.Element) (y : D₁.Element) : fstTok (pairTok x y) = x

@[simp]

theorem Domain.Neighborhood.Exercise619.sndTok_pairTok {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (x : D₀.Element) (y : D₁.Element) : sndTok (pairTok x y) = y

def Domain.Neighborhood.Exercise619.prodTokEquiv {D₀ D₁ : NeighborhoodSystem ExampleB.Str} : (prodTok D₀ D₁).Element ≃o D₀.Element × D₁.Element

The order-isomorphism |D₀ × D₁|ₜₒₖ ≃o |D₀| × |D₁| (Scott's Proposition 3.2, token-level).

Equations

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

theorem Domain.Neighborhood.Exercise619.prodTok_iso_prod {D₀ D₁ : NeighborhoodSystem ExampleB.Str} : prodTok D₀ D₁ ≅ᴰ prod D₀ D₁

Exercise 6.19 — "Are these correct up to isomorphism?" (product). Scott's uniform {0,1}*-presentation 𝒟₀ × 𝒟₁ is isomorphic, as a domain, to the abstract product of Definition 3.1. Both compute the same domain |D₀| × |D₁| (via prodTokEquiv and Scott's prodEquiv).