Morphisms of categorical cospans.

Given F : A ⥤ B, G : C ⥤ B, F' : A' ⥤ B' and G' : C' ⥤ B', this file defines CatCospanTransform F G F' G', the category of "categorical transformations" from the (categorical) cospan F G to the (categorical) cospan F' G'. Such a transformation consists of a diagram

    F   G
  A ⥤ B ⥢ C
H₁|   |H₂ |H₃
  v   v   v
  A'⥤ B'⥢ C'
    F'  G'

with specified CatCommSqs expressing 2-commutativity of the squares. These transformations are used to encode 2-functoriality of categorical pullback squares.

structure CategoryTheory.Limits.CatCospanTransform {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor C B) {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] (F' : Functor A' B') (G' : Functor C' B') : Type (max (max (max (max (max (max (max (max (max (max (max u₁ u₂) u₃) u₄) u₅) u₆) v₁) v₂) v₃) v₄) v₅) v₆)

A CatCospanTransform F G F' G' is a diagram

    F   G
  A ⥤ B ⥢ C
H₁|   |H₂ |H₃
  v   v   v
  A'⥤ B'⥢ C'
    F'  G'

with specified CatCommSqs expressing 2-commutativity of the squares.

• left : Functor A A'

  the functor on the left component

• base : Functor B B'

  the functor on the base component

• right : Functor C C'

  the functor on the right component

• squareLeft : CatCommSq F self.left self.base F'

  a CatCommSq bundling the natural isomorphism F ⋙ base ≅ left ⋙ F'.

• squareRight : CatCommSq G self.right self.base G'

  a CatCommSq bundling the natural isomorphism G ⋙ base ≅ right ⋙ G'.

def CategoryTheory.Limits.CatCospanTransform.id {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor C B) : CatCospanTransform F G F G

The identity CatCospanTransform

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.id_squareRight {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor C B) : (id F G).squareRight = inferInstance

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.id_left {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor C B) : (id F G).left = Functor.id A

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.id_squareLeft {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor C B) : (id F G).squareLeft = inferInstance

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.id_right {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor C B) : (id F G).right = Functor.id C

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.id_base {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor C B) : (id F G).base = Functor.id B

