diff options
Diffstat (limited to 'Nominal/Category.lean')
| -rw-r--r-- | Nominal/Category.lean | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Nominal/Category.lean b/Nominal/Category.lean index 29a0b73..721dfb0 100644 --- a/Nominal/Category.lean +++ b/Nominal/Category.lean @@ -66,6 +66,10 @@ instance : ConcreteCategory (Nom 𝔸) (· →ₑ[𝔸] ·) where instance : HasForget₂ (Nom 𝔸) (Action Type (FPerm 𝔸)) where forget₂ := { obj X := Action.ofMulAction (FPerm 𝔸) X.carrier - map f := ⟨f.toFun, by intro π; ext x; simp; apply f.equivariant⟩ } + map f := ⟨f.toFun, by + intro π + ext x + simp only [EquivariantMap.toFun_eq_coe, types_comp_apply, Action.ofMulAction_apply] + apply f.equivariant⟩ } end Forget |