Theorems · Definition · category theory
HomotopicalAlgebra.FibrantObject
(C : Type u) →
[inst : CategoryTheory.Category.{v, u} C] →
[HomotopicalAlgebra.CategoryWithFibrations C] → [CategoryTheory.Limits.HasTerminal C] → Type uThe full subcategory of fibrant objects.
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- CategoryTheory.ObjectProperty.FullSubcategoryproof · cited by 726
- CategoryTheory.Limits.HasTerminalstatement and proof · cited by 142
- HomotopicalAlgebra.CategoryWithFibrationsstatement and proof · cited by 46
- HomotopicalAlgebra.fibrantObjectsproof · cited by 20
Cited by40
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.FibrantObject.homRelstatement and proof · cited by 12
- HomotopicalAlgebra.FibrantObject.mkstatement · cited by 10
- HomotopicalAlgebra.FibrantObject.homMkstatement · cited by 8
- HomotopicalAlgebra.FibrantObject.toHoCatstatement · cited by 8
- HomotopicalAlgebra.FibrantObject.ιstatement · cited by 2
- HomotopicalAlgebra.BifibrantObject.ιFibrantObjectstatement · cited by 2
- HomotopicalAlgebra.FibrantObject.HoCat.resolutionstatement · cited by 2
- HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObjectstatement · cited by 2
- HomotopicalAlgebra.FibrantObject.homMk_homMkstatement · cited by 1
- HomotopicalAlgebra.FibrantObject.homRel_equivalence_of_isCofibrant_srcstatement and proof · cited by 1
- HomotopicalAlgebra.FibrantObject.homRel_iff_leftHomotopyRelstatement and proof · cited by 1
- HomotopicalAlgebra.FibrantObject.localizerMorphismstatement · cited by 1