Structures · Category theory
CategoryTheory.HasLiftingProperty
HasLiftingProperty i p means that i has the left lifting
property with respect to p, or equivalently that p has
the right lifting property with respect to i.
- Shape
- 2 explicit arguments · adds sq_hasLift
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- SSet
- CochainComplex.Plus
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- CategoryTheory.HasLiftingProperty.of_arrow_iso_left
- CategoryTheory.HasLiftingProperty.of_arrow_iso_right
- CategoryTheory.RetractArrow.ofRightLiftingProperty
- CategoryTheory.RetractArrow.ofLeftLiftingProperty
- CategoryTheory.HasLiftingProperty.of_comp_right
- CategoryTheory.instHasLiftingPropertyInl
- CategoryTheory.instHasLiftingPropertyMap_1
- CategoryTheory.HasLiftingProperty.sq_hasLift
- CategoryTheory.HasLiftingProperty.over
- CategoryTheory.HasLiftingProperty.of_comp_left
- CategoryTheory.RetractArrow.rightLiftingProperty
- CategoryTheory.instHasLiftingPropertyInr
- CategoryTheory.RetractArrow.leftLiftingProperty
- CategoryTheory.instHasLiftingPropertyMap
- CategoryTheory.instHasLiftingPropertyFst
- CategoryTheory.sq_hasLift_of_hasLiftingProperty
- CategoryTheory.IsPushout.hasLiftingProperty
- CategoryTheory.IsPullback.hasLiftingProperty
- CategoryTheory.instHasLiftingPropertySnd
Ancestors0
No ancestors.