Theorems · Definition · category theory

HomotopicalAlgebra.fibrations

(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithFibrations C] → CategoryTheory.MorphismProperty C

The class of fibrations in a category with fibrations.

Defined in: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
Cited by: 40 results in Mathlib
Foundations: Depth 4 from the axioms · uses no axioms
Assumes: CategoryTheory.Category HomotopicalAlgebra.CategoryWithFibrations

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

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.MorphismPropertystatement · cited by 2,179
HomotopicalAlgebra.CategoryWithFibrationsstatement and proof · cited by 46
HomotopicalAlgebra.CategoryWithFibrations.fibrationsproof · cited by 0

Cited by60

Results whose statement or proof uses this declaration.

HomotopicalAlgebra.trivialFibrationsproof · cited by 30
SSet.anodyneExtensionsproof · cited by 16
HomotopicalAlgebra.FibrantBrownFactorization.toMapFactorizationDatastatement · cited by 6
HomotopicalAlgebra.PathObject.ofFactorizationDatastatement and proof · cited by 6
HomotopicalAlgebra.fibration_iffstatement and proof · cited by 6
HomotopicalAlgebra.FibrantBrownFactorization.mk'statement and proof · cited by 4
HomotopicalAlgebra.FibrantBrownFactorization.rstatement · cited by 4
SSet.anodyneExtensions_pushoutObjObjιproof · cited by 3
HomotopicalAlgebra.isFibrant_iff_of_isTerminalstatement and proof · cited by 2
HomotopicalAlgebra.FibrantBrownFactorization.i_rstatement · cited by 2
HomotopicalAlgebra.mem_fibrationsstatement · cited by 2
HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinderproof · cited by 2