import Mathlib
import Nominal.Support
import Nominal.Equivariance

/-!
# Nominal Set Category

Nominal sets form a category, where the morphisms are exactly equivariant functions between them.
This file contains formalizations for this category-theoretical view.
-/

variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]

open CategoryTheory

/-!
## Category Definition

Definition of the Nom category instance.
-/
section Definition

/-- An object in the category of nominal sets; i.e., a nominal set. -/
structure Nom where
  /-- The underlying set. -/
  carrier : Type
  /-- Nominal set instance. -/
  [nom : NominalSet 𝔸 carrier]

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⟩

/-- A morphism in the category of nominal sets; i.e., an equivariant function. -/
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 : Category (Nom 𝔸) where
  Hom := Nom.Hom 𝔸
  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 f := ⟨f.toFun, by
        intro π
        ext x
        simp only [types_comp_apply, Action.ofMulAction_apply]
        rw [Function.equivariant 𝔸 f.toFun]⟩ }

end Forget