refactor equivariance namespaces

2 files changed, 20 insertions, 20 deletions

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index 943bd43..ba2fbf9 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -60,7 +60,7 @@ private lemma ofPair_surjective : Function.Surjective (ofPair 𝔸 X) := by
   use ⟨x.atom, x.body⟩
   simp [ofPair]
 
-private lemma ofPair_equivariant : Equivariant 𝔸 (ofPair 𝔸 X) := by
+private lemma ofPair_equivariant : Function.Equivariant 𝔸 (ofPair 𝔸 X) := by
   intro x π
   ext <;> simp [ofPair]
 
@@ -69,7 +69,7 @@ instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) :=
 
 @[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by
   have h : NominalSet.supp 𝔸 (ofPair 𝔸 X (x.atom, x.body)) = NominalSet.supp 𝔸 (x.atom, x.body) :=
-    Equivariant.supp_eq_if_inj 𝔸 (ofPair_equivariant 𝔸 X) (ofPair_injective 𝔸 X)
+    Function.Equivariant.supp_eq_if_inj 𝔸 (ofPair_equivariant 𝔸 X) (ofPair_injective 𝔸 X)
   simp only [Prod.supp, NominalSet.supp_atom, ofPair] at h
   rwa [Set.union_comm] at h
 
@@ -105,7 +105,7 @@ private lemma alpha_eq_iff_pred {x y : NameAbstraction' 𝔸 X} : AlphaEq x y =
   apply NominalSet.for_fresh_ext
   simp [AlphaEqPred]
 
-private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by
+private lemma alpha_eq_pred_equivariant : Rel.Equivariant 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by
   intro a x π
   rw [AlphaEqPred, AlphaEqPred]
   intro h
@@ -116,14 +116,14 @@ private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred
 private lemma alpha_eq_iff_exists' {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by
   suffices (∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∃ c, c # (x, y) ∧ AlphaEqPred c (x, y)) by
     rw [alpha_eq_iff_pred, this]
-    apply Equivariance.for_fresh_iff_exists
+    apply Rel.Equivariant.for_fresh_iff_exists
     exact alpha_eq_pred_equivariant
   simp [Prod.fresh, AlphaEqPred, @and_assoc]
 
 private lemma alpha_eq_iff_all' {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by
   suffices (∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∀ c, c # (x, y) → AlphaEqPred c (x, y)) by
     rw [alpha_eq_iff_pred, this]
-    apply Equivariance.for_fresh_iff_all
+    apply Rel.Equivariant.for_fresh_iff_all
     exact alpha_eq_pred_equivariant
   simp [Prod.fresh, AlphaEqPred]
 
@@ -202,7 +202,7 @@ private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y →
   · intro c ⟨hxy, hyz⟩
     rw [hxy, hyz]
 
-private lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by
+private lemma alpha_eq_equivariant : Rel.Equivariant 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by
   intro x y π h
   rw [alpha_eq_iff_exists'] at *
   obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h
@@ -377,11 +377,11 @@ private def map' (f : X →ₑ[𝔸] Y) : NameAbstraction 𝔸 X → NameAbstrac
     exact
       ⟨hcx.left,
        hcy.left,
-       Equivariant.preserve_fresh 𝔸 f.equivariant hcx.right,
-       Equivariant.preserve_fresh 𝔸 f.equivariant hcy.right,
+       Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcx.right,
+       Function.Equivariant.preserve_fresh 𝔸 f.equivariant hcy.right,
        hc'⟩)
 
-private lemma map_equivariant (f : X →ₑ[𝔸] Y) : Equivariant 𝔸 (map' 𝔸 f) := by
+private lemma map_equivariant (f : X →ₑ[𝔸] Y) : Function.Equivariant 𝔸 (map' 𝔸 f) := by
   apply Quotient.ind
   intro x π
   rw [← Quotient.mk_equivariant]
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 2ebe9b1..d41e87f 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -140,11 +140,11 @@ instance : NominalSet 𝔸 (X × Y) where
 lemma supp_comm {x : X} {y : Y} : NominalSet.supp 𝔸 (x, y) = NominalSet.supp 𝔸 (y, x) := by
   simp; apply Set.union_comm
 
-lemma fst_equivariant : Equivariant 𝔸 (Prod.fst : X × Y → X) := by
-  simp [Equivariant]
+lemma fst_equivariant : Function.Equivariant 𝔸 (Prod.fst : X × Y → X) := by
+  simp [Function.Equivariant]
 
-lemma snd_equivariant : Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
-  simp [Equivariant]
+lemma snd_equivariant : Function.Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
+  simp [Function.Equivariant]
 
 end Prod
 
@@ -212,11 +212,11 @@ instance : NominalSet 𝔸 (X ⊕ Y) where
 @[simp] lemma fresh_inr {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by
   simp [NominalSet.IsFresh]
 
-lemma inl_equivariant : Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
-  simp [Equivariant]
+lemma inl_equivariant : Function.Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
+  simp [Function.Equivariant]
 
-lemma inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
-  simp [Equivariant]
+lemma inr_equivariant : Function.Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
+  simp [Function.Equivariant]
 
 end Sum
 
@@ -251,8 +251,8 @@ instance : PermSet 𝔸 (Quotient setoid.toSetoid) where
     apply Quotient.ind
     simp [mul_smul]
 
-lemma mk_equivariant : Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by
-  simp [Equivariant]
+lemma mk_equivariant : Function.Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by
+  simp [Function.Equivariant]
 
 variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X}
 
@@ -265,7 +265,7 @@ lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a |
   · intro ha x' hx'
     rw [← Quotient.sound hx'] at ha
     have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x') ⊆ NominalSet.supp 𝔸 x' :=
-      Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸)
+      Function.Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸)
     exact hsub ha
   · contrapose; intro ha
     simp only [Set.mem_setOf_eq, Classical.not_imp, not_forall]