Line length

leanprover-community · Feb 17, 2022 · 0493271 · 0493271
1 parent eed8fbc
commit 0493271
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/src/category_theory/discrete_category.lean b/src/category_theory/discrete_category.lean
@@ -32,7 +32,8 @@ discrete categories.
 
 namespace category_theory
 
-universes v₁ v₂ v₃ u₁ u₂ u₃ -- morphism levels before object levels. See note [category_theory universes].
+-- morphism levels before object levels. See note [category_theory universes].
+universes v₁ v₂ v₃ u₁ u₂ u₃
 
 /--
 A type synonym for promoting any type to a category,

diff --git a/src/category_theory/limits/shapes/biproducts.lean b/src/category_theory/limits/shapes/biproducts.lean
@@ -1249,8 +1249,8 @@ end
 
 /-- In a preadditive category, any binary bicone which is a colimit cocone is in fact a
     bilimit bicone. -/
-def is_binary_bilimit_of_is_colimit {X Y : C} (t : binary_bicone X Y) (ht : is_colimit t.to_cocone) :
-  t.is_bilimit :=
+def is_binary_bilimit_of_is_colimit {X Y : C} (t : binary_bicone X Y)
+  (ht : is_colimit t.to_cocone) : t.is_bilimit :=
 is_binary_bilimit_of_total _
 begin
   refine binary_cofan.is_colimit.hom_ext ht _ _,