Lean4
/-- Given a diagram `F : J ⥤ C` and two `Cone F`s, we can join them into a diagram `Bicone J ⥤ C`.
-/
@[simps]
def biconeMk {C : Type u₁} [Category.{v₁} C] {F : J ⥤ C} (c₁ c₂ : Cone F) : Bicone J ⥤ C
where
obj X := Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j
map
f := by
rcases f with (_ | _ | _ | _ | f)
· exact 𝟙 _
· exact 𝟙 _
· exact c₁.π.app _
· exact c₂.π.app _
· exact F.map f
map_id X := by cases X <;> simp
map_comp f
g := by
rcases f with (_ | _ | _ | _ | _)
· exact (Category.id_comp _).symm
· exact (Category.id_comp _).symm
· cases g
exact (Category.id_comp _).symm.trans (c₁.π.naturality _)
· cases g
exact (Category.id_comp _).symm.trans (c₂.π.naturality _)
· cases g
apply F.map_comp
