Update Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Co-authored-by: Joël Riou <[email protected]>
leanprover-community · Feb 25, 2025 · d90e5fe · d90e5fe
1 parent 14a1fbd
commit d90e5fe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean b/Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
@@ -77,7 +77,7 @@ theorem nerve₂Adj.counit.naturality {C D : Type u} [SmallCategory C] [SmallCat
     ReflQuiv.adj.counit).naturality _
 
 /-- The counit of `nerve₂Adj.` -/
-def nerve₂Adj.counit : nerveFunctor₂ ⋙ hoFunctor₂.{u} ⟶ (𝟭 Cat) where
+def nerve₂Adj.counit : nerveFunctor₂ ⋙ hoFunctor₂.{u} ⟶ 𝟭 Cat where
   app C := nerve₂Adj.counit.app (Cat.of C)
   naturality _ _ F := nerve₂Adj.counit.naturality F