Sketches for arithmetic universes

STEVEN VICKERS

The article discusses pushouts. Here we construct a version of pushouts by hand.

def pushout {U : Type u_1} {V : Type u_2} {W : Type u_3} (f : U → V) (g : U → W) (hf : Function.Injective f) (hg : Function.Injective g) : Setoid (V ⊕ W)

Equations

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

def ambient⅋ (V : Type u_1) (W : Type u_2) [Zero V] [Zero W] : Setoid (Fin 2 × V ⊕ Fin 2 × W)

A model for the linear logic ⅋ connective. This is only the ambient space though.

Equations

• ambient⅋ V W = pushout (fun (i : Fin 2) => (i, 0)) (fun (i : Fin 2) => (i, 0)) ⋯ ⋯

def ⅋' {V : Type u_1} {W : Type u_2} [Zero V] [Zero W] (𝓐 : Set V) (𝓑 : Set W) : Set (Quotient (ambient⅋ V W))

The ⅋ for propositions A, B.

Equations

• ⅋' 𝓐 𝓑 c = ((∃ (C : Fin 2 × V), c = ⟦Sum.inl C⟧ ∧ 𝓐 C.2) ∨ ∃ (C : Fin 2 × W), c = ⟦Sum.inr C⟧ ∧ 𝓑 C.2)

def opl {V : Type u_1} {W : Type u_2} [Zero V] [Zero W] (𝓐 : Set V) (𝓑 : Set W) : Set (Quotient (ambient⅋ V W))

Equations

• opl 𝓐 𝓑 c = ((∃ (C : Fin 2 × V), c = ⟦Sum.inl C⟧ ∧ 𝓐 C.2 ∧ C.1 = 0) ∨ ∃ (C : Fin 2 × W), c = ⟦Sum.inr C⟧ ∧ 𝓑 C.2 ∧ C.1 = 0)

instance instZeroSubtypeMemSubmodule_marginis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (𝓐 : Submodule 𝕜 E) : Zero ↥𝓐

Equations

• instZeroSubtypeMemSubmodule_marginis 𝓐 = 𝓐.zero

theorem ⅋_of_opl {V : Type u_1} {W : Type u_2} [Zero V] [Zero W] (𝓐 : Set V) (𝓑 : Set W) (C : Quotient (ambient⅋ V W)) : opl 𝓐 𝓑 C → ⅋' 𝓐 𝓑 C

𝓐 ⊕ 𝓑 implies 𝓐 ⅋ 𝓑.