From 1e949cb9ade16c6b7326b448b3a50549c2abcb0e Mon Sep 17 00:00:00 2001 From: pingu Date: Thu, 25 Dec 2025 14:04:20 +0100 Subject: [PATCH] Also have one example of K in it :D --- mambo.agda | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/mambo.agda b/mambo.agda index 0f24222..62c8e19 100644 --- a/mambo.agda +++ b/mambo.agda @@ -84,6 +84,11 @@ ExampleModel .M.L 1 = 1 ∷ 2 ∷ [] ExampleModel .M.L 2 = 0 ∷ 2 ∷ [] ExampleModel .M.L _ = [] + +KSem : ExampleModel , 0 ⊩ □ (atom 1 ⇒ atom 2) ⇒ (□ atom 1 ⇒ □ atom 2) +KSem x x₁ y zeroone = succ 2 (2 ∷ []) (zero 2 []) +KSem x x₁ y zerotwo = succ 2 (2 ∷ []) (zero 2 []) + ExampleSem : ExampleModel , 0 ⊩ □ (atom 2) ExampleSem y zeroone = succ 2 (2 ∷ []) (zero 2 []) ExampleSem y zerotwo = succ 2 (2 ∷ []) (zero 2 []) @@ -122,8 +127,8 @@ data _/_⊢_ (Δ Γ : Context) : Formula → Type where □ₑ : Δ / Γ ⊢ □ X → (Δ , X) / Γ ⊢ Y → Δ / Γ ⊢ Y -- TODO: Maybe make it KT45 -K : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y) -K {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y))))) +KSym : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y) +KSym {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y))))) (□ₑ (var (succ (□(X ⇒ Y)) ([] , (□ (X ⇒ Y))) (zero (□ (X ⇒ Y)) []))) (□ᵢ (mp (var (zero (X ⇒ Y) ([] , X)))