From 16ba1b2a241f9ffcf6859fecb38e39b95c9b991f Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 16:22:09 -0800
Subject: [PATCH] Correct a typo

---
 Adjunction/Natural/Transformation/Universal.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Adjunction/Natural/Transformation/Universal.v b/Adjunction/Natural/Transformation/Universal.v
index 6a1f7d4b..f8364bab 100644
--- a/Adjunction/Natural/Transformation/Universal.v
+++ b/Adjunction/Natural/Transformation/Universal.v
@@ -18,7 +18,7 @@ Context {U : C ⟶ D}.
 
 Program Definition Adjunction_from_Transform (A : F ∹ U) : F ⊣ U := {|
   adj := fun a b =>
-    {| to   := {| morphism := fun f =>n fmap f ∘ transform[unit[A]] a |}
+    {| to   := {| morphism := fun f => fmap f ∘ transform[unit[A]] a |}
      ; from := {| morphism := fun f => transform[counit[A]] b ∘ fmap f |} |}
 |}.
 Next Obligation. proper; now rewrites. Qed.