Skip to main content

Syntactic Categories

Defining the syntactic category​

semantics/syntacticCat.lean
namespace synCat
  open synPoset

  variable {Form : Type}

  def syn_cat [Der : has_derives Form] : thin_cat (Form _eq)
    := thin_cat.from_preorder synPoset.syn_eq_pre
  instance [Der : has_derives Form] : thin_cat (Form _eq) := syn_cat
semantics/syntacticCat.lean
def syn_obj [Der : has_derives Form] (φ : Form) : Form _eq := Form_eq_in φ
def syn_hom [Der : has_derives Form] : ∀ {φ ψ : Form}, 
      (φ ⊢ ψ) → (syn_obj φ ⟶ syn_obj ψ) :=
  begin
    assume φ ψ h,
    apply hom_of_le,
    exact h,
  end

def derives_of_hom [Der : has_derives Form] {φ ψ : Form} (f : syn_obj φ ⟶ syn_obj ψ): 
      Der.derives (Der.singleHyp.singleton φ) ψ :=
    Exists.fst(thin_cat.preorder_cat_full f)