From 71a6a3d5b6f4b428b463bc4a0766c91d8c1d5768 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Wed, 3 Dec 2025 20:34:41 +0100
Subject: refactor equivariant props to use type classes

---
 Nominal/Category.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Nominal/Category.lean')

diff --git a/Nominal/Category.lean b/Nominal/Category.lean
index 721dfb0..343c40c 100644
--- a/Nominal/Category.lean
+++ b/Nominal/Category.lean
@@ -69,7 +69,7 @@ instance : HasForget₂ (Nom 𝔸) (Action Type (FPerm 𝔸)) where
       map f := ⟨f.toFun, by
         intro π
         ext x
-        simp only [EquivariantMap.toFun_eq_coe, types_comp_apply, Action.ofMulAction_apply]
-        apply f.equivariant⟩ }
+        simp only [types_comp_apply, Action.ofMulAction_apply]
+        rw [Function.equivariant 𝔸 f.toFun]⟩ }
 
 end Forget
-- 
cgit v1.3.1