English
Replacing an empty cocone in IsColimit by another cocone with the same apex yields an equivalence of IsColimit objects; i.e., the colimit structure is preserved under apex isomorphism of empty cocones.
Русский
Замена пустого кокона в IsColimit на другой кокон с тем же апексом порождает эквивалентность структур колимита; то есть колимитная структура сохраняется при изоморфизме апекса пустого кокона.
LaTeX
$$$\text{isColimitEmptyCoconeEquiv}(c_1,c_2,h):\;\text{IsColimit } c_1 \simeq \text{IsColimit } c_2.$$$
Lean4
/-- Replacing an empty cocone in `IsColimit` by another with the same cocone point
is an equivalence. -/
def isColimitEmptyCoconeEquiv (c₁ : Cocone F₁) (c₂ : Cocone F₂) (h : c₁.pt ≅ c₂.pt) : IsColimit c₁ ≃ IsColimit c₂
where
toFun hl := isColimitChangeEmptyCocone C hl c₂ h
invFun hl := isColimitChangeEmptyCocone C hl c₁ h.symm
left_inv := by dsimp [Function.LeftInverse]; intro; simp only [eq_iff_true_of_subsingleton]
right_inv := by
dsimp [Function.LeftInverse, Function.RightInverse]; intro
simp only [eq_iff_true_of_subsingleton]
