From 45b888cc73060a2e6d8a3d94c4f31cd47c6434a0 Mon Sep 17 00:00:00 2001
From: pingu <nor@acorneroftheweb.com>
Date: Thu, 25 Dec 2025 13:58:52 +0100
Subject: [PATCH] It kinda works :D

---
 mambo.agda | 63 ++++++++++++++++++++++++++++++++----------------------
 1 file changed, 38 insertions(+), 25 deletions(-)

diff --git a/mambo.agda b/mambo.agda
index 1cd9f14..0f24222 100644
--- a/mambo.agda
+++ b/mambo.agda
@@ -36,9 +36,10 @@ data Formula : Type where
   _⇒_ : Formula → Formula → Formula
 
 infixr 4 _⇒_
+infix 19 _∧_
 
 variable
-  X Y Z : Formula
+  A B C X Y Z : Formula
 
 _⇔_ : Formula → Formula → Formula
 X ⇔ Y = (X ⇒ Y) ∧ (Y ⇒ X)
@@ -83,12 +84,12 @@ ExampleModel .M.L 1 = 1 ∷ 2 ∷ []
 ExampleModel .M.L 2 = 0 ∷ 2 ∷ []
 ExampleModel .M.L _ = []
 
-Example : ExampleModel , 0 ⊩ □ (atom 2)
-Example y zeroone = succ 2 (2 ∷ []) (zero 2 [])
-Example 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 [])
 
-Example2 : ExampleModel , 0 ⊩ ◇ (atom 1)
-Example2 = pair 1 (λ _ → zero 1 (2 ∷ []))
+Example2Sem : ExampleModel , 0 ⊩ ◇ (atom 1)
+Example2Sem = pair 1 (λ _ → zero 1 (2 ∷ []))
 
 Context : Type
 Context = List Formula
@@ -104,23 +105,35 @@ _++_ : {A : Type} → List A → List A → List A
 [] ++ ys = ys
 (xs , x) ++ ys = xs ++ (x ∷ ys)
 
-boxed : Context → Context
-boxed [] = []
-boxed (xs , x) =  boxed xs , □ x
-
-infixr 2 _⊢_
-data _⊢_ : Context → Formula → Type where
-  var : X ∈ Γ → Γ ⊢ X
-  ∧ᵢ : Γ ⊢ X → Γ ⊢ Y → Γ ⊢ X ∧ Y
-  ∧ₑ₁ : Γ ⊢ X ∧ Y → Γ ⊢ X
-  ∧ₑ₂ : Γ ⊢ X ∧ Y → Γ ⊢ Y
-  ∨ᵢ₁ : Γ ⊢ X → Γ ⊢ X ∨ Y
-  ∨ᵢ₂ : Γ ⊢ Y → Γ ⊢ X ∨ Y
-  ∨ₑ : Γ ⊢ X ∨ Y → Γ , X ⊢ Z → Γ , Y ⊢ Z → Γ ⊢ Z
-  mp : Γ ⊢ X ⇒ Y → Γ ⊢ X → Γ ⊢ Y
-  ⇒ᵢ : Γ , X ⊢ Y → Γ ⊢ X ⇒ Y
-  ¬ᵢ : Γ , X ⊢ ⊥ → Γ ⊢ ∼ X
-  ¬ₑ : Γ ⊢ X → Γ ⊢ ∼ X → Γ ⊢ ⊥
-  □ₑ : Γ ⊢ □ X → X ∈ Δ → Γ ++ boxed Δ ⊢ Y
-  □ᵢ : X ∈ Δ → Γ ++ boxed Δ ⊢ □ X
+infixr 2 _/_⊢_
+data _/_⊢_ (Δ Γ : Context) : Formula → Type where
+  var : X ∈ Γ → Δ / Γ ⊢ X
+  mp : Δ / Γ ⊢ X ⇒ Y → Δ / Γ ⊢ X → Δ / Γ ⊢ Y
+  ∧ᵢ : Δ / Γ ⊢ X → Δ / Γ ⊢ Y → Δ / Γ ⊢ X ∧ Y
+  ∧ₑ₁ : Δ / Γ ⊢ X ∧ Y → Δ / Γ ⊢ X
+  ∧ₑ₂ : Δ / Γ ⊢ X ∧ Y → Δ / Γ ⊢ Y
+  ∨ᵢ₁ : Δ / Γ ⊢ X → Δ / Γ ⊢ X ∨ Y
+  ∨ᵢ₂ : Δ / Γ ⊢ Y → Δ / Γ ⊢ X ∨ Y
+  ∨ₑ : Δ / Γ ⊢ X ∨ Y → Δ / Γ , X ⊢ Z → Δ / Γ , Y ⊢ Z → Δ / Γ ⊢ Z
+  ⇒ᵢ : Δ / Γ , X ⊢ Y → Δ / Γ ⊢ X ⇒ Y
+  ¬ᵢ : Δ / Γ , X ⊢ ⊥ → Δ / Γ ⊢ ∼ X
+  ¬ₑ : Δ / Γ ⊢ X → Δ / Γ ⊢ ∼ X → Δ / Γ ⊢ ⊥
+  □ᵢ : [] / Δ ⊢ X → Δ / Γ ⊢ □ X
+  □ₑ : Δ / Γ ⊢ □ X → (Δ , X) / Γ ⊢ Y → Δ / Γ ⊢ Y
   -- TODO: Maybe make it KT45
+
+K : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y)
+K {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y)))))
+                      (□ₑ (var (succ (□(X ⇒ Y)) ([] , (□ (X ⇒ Y))) (zero (□ (X ⇒ Y)) [])))
+                      (□ᵢ (mp
+                        (var (zero (X ⇒ Y) ([] , X)))
+                        (var (succ X ([] , X) (zero X []))))))))
+
+ExampleSyn : [] / [] ⊢ □ X ⇒ □ (Y ⇒ X)
+ExampleSyn {X} {Y} = ⇒ᵢ (□ₑ (var (zero (□ X) [])) (□ᵢ (⇒ᵢ (var (succ X ([] , X) (zero X []))))))
+
+ExampleSyn2 : [] / [] ⊢ □(A ∧ B) ⇒ (□ A ∧ □ B)
+ExampleSyn2 {A} {B} = ⇒ᵢ (∧ᵢ (□ₑ (var (zero (□ (A ∧ B)) [])) (□ᵢ (∧ₑ₁ (var (zero (A ∧ B) []))))) (□ₑ (var (zero (□ (A ∧ B)) [])) (□ᵢ (∧ₑ₂ (var (zero (A ∧ B) []))))))
+
+ExampleSyn3 : [] / [] ⊢ (□ A ∧ □ B) ⇒ □(A ∧ B)
+ExampleSyn3 {A} {B} = ⇒ᵢ (□ₑ (∧ₑ₁ (var (zero ((□ A) ∧ (□ B)) []))) (□ₑ (∧ₑ₂ (var (zero ((□ A) ∧ (□ B)) []))) (□ᵢ (∧ᵢ (var (succ A ([] , A) (zero A []))) (var (zero B ([] , A)))))))