Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Added exchange

  • Loading branch information...
commit c3c10e7110e5493174b58a9c80f1b6c343c8b5a0 1 parent c1bcf08
@leugenea authored
Showing with 9 additions and 1 deletion.
  1. +9 −1 agda/Simply-Typed.agda
View
10 agda/Simply-Typed.agda
@@ -42,4 +42,12 @@ wk θ (y₁ ∙ y₂) = wk θ y₁ ∙ wk θ y₂
wk θ (Λ y) = Λ (wk (⊆cong Refl θ) y)
weaking : {Γ A B} Term Γ B Term (A ∷ Γ) B
-weaking = wk xs⊆x∷xs
+weaking = wk xs⊆x∷xs
+
+x∷y∷s⊆y∷x∷s : {a} {A : Set a} {x y : A} {s : List A} ((x ∷ y ∷ s) ⊆ (y ∷ x ∷ s))
+x∷y∷s⊆y∷x∷s Z = S Z
+x∷y∷s⊆y∷x∷s (S Z) = Z
+x∷y∷s⊆y∷x∷s (S (S n)) = S (S n)
+
+exchange : {Γ A B C} Term (A ∷ B ∷ Γ) C Term (B ∷ A ∷ Γ) C
+exchange = wk x∷y∷s⊆y∷x∷s
Please sign in to comment.
Something went wrong with that request. Please try again.