Pullbacks

Statistics

Metric	Count
Definitions	0
Theorems `hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair`, `hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair`, `hasPullbacks_of_hasBinaryProducts_of_hasEqualizers`, `hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair` 📖	mathematical	—	`HasColimit` `WalkingSpan` `WidePushoutShape.category` `WalkingPair` `span`	—	`CategoryTheory.Category.assoc` `coequalizer.condition` `colimit.ι_desc` `PushoutCocone.condition` `coequalizer.hom_ext` `coprod.hom_ext`
`hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair` 📖	mathematical	—	`HasLimit` `WalkingCospan` `WidePullbackShape.category` `WalkingPair` `cospan`	—	`CategoryTheory.Category.assoc` `equalizer.condition` `limit.lift_π` `PullbackCone.condition` `limit.lift_π_assoc` `equalizer.hom_ext` `prod.hom_ext`
`hasPullbacks_of_hasBinaryProducts_of_hasEqualizers` 📖	mathematical	—	`HasPullbacks`	—	`hasLimit_of_iso` `hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair` `hasLimitOfHasLimitsOfShape`
`hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers` 📖	mathematical	—	`HasPushouts`	—	`hasPushouts_of_hasColimit_span` `hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair` `hasColimitOfHasColimitsOfShape`

---