Functors out of sums of categories.

This file records the universal property of sums of categories as an equivalence of categories Sum.functorEquiv : A ⊕ A' ⥤ B ≌ (A ⥤ B) × (A' ⥤ B), and characterizes its precompositions with the left and right inclusion as corresponding to the projections on the product side.

def CategoryTheory.Sum.functorEquiv (A : Type u_1) [Category.{u_3, u_1} A] (A' : Type u_2) [Category.{u_4, u_2} A'] (B : Type u) [Category.{v, u} B] : Functor (A ⊕ A') B ≌ Functor A B × Functor A' B

The equivalence between functors from a sum and the product of the functor categories.

@[simp]

theorem CategoryTheory.Sum.functorEquiv_inverse_obj (A : Type u_1) [Category.{u_3, u_1} A] (A' : Type u_2) [Category.{u_4, u_2} A'] (B : Type u) [Category.{v, u} B] (F : Functor A B × Functor A' B) : (functorEquiv A A' B).inverse.obj F = F.1.sum' F.2

@[simp]

theorem CategoryTheory.Sum.functorEquiv_counitIso (A : Type u_1) [Category.{u_3, u_1} A] (A' : Type u_2) [Category.{u_4, u_2} A'] (B : Type u) [Category.{v, u} B] : (functorEquiv A A' B).counitIso = NatIso.ofComponents (fun (F : Functor A B × Functor A' B) => (F.1.inlCompSum' F.2).prod (F.1.inrCompSum' F.2) ≪≫ prod.etaIso F) ⋯

@[simp]

theorem CategoryTheory.Sum.functorEquiv_inverse_map (A : Type u_1) [Category.{u_3, u_1} A] (A' : Type u_2) [Category.{u_4, u_2} A'] (B : Type u) [Category.{v, u} B] {X✝ Y✝ : Functor A B × Functor A' B} (η : X✝ ⟶ Y✝) : (functorEquiv A A' B).inverse.map η = NatTrans.sum' η.1 η.2

@[simp]

theorem CategoryTheory.Sum.functorEquiv_functor_obj (A : Type u_1) [Category.{u_3, u_1} A] (A' : Type u_2) [Category.{u_4, u_2} A'] (B : Type u) [Category.{v, u} B] (F : Functor (A ⊕ A') B) : (functorEquiv A A' B).functor.obj F = ((inl_ A A').comp F, (inr_ A A').comp F)

@[simp]

theorem CategoryTheory.Sum.functorEquiv_functor_map (A : Type u_1) [Category.{u_3, u_1} A] (A' : Type u_2) [Category.{u_4, u_2} A'] (B : Type u) [Category.{v, u} B] {X✝ Y✝ : Functor (A ⊕ A') B} (η : X✝ ⟶ Y✝) : (functorEquiv A A' B).functor.map η = ((inl_ A A').whiskerLeft η, (inr_ A A').whiskerLeft η)

@[simp]

theorem CategoryTheory.Sum.functorEquiv_unitIso (A : Type u_1) [Category.{u_3, u_1} A] (A' : Type u_2) [Category.{u_4, u_2} A'] (B : Type u) [Category.{v, u} B] : (functorEquiv A A' B).unitIso = NatIso.ofComponents (fun (F : Functor (A ⊕ A') B) => F.isoSum) ⋯

@[simp]

