Theorems · Definition · category theory
HomotopicalAlgebra.IsFibrant
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[HomotopicalAlgebra.CategoryWithFibrations C] → [CategoryTheory.Limits.HasTerminal C] → C → PropAn object X is fibrant if X ⟶ ⊤_ C is a fibration.
- Cited by
- 56 results in Mathlib
- Foundations
- Depth 25 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.Limits.HasTerminalstatement and proof · cited by 142
- CategoryTheory.Limits.terminal.fromproof · cited by 77
- HomotopicalAlgebra.CategoryWithFibrationsstatement and proof · cited by 46
- HomotopicalAlgebra.Fibrationproof · cited by 32
Cited by71
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.fibrantObjectsproof · cited by 20
- HomotopicalAlgebra.BifibrantObject.mkstatement and proof · cited by 15
- HomotopicalAlgebra.BifibrantObject.homMkstatement and proof · cited by 14
- HomotopicalAlgebra.FibrantObject.mkstatement and proof · cited by 10
- HomotopicalAlgebra.FibrantObject.homMkstatement and proof · cited by 8
- SSet.KanComplexproof · cited by 6
- HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iffstatement and proof · cited by 5
- HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClassstatement and proof · cited by 4
- HomotopicalAlgebra.FibrantBrownFactorization.mk'statement and proof · cited by 4
- HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalencestatement and proof · cited by 4
- HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRightstatement and proof · cited by 4
- HomotopicalAlgebra.PathObject.transstatement and proof · cited by 4