Skip to content

Commit bdd3299

Browse files
committed
chore(CategoryTheory/IsConnected): fix usage of Relation.ReflTransGen.lift in zigzag_prefunctor_obj_of_zigzag
1 parent fb031f6 commit bdd3299

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/CategoryTheory/IsConnected.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -353,7 +353,7 @@ def Zigzag.setoid (J : Type u₂) [Category.{v₁} J] : Setoid J where
353353
-/
354354
theorem zigzag_prefunctor_obj_of_zigzag (F : J ⥤q K) {j₁ j₂ : J} (h : Zigzag j₁ j₂) :
355355
Zigzag (F.obj j₁) (F.obj j₂) :=
356-
h.lift _ fun _ _ => Or.imp (Nonempty.map fun f => F.map f) (Nonempty.map fun f => F.map f)
356+
h.lift F.obj <| Or.imp (Nonempty.map fun f => F.map f) (Nonempty.map fun f => F.map f)
357357

358358
/-- If there is a zigzag from `j₁` to `j₂`, then there is a zigzag from `F j₁` to
359359
`F j₂` as long as `F` is a functor.

0 commit comments

Comments
 (0)