add forgetful functors

1 files changed, 49 insertions, 3 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index c9a5261..ac50519 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -71,11 +71,11 @@ lemma id_equivariant : Equivariant 𝔸 (id : X → X) := by
   simp [Equivariant]
 
 /-- The composition of two equivariant functions is equivariant. -/
-lemma comp_equivariant {f : X → Y} {g : Y → Z} : Equivariant 𝔸 f → Equivariant 𝔸 g → Equivariant 𝔸 (g ∘ f) := by
+lemma comp_equivariant {f : Y → Z} {g : X → Y} : Equivariant 𝔸 f → Equivariant 𝔸 g → Equivariant 𝔸 (f ∘ g) := by
   intro hf hg x π
   calc
-    g (f (π • x)) = g (π • f x)   := by rw [hf]
-    _             = π • (g (f x)) := by rw [hg]
+    f (g (π • x)) = f (π • g x)   := by rw [hg]
+    _             = π • (f (g x)) := by rw [hf]
 
 /-- The subset relation is equivariant. -/
 lemma subset_equivariant : EquivariantRelation 𝔸 (Set.Subset : Set X → Set X → Prop) := by
@@ -183,3 +183,49 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸
       exact hS.out.right
 
 end Nominal
+
+/-!
+## Bundled Functions
+
+In the following, we also define a bundled function type for equivariant functions.
+-/
+section BundledFunction
+
+/-- A function carrying a proof of its equivariance. -/
+structure EquivariantMap (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] where
+  /-- The underlying function. -/
+  toFun : X → Y
+  /-- Proof of equivariance. -/
+  equivariant : Equivariant 𝔸 toFun
+
+/-- We write `X →ₑ Y` or `X →ₑ[𝔸] Y` for an equivariant map X → Y. -/
+infixr:25 " →ₑ " => EquivariantMap _
+
+/-- We write `X →ₑ Y` or `X →ₑ[𝔸] Y` for an equivariant map X → Y. -/
+notation:25 X " →ₑ[" A "] " Y => EquivariantMap A X Y
+
+variable {X Y Z : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] [PermSet 𝔸 Z]
+
+instance : FunLike (X →ₑ[𝔸] Y) X Y where
+  coe := EquivariantMap.toFun
+  coe_injective' f g h := by cases f; cases g; congr
+
+namespace EquivariantMap
+
+/-- The identity function. -/
+def id : X →ₑ[𝔸] X := ⟨_root_.id, id_equivariant 𝔸⟩
+
+/-- Function composition. -/
+def comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : X →ₑ[𝔸] Z := ⟨f ∘ g, comp_equivariant 𝔸 f.equivariant g.equivariant⟩
+
+@[simp]
+lemma toFun_eq_coe {f : X →ₑ[𝔸] Y} : f.toFun = (f : X → Y) :=
+  rfl
+
+@[ext]
+lemma ext {f g : X →ₑ[𝔸] Y} (h : ∀ a, f a = g a) : f = g :=
+  DFunLike.ext _ _ h
+
+end EquivariantMap
+
+end BundledFunction