From e3ad9763c3c14fc6eda06e86a44a22186abb0aa4 Mon Sep 17 00:00:00 2001
From: pingu <nor@acorneroftheweb.com>
Date: Tue, 30 Dec 2025 09:27:37 +0100
Subject: [PATCH] Tehee

---
 mambo.agda | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/mambo.agda b/mambo.agda
index ffa3fbb..1c3d7d6 100644
--- a/mambo.agda
+++ b/mambo.agda
@@ -214,8 +214,8 @@ weak-modal (⊥ₑ x) x₁ = ⊥ₑ (weak-modal x x₁)
 weak-modal (□ᵢ x) x₁ = □ᵢ (weak x x₁)
 weak-modal (□ₑ x x₂) x₁ = □ₑ (weak-modal x x₁) (weak-modal x₂ (inBoth x₁))
 
-cut : Δ / Γ ⊢ A → Δ / Γ' ++ (Γ , A) ⊢ B → Δ / Γ' ++ Γ ⊢ B
-cut = {!!}
+cut : (Γ' : Context) → Δ / Γ ⊢ A → Δ / Γ' ++ (Γ , A) ⊢ B → Δ / Γ' ++ Γ ⊢ B
+cut Γ' x x₁ = {!!}
 
 cut-modal : Δ / Γ ⊢ A → Δ' ++ (Δ , A) / Γ ⊢ B → Δ' ++ Δ / Γ ⊢ B
 cut-modal = {!!}
@@ -232,13 +232,16 @@ MTSym {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (¬ₑ (var (succ (∼ B) ([] , (A ⇒ B)
 
 DedSym : Δ / Γ ⊢ A ⇒ B → Δ / Γ , A ⊢ B
 DedSym {Δ} {Γ} {A} {B} (var x) = mp (var (succ (A ⇒ B) Γ x)) (var (zero A Γ))
-DedSym {Δ} {Γ} {A} {B} (mp x x₁) = {!!}
-DedSym {Δ} {Γ} {A} {B} (∧ₑ₁ x) = {!!}
-DedSym {Δ} {Γ} {A} {B} (∧ₑ₂ x) = {!!}
-DedSym {Δ} {Γ} {A} {B} (∨ₑ x x₁ x₂) = {!!}
+DedSym {Δ} {Γ} {A} {B} (mp x x₁) = mp (mp (weak x λ {X = X₁} → succ X₁ Γ) (weak x₁ (λ {X = X₁} → succ X₁ Γ))) (var (zero A Γ))
+DedSym {Δ} {Γ} {A} {B} (∧ₑ₁ x) = mp (weak (∧ₑ₁ x) (λ {X} → succ X Γ)) (var (zero A Γ))
+DedSym {Δ} {Γ} {A} {B} (∧ₑ₂ x) = mp (weak (∧ₑ₂ x) (λ {X = X₁} → succ X₁ Γ)) (var (zero A Γ))
+DedSym {Δ} {Γ} {A} {B} (∨ₑ x x₁ x₂) = mp (weak (∨ₑ x x₁ x₂) λ {X = X₁} → succ X₁ Γ) (var (zero A Γ))
 DedSym {Δ} {Γ} {A} {B} (⇒ᵢ x) = x
 DedSym {Δ} {Γ} {A} {B} (⊥ₑ x) = weak (⊥ₑ x) λ {X} → succ X Γ
-DedSym {Δ} {Γ} {A} {B} (□ₑ x x₁) = {!!}
+DedSym {Δ} {Γ} {A} {B} (□ₑ x x₁) = mp (weak (□ₑ x x₁) (λ {X = X₁} → succ X₁ Γ)) (var (zero A Γ))
+
+DedSymInv : Δ / Γ , A ⊢ B → Δ / Γ ⊢ A ⇒ B
+DedSymInv {Δ} {Γ} {A} {B} x = ⇒ᵢ x
 
 ExampleSyn : [] / [] ⊢ □ X ⇒ □ (Y ⇒ X)
 ExampleSyn {X} {Y} = ⇒ᵢ (□ₑ (var (zero (□ X) [])) (□ᵢ (⇒ᵢ (var (succ X ([] , X) (zero X []))))))