Structures · Category theory
CategoryTheory.ChosenPullbacksAlong
A functorial choice of pullbacks along a morphism f : Y ⟶ X in C given by a functor
Over X ⥤ Over Y which is a right adjoint to the functor Over.map f.
- Shape
- One type argument · adds pullback, mapPullbackAdj
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
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 by108
- CategoryTheory.ChosenPullbacksAlong.pullback
- CategoryTheory.ChosenPullbacksAlong.snd
- CategoryTheory.ChosenPullbacksAlong.pullbackObj
- CategoryTheory.ChosenPullbacksAlong.fst
- CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj
- CategoryTheory.ChosenPullbacksAlong.pullbackMap
- CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback
- CategoryTheory.ChosenPullbacksAlong.lift
- CategoryTheory.ExponentiableMorphism.coev
- CategoryTheory.ExponentiableMorphism.ev
- CategoryTheory.Over.sections
- CategoryTheory.ChosenPullbacksAlong.pullbackId
- CategoryTheory.ExponentiableMorphism.comp
- CategoryTheory.Over.sectionsUncurry
- CategoryTheory.ExponentiableMorphism.id
- CategoryTheory.ChosenPullbacksAlong.hom_ext
- CategoryTheory.ExponentiableMorphism.pushforwardComp
- CategoryTheory.Over.sectionsCurry
- CategoryTheory.ExponentiableMorphism.pushforwardId
- CategoryTheory.ChosenPullbacksAlong.pullbackComp
- CategoryTheory.ChosenPullbacksAlong.comp
- CategoryTheory.ChosenPullbacksAlong.lift_fst
- CategoryTheory.ChosenPullbacksAlong.fst'
- CategoryTheory.ExponentiableMorphism.pushforwardUncurry
- CategoryTheory.ExponentiableMorphism.pushforwardCurry
- CategoryTheory.ChosenPullbacksAlong.pullbackMap_fst
- CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd
- CategoryTheory.ChosenPullbacksAlong.condition
- CategoryTheory.ChosenPullbacksAlong.lift_snd
- CategoryTheory.ChosenPullbacksAlong.pullbackCone
- CategoryTheory.Over.sectionsCurry_sectionUncurry
- CategoryTheory.toOverPullbackIsoToOver
- CategoryTheory.Over.sectionsUncurry_sectionsCurry
- CategoryTheory.Over.toOverSectionsAdj
- CategoryTheory.ChosenPullbacksAlong.snd'
- CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom_app
- CategoryTheory.ChosenPullbacksAlong.lift.congr_simp
- CategoryTheory.ExponentiableMorphism.ev_coev
- CategoryTheory.ChosenPullbacksAlong.unit_pullbackComp_hom
- CategoryTheory.ExponentiableMorphism.ev_naturality
- CategoryTheory.ExponentiableMorphism.pushforwardComp_hom_counit
- CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit
- CategoryTheory.ChosenPullbacksAlong.pullbackComp_hom_counit
- CategoryTheory.ExponentiableMorphism.coev_ev
- CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom
- CategoryTheory.ChosenPullbacksAlong.pullbackId_hom_counit
- CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_snd
- CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd_assoc
- CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst
- CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom
Ancestors0
No ancestors.