Exercise 3.23 (Scott 1981, PRG-19, §3) — the category of domains is cartesian

closed

Exercise 3.23 asks (for category theorists) to read off from Theorems 3.11 and 3.12 that the category of domains and approximable mappings is cartesian closed, to identify its terminal object, and to say what sort of functor (𝒟₀ → 𝒟₁) is.

The three ingredients are already in the development; this file packages them and supplies the missing terminal object:

• Terminal object. The one-point domain 𝟙 = unitSys (Exercise 3.15) is terminal: there is a unique approximable mapping 𝒟 → 𝟙 (Unique (ApproximableMap V unitSys)), because |𝟙| is a subsingleton.
• Finite products. prod with proj₀, proj₁ is the categorical product (Exercise 3.20).
• Exponentials. curryEquiv (Theorem 3.12) is the natural adjunction Hom(𝒟₀ × 𝒟₁, 𝒟₂) ≃o Hom(𝒟₀, (𝒟₁ → 𝒟₂)), exhibiting (𝒟₁ → 𝒟₂) as the exponential 𝒟₂^𝒟₁.

So 𝟙, ×, and → make the category cartesian closed, and (𝒟₀ → -) is a (covariant) functor right adjoint to - × 𝒟₀. Everything is choice-free (#print axioms ⊆ {propext, Quot.sound}).

The terminal domain.

instance Domain.Neighborhood.instSubsingletonApproximableMapUnitUnitSys {α : Type u_1} (V : NeighborhoodSystem α) : Subsingleton (ApproximableMap V unitSys)

There is at most one approximable mapping into the terminal domain 𝟙: the codomain |𝟙| is a subsingleton, so any two maps have the same elementwise action.

@[implicit_reducible]

instance Domain.Neighborhood.instUniqueApproximableMapUnitUnitSys {α : Type u_1} (V : NeighborhoodSystem α) : Unique (ApproximableMap V unitSys)

Exercise 3.23 (Scott 1981, PRG-19). 𝟙 = unitSys is the terminal object: for every domain 𝒟 there is a unique approximable mapping 𝒟 → 𝟙 (the constant map at ⊥).

Equations

• Domain.Neighborhood.instUniqueApproximableMapUnitUnitSys V = { default := Domain.Neighborhood.constMap V default, uniq := ⋯ }

def Domain.Neighborhood.toUnit {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap V unitSys

Exercise 3.23 (Scott 1981, PRG-19). The unique map to the terminal object, named.

Equations

• Domain.Neighborhood.toUnit V = default

theorem Domain.Neighborhood.toUnit_unique {α : Type u_1} (V : NeighborhoodSystem α) (f : ApproximableMap V unitSys) : f = toUnit V

The exponential adjunction (cartesian closure).

def Domain.Neighborhood.homAdjunction {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap (prod V₀ V₁) V₂ ≃o ApproximableMap V₀ (funSpace V₁ V₂)

Exercise 3.23 (Scott 1981, PRG-19). The cartesian-closed adjunction Hom(𝒟₀ × 𝒟₁, 𝒟₂) ≃o Hom(𝒟₀, (𝒟₁ → 𝒟₂)), exhibiting (𝒟₁ → 𝒟₂) as the exponential object. This is exactly curryEquiv of Theorem 3.12.

Equations

• Domain.Neighborhood.homAdjunction V₀ V₁ V₂ = Domain.Neighborhood.curryEquiv V₀ V₁ V₂