Structures · Category theory
CategoryTheory.MorphismProperty.HasPullbacksAlong
P.HasPullbacksAlong f states that for any morphism satisfying P with the same codomain
as f, the pullback of that morphism along f exists.
- 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 by24
- CategoryTheory.MorphismProperty.Over.pullback
- CategoryTheory.MorphismProperty.Over.pullbackComp
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj
- CategoryTheory.MorphismProperty.Over.pullbackCongr
- CategoryTheory.MorphismProperty.HasPullbacksAlong.hasPullback
- CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst
- CategoryTheory.MorphismProperty.isRightAdjoint_pullback
- CategoryTheory.MorphismProperty.instHasPullbacksAlongCompOfIsStableUnderBaseChangeAlong
- CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong
- CategoryTheory.MorphismProperty.Over.pullback_obj_hom
- CategoryTheory.MorphismProperty.Over.pullback_obj_left
- CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongCompOfHasPullbacksAlong
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app
- CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left
- CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app
- CategoryTheory.MorphismProperty.Over.pullbackComp.congr_simp
- CategoryTheory.MorphismProperty.Over.pullback_map_left
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj.congr_simp
- CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst
- CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left
- CategoryTheory.MorphismProperty.Over.pullback.congr_simp
- CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong
- CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong
Ancestors0
No ancestors.