refactor equivariance namespaces

1 files changed, 9 insertions, 9 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]