Structures · Category theory
CategoryTheory.MorphismProperty.HasPushoutsAlong
P.HasPushoutsAlong f states that for any morphism satisfying P with the same domain
as f, the pushout of that morphism along f exists.
- Shape
- 2 explicit arguments · adds hasPushout
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 by20
- CategoryTheory.MorphismProperty.Under.pushout
- CategoryTheory.MorphismProperty.Under.mapPushoutAdj
- CategoryTheory.MorphismProperty.HasPushoutsAlong.hasPushout
- CategoryTheory.MorphismProperty.Under.pushoutCongr
- CategoryTheory.MorphismProperty.Under.pushoutComp
- CategoryTheory.MorphismProperty.Under.pushoutCongr_hom_app_left_fst
- CategoryTheory.MorphismProperty.Under.pushoutCongr_hom_app_left_fst_assoc
- CategoryTheory.MorphismProperty.Under.pushoutComp_inv_app_right
- CategoryTheory.MorphismProperty.instHasPushoutsAlongCompOfIsStableUnderCobaseChangeAlong
- CategoryTheory.MorphismProperty.instIsRightAdjointUnderTopMapOfHasPushoutsAlongOfIsStableUnderCobaseChangeAlong
- CategoryTheory.MorphismProperty.Under.pushout_obj_right
- CategoryTheory.MorphismProperty.isLeftAdjoint_pushout
- CategoryTheory.MorphismProperty.Under.mapPushoutAdj_unit_app
- CategoryTheory.MorphismProperty.instHasPushoutHomDiscretePUnitOfHasPushoutsAlong
- CategoryTheory.MorphismProperty.Under.pushoutComp_hom_app_right
- CategoryTheory.MorphismProperty.Under.pushout_obj_hom
- CategoryTheory.MorphismProperty.Under.mapPushoutAdj_counit_app
- CategoryTheory.MorphismProperty.instHasPushoutInrHomDiscretePUnitOfHasPushoutsAlongOfIsStableUnderCobaseChangeAlong
- CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeAlongCompOfHasPushoutsAlong
- CategoryTheory.MorphismProperty.Under.pushout_map_right
Ancestors0
No ancestors.