1 files changed, 33 insertions, 8 deletions
diff --git a/Nominal/Category.lean b/Nominal/Category.lean
index fc7e161..9ee4fe3 100644
--- a/Nominal/Category.lean
+++ b/Nominal/Category.lean
@@ -11,6 +11,8 @@ This file contains formalizations for this category-theoretical view.
 
 variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
+open CategoryTheory
+
 /-!
 ## Category Definition
 
@@ -27,17 +29,40 @@ structure Nom where
 
 attribute [instance] Nom.nom
 
+/-- Objects in Nom can be coerced to the underlying nominal set type. -/
+instance : CoeSort (Nom 𝔸) Type := ⟨Nom.carrier⟩
+
 /-- A morphism in the category of nominal sets; i.e., an equivariant function. -/
-structure Nom.Hom (X Y : Nom 𝔸) where
-  /-- The underlying function. -/
-  toFun : X.carrier → Y.carrier
-  /-- Equivariance of the function. -/
-  equivariant : Equivariant 𝔸 toFun
+def Nom.Hom (X Y : Nom 𝔸) := X →ₑ[𝔸] Y
+
+/-- Coerce morphisms to functions between the underlying sets. -/
+instance (X Y : Nom 𝔸) : CoeFun (Nom.Hom 𝔸 X Y) (fun _ => X.carrier → Y.carrier) where
+  coe f := f.toFun
 
 /-- Nominal sets form a category with equivariant functions as morphisms. -/
-instance : CategoryTheory.Category (Nom 𝔸) where
+instance : Category (Nom 𝔸) where
   Hom := Nom.Hom 𝔸
-  id X := ⟨id, id_equivariant 𝔸⟩
-  comp f g := ⟨g.toFun ∘ f.toFun, comp_equivariant 𝔸 f.equivariant g.equivariant⟩
+  id X := EquivariantMap.id 𝔸
+  comp f g := EquivariantMap.comp 𝔸 g f
 
 end Definition
+
+/-!
+## Forgetful Functors
+
+Definitions of forgetful functors from the Nom category.
+-/
+section Forget
+
+/-- The Nom category is a ConcreteCategory where objects correspond to types. -/
+instance : ConcreteCategory (Nom 𝔸) (· →ₑ[𝔸] ·) where
+  hom := id
+  ofHom := id
+
+/-- There is a forgetful functor from Nom to the category of monoidal actions. -/
+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⟩ }
+
+end Forget