English
For a functor F, the comparison between Pi-types indexed by a coproduct (op) of X and a cocone built from coproduct data yields an explicit isomorphism with a Fork map. More precisely, piComparison F (fun x ↦ op (X x)) equals the composition of F with a specified inverse coproduct–product isomorphism, followed by forkMap.
Русский
Для функторa F сравнение по индексам над копроизведением (op) X и кокон над данными копроизведения эквивалентно композиции F с указанной обратной изоморфностью над копроизведением и произведением, за которой идёт forkMap.
LaTeX
$$$\text{piComparison}_F(\lambda x.\,\mathrm{op}(X(x))) = F.map(\mathrm{opCoproductIsoProduct}'\,hc\,\mathrm{(productIsProduct }\\_\text{)} )^{-1} \circ \mathrm{Equalizer.Presieve.Arrows.forkMap} F X c.inj.$$$
Lean4
theorem piComparison_fac :
have : HasCoproduct X := ⟨⟨c, hc⟩⟩
piComparison F (fun x ↦ op (X x)) =
F.map (opCoproductIsoProduct' hc (productIsProduct _)).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj :=
by
have : HasCoproduct X := ⟨⟨c, hc⟩⟩
dsimp only [Equalizer.Presieve.Arrows.forkMap]
have h : Pi.lift (fun i ↦ F.map (c.inj i).op) = F.map (Pi.lift (fun i ↦ (c.inj i).op)) ≫ piComparison F _ := by simp
rw [h, ← Category.assoc, ← Functor.map_comp]
have hh : Pi.lift (fun i ↦ (c.inj i).op) = (productIsProduct (op <| X ·)).lift c.op := by
simp [Pi.lift, productIsProduct]
rw [hh, ← desc_op_comp_opCoproductIsoProduct'_hom hc]
simp
