From 4ddf204ae884c543280df9b1ccf30865a5cfdc9e Mon Sep 17 00:00:00 2001
From: pingu <nor@acorneroftheweb.com>
Date: Thu, 25 Dec 2025 23:09:33 +0100
Subject: [PATCH] Todos

---
 mambo.agda | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/mambo.agda b/mambo.agda
index 5fbdabe..e0632ca 100644
--- a/mambo.agda
+++ b/mambo.agda
@@ -145,3 +145,12 @@ ExampleSyn2 {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)))))))
+
+ExampleSyn4 : [] / [] ⊢ □ (A ⇒ B) ⇒ (◇ A ⇒ ◇ B)
+ExampleSyn4 {A} {B} = {!!}
+
+Soundness : {W : Type} → (p : Formula) → [] / [] ⊢ p → (∀ (m : M W) (x : W) → m , x ⊩ p)
+Soundness p x m w = {!!}
+
+Completeness : {W : Type} → (p : Formula) → (∀ (m : M W) (x : W) → m , x ⊩ p) → [] / [] ⊢ p
+Completeness p x = {!!}