Structures · Category theory
CategoryTheory.Localization.Lifting₂
Given functors L₁ : C₁ ⥤ D₁, L₂ : C₂ ⥤ D₂, morphisms properties W₁ on C₁
and W₂ on C₂, and functors F : C₁ ⥤ C₂ ⥤ E and F' : D₁ ⥤ D₂ ⥤ E, we say
Lifting₂ L₁ L₂ W₁ W₂ F F' holds if F is induced by F', up to an isomorphism.
- Shape
- 6 explicit arguments · adds iso
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 by18
- CategoryTheory.Localization.Lifting₂.iso
- CategoryTheory.Localization.lift₂NatTrans
- CategoryTheory.Localization.lift₂NatIso
- CategoryTheory.Localization.associator
- CategoryTheory.Localization.lift₂NatTrans_app_app
- CategoryTheory.Localization.associator_hom_app_app_app
- CategoryTheory.Localization.Lifting₂.snd
- CategoryTheory.Localization.lift₂NatIso_inv
- CategoryTheory.Localization.Lifting₃.bifunctorComp₂₃
- CategoryTheory.Localization.Lifting₃.bifunctorComp₁₂
- CategoryTheory.Localization.Lifting₂.uncurry
- CategoryTheory.Localization.lift₂NatTrans.congr_simp
- CategoryTheory.Localization.associator.congr_simp
- CategoryTheory.Localization.Lifting₂.fst
- CategoryTheory.Localization.lift₂NatIso_hom
- CategoryTheory.Localization.lift₂NatIso.congr_simp
- CategoryTheory.Localization.Lifting₂.compRight
- CategoryTheory.Localization.Lifting₂.flip
Ancestors0
No ancestors.