add equivariant instances

1 files changed, 13 insertions, 0 deletions

diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean
index e28fe28..b637b32 100644
--- a/Nominal/Instances.lean
+++ b/Nominal/Instances.lean
@@ -1,5 +1,6 @@
 import Mathlib
 import Nominal.Support
+import Nominal.Equivariance
 
 /-!
 # Instances
@@ -132,6 +133,12 @@ instance : NominalSet 𝔸 (X × Y) where
 lemma NominalSet.supp_product_comm {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 (y, x) := by
   simp; apply Set.union_comm
 
+lemma Prod.fst_equivariant : Equivariant 𝔸 (Prod.fst : X × Y → X) := by
+  simp [Equivariant]
+
+lemma Prod.snd_equivariant : Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
+  simp [Equivariant]
+
 end Products
 
 /-!
@@ -190,4 +197,10 @@ instance : NominalSet 𝔸 (X ⊕ Y) where
 @[simp] lemma NominalSet.fresh_coproduct₂ {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by
   simp [IsFresh]
 
+lemma Sum.inl_equivariant : Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
+  simp [Equivariant]
+
+lemma Sum.inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
+  simp [Equivariant]
+
 end Coproducts