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 𝔸]

/-!
## 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

/-- 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

/-- Nominal sets form a category with equivariant functions as morphisms. -/
instance : CategoryTheory.Category (Nom 𝔸) where
  Hom := Nom.Hom 𝔸
  id X := ⟨id, id_equivariant 𝔸⟩
  comp f g := ⟨g.toFun ∘ f.toFun, comp_equivariant 𝔸 f.equivariant g.equivariant⟩

end Definition