2-commutative squares of categories of arrows #
@[instance_reducible]
instance CategoryTheory.Arrow.catCommSq {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] (T : Functor C₁ C₂) (L : Functor C₁ D₁) (R : Functor C₂ D₂) (B : Functor D₁ D₂) [CatCommSq T L R B] :
Equations
- CategoryTheory.Arrow.catCommSq T L R B = { iso := (CategoryTheory.Functor.mapArrowFunctor C₁ D₂).mapIso (CategoryTheory.CatCommSq.iso T L R B) }
@[simp]
theorem CategoryTheory.Arrow.catCommSq_iso {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] (T : Functor C₁ C₂) (L : Functor C₁ D₁) (R : Functor C₂ D₂) (B : Functor D₁ D₂) [CatCommSq T L R B] :
CatCommSq.iso T.mapArrow L.mapArrow R.mapArrow B.mapArrow = (Functor.mapArrowFunctor C₁ D₂).mapIso (CatCommSq.iso T L R B)