Structures · Category theory
CategoryTheory.Presieve.HasPullbacks
A presieve R has pullbacks along f if for every h in R, the pullback
with f exists.
- Defined in
- Mathlib.CategoryTheory.Sites.Sieves
- Shape
- 2 explicit arguments · adds hasPullback
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- CategoryTheory.Sieve.pullbackArrows_comm
- CategoryTheory.Presieve.HasPullbacks.hasPullback
- CategoryTheory.Presieve.hasPullback
- CategoryTheory.Precoverage.pullbackArrows_mem
- CategoryTheory.Presieve.FactorsThruAlong.pullbackArrows
- CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1
- CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀
- CategoryTheory.Presieve.pullbackArrows.congr_simp
Ancestors0
No ancestors.