Theorems · Definition · category theory
CategoryTheory.Limits.Types.Small.productIso
{J : Type v} → (F : J → Type u) → [inst : Small.{u, v} J] → ∏ᶜ F ≅ Shrink.{u, max u v} ((j : J) → F j)The categorical product in Type u indexed in Type v
is the type-theoretic product Π j, F j, after shrinking back to Type u.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Small
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Isostatement · cited by 3,963
- CategoryTheory.Discretestatement · cited by 2,447
- CategoryTheory.Discrete.functorstatement · cited by 633
- Smallstatement and proof · cited by 369
- CategoryTheory.Limits.piObjstatement · cited by 237
- Shrinkstatement · cited by 132
- CategoryTheory.Limits.limit.isoLimitConeproof · cited by 8
- CategoryTheory.Limits.Types.Small.productLimitConeproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.FintypeCat.productEquivproof · cited by 3
- CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_applystatement and proof · cited by 3
- CategoryTheory.Limits.Types.Small.productIso_hom_comp_evalstatement · cited by 1
- CategoryTheory.Limits.Types.Small.productIso_inv_comp_πstatement · cited by 1
- CategoryTheory.Equalizer.Presieve.Arrows.sheaf_conditionproof · cited by 1
- CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_smallstatement and proof · cited by 0
- CategoryTheory.Limits.Types.Small.productIso_inv_comp_π_applystatement and proof · cited by 0