From f8b2f5190e33f3d1694442a6be32cba97fcef004 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Thu, 23 Oct 2025 23:41:16 +0200 Subject: basic structure for name abstraction --- Nominal/Category.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'Nominal/Category.lean') 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 -- cgit v1.3.1