pingu/mambo
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Tehee

Browse Source
This commit is contained in:
pingu
2025-12-30 09:27:37 +01:00
parent e1212b208c
commit e3ad9763c3
1 changed files with 10 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

17
mambo.agda
View File

@@ -214,8 +214,8 @@ weak-modal (⊥ₑ x) x₁ = ⊥ₑ (weak-modal x x₁)
weak-modal (□ᵢ x) x₁ = □ᵢ (weak x x₁) weak-modal (□ᵢ x) x₁ = □ᵢ (weak x x₁)
weak-modal (□ₑ x x₂) x₁ = □ₑ (weak-modal x x₁) (weak-modal x₂ (inBoth x₁)) weak-modal (□ₑ x x₂) x₁ = □ₑ (weak-modal x x₁) (weak-modal x₂ (inBoth x₁))
cut : Δ / Γ ⊢ A → Δ / Γ' ++ (Γ , A) ⊢ B → Δ / Γ' ++ Γ ⊢ B cut : (Γ' : Context) → Δ / Γ ⊢ A → Δ / Γ' ++ (Γ , A) ⊢ B → Δ / Γ' ++ Γ ⊢ B
cut = {!!} cut Γ' x x₁ = {!!}
cut-modal : Δ / Γ ⊢ A → Δ' ++ (Δ , A) / Γ ⊢ B → Δ' ++ Δ / Γ ⊢ B cut-modal : Δ / Γ ⊢ A → Δ' ++ (Δ , A) / Γ ⊢ B → Δ' ++ Δ / Γ ⊢ B
cut-modal = {!!} cut-modal = {!!}
@@ -232,13 +232,16 @@ MTSym {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (¬ₑ (var (succ (∼ B) ([] , (A ⇒ B)
DedSym : Δ / Γ ⊢ A ⇒ 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} (var x) = mp (var (succ (A ⇒ B) Γ x)) (var (zero A Γ))
DedSym {Δ} {Γ} {A} {B} (mp 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) = {!!} DedSym {Δ} {Γ} {A} {B} (∧ₑ₁ x) = mp (weak (∧ₑ₁ x) (λ {X} → succ X Γ)) (var (zero A Γ))
DedSym {Δ} {Γ} {A} {B} (∧ₑ₂ x) = {!!} DedSym {Δ} {Γ} {A} {B} (∧ₑ₂ x) = mp (weak (∧ₑ₂ x) (λ {X = X₁} → succ X₁ Γ)) (var (zero A Γ))
DedSym {Δ} {Γ} {A} {B} (∨ₑ x x₁ x₂) = {!!} 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) = x
DedSym {Δ} {Γ} {A} {B} (⊥ₑ x) = weak (⊥ₑ x) λ {X} → succ 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 ⇒ X)
ExampleSyn {X} {Y} = ⇒ᵢ (□ₑ (var (zero (□ X) [])) (□ᵢ (⇒ᵢ (var (succ X ([] , X) (zero X [])))))) ExampleSyn {X} {Y} = ⇒ᵢ (□ₑ (var (zero (□ X) [])) (□ᵢ (⇒ᵢ (var (succ X ([] , X) (zero X []))))))