basic structure for name abstraction

1 files changed, 4 insertions, 1 deletions

diff --git a/Nominal/Category.lean b/Nominal/Category.lean
index 9ee4fe3..29a0b73 100644
--- a/Nominal/Category.lean
+++ b/Nominal/Category.lean
@@ -29,6 +29,9 @@ structure Nom where
 
 attribute [instance] Nom.nom
 
+/-- Construct a nominal set object from a nominal set. -/
+def Nom.of (X : Type) [NominalSet 𝔸 X] : Nom 𝔸 := ⟨X⟩
+
 /-- Objects in Nom can be coerced to the underlying nominal set type. -/
 instance : CoeSort (Nom 𝔸) Type := ⟨Nom.carrier⟩
 
@@ -63,6 +66,6 @@ instance : ConcreteCategory (Nom 𝔸) (· →ₑ[𝔸] ·) where
 instance : HasForget₂ (Nom 𝔸) (Action Type (FPerm 𝔸)) where
   forget₂ :=
     { obj X := Action.ofMulAction (FPerm 𝔸) X.carrier
-      map {X Y} f := ⟨f.toFun, by intro π; ext x; simp; apply f.equivariant⟩ }
+      map f := ⟨f.toFun, by intro π; ext x; simp; apply f.equivariant⟩ }
 
 end Forget