Theorems · Theorem · category theory
CategoryTheory.Limits.terminal.comp_from
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] {P Q : C}
(f : P ⟶ Q),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.terminal.from Q) = CategoryTheory.Limits.terminal.from P- Cited by
- 21 results in Mathlib
- Foundations
- Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound
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.HasTerminalstatement and proof · cited by 142
- CategoryTheory.Limits.terminalstatement · cited by 141
- CategoryTheory.Limits.terminal.fromstatement and proof · cited by 77
Cited by21
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.isFibrant_iff_of_isTerminalproof · cited by 2
- AlgebraicGeometry.AffineSpace.isPullback_mapproof · cited by 2
- CategoryTheory.Dial.leftUnitor_hom_Fproof · cited by 2
- HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinderproof · cited by 2
- CategoryTheory.Dial.rightUnitor_hom_Fproof · cited by 2
- SSet.horn.IsCompatible.exists_lift_of_kanComplexproof · cited by 2
- CategoryTheory.Functor.relativelyRepresentable.of_diagproof · cited by 1
- HomotopicalAlgebra.CofibrantObject.exists_bifibrant_mapproof · cited by 1
- CategoryTheory.Functor.relativelyRepresentable.toPullbackTerminalproof · cited by 1
- HomotopicalAlgebra.FibrantObject.HoCat.exists_resolution_mapproof · cited by 1