English
The categorical product of a finite family in FintypeCat is equivalent to the product as types.
Русский
Категориальный произведение конечной семьи объектов в FintypeCat эквивалентно обычному произведению как множеств.
LaTeX
$$$(\\prod^{\\mathrm{c}}_{i} X_i) \\simeq \\prod_{i} X_i$$$
Lean4
/-- The categorical product of a finite family in `FintypeCat` is equivalent to the product
as types. -/
noncomputable def productEquiv {ι : Type*} [Finite ι] (X : ι → FintypeCat.{u}) : (∏ᶜ X : FintypeCat) ≃ ∀ i, X i :=
letI : Fintype ι := Fintype.ofFinite _
haveI : Small.{u} ι := ⟨ULift (Fin (Fintype.card ι)), ⟨(Fintype.equivFin ι).trans Equiv.ulift.symm⟩⟩
let is₁ : FintypeCat.incl.obj (∏ᶜ fun i ↦ X i) ≅ (∏ᶜ fun i ↦ X i : Type u) :=
PreservesProduct.iso FintypeCat.incl (fun i ↦ X i)
let is₂ : (∏ᶜ fun i ↦ X i : Type u) ≅ Shrink.{u} (∀ i, X i) := Types.Small.productIso (fun i ↦ X i)
let e : (∀ i, X i) ≃ Shrink.{u} (∀ i, X i) := equivShrink _
(equivEquivIso.symm is₁).trans ((equivEquivIso.symm is₂).trans e.symm)
