English
For f and X with appropriate structure, Y.map (sigmaIncl f a).op (counitAppApp S Y f) equals counitAppAppImage f a.
Русский
Для f и X выполняется равенство: Y.map( sigmaIncl f a ).op (counitAppApp S Y f) = counitAppAppImage f a.
LaTeX
$$$Y.map( \sigmaIncl(f,a).\mathrm{op} \; (\mathrm{counitAppApp}\; S\; Y\; f) = \mathrm{counitAppAppImage}\; f\; a$$$
Lean4
theorem incl_of_counitAppApp [PreservesFiniteProducts Y] [HasExplicitFiniteCoproducts.{u} P] (a : Fiber f) :
Y.map (sigmaIncl f a).op (counitAppApp S Y f) = counitAppAppImage f a :=
by
rw [← sigmaComparison_comp_sigmaIso, Functor.mapIso_hom, Iso.op_hom, types_comp_apply]
simp only [counitAppApp, Functor.mapIso_inv, ← Iso.op_hom, types_comp_apply, ← FunctorToTypes.map_comp_apply,
Iso.inv_hom_id, FunctorToTypes.map_id_apply]
exact congrFun (inv_hom_id_apply (asIso (sigmaComparison Y (fun a ↦ (fiber f a).1))) (counitAppAppImage f)) _