theorem CategoryTheory.Sum.functorEquiv_unit_app_app_inl {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) (a : A) : ((functorEquiv A A' B).unit.app X).app (Sum.inl a) = CategoryStruct.id (X.obj (Sum.inl a))

@[simp]

theorem CategoryTheory.Sum.functorEquiv_unit_app_app_inr {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) (a' : A') : ((functorEquiv A A' B).unit.app X).app (Sum.inr a') = CategoryStruct.id (X.obj (Sum.inr a'))

@[simp]

theorem CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inl {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) (a : A) : ((functorEquiv A A' B).unitIso.inv.app X).app (Sum.inl a) = CategoryStruct.id (X.obj (Sum.inl a))

@[simp]

theorem CategoryTheory.Sum.functorEquiv_unitIso_inv_app_app_inr {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) (a' : A') : ((functorEquiv A A' B).unitIso.inv.app X).app (Sum.inr a') = CategoryStruct.id (X.obj (Sum.inr a'))

def CategoryTheory.Sum.functorEquivFunctorCompFstIso {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] : (functorEquiv A A' B).functor.comp (Prod.fst (Functor A B) (Functor A' B)) ≅ (Functor.whiskeringLeft A (A ⊕ A') B).obj (inl_ A A')

Composing the forward direction of functorEquiv with the first projection is the same as precomposition with inl_ A A'.

@[simp]

theorem CategoryTheory.Sum.functorEquivFunctorCompFstIso_hom_app_app {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) (X✝ : A) : (functorEquivFunctorCompFstIso.hom.app X).app X✝ = CategoryStruct.id (X.obj (Sum.inl X✝))

@[simp]

theorem CategoryTheory.Sum.functorEquivFunctorCompFstIso_inv_app_app {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) (X✝ : A) : (functorEquivFunctorCompFstIso.inv.app X).app X✝ = CategoryStruct.id (X.obj (Sum.inl X✝))

def CategoryTheory.Sum.functorEquivFunctorCompSndIso {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] : (functorEquiv A A' B).functor.comp (Prod.snd (Functor A B) (Functor A' B)) ≅ (Functor.whiskeringLeft A' (A ⊕ A') B).obj (inr_ A A')

Composing the forward direction of functorEquiv with the second projection is the same as precomposition with inr_ A A'.

@[simp]

theorem CategoryTheory.Sum.functorEquivFunctorCompSndIso_hom_app_app {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) (X✝ : A') : (functorEquivFunctorCompSndIso.hom.app X).app X✝ = CategoryStruct.id (X.obj (Sum.inr X✝))

@[simp]

theorem CategoryTheory.Sum.functorEquivFunctorCompSndIso_inv_app_app {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) (X✝ : A') : (functorEquivFunctorCompSndIso.inv.app X).app X✝ = CategoryStruct.id (X.obj (Sum.inr X✝))

def CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] : (functorEquiv A A' B).inverse.comp ((Functor.whiskeringLeft A (A ⊕ A') B).obj (inl_ A A')) ≅ Prod.fst (Functor A B) (Functor A' B)

Composing the backward direction of functorEquiv with precomposition with inl_ A A'. is naturally isomorphic to the first projection.

@[simp]

theorem CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_inv_app_app {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor A B × Functor A' B) (X✝ : A) : (functorEquivInverseCompWhiskeringLeftInlIso.inv.app X).app X✝ = CategoryStruct.id (X.1.obj X✝)

@[simp]

theorem CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso_hom_app_app {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor A B × Functor A' B) (X✝ : A) : (functorEquivInverseCompWhiskeringLeftInlIso.hom.app X).app X✝ = CategoryStruct.id (X.1.obj X✝)

def CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] : (functorEquiv A A' B).inverse.comp ((Functor.whiskeringLeft A' (A ⊕ A') B).obj (inr_ A A')) ≅ Prod.snd (Functor A B) (Functor A' B)

Composing the backward direction of functorEquiv with the second projection is the same as precomposition with inr_ A A'.

@[simp]

theorem CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_hom_app_app {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor A B × Functor A' B) (X✝ : A') : (functorEquivInverseCompWhiskeringLeftInrIso.hom.app X).app X✝ = CategoryStruct.id (X.2.obj X✝)

@[simp]

theorem CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_inv_app_app {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor A B × Functor A' B) (X✝ : A') : (functorEquivInverseCompWhiskeringLeftInrIso.inv.app X).app X✝ = CategoryStruct.id (X.2.obj X✝)

def CategoryTheory.Sum.natTransOfWhiskerLeftInlInr {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] {F G : Functor (A ⊕ A') B} (η₁ : (inl_ A A').comp F ⟶ (inl_ A A').comp G) (η₂ : (inr_ A A').comp F ⟶ (inr_ A A').comp G) : F ⟶ G

A consequence of functorEquiv: we can construct a natural transformation of functors A ⊕ A' ⥤ B from the data of natural transformations of their whiskering with inl_ and inr_.

@[simp]

theorem CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_app {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] {F G : Functor (A ⊕ A') B} (η₁ : (inl_ A A').comp F ⟶ (inl_ A A').comp G) (η₂ : (inr_ A A').comp F ⟶ (inr_ A A').comp G) (X : A ⊕ A') : (natTransOfWhiskerLeftInlInr η₁ η₂).app X = CategoryStruct.comp (((functorEquiv A A' B).unit.app F).app X) (CategoryStruct.comp ((NatTrans.sum' η₁ η₂).app X) (((functorEquiv A A' B).unitInv.app G).app X))

@[simp]

theorem CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_id {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] {F : Functor (A ⊕ A') B} : natTransOfWhiskerLeftInlInr (CategoryStruct.id ((inl_ A A').comp F)) (CategoryStruct.id ((inr_ A A').comp F)) = CategoryStruct.id F

@[simp]

theorem CategoryTheory.Sum.natTransOfWhiskerLeftInlInr_comp {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] {F G H : Functor (A ⊕ A') B} (η₁ : (inl_ A A').comp F ⟶ (inl_ A A').comp G) (η₂ : (inr_ A A').comp F ⟶ (inr_ A A').comp G) (ν₁ : (inl_ A A').comp G ⟶ (inl_ A A').comp H) (ν₂ : (inr_ A A').comp G ⟶ (inr_ A A').comp H) : natTransOfWhiskerLeftInlInr (CategoryStruct.comp η₁ ν₁) (CategoryStruct.comp η₂ ν₂) = CategoryStruct.comp (natTransOfWhiskerLeftInlInr η₁ η₂) (natTransOfWhiskerLeftInlInr ν₁ ν₂)

def CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] {F G : Functor (A ⊕ A') B} (η₁ : (inl_ A A').comp F ≅ (inl_ A A').comp G) (η₂ : (inr_ A A').comp F ≅ (inr_ A A').comp G) : F ≅ G

A consequence of functorEquiv: we can construct a natural isomorphism of functors A ⊕ A' ⥤ B from the data of natural isomorphisms of their whiskering with inl_ and inr_.

@[simp]

theorem CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_hom {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] {F G : Functor (A ⊕ A') B} (η₁ : (inl_ A A').comp F ≅ (inl_ A A').comp G) (η₂ : (inr_ A A').comp F ≅ (inr_ A A').comp G) : (natIsoOfWhiskerLeftInlInr η₁ η₂).hom = natTransOfWhiskerLeftInlInr η₁.hom η₂.hom

@[simp]

theorem CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_inv {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] {F G : Functor (A ⊕ A') B} (η₁ : (inl_ A A').comp F ≅ (inl_ A A').comp G) (η₂ : (inr_ A A').comp F ≅ (inr_ A A').comp G) : (natIsoOfWhiskerLeftInlInr η₁ η₂).inv = natTransOfWhiskerLeftInlInr η₁.inv η₂.inv

theorem CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr_eq {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] {F G : Functor (A ⊕ A') B} (η₁ : (inl_ A A').comp F ≅ (inl_ A A').comp G) (η₂ : (inr_ A A').comp F ≅ (inr_ A A').comp G) : natIsoOfWhiskerLeftInlInr η₁ η₂ = (functorEquiv A A' B).unitIso.app F ≪≫ (functorEquiv A A' B).inverse.mapIso (η₁.prod η₂) ≪≫ (functorEquiv A A' B).unitIso.symm.app G

def CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] : ((equivalence A A').congrLeft.trans (functorEquiv A' A B)).functor ≅ ((functorEquiv A A' B).trans (Prod.braiding (Functor A B) (Functor A' B))).functor

functorEquiv A A' B transforms Swap.equivalence into Prod.braiding.

@[simp]

theorem CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_fst {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) : (equivalenceFunctorEquivFunctorIso.inv.app X).1 = CategoryStruct.comp (Functor.whiskerRight (swapCompInl A' A).inv X) ((inl_ A' A).associator (swap A' A) X).hom

@[simp]

theorem CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_fst {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) : (equivalenceFunctorEquivFunctorIso.hom.app X).1 = CategoryStruct.comp ((inl_ A' A).associator (swap A' A) X).inv (Functor.whiskerRight (swapCompInl A' A).hom X)

@[simp]

theorem CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_hom_app_snd {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) : (equivalenceFunctorEquivFunctorIso.hom.app X).2 = CategoryStruct.comp ((inr_ A' A).associator (swap A' A) X).inv (Functor.whiskerRight (swapCompInr A' A).hom X)

@[simp]

theorem CategoryTheory.Sum.Swap.equivalenceFunctorEquivFunctorIso_inv_app_snd {A : Type u_1} [Category.{u_3, u_1} A] {A' : Type u_2} [Category.{u_4, u_2} A'] {B : Type u} [Category.{v, u} B] (X : Functor (A ⊕ A') B) : (equivalenceFunctorEquivFunctorIso.inv.app X).2 = CategoryStruct.comp (Functor.whiskerRight (swapCompInr A' A).inv X) ((inr_ A' A).associator (swap A' A) X).hom

def CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso {A : Type u_1} [Category.{u_4, u_1} A] {A' : Type u_2} [Category.{u_5, u_2} A'] {B : Type u} [Category.{v, u} B] (T : Type u_3) [Category.{u_6, u_3} T] : ((sum.associativity A A' T).congrLeft.trans ((functorEquiv A (A' ⊕ T) B).trans (Equivalence.refl.prod (functorEquiv A' T B)))).functor ≅ (((functorEquiv (A ⊕ A') T B).trans ((functorEquiv A A' B).prod Equivalence.refl)).trans (prod.associativity (Functor A B) (Functor A' B) (Functor T B))).functor

The equivalence Sum.functorEquiv sends associativity of sums to associativity of products

@[simp]

theorem CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst {A : Type u_1} [Category.{u_4, u_1} A] {A' : Type u_2} [Category.{u_5, u_2} A'] {B : Type u} [Category.{v, u} B] (T : Type u_3) [Category.{u_6, u_3} T] (X : Functor ((A ⊕ A') ⊕ T) B) : ((associativityFunctorEquivNaturalityFunctorIso T).hom.app X).1 = CategoryStruct.comp ((inl_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).inv (CategoryStruct.comp (Functor.whiskerRight (sum.inlCompInverseAssociator A A' T).hom X) ((inl_ A A').associator (inl_ (A ⊕ A') T) X).hom)

@[simp]

theorem CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd {A : Type u_1} [Category.{u_4, u_1} A] {A' : Type u_2} [Category.{u_5, u_2} A'] {B : Type u} [Category.{v, u} B] (T : Type u_3) [Category.{u_6, u_3} T] (X : Functor ((A ⊕ A') ⊕ T) B) : ((associativityFunctorEquivNaturalityFunctorIso T).inv.app X).2.2 = CategoryStruct.comp (Functor.whiskerRight (sum.inrCompInrCompInverseAssociator A A' T).inv X) (CategoryStruct.comp ((inr_ A' T).associator ((inr_ A (A' ⊕ T)).comp (sum.inverseAssociator A A' T)) X).hom ((inr_ A' T).whiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).hom))

@[simp]

theorem CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst {A : Type u_1} [Category.{u_4, u_1} A] {A' : Type u_2} [Category.{u_5, u_2} A'] {B : Type u} [Category.{v, u} B] (T : Type u_3) [Category.{u_6, u_3} T] (X : Functor ((A ⊕ A') ⊕ T) B) : ((associativityFunctorEquivNaturalityFunctorIso T).inv.app X).2.1 = CategoryStruct.comp ((inr_ A A').associator (inl_ (A ⊕ A') T) X).inv (CategoryStruct.comp (Functor.whiskerRight (sum.inlCompInrCompInverseAssociator A A' T).inv X) (CategoryStruct.comp ((inl_ A' T).associator ((inr_ A (A' ⊕ T)).comp (sum.inverseAssociator A A' T)) X).hom ((inl_ A' T).whiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).hom)))

@[simp]

theorem CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd {A : Type u_1} [Category.{u_4, u_1} A] {A' : Type u_2} [Category.{u_5, u_2} A'] {B : Type u} [Category.{v, u} B] (T : Type u_3) [Category.{u_6, u_3} T] (X : Functor ((A ⊕ A') ⊕ T) B) : ((associativityFunctorEquivNaturalityFunctorIso T).hom.app X).2.2 = CategoryStruct.comp ((inr_ A' T).whiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).inv) (CategoryStruct.comp ((inr_ A' T).associator ((inr_ A (A' ⊕ T)).comp (sum.inverseAssociator A A' T)) X).inv (Functor.whiskerRight (sum.inrCompInrCompInverseAssociator A A' T).hom X))

@[simp]

theorem CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst {A : Type u_1} [Category.{u_4, u_1} A] {A' : Type u_2} [Category.{u_5, u_2} A'] {B : Type u} [Category.{v, u} B] (T : Type u_3) [Category.{u_6, u_3} T] (X : Functor ((A ⊕ A') ⊕ T) B) : ((associativityFunctorEquivNaturalityFunctorIso T).inv.app X).1 = CategoryStruct.comp ((inl_ A A').associator (inl_ (A ⊕ A') T) X).inv (CategoryStruct.comp (Functor.whiskerRight (sum.inlCompInverseAssociator A A' T).inv X) ((inl_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).hom)

@[simp]

theorem CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst {A : Type u_1} [Category.{u_4, u_1} A] {A' : Type u_2} [Category.{u_5, u_2} A'] {B : Type u} [Category.{v, u} B] (T : Type u_3) [Category.{u_6, u_3} T] (X : Functor ((A ⊕ A') ⊕ T) B) : ((associativityFunctorEquivNaturalityFunctorIso T).hom.app X).2.1 = CategoryStruct.comp ((inl_ A' T).whiskerLeft ((inr_ A (A' ⊕ T)).associator (sum.inverseAssociator A A' T) X).inv) (CategoryStruct.comp ((inl_ A' T).associator ((inr_ A (A' ⊕ T)).comp (sum.inverseAssociator A A' T)) X).inv (CategoryStruct.comp (Functor.whiskerRight (sum.inlCompInrCompInverseAssociator A A' T).hom X) ((inr_ A A').associator (inl_ (A ⊕ A') T) X).hom))