English
The right unitor cofan is a colimit cone which realizes the isomorphism between the right-hand side and X via the colimit of a specified diagram.
Русский
Кофан правого унитора является колимитным конусом, реализующим изоморфизм между правой частью и X через колимит заданного диаграммы.
LaTeX
$$$ mapBifunctorRightUnitorCofan F Y e p hp X j \\text{ is a colimit cone with }$$
Lean4
/-- Given `F : D ⥤ C ⥤ D`, `Y : C`, `e : F.flip.obj Y ≅ 𝟭 D`, `X : GradedObject J D` and
`p : J × I → J` such that `p ⟨j, 0⟩ = j` for all `j`,
this is the (colimit) cofan which shall be used to construct the isomorphism
`mapBifunctorMapObj F p X ((single₀ I).obj Y) ≅ X`, see `mapBifunctorRightUnitor`. -/
noncomputable def mapBifunctorRightUnitorCofan (hp : ∀ (j : J), p ⟨j, 0⟩ = j) (X) (j : J) :
(((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).CofanMapObjFun p j :=
CofanMapObjFun.mk _ _ _ (X j)
(fun a ha =>
if ha : a.2 = 0 then (mapBifunctorObjObjSingle₀Iso F Y e X a ha).hom ≫ eqToHom (by aesop)
else (mapBifunctorObjObjSingle₀IsInitial F Y X a ha).to _)