def CategoryTheory.Limits.CatCospanTransform.comp {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (ψ : CatCospanTransform F G F' G') (ψ' : CatCospanTransform F' G' F'' G'') : CatCospanTransform F G F'' G''

Composition of CatCospanTransforms is defined "componentwise".

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.comp_base {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (ψ : CatCospanTransform F G F' G') (ψ' : CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').base = ψ.base.comp ψ'.base

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.comp_right {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (ψ : CatCospanTransform F G F' G') (ψ' : CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').right = ψ.right.comp ψ'.right

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.comp_squareRight {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (ψ : CatCospanTransform F G F' G') (ψ' : CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').squareRight = ψ.squareRight.vComp' ψ'.squareRight

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.comp_left {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (ψ : CatCospanTransform F G F' G') (ψ' : CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').left = ψ.left.comp ψ'.left

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.comp_squareLeft {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (ψ : CatCospanTransform F G F' G') (ψ' : CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').squareLeft = ψ.squareLeft.vComp' ψ'.squareLeft

structure CategoryTheory.Limits.CatCospanTransformMorphism {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (ψ ψ' : CatCospanTransform F G F' G') : Type (max (max (max (max (max u₁ u₂) u₃) v₄) v₅) v₆)

A morphism of CatCospanTransform F G F' G' is a triple of natural transformations between the component functors, subjects to coherence conditions respective to the squares.

• left : ψ.left ⟶ ψ'.left

  the natural transformations between the left components

• right : ψ.right ⟶ ψ'.right

  the natural transformations between the right components

• base : ψ.base ⟶ ψ'.base

  the natural transformations between the base components

• left_coherence : CategoryStruct.comp (CatCommSq.iso F ψ.left ψ.base F').hom (Functor.whiskerRight self.left F') = CategoryStruct.comp (F.whiskerLeft self.base) (CatCommSq.iso F ψ'.left ψ'.base F').hom

  the coherence condition for the left square

• right_coherence : CategoryStruct.comp (CatCommSq.iso G ψ.right ψ.base G').hom (Functor.whiskerRight self.right G') = CategoryStruct.comp (G.whiskerLeft self.base) (CatCommSq.iso G ψ'.right ψ'.base G').hom

  the coherence condition for the right square

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (self : CatCospanTransformMorphism ψ ψ') {Z : Functor C B'} (h : ψ'.right.comp G' ⟶ Z) : CategoryStruct.comp (CatCommSq.iso G ψ.right ψ.base G').hom (CategoryStruct.comp (Functor.whiskerRight self.right G') h) = CategoryStruct.comp (G.whiskerLeft self.base) (CategoryStruct.comp (CatCommSq.iso G ψ'.right ψ'.base G').hom h)

the coherence condition for the right square

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (self : CatCospanTransformMorphism ψ ψ') {Z : Functor A B'} (h : ψ'.left.comp F' ⟶ Z) : CategoryStruct.comp (CatCommSq.iso F ψ.left ψ.base F').hom (CategoryStruct.comp (Functor.whiskerRight self.left F') h) = CategoryStruct.comp (F.whiskerLeft self.base) (CategoryStruct.comp (CatCommSq.iso F ψ'.left ψ'.base F').hom h)

the coherence condition for the left square

@[implicit_reducible]

instance CategoryTheory.Limits.CatCospanTransform.category {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} : Category.{max (max (max (max (max u₃ u₂) u₁) v₆) v₅) v₄, max (max (max (max (max (max (max (max (max (max (max u₆ u₅) u₄) u₃) u₂) u₁) v₆) v₅) v₄) v₃) v₂) v₁} (CatCospanTransform F G F' G')

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.category_id_base {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (ψ : CatCospanTransform F G F' G') : (CategoryStruct.id ψ).base = CategoryStruct.id ψ.base

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.category_id_left {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (ψ : CatCospanTransform F G F' G') : (CategoryStruct.id ψ).left = CategoryStruct.id ψ.left

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.category_id_right {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (ψ : CatCospanTransform F G F' G') : (CategoryStruct.id ψ).right = CategoryStruct.id ψ.right

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.category_comp_right {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {X✝ Y✝ Z✝ : CatCospanTransform F G F' G'} (α : CatCospanTransformMorphism X✝ Y✝) (β : CatCospanTransformMorphism Y✝ Z✝) : (CategoryStruct.comp α β).right = CategoryStruct.comp α.right β.right

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.category_comp_left {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {X✝ Y✝ Z✝ : CatCospanTransform F G F' G'} (α : CatCospanTransformMorphism X✝ Y✝) (β : CatCospanTransformMorphism Y✝ Z✝) : (CategoryStruct.comp α β).left = CategoryStruct.comp α.left β.left

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.category_comp_base {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {X✝ Y✝ Z✝ : CatCospanTransform F G F' G'} (α : CatCospanTransformMorphism X✝ Y✝) (β : CatCospanTransformMorphism Y✝ Z✝) : (CategoryStruct.comp α β).base = CategoryStruct.comp α.base β.base

theorem CategoryTheory.Limits.CatCospanTransformMorphism.ext_iff {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {inst✝ : Category.{v₁, u₁} A} {inst✝¹ : Category.{v₂, u₂} B} {inst✝² : Category.{v₃, u₃} C} {F : Functor A B} {G : Functor C B} {inst✝³ : Category.{v₄, u₄} A'} {inst✝⁴ : Category.{v₅, u₅} B'} {inst✝⁵ : Category.{v₆, u₆} C'} {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} {x y : CatCospanTransformMorphism ψ ψ'} : x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.base = y.base

theorem CategoryTheory.Limits.CatCospanTransformMorphism.ext {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {inst✝ : Category.{v₁, u₁} A} {inst✝¹ : Category.{v₂, u₂} B} {inst✝² : Category.{v₃, u₃} C} {F : Functor A B} {G : Functor C B} {inst✝³ : Category.{v₄, u₄} A'} {inst✝⁴ : Category.{v₅, u₅} B'} {inst✝⁵ : Category.{v₆, u₆} C'} {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} {x y : CatCospanTransformMorphism ψ ψ'} (left : x.left = y.left) (right : x.right = y.right) (base : x.base = y.base) : x = y

theorem CategoryTheory.Limits.CatCospanTransform.hom_ext {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} {θ θ' : ψ ⟶ ψ'} (hl : θ.left = θ'.left) (hr : θ.right = θ'.right) (hb : θ.base = θ'.base) : θ = θ'

theorem CategoryTheory.Limits.CatCospanTransform.hom_ext_iff {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} {θ θ' : ψ ⟶ ψ'} : θ = θ' ↔ θ.left = θ'.left ∧ θ.right = θ'.right ∧ θ.base = θ'.base

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : A) : CategoryStruct.comp ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) (F'.map (α.left.app x)) = CategoryStruct.comp (α.base.app (F.obj x)) ((CatCommSq.iso F ψ'.left ψ'.base F').hom.app x)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_app_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : A) {Z : B'} (h : F'.obj (ψ'.left.obj x) ⟶ Z) : CategoryStruct.comp ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) (CategoryStruct.comp (F'.map (α.left.app x)) h) = CategoryStruct.comp (α.base.app (F.obj x)) (CategoryStruct.comp ((CatCommSq.iso F ψ'.left ψ'.base F').hom.app x) h)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : C) : CategoryStruct.comp ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) (G'.map (α.right.app x)) = CategoryStruct.comp (α.base.app (G.obj x)) ((CatCommSq.iso G ψ'.right ψ'.base G').hom.app x)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_app_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : C) {Z : B'} (h : G'.obj (ψ'.right.obj x) ⟶ Z) : CategoryStruct.comp ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) (CategoryStruct.comp (G'.map (α.right.app x)) h) = CategoryStruct.comp (α.base.app (G.obj x)) (CategoryStruct.comp ((CatCommSq.iso G ψ'.right ψ'.base G').hom.app x) h)

def CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (φ : CatCospanTransform F G F' G') {ψ ψ' : CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ') : φ.comp ψ ⟶ φ.comp ψ'

Whiskering left of a CatCospanTransformMorphism by a CatCospanTransform.

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_left {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (φ : CatCospanTransform F G F' G') {ψ ψ' : CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ') : (whiskerLeft φ α).left = φ.left.whiskerLeft α.left

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_right {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (φ : CatCospanTransform F G F' G') {ψ ψ' : CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ') : (whiskerLeft φ α).right = φ.right.whiskerLeft α.right

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_base {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} (φ : CatCospanTransform F G F' G') {ψ ψ' : CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ') : (whiskerLeft φ α).base = φ.base.whiskerLeft α.base

def CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' : CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (φ : CatCospanTransform F' G' F'' G'') : ψ.comp φ ⟶ ψ'.comp φ

Whiskering right of a CatCospanTransformMorphism by a CatCospanTransform.

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_right {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' : CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (φ : CatCospanTransform F' G' F'' G'') : (whiskerRight α φ).right = Functor.whiskerRight α.right φ.right

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_left {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' : CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (φ : CatCospanTransform F' G' F'' G'') : (whiskerRight α φ).left = Functor.whiskerRight α.left φ.left

@[simp]

theorem CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_base {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' : CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (φ : CatCospanTransform F' G' F'' G'') : (whiskerRight α φ).base = Functor.whiskerRight α.base φ.base

def CategoryTheory.Limits.CatCospanTransform.mkIso {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryStruct.comp (CatCommSq.iso F ψ.left ψ.base F').hom (Functor.whiskerRight left.hom F') = CategoryStruct.comp (F.whiskerLeft base.hom) (CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryStruct.comp (CatCommSq.iso G ψ.right ψ.base G').hom (Functor.whiskerRight right.hom G') = CategoryStruct.comp (G.whiskerLeft base.hom) (CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : ψ ≅ ψ'

A constructor for isomorphisms of CatCospanTransform's.

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.mkIso_inv_left {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryStruct.comp (CatCommSq.iso F ψ.left ψ.base F').hom (Functor.whiskerRight left.hom F') = CategoryStruct.comp (F.whiskerLeft base.hom) (CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryStruct.comp (CatCommSq.iso G ψ.right ψ.base G').hom (Functor.whiskerRight right.hom G') = CategoryStruct.comp (G.whiskerLeft base.hom) (CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (mkIso left right base left_coherence right_coherence).inv.left = left.inv

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.mkIso_inv_right {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryStruct.comp (CatCommSq.iso F ψ.left ψ.base F').hom (Functor.whiskerRight left.hom F') = CategoryStruct.comp (F.whiskerLeft base.hom) (CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryStruct.comp (CatCommSq.iso G ψ.right ψ.base G').hom (Functor.whiskerRight right.hom G') = CategoryStruct.comp (G.whiskerLeft base.hom) (CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (mkIso left right base left_coherence right_coherence).inv.right = right.inv

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.mkIso_hom_base {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryStruct.comp (CatCommSq.iso F ψ.left ψ.base F').hom (Functor.whiskerRight left.hom F') = CategoryStruct.comp (F.whiskerLeft base.hom) (CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryStruct.comp (CatCommSq.iso G ψ.right ψ.base G').hom (Functor.whiskerRight right.hom G') = CategoryStruct.comp (G.whiskerLeft base.hom) (CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (mkIso left right base left_coherence right_coherence).hom.base = base.hom

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.mkIso_inv_base {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryStruct.comp (CatCommSq.iso F ψ.left ψ.base F').hom (Functor.whiskerRight left.hom F') = CategoryStruct.comp (F.whiskerLeft base.hom) (CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryStruct.comp (CatCommSq.iso G ψ.right ψ.base G').hom (Functor.whiskerRight right.hom G') = CategoryStruct.comp (G.whiskerLeft base.hom) (CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (mkIso left right base left_coherence right_coherence).inv.base = base.inv

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.mkIso_hom_left {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryStruct.comp (CatCommSq.iso F ψ.left ψ.base F').hom (Functor.whiskerRight left.hom F') = CategoryStruct.comp (F.whiskerLeft base.hom) (CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryStruct.comp (CatCommSq.iso G ψ.right ψ.base G').hom (Functor.whiskerRight right.hom G') = CategoryStruct.comp (G.whiskerLeft base.hom) (CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (mkIso left right base left_coherence right_coherence).hom.left = left.hom

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.mkIso_hom_right {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryStruct.comp (CatCommSq.iso F ψ.left ψ.base F').hom (Functor.whiskerRight left.hom F') = CategoryStruct.comp (F.whiskerLeft base.hom) (CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryStruct.comp (CatCommSq.iso G ψ.right ψ.base G').hom (Functor.whiskerRight right.hom G') = CategoryStruct.comp (G.whiskerLeft base.hom) (CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (mkIso left right base left_coherence right_coherence).hom.right = right.hom

instance CategoryTheory.Limits.CatCospanTransform.isIso_left {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ' : CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [IsIso f] : IsIso f.left

instance CategoryTheory.Limits.CatCospanTransform.isIso_right {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ' : CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [IsIso f] : IsIso f.right

instance CategoryTheory.Limits.CatCospanTransform.isIso_base {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ' : CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [IsIso f] : IsIso f.base

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.inv_left {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ' : CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [IsIso f] : inv f.left = (inv f).left

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.inv_right {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ' : CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [IsIso f] : inv f.right = (inv f).right

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.inv_base {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ' : CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [IsIso f] : inv f.base = (inv f).base

def CategoryTheory.Limits.CatCospanTransform.leftIso {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : ψ.left ≅ ψ'.left

Extract an isomorphism between left components from an isomorphism in CatCospanTransform F G F' G'.

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.leftIso_inv {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (leftIso e).inv = e.inv.left

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.leftIso_hom {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (leftIso e).hom = e.hom.left

def CategoryTheory.Limits.CatCospanTransform.rightIso {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : ψ.right ≅ ψ'.right

Extract an isomorphism between right components from an isomorphism in CatCospanTransform F G F' G'.

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.rightIso_inv {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (rightIso e).inv = e.inv.right

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.rightIso_hom {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (rightIso e).hom = e.hom.right

def CategoryTheory.Limits.CatCospanTransform.baseIso {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : ψ.base ≅ ψ'.base

Extract an isomorphism between base components from an isomorphism in CatCospanTransform F G F' G'.

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.baseIso_inv {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (baseIso e).inv = e.inv.base

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.baseIso_hom {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (baseIso e).hom = e.hom.base

theorem CategoryTheory.Limits.CatCospanTransform.isIso_iff {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ' : CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') : IsIso f ↔ IsIso f.left ∧ IsIso f.base ∧ IsIso f.right

def CategoryTheory.Limits.CatCospanTransform.leftUnitor {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') : (id F G).comp φ ≅ φ

The left unitor isomorphism for categorical cospan transformations.

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.leftUnitor_inv_left_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : A) : φ.leftUnitor.inv.left.app X = CategoryStruct.id (φ.left.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.leftUnitor_hom_right_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : C) : φ.leftUnitor.hom.right.app X = CategoryStruct.id (φ.right.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.leftUnitor_inv_base_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : B) : φ.leftUnitor.inv.base.app X = CategoryStruct.id (φ.base.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.leftUnitor_hom_left_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : A) : φ.leftUnitor.hom.left.app X = CategoryStruct.id (φ.left.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.leftUnitor_inv_right_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : C) : φ.leftUnitor.inv.right.app X = CategoryStruct.id (φ.right.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.leftUnitor_hom_base_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : B) : φ.leftUnitor.hom.base.app X = CategoryStruct.id (φ.base.obj X)

def CategoryTheory.Limits.CatCospanTransform.rightUnitor {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') : φ.comp (id F' G') ≅ φ

The right unitor isomorphism for categorical cospan transformations.

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.rightUnitor_hom_base_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : B) : φ.rightUnitor.hom.base.app X = CategoryStruct.id (φ.base.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.rightUnitor_inv_base_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : B) : φ.rightUnitor.inv.base.app X = CategoryStruct.id (φ.base.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.rightUnitor_hom_left_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : A) : φ.rightUnitor.hom.left.app X = CategoryStruct.id (φ.left.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.rightUnitor_inv_right_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : C) : φ.rightUnitor.inv.right.app X = CategoryStruct.id (φ.right.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.rightUnitor_inv_left_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : A) : φ.rightUnitor.inv.left.app X = CategoryStruct.id (φ.left.obj X)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.rightUnitor_hom_right_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} (φ : CatCospanTransform F G F' G') (X : C) : φ.rightUnitor.hom.right.app X = CategoryStruct.id (φ.right.obj X)

def CategoryTheory.Limits.CatCospanTransform.associator {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} (φ : CatCospanTransform F G F' G') (φ' : CatCospanTransform F' G' F'' G'') (φ'' : CatCospanTransform F'' G'' F''' G''') : (φ.comp φ').comp φ'' ≅ φ.comp (φ'.comp φ'')

The associator isomorphism for categorical cospan transformations.

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.associator_hom_base_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} (φ : CatCospanTransform F G F' G') (φ' : CatCospanTransform F' G' F'' G'') (φ'' : CatCospanTransform F'' G'' F''' G''') (x✝ : B) : (φ.associator φ' φ'').hom.base.app x✝ = CategoryStruct.id (φ''.base.obj (φ'.base.obj (φ.base.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.associator_inv_base_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} (φ : CatCospanTransform F G F' G') (φ' : CatCospanTransform F' G' F'' G'') (φ'' : CatCospanTransform F'' G'' F''' G''') (x✝ : B) : (φ.associator φ' φ'').inv.base.app x✝ = CategoryStruct.id (φ''.base.obj (φ'.base.obj (φ.base.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.associator_hom_left_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} (φ : CatCospanTransform F G F' G') (φ' : CatCospanTransform F' G' F'' G'') (φ'' : CatCospanTransform F'' G'' F''' G''') (x✝ : A) : (φ.associator φ' φ'').hom.left.app x✝ = CategoryStruct.id (φ''.left.obj (φ'.left.obj (φ.left.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.associator_inv_left_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} (φ : CatCospanTransform F G F' G') (φ' : CatCospanTransform F' G' F'' G'') (φ'' : CatCospanTransform F'' G'' F''' G''') (x✝ : A) : (φ.associator φ' φ'').inv.left.app x✝ = CategoryStruct.id (φ''.left.obj (φ'.left.obj (φ.left.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.associator_inv_right_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} (φ : CatCospanTransform F G F' G') (φ' : CatCospanTransform F' G' F'' G'') (φ'' : CatCospanTransform F'' G'' F''' G''') (x✝ : C) : (φ.associator φ' φ'').inv.right.app x✝ = CategoryStruct.id (φ''.right.obj (φ'.right.obj (φ.right.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.associator_hom_right_app {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} (φ : CatCospanTransform F G F' G') (φ' : CatCospanTransform F' G' F'' G'') (φ'' : CatCospanTransform F'' G'' F''' G''') (x✝ : C) : (φ.associator φ' φ'').hom.right.app x✝ = CategoryStruct.id (φ''.right.obj (φ'.right.obj (φ.right.obj x✝)))

def CategoryTheory.Limits.CatCospanTransform.«term_◁_» : Lean.TrailingParserDescr

Whiskering left of a CatCospanTransformMorphism by a CatCospanTransform.

def CategoryTheory.Limits.CatCospanTransform.«term_▷_» : Lean.TrailingParserDescr

Whiskering right of a CatCospanTransformMorphism by a CatCospanTransform.

def CategoryTheory.Limits.CatCospanTransform.termα_ : Lean.ParserDescr

The associator isomorphism for categorical cospan transformations.

def CategoryTheory.Limits.CatCospanTransform.«termλ_» : Lean.ParserDescr

The left unitor isomorphism for categorical cospan transformations.

def CategoryTheory.Limits.CatCospanTransform.termρ_ : Lean.ParserDescr

The right unitor isomorphism for categorical cospan transformations.

theorem CategoryTheory.Limits.CatCospanTransform.whisker_exchange {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {φ φ' : CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') : CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ θ) (CatCospanTransformMorphism.whiskerRight η φ') = CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight η φ) (CatCospanTransformMorphism.whiskerLeft ψ' θ)

theorem CategoryTheory.Limits.CatCospanTransform.whisker_exchange_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {φ φ' : CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') {Z : CatCospanTransform F G F'' G''} (h : ψ'.comp φ' ⟶ Z) : CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ θ) (CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight η φ') h) = CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight η φ) (CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ' θ) h)

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.id_whiskerRight {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} : CatCospanTransformMorphism.whiskerRight (CategoryStruct.id ψ) φ = CategoryStruct.id (ψ.comp φ)

theorem CategoryTheory.Limits.CatCospanTransform.whiskerRight_id {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') : CatCospanTransformMorphism.whiskerRight η (id F' G') = CategoryStruct.comp ψ.rightUnitor.hom (CategoryStruct.comp η ψ'.rightUnitor.inv)

theorem CategoryTheory.Limits.CatCospanTransform.whiskerRight_id_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {Z : CatCospanTransform F G F' G'} (h : ψ'.comp (id F' G') ⟶ Z) : CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight η (id F' G')) h = CategoryStruct.comp ψ.rightUnitor.hom (CategoryStruct.comp η (CategoryStruct.comp ψ'.rightUnitor.inv h))

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' ψ'' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') (η' : ψ' ⟶ ψ'') {φ : CatCospanTransform F' G' F'' G''} : CatCospanTransformMorphism.whiskerRight (CategoryStruct.comp η η') φ = CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight η φ) (CatCospanTransformMorphism.whiskerRight η' φ)

theorem CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' ψ'' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') (η' : ψ' ⟶ ψ'') {φ : CatCospanTransform F' G' F'' G''} {Z : CatCospanTransform F G F'' G''} (h : ψ''.comp φ ⟶ Z) : CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight (CategoryStruct.comp η η') φ) h = CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight η φ) (CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight η' φ) h)

theorem CategoryTheory.Limits.CatCospanTransform.whiskerRight_comp {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {φ : CatCospanTransform F' G' F'' G''} {τ : CatCospanTransform F'' G'' F''' G'''} : CatCospanTransformMorphism.whiskerRight η (φ.comp τ) = CategoryStruct.comp (ψ.associator φ τ).inv (CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight (CatCospanTransformMorphism.whiskerRight η φ) τ) (ψ'.associator φ τ).hom)

theorem CategoryTheory.Limits.CatCospanTransform.whiskerRight_comp_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {φ : CatCospanTransform F' G' F'' G''} {τ : CatCospanTransform F'' G'' F''' G'''} {Z : CatCospanTransform F G F''' G'''} (h : ψ'.comp (φ.comp τ) ⟶ Z) : CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight η (φ.comp τ)) h = CategoryStruct.comp (ψ.associator φ τ).inv (CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight (CatCospanTransformMorphism.whiskerRight η φ) τ) (CategoryStruct.comp (ψ'.associator φ τ).hom h))

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.whiskerleft_id {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} : CatCospanTransformMorphism.whiskerLeft ψ (CategoryStruct.id φ) = CategoryStruct.id (ψ.comp φ)

theorem CategoryTheory.Limits.CatCospanTransform.id_whiskerLeft {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') : CatCospanTransformMorphism.whiskerLeft (id F G) η = CategoryStruct.comp ψ.leftUnitor.hom (CategoryStruct.comp η ψ'.leftUnitor.inv)

theorem CategoryTheory.Limits.CatCospanTransform.id_whiskerLeft_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {Z : CatCospanTransform F G F' G'} (h : (id F G).comp ψ' ⟶ Z) : CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft (id F G) η) h = CategoryStruct.comp ψ.leftUnitor.hom (CategoryStruct.comp η (CategoryStruct.comp ψ'.leftUnitor.inv h))

@[simp]

theorem CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ φ' φ'' : CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') (θ' : φ' ⟶ φ'') : CatCospanTransformMorphism.whiskerLeft ψ (CategoryStruct.comp θ θ') = CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ θ) (CatCospanTransformMorphism.whiskerLeft ψ θ')

theorem CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ φ' φ'' : CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') (θ' : φ' ⟶ φ'') {Z : CatCospanTransform F G F'' G''} (h : ψ.comp φ'' ⟶ Z) : CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ (CategoryStruct.comp θ θ')) h = CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ θ) (CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ θ') h)

theorem CategoryTheory.Limits.CatCospanTransform.comp_whiskerLeft {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} {τ τ' : CatCospanTransform F'' G'' F''' G'''} (γ : τ ⟶ τ') : CatCospanTransformMorphism.whiskerLeft (ψ.comp φ) γ = CategoryStruct.comp (ψ.associator φ τ).hom (CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ (CatCospanTransformMorphism.whiskerLeft φ γ)) (ψ.associator φ τ').inv)

theorem CategoryTheory.Limits.CatCospanTransform.comp_whiskerLeft_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} {τ τ' : CatCospanTransform F'' G'' F''' G'''} (γ : τ ⟶ τ') {Z : CatCospanTransform F G F''' G'''} (h : (ψ.comp φ).comp τ' ⟶ Z) : CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft (ψ.comp φ) γ) h = CategoryStruct.comp (ψ.associator φ τ).hom (CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ (CatCospanTransformMorphism.whiskerLeft φ γ)) (CategoryStruct.comp (ψ.associator φ τ').inv h))

theorem CategoryTheory.Limits.CatCospanTransform.pentagon {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} {τ : CatCospanTransform F'' G'' F''' G'''} {A'''' : Type u₁₃} {B'''' : Type u₁₄} {C'''' : Type u₁₅} [Category.{v₁₃, u₁₃} A''''] [Category.{v₁₄, u₁₄} B''''] [Category.{v₁₅, u₁₅} C''''] {F'''' : Functor A'''' B''''} {G'''' : Functor C'''' B''''} {σ : CatCospanTransform F''' G''' F'''' G''''} : CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight (ψ.associator φ τ).hom σ) (CategoryStruct.comp (ψ.associator (φ.comp τ) σ).hom (CatCospanTransformMorphism.whiskerLeft ψ (φ.associator τ σ).hom)) = CategoryStruct.comp ((ψ.comp φ).associator τ σ).hom (ψ.associator φ (τ.comp σ)).hom

theorem CategoryTheory.Limits.CatCospanTransform.pentagon_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [Category.{v₁₀, u₁₀} A'''] [Category.{v₁₁, u₁₁} B'''] [Category.{v₁₂, u₁₂} C'''] {F''' : Functor A''' B'''} {G''' : Functor C''' B'''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} {τ : CatCospanTransform F'' G'' F''' G'''} {A'''' : Type u₁₃} {B'''' : Type u₁₄} {C'''' : Type u₁₅} [Category.{v₁₃, u₁₃} A''''] [Category.{v₁₄, u₁₄} B''''] [Category.{v₁₅, u₁₅} C''''] {F'''' : Functor A'''' B''''} {G'''' : Functor C'''' B''''} {σ : CatCospanTransform F''' G''' F'''' G''''} {Z : CatCospanTransform F G F'''' G''''} (h : ψ.comp (φ.comp (τ.comp σ)) ⟶ Z) : CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight (ψ.associator φ τ).hom σ) (CategoryStruct.comp (ψ.associator (φ.comp τ) σ).hom (CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ (φ.associator τ σ).hom) h)) = CategoryStruct.comp ((ψ.comp φ).associator τ σ).hom (CategoryStruct.comp (ψ.associator φ (τ.comp σ)).hom h)

theorem CategoryTheory.Limits.CatCospanTransform.triangle {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} : CategoryStruct.comp (ψ.associator (id F' G') φ).hom (CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom) = CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ

theorem CategoryTheory.Limits.CatCospanTransform.triangle_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} {Z : CatCospanTransform F G F'' G''} (h : ψ.comp φ ⟶ Z) : CategoryStruct.comp (ψ.associator (id F' G') φ).hom (CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom) h) = CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ) h

theorem CategoryTheory.Limits.CatCospanTransform.triangle_inv {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} : CategoryStruct.comp (ψ.associator (id F' G') φ).inv (CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ) = CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom

theorem CategoryTheory.Limits.CatCospanTransform.triangle_inv_assoc {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ : CatCospanTransform F' G' F'' G''} {Z : CatCospanTransform F G F'' G''} (h : ψ.comp φ ⟶ Z) : CategoryStruct.comp (ψ.associator (id F' G') φ).inv (CategoryStruct.comp (CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ) h) = CategoryStruct.comp (CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom) h

instance CategoryTheory.Limits.CatCospanTransform.instIsIsoWhiskerLeft {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ φ' : CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') [IsIso θ] : IsIso (CatCospanTransformMorphism.whiskerLeft ψ θ)

theorem CategoryTheory.Limits.CatCospanTransform.inv_whiskerLeft {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ : CatCospanTransform F G F' G'} {φ φ' : CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') [IsIso θ] : inv (CatCospanTransformMorphism.whiskerLeft ψ θ) = CatCospanTransformMorphism.whiskerLeft ψ (inv θ)

instance CategoryTheory.Limits.CatCospanTransform.instIsIsoWhiskerRight {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') [IsIso η] {φ : CatCospanTransform F' G' F'' G''} : IsIso (CatCospanTransformMorphism.whiskerRight η φ)

theorem CategoryTheory.Limits.CatCospanTransform.inv_whiskerRight {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {F : Functor A B} {G : Functor C B} [Category.{v₄, u₄} A'] [Category.{v₅, u₅} B'] [Category.{v₆, u₆} C'] {F' : Functor A' B'} {G' : Functor C' B'} [Category.{v₇, u₇} A''] [Category.{v₈, u₈} B''] [Category.{v₉, u₉} C''] {F'' : Functor A'' B''} {G'' : Functor C'' B''} {ψ ψ' : CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') [IsIso η] {φ : CatCospanTransform F' G' F'' G''} : inv (CatCospanTransformMorphism.whiskerRight η φ) = CatCospanTransformMorphism.whiskerRight (inv η) φ