2-commutative squares of categories of arrows #
@[implicit_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)