Structures · Category theory
CategoryTheory.HomRel.IsStableUnderPostcomp
The condition that a HomRel is stable under postcomposition.
- Defined in
- Mathlib.CategoryTheory.Quotient
- Shape
- One type argument · adds comp_right
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- HomotopicalAlgebra.CofibrantObject
- HomotopicalAlgebra.BifibrantObject
- HomotopicalAlgebra.FibrantObject
How is a type an instance?
Loading the hierarchy index…
Assumed by7
- CategoryTheory.HomRel.compClosure_eq_self
- CategoryTheory.MorphismProperty.quotient_iff
- CategoryTheory.MorphismProperty.quotient
- CategoryTheory.MorphismProperty.HasQuotient.iff_of_eqvGen
- CategoryTheory.HomRel.IsStableUnderPostcomp.comp_right
- CategoryTheory.HomRel.compClosure_iff_self
- CategoryTheory.MorphismProperty.eq_inverseImage_quotientFunctor
Ancestors0
No ancestors.