Theorems · Theorem · category theory
CategoryTheory.Limits.IsTerminal.comp_from
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z : C} (t : CategoryTheory.Limits.IsTerminal Z) {X Y : C}
(f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (t.from Y) = t.from X- Cited by
- 13 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
- CategoryTheory.Limits.IsTerminal.fromstatement and proof · cited by 160
- CategoryTheory.Limits.IsTerminalstatement and proof · cited by 153
- CategoryTheory.Limits.IsTerminal.hom_extproof · cited by 29
Cited by13
Results whose statement or proof uses this declaration.
- CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fstproof · cited by 24
- CategoryTheory.CartesianMonoidalCategory.whiskerRight_sndproof · cited by 16
- CategoryTheory.CartesianMonoidalCategory.associator_hom_fstproof · cited by 8
- CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fstproof · cited by 7
- CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_sndproof · cited by 6
- CategoryTheory.CartesianMonoidalCategory.associator_inv_sndproof · cited by 6
- HomotopicalAlgebra.isFibrant_iff_of_isTerminalproof · cited by 2
- CategoryTheory.Limits.IsTerminal.isCardinalFilteredproof · cited by 1
- CategoryTheory.Limits.isIso_of_isTerminalproof · cited by 1
- SkyscraperPresheafFunctor.map'_compproof · cited by 0
- SSet.quasicategory_iff_of_isTerminalproof · cited by 0