Structures · Category theory
CategoryTheory.MorphismProperty.HasPullbacks
P has pullbacks if for every f satisfying P, pullbacks of arbitrary morphisms along f
exist.
- Shape
- One type argument · adds hasPullback
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- AlgebraicGeometry.Scheme
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- CategoryTheory.MorphismProperty.coverage
- CategoryTheory.MorphismProperty.HasPullbacks.hasPullback
- CategoryTheory.MorphismProperty.grothendieckTopology
- CategoryTheory.MorphismProperty.coverage_toPrecoverage
- CategoryTheory.MorphismProperty.instHasPullbacksAgainstOfHasPullbacks
- CategoryTheory.MorphismProperty.hasPullback
- CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks
- AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks
Ancestors0
No ancestors.