Domains for the monotonicity calculus

This file interprets the marked types of the [IMT17] monotonicity calculus as preordered domains: base types by a given assignment, +-arrows as the monotone maps (→o), −-arrows as the antitone maps (·ᵒᵈ →o ·), unmarked arrows as all maps, each with the pointwise order. Each subtyping σ ≤ τ is interpreted as an order-preserving coercion, functorial in ≤.

Main declarations

• Ty.Dom: the domain interpretation of a marked type.
• Ty.castLE: the coercion along subtyping — the identity on base types, conjugation by the inner coercions on arrows.
• Ty.castLE_rfl, Ty.castLE_castLE: the functor laws ([IMT17] Definition 3.5's coherence conditions).

References

• [IMT17] — Definitions 3.5–3.6.

@[instance_reducible]

instance NaturalLogic.instPreorderα_linglib (D : CategoryTheory.Bundled Preorder) : Preorder ↑D

Equations

• NaturalLogic.instPreorderα_linglib D = D.str

def NaturalLogic.Ty.Dom {B : Type u_1} (Db : B → CategoryTheory.Bundled Preorder) : Ty B → CategoryTheory.Bundled Preorder

Interpret each marked type as a preordered domain over the base assignment Db ([IMT17] Definition 3.6): +-arrows as the monotone maps, −-arrows as the antitone maps, unmarked arrows as all maps, ordered pointwise.

Equations

• NaturalLogic.Ty.Dom Db (NaturalLogic.Ty.base b) = Db b
• NaturalLogic.Ty.Dom Db (σ.arr SignType.pos τ) = CategoryTheory.Bundled.of (↑(NaturalLogic.Ty.Dom Db σ) →o ↑(NaturalLogic.Ty.Dom Db τ))
• NaturalLogic.Ty.Dom Db (σ.arr SignType.neg τ) = CategoryTheory.Bundled.of ((↑(NaturalLogic.Ty.Dom Db σ))ᵒᵈ →o ↑(NaturalLogic.Ty.Dom Db τ))
• NaturalLogic.Ty.Dom Db (σ.arr SignType.zero τ) = CategoryTheory.Bundled.of (↑(NaturalLogic.Ty.Dom Db σ) → ↑(NaturalLogic.Ty.Dom Db τ))

@[irreducible]

def NaturalLogic.Ty.castLE {B : Type u_1} {Db : B → CategoryTheory.Bundled Preorder} {σ τ : Ty B} : σ ≤ τ → ↑(Dom Db σ) →o ↑(Dom Db τ)

The coercion along subtyping ([IMT17] Definition 3.5): the identity on base types; on arrows, conjugation by the inner coercions, forgetting the order-behaviour where the marking weakens to ·.

Equations

• One or more equations did not get rendered due to their size.
• NaturalLogic.Ty.castLE h_2 = OrderHom.id
• NaturalLogic.Ty.castLE h = absurd h ⋯
• NaturalLogic.Ty.castLE h = absurd h ⋯
• NaturalLogic.Ty.castLE h = absurd ⋯ NaturalLogic.Ty.castLE._proof_5
• NaturalLogic.Ty.castLE h = absurd ⋯ NaturalLogic.Ty.castLE._proof_6
• NaturalLogic.Ty.castLE h = absurd ⋯ NaturalLogic.Ty.castLE._proof_7
• NaturalLogic.Ty.castLE h = absurd ⋯ NaturalLogic.Ty.castLE._proof_8

Application lemmas

@[simp]

theorem NaturalLogic.Ty.castLE_base {B : Type u_1} {Db : B → CategoryTheory.Bundled Preorder} {b : B} (h : base b ≤ base b) : castLE h = OrderHom.id

@[simp]

theorem NaturalLogic.Ty.castLE_one_one {B : Type u_1} {Db : B → CategoryTheory.Bundled Preorder} {σ₁ σ₂ τ₁ τ₂ : Ty B} (h : σ₁.arr 1 τ₁ ≤ σ₂.arr 1 τ₂) (k : ↑(Dom Db σ₁) →o ↑(Dom Db τ₁)) : (castLE h) k = (castLE ⋯).comp (k.comp (castLE ⋯))

@[simp]

theorem NaturalLogic.Ty.castLE_neg_one_neg_one {B : Type u_1} {Db : B → CategoryTheory.Bundled Preorder} {σ₁ σ₂ τ₁ τ₂ : Ty B} (h : σ₁.arr (-1) τ₁ ≤ σ₂.arr (-1) τ₂) (k : (↑(Dom Db σ₁))ᵒᵈ →o ↑(Dom Db τ₁)) : (castLE h) k = (castLE ⋯).comp (k.comp (OrderHom.dual (castLE ⋯)))

@[simp]

theorem NaturalLogic.Ty.castLE_one_zero {B : Type u_1} {Db : B → CategoryTheory.Bundled Preorder} {σ₁ σ₂ τ₁ τ₂ : Ty B} (h : σ₁.arr 1 τ₁ ≤ σ₂.arr 0 τ₂) (k : ↑(Dom Db σ₁) →o ↑(Dom Db τ₁)) (a : ↑(Dom Db σ₂)) : (castLE h) k a = (castLE ⋯) (k ((castLE ⋯) a))

@[simp]

theorem NaturalLogic.Ty.castLE_neg_one_zero {B : Type u_1} {Db : B → CategoryTheory.Bundled Preorder} {σ₁ σ₂ τ₁ τ₂ : Ty B} (h : σ₁.arr (-1) τ₁ ≤ σ₂.arr 0 τ₂) (k : (↑(Dom Db σ₁))ᵒᵈ →o ↑(Dom Db τ₁)) (a : ↑(Dom Db σ₂)) : (castLE h) k a = (castLE ⋯) (k (OrderDual.toDual ((castLE ⋯) a)))

@[simp]

theorem NaturalLogic.Ty.castLE_zero_zero {B : Type u_1} {Db : B → CategoryTheory.Bundled Preorder} {σ₁ σ₂ τ₁ τ₂ : Ty B} (h : σ₁.arr 0 τ₁ ≤ σ₂.arr 0 τ₂) (k : ↑(Dom Db σ₁) → ↑(Dom Db τ₁)) (a : ↑(Dom Db σ₂)) : (castLE h) k a = (castLE ⋯) (k ((castLE ⋯) a))

Functor laws

@[simp]

theorem NaturalLogic.Ty.castLE_rfl {B : Type u_1} {Db : B → CategoryTheory.Bundled Preorder} (σ : Ty B) : castLE ⋯ = OrderHom.id

The coercion along le_refl is the identity.

theorem NaturalLogic.Ty.castLE_castLE {B : Type u_1} {Db : B → CategoryTheory.Bundled Preorder} {σ τ μ : Ty B} (h₁ : σ ≤ τ) (h₂ : τ ≤ μ) (a : ↑(Dom Db σ)) : (castLE h₂) ((castLE h₁) a) = (castLE ⋯) a

The coercions compose: casting along h₁ then h₂ is casting along h₁.trans h₂.