diff options
Diffstat (limited to 'Nominal/Category.lean')
| -rw-r--r-- | Nominal/Category.lean | 5 |
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 |