From d75abcb4dc8bdc9feb93941f05d2e162abaf0af3 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Thu, 23 Oct 2025 13:24:26 +0200
Subject: add equivariant instances

---
 Nominal/Instances.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'Nominal/Instances.lean')

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
-- 
cgit v1.3.1