Lean4
/-- Given `ℌ : DayConvolutionInternalHom F H`, if we think of `H.obj G`
as the internal hom `[F, G]`, then this is the transformation
corresponding to the component at `G` of the "coevaluation" natural morphism
`𝟭 ⟶ [F, F ⊛ _]`. -/
def coev_app : G ⟶ H
where
app
c :=
Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' => MonoidalClosed.curry <| (DayConvolution.unit F G).app (c', c))
(fun {c' c''} f => by
have := DayConvolution.unit_naturality F G f (𝟙 c)
simp only [Functor.map_id, tensorHom_id] at this
replace this := congrArg MonoidalClosed.curry this
simp only [MonoidalClosed.curry_natural_right] at this
dsimp
rw [← this]
simp [MonoidalClosed.curry_eq])
naturality {c c'}
f := by
dsimp
apply Wedge.IsLimit.hom_ext <| ℌ.isLimitWedge c'
intro (j : C)
simp only [multicospanIndexEnd_left, dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_obj, Multifork.ofι_pt,
Wedge.mk_ι, Category.assoc, map_comp_π]
rw [← Wedge.mk_ι (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c) (H.obj c) (ℌ.π c) (ℌ.hπ c), ←
Wedge.mk_ι (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c') (H.obj c') (ℌ.π c') (ℌ.hπ c'),
Wedge.IsLimit.lift_ι_assoc, Wedge.IsLimit.lift_ι]
have := DayConvolution.unit_naturality F G (𝟙 j) f
simp only [Functor.map_id, id_tensorHom] at this
replace this := congrArg MonoidalClosed.curry this
simp only [MonoidalClosed.curry_natural_right] at this
rw [← this]
simp [MonoidalClosed.curry_eq]
