Loogle!

Result

Found 158 declarations mentioning CategoryTheory.Limits.CatCospanTransform.

• CategoryTheory.Limits.CatCospanTransform.id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) : CategoryTheory.Limits.CatCospanTransform F G F G
• CategoryTheory.Limits.CatCospanTransform 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] (F' : CategoryTheory.Functor A' B') (G' : CategoryTheory.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₆)
• CategoryTheory.Limits.CatCospanTransform.category 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} : CategoryTheory.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₁} (CategoryTheory.Limits.CatCospanTransform F G F' G')
• CategoryTheory.Limits.CatCospanTransform.base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (self : CategoryTheory.Limits.CatCospanTransform F G F' G') : CategoryTheory.Functor B B'
• CategoryTheory.Limits.CatCospanTransform.left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (self : CategoryTheory.Limits.CatCospanTransform F G F' G') : CategoryTheory.Functor A A'
• CategoryTheory.Limits.CatCospanTransform.right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (self : CategoryTheory.Limits.CatCospanTransform F G F' G') : CategoryTheory.Functor C C'
• CategoryTheory.Limits.CatCospanTransformMorphism 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G') : Type (max (max (max (max (max u₁ u₂) u₃) v₄) v₅) v₆)
• CategoryTheory.Limits.CatCospanTransform.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (left : CategoryTheory.Functor A A') (base : CategoryTheory.Functor B B') (right : CategoryTheory.Functor C C') (squareLeft : CategoryTheory.CatCommSq F left base F' := by infer_instance) (squareRight : CategoryTheory.CatCommSq G right base G' := by infer_instance) : CategoryTheory.Limits.CatCospanTransform F G F' G'
• CategoryTheory.Limits.CatCospanTransform.squareLeft 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (self : CategoryTheory.Limits.CatCospanTransform F G F' G') : CategoryTheory.CatCommSq F self.left self.base F'
• CategoryTheory.Limits.CatCospanTransform.squareRight 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (self : CategoryTheory.Limits.CatCospanTransform F G F' G') : CategoryTheory.CatCommSq G self.right self.base G'
• CategoryTheory.Limits.CatCospanTransform.comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G') (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : CategoryTheory.Limits.CatCospanTransform F G F'' G''
• CategoryTheory.Limits.CatCospanTransform.leftUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') : (CategoryTheory.Limits.CatCospanTransform.id F G).comp φ ≅ φ
• CategoryTheory.Limits.CatCospanTransform.rightUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') : φ.comp (CategoryTheory.Limits.CatCospanTransform.id F' G') ≅ φ
• CategoryTheory.Limits.CatCospanTransformMorphism.base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ') : ψ.base ⟶ ψ'.base
• CategoryTheory.Limits.CatCospanTransformMorphism.left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ') : ψ.left ⟶ ψ'.left
• CategoryTheory.Limits.CatCospanTransformMorphism.right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ') : ψ.right ⟶ ψ'.right
• CategoryTheory.Limits.CatCospanTransform.baseIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : ψ.base ≅ ψ'.base
• CategoryTheory.Limits.CatCospanTransform.leftIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : ψ.left ≅ ψ'.left
• CategoryTheory.Limits.CatCospanTransform.rightIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : ψ.right ≅ ψ'.right
• CategoryTheory.Limits.CatCospanTransform.comp_base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G') (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').base = ψ.base.comp ψ'.base
• CategoryTheory.Limits.CatCospanTransform.comp_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G') (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').left = ψ.left.comp ψ'.left
• CategoryTheory.Limits.CatCospanTransform.comp_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G') (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').right = ψ.right.comp ψ'.right
• CategoryTheory.Limits.CatCospanTransform.category_id_base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G') : (CategoryTheory.CategoryStruct.id ψ).base = CategoryTheory.CategoryStruct.id ψ.base
• CategoryTheory.Limits.CatCospanTransform.category_id_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G') : (CategoryTheory.CategoryStruct.id ψ).left = CategoryTheory.CategoryStruct.id ψ.left
• CategoryTheory.Limits.CatCospanTransform.category_id_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G') : (CategoryTheory.CategoryStruct.id ψ).right = CategoryTheory.CategoryStruct.id ψ.right
• CategoryTheory.Limits.CatCospanTransform.isIso_base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.base
• CategoryTheory.Limits.CatCospanTransform.isIso_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.left
• CategoryTheory.Limits.CatCospanTransform.isIso_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.right
• CategoryTheory.Limits.CatCospanTransform.associator 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') : (φ.comp φ').comp φ'' ≅ φ.comp (φ'.comp φ'')
• CategoryTheory.Limits.CatCospanTransform.baseIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (CategoryTheory.Limits.CatCospanTransform.baseIso e).hom = e.hom.base
• CategoryTheory.Limits.CatCospanTransform.baseIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (CategoryTheory.Limits.CatCospanTransform.baseIso e).inv = e.inv.base
• CategoryTheory.Limits.CatCospanTransform.leftIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (CategoryTheory.Limits.CatCospanTransform.leftIso e).hom = e.hom.left
• CategoryTheory.Limits.CatCospanTransform.leftIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (CategoryTheory.Limits.CatCospanTransform.leftIso e).inv = e.inv.left
• CategoryTheory.Limits.CatCospanTransform.rightIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (CategoryTheory.Limits.CatCospanTransform.rightIso e).hom = e.hom.right
• CategoryTheory.Limits.CatCospanTransform.rightIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ') : (CategoryTheory.Limits.CatCospanTransform.rightIso e).inv = e.inv.right
• CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ') : φ.comp ψ ⟶ φ.comp ψ'
• CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : ψ.comp φ ⟶ ψ'.comp φ
• CategoryTheory.Limits.CatCospanTransform.instIsIsoWhiskerLeft 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') [CategoryTheory.IsIso θ] : CategoryTheory.IsIso (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ)
• CategoryTheory.Limits.CatCospanTransform.instIsIsoWhiskerRight 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') [CategoryTheory.IsIso η] {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} : CategoryTheory.IsIso (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ)
• CategoryTheory.Limits.CatCospanTransform.comp_squareLeft 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G') (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').squareLeft = ψ.squareLeft.vComp' ψ'.squareLeft
• CategoryTheory.Limits.CatCospanTransform.comp_squareRight 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {A'' : Type u₇} {B'' : Type u₈} {C'' : Type u₉} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G') (ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : (ψ.comp ψ').squareRight = ψ.squareRight.vComp' ψ'.squareRight
• CategoryTheory.Limits.CatCospanTransform.leftUnitor_hom_base_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : B) : φ.leftUnitor.hom.base.app X = CategoryTheory.CategoryStruct.id (φ.base.obj X)
• CategoryTheory.Limits.CatCospanTransform.leftUnitor_hom_left_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : A) : φ.leftUnitor.hom.left.app X = CategoryTheory.CategoryStruct.id (φ.left.obj X)
• CategoryTheory.Limits.CatCospanTransform.leftUnitor_hom_right_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : C) : φ.leftUnitor.hom.right.app X = CategoryTheory.CategoryStruct.id (φ.right.obj X)
• CategoryTheory.Limits.CatCospanTransform.leftUnitor_inv_base_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : B) : φ.leftUnitor.inv.base.app X = CategoryTheory.CategoryStruct.id (φ.base.obj X)
• CategoryTheory.Limits.CatCospanTransform.leftUnitor_inv_left_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : A) : φ.leftUnitor.inv.left.app X = CategoryTheory.CategoryStruct.id (φ.left.obj X)
• CategoryTheory.Limits.CatCospanTransform.leftUnitor_inv_right_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : C) : φ.leftUnitor.inv.right.app X = CategoryTheory.CategoryStruct.id (φ.right.obj X)
• CategoryTheory.Limits.CatCospanTransform.rightUnitor_hom_base_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : B) : φ.rightUnitor.hom.base.app X = CategoryTheory.CategoryStruct.id (φ.base.obj X)
• CategoryTheory.Limits.CatCospanTransform.rightUnitor_hom_left_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : A) : φ.rightUnitor.hom.left.app X = CategoryTheory.CategoryStruct.id (φ.left.obj X)
• CategoryTheory.Limits.CatCospanTransform.rightUnitor_hom_right_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : C) : φ.rightUnitor.hom.right.app X = CategoryTheory.CategoryStruct.id (φ.right.obj X)
• CategoryTheory.Limits.CatCospanTransform.rightUnitor_inv_base_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : B) : φ.rightUnitor.inv.base.app X = CategoryTheory.CategoryStruct.id (φ.base.obj X)
• CategoryTheory.Limits.CatCospanTransform.rightUnitor_inv_left_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : A) : φ.rightUnitor.inv.left.app X = CategoryTheory.CategoryStruct.id (φ.left.obj X)
• CategoryTheory.Limits.CatCospanTransform.rightUnitor_inv_right_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : C) : φ.rightUnitor.inv.right.app X = CategoryTheory.CategoryStruct.id (φ.right.obj X)
• CategoryTheory.Limits.CatCospanTransform.isIso_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.left ∧ CategoryTheory.IsIso f.base ∧ CategoryTheory.IsIso f.right
• CategoryTheory.Limits.CatCospanTransform.inv_base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [CategoryTheory.IsIso f] : CategoryTheory.inv f.base = (CategoryTheory.inv f).base
• CategoryTheory.Limits.CatCospanTransform.inv_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [CategoryTheory.IsIso f] : CategoryTheory.inv f.left = (CategoryTheory.inv f).left
• CategoryTheory.Limits.CatCospanTransform.inv_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [CategoryTheory.IsIso f] : CategoryTheory.inv f.right = (CategoryTheory.inv f).right
• CategoryTheory.Limits.CatCospanTransform.category_comp_base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {X✝ Y✝ Z✝ : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : CategoryTheory.Limits.CatCospanTransformMorphism X✝ Y✝) (β : CategoryTheory.Limits.CatCospanTransformMorphism Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp α β).base = CategoryTheory.CategoryStruct.comp α.base β.base
• CategoryTheory.Limits.CatCospanTransform.category_comp_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {X✝ Y✝ Z✝ : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : CategoryTheory.Limits.CatCospanTransformMorphism X✝ Y✝) (β : CategoryTheory.Limits.CatCospanTransformMorphism Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp α β).left = CategoryTheory.CategoryStruct.comp α.left β.left
• CategoryTheory.Limits.CatCospanTransform.category_comp_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {X✝ Y✝ Z✝ : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : CategoryTheory.Limits.CatCospanTransformMorphism X✝ Y✝) (β : CategoryTheory.Limits.CatCospanTransformMorphism Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp α β).right = CategoryTheory.CategoryStruct.comp α.right β.right
• CategoryTheory.Limits.CatCospanTransform.id_whiskerRight 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} : CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.CategoryStruct.id ψ) φ = CategoryTheory.CategoryStruct.id (ψ.comp φ)
• CategoryTheory.Limits.CatCospanTransform.whiskerleft_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} : CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.CategoryStruct.id φ) = CategoryTheory.CategoryStruct.id (ψ.comp φ)
• CategoryTheory.Limits.CatCospanTransformMorphism.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {inst✝ : CategoryTheory.Category.{v₁, u₁} A} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} B} {inst✝² : CategoryTheory.Category.{v₃, u₃} C} {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {inst✝³ : CategoryTheory.Category.{v₄, u₄} A'} {inst✝⁴ : CategoryTheory.Category.{v₅, u₅} B'} {inst✝⁵ : CategoryTheory.Category.{v₆, u₆} C'} {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} {x y : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ'} (left : x.left = y.left) (right : x.right = y.right) (base : x.base = y.base) : x = y
• CategoryTheory.Limits.CatCospanTransformMorphism.ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {inst✝ : CategoryTheory.Category.{v₁, u₁} A} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} B} {inst✝² : CategoryTheory.Category.{v₃, u₃} C} {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {inst✝³ : CategoryTheory.Category.{v₄, u₄} A'} {inst✝⁴ : CategoryTheory.Category.{v₅, u₅} B'} {inst✝⁵ : CategoryTheory.Category.{v₆, u₆} C'} {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} {x y : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ'} : x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.base = y.base
• CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ') : (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ α).base = φ.base.whiskerLeft α.base
• CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ') : (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ α).left = φ.left.whiskerLeft α.left
• CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ') : (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ α).right = φ.right.whiskerLeft α.right
• CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight α φ).base = CategoryTheory.Functor.whiskerRight α.base φ.base
• CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight α φ).left = CategoryTheory.Functor.whiskerRight α.left φ.left
• CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') : (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight α φ).right = CategoryTheory.Functor.whiskerRight α.right φ.right
• CategoryTheory.Limits.CatCospanTransform.inv_whiskerLeft 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') [CategoryTheory.IsIso θ] : CategoryTheory.inv (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ) = CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.inv θ)
• CategoryTheory.Limits.CatCospanTransform.inv_whiskerRight 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') [CategoryTheory.IsIso η] {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} : CategoryTheory.inv (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) = CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.inv η) φ
• CategoryTheory.Limits.CatCospanTransform.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} {θ θ' : ψ ⟶ ψ'} (hl : θ.left = θ'.left) (hr : θ.right = θ'.right) (hb : θ.base = θ'.base) : θ = θ'
• CategoryTheory.Limits.CatCospanTransform.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} {θ θ' : ψ ⟶ ψ'} : θ = θ' ↔ θ.left = θ'.left ∧ θ.right = θ'.right ∧ θ.base = θ'.base
• CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' ψ'' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') (η' : ψ' ⟶ ψ'') {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} : CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.CategoryStruct.comp η η') φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η' φ)
• CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ φ' φ'' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') (θ' : φ' ⟶ φ'') : CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.CategoryStruct.comp θ θ') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ) (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ')
• CategoryTheory.Limits.CatCospanTransform.id_whiskerLeft 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') : CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft (CategoryTheory.Limits.CatCospanTransform.id F G) η = CategoryTheory.CategoryStruct.comp ψ.leftUnitor.hom (CategoryTheory.CategoryStruct.comp η ψ'.leftUnitor.inv)
• CategoryTheory.Limits.CatCospanTransform.whiskerRight_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') : CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η (CategoryTheory.Limits.CatCospanTransform.id F' G') = CategoryTheory.CategoryStruct.comp ψ.rightUnitor.hom (CategoryTheory.CategoryStruct.comp η ψ'.rightUnitor.inv)
• CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ') : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.Functor.whiskerRight self.left F') = CategoryTheory.CategoryStruct.comp (F.whiskerLeft self.base) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom
• CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ') : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.Functor.whiskerRight self.right G') = CategoryTheory.CategoryStruct.comp (G.whiskerLeft self.base) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom
• CategoryTheory.Limits.CatCospanTransform.whisker_exchange 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {φ φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ) (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ' θ)
• CategoryTheory.Limits.CatCospanTransform.associator_hom_base_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x✝ : B) : (φ.associator φ' φ'').hom.base.app x✝ = CategoryTheory.CategoryStruct.id (φ''.base.obj (φ'.base.obj (φ.base.obj x✝)))
• CategoryTheory.Limits.CatCospanTransform.associator_hom_left_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x✝ : A) : (φ.associator φ' φ'').hom.left.app x✝ = CategoryTheory.CategoryStruct.id (φ''.left.obj (φ'.left.obj (φ.left.obj x✝)))
• CategoryTheory.Limits.CatCospanTransform.associator_hom_right_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x✝ : C) : (φ.associator φ' φ'').hom.right.app x✝ = CategoryTheory.CategoryStruct.id (φ''.right.obj (φ'.right.obj (φ.right.obj x✝)))
• CategoryTheory.Limits.CatCospanTransform.associator_inv_base_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x✝ : B) : (φ.associator φ' φ'').inv.base.app x✝ = CategoryTheory.CategoryStruct.id (φ''.base.obj (φ'.base.obj (φ.base.obj x✝)))
• CategoryTheory.Limits.CatCospanTransform.associator_inv_left_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x✝ : A) : (φ.associator φ' φ'').inv.left.app x✝ = CategoryTheory.CategoryStruct.id (φ''.left.obj (φ'.left.obj (φ.left.obj x✝)))
• CategoryTheory.Limits.CatCospanTransform.associator_inv_right_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'') (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x✝ : C) : (φ.associator φ' φ'').inv.right.app x✝ = CategoryTheory.CategoryStruct.id (φ''.right.obj (φ'.right.obj (φ.right.obj x✝)))
• CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ') {Z : CategoryTheory.Functor A B'} (h : ψ'.left.comp F' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.left F') h) = CategoryTheory.CategoryStruct.comp (F.whiskerLeft self.base) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom h)
• CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ') {Z : CategoryTheory.Functor C B'} (h : ψ'.right.comp G' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.right G') h) = CategoryTheory.CategoryStruct.comp (G.whiskerLeft self.base) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom h)
• CategoryTheory.Limits.CatCospanTransform.id_whiskerLeft_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {Z : CategoryTheory.Limits.CatCospanTransform F G F' G'} (h : (CategoryTheory.Limits.CatCospanTransform.id F G).comp ψ' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft (CategoryTheory.Limits.CatCospanTransform.id F G) η) h = CategoryTheory.CategoryStruct.comp ψ.leftUnitor.hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp ψ'.leftUnitor.inv h))
• CategoryTheory.Limits.CatCospanTransform.whiskerRight_id_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {Z : CategoryTheory.Limits.CatCospanTransform F G F' G'} (h : ψ'.comp (CategoryTheory.Limits.CatCospanTransform.id F' G') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η (CategoryTheory.Limits.CatCospanTransform.id F' G')) h = CategoryTheory.CategoryStruct.comp ψ.rightUnitor.hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp ψ'.rightUnitor.inv h))
• CategoryTheory.Limits.CatCospanTransform.triangle 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} : CategoryTheory.CategoryStruct.comp (ψ.associator (CategoryTheory.Limits.CatCospanTransform.id F' G') φ).hom (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom) = CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ
• CategoryTheory.Limits.CatCospanTransform.triangle_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} : CategoryTheory.CategoryStruct.comp (ψ.associator (CategoryTheory.Limits.CatCospanTransform.id F' G') φ).inv (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ) = CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom
• CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' ψ'' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') (η' : ψ' ⟶ ψ'') {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ''.comp φ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.CategoryStruct.comp η η') φ) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η' φ) h)
• CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ φ' φ'' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') (θ' : φ' ⟶ φ'') {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ.comp φ'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.CategoryStruct.comp θ θ')) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ') h)
• CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : A) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom.app x) (F'.map (α.left.app x)) = CategoryTheory.CategoryStruct.comp (α.base.app (F.obj x)) ((CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom.app x)
• CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom.app x) (G'.map (α.right.app x)) = CategoryTheory.CategoryStruct.comp (α.base.app (G.obj x)) ((CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom.app x)
• CategoryTheory.Limits.CatCospanTransform.whisker_exchange_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {φ φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ'.comp φ' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ' θ) h)
• CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_app_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : A) {Z : B'} (h : F'.obj (ψ'.left.obj x) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom.app x) (CategoryTheory.CategoryStruct.comp (F'.map (α.left.app x)) h) = CategoryTheory.CategoryStruct.comp (α.base.app (F.obj x)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom.app x) h)
• CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_app_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') (x : C) {Z : B'} (h : G'.obj (ψ'.right.obj x) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom.app x) (CategoryTheory.CategoryStruct.comp (G'.map (α.right.app x)) h) = CategoryTheory.CategoryStruct.comp (α.base.app (G.obj x)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom.app x) h)
• CategoryTheory.Limits.CatCospanTransform.triangle_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ.comp φ ⟶ Z) : CategoryTheory.CategoryStruct.comp (ψ.associator (CategoryTheory.Limits.CatCospanTransform.id F' G') φ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ) h
• CategoryTheory.Limits.CatCospanTransform.triangle_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ.comp φ ⟶ Z) : CategoryTheory.CategoryStruct.comp (ψ.associator (CategoryTheory.Limits.CatCospanTransform.id F' G') φ).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom) h
• CategoryTheory.Limits.CatCospanTransform.comp_whiskerLeft 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} {τ τ' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} (γ : τ ⟶ τ') : CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft (ψ.comp φ) γ = CategoryTheory.CategoryStruct.comp (ψ.associator φ τ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ γ)) (ψ.associator φ τ').inv)
• CategoryTheory.Limits.CatCospanTransform.whiskerRight_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} {τ : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} : CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η (φ.comp τ) = CategoryTheory.CategoryStruct.comp (ψ.associator φ τ).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) τ) (ψ'.associator φ τ).hom)
• CategoryTheory.Limits.CatCospanTransformMorphism.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ⟶ ψ'.left) (right : ψ.right ⟶ ψ'.right) (base : ψ.base ⟶ ψ'.base) (left_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.Functor.whiskerRight left F') = CategoryTheory.CategoryStruct.comp (F.whiskerLeft base) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.Functor.whiskerRight right G') = CategoryTheory.CategoryStruct.comp (G.whiskerLeft base) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ'
• CategoryTheory.Limits.CatCospanTransform.comp_whiskerLeft_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} {τ τ' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} (γ : τ ⟶ τ') {Z : CategoryTheory.Limits.CatCospanTransform F G F''' G'''} (h : (ψ.comp φ).comp τ' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft (ψ.comp φ) γ) h = CategoryTheory.CategoryStruct.comp (ψ.associator φ τ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ γ)) (CategoryTheory.CategoryStruct.comp (ψ.associator φ τ').inv h))
• CategoryTheory.Limits.CatCospanTransform.whiskerRight_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ') {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} {τ : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} {Z : CategoryTheory.Limits.CatCospanTransform F G F''' G'''} (h : ψ'.comp (φ.comp τ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η (φ.comp τ)) h = CategoryTheory.CategoryStruct.comp (ψ.associator φ τ).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) τ) (CategoryTheory.CategoryStruct.comp (ψ'.associator φ τ).hom h))
• CategoryTheory.Limits.CatCospanTransform.mkIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.Functor.whiskerRight left.hom F') = CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.Functor.whiskerRight right.hom G') = CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : ψ ≅ ψ'
• CategoryTheory.Limits.CatCospanTransform.mkIso_hom_base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.Functor.whiskerRight left.hom F') = CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.Functor.whiskerRight right.hom G') = CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).hom.base = base.hom
• CategoryTheory.Limits.CatCospanTransform.mkIso_hom_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.Functor.whiskerRight left.hom F') = CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.Functor.whiskerRight right.hom G') = CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).hom.left = left.hom
• CategoryTheory.Limits.CatCospanTransform.mkIso_hom_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.Functor.whiskerRight left.hom F') = CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.Functor.whiskerRight right.hom G') = CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).hom.right = right.hom
• CategoryTheory.Limits.CatCospanTransform.mkIso_inv_base 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.Functor.whiskerRight left.hom F') = CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.Functor.whiskerRight right.hom G') = CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).inv.base = base.inv
• CategoryTheory.Limits.CatCospanTransform.mkIso_inv_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.Functor.whiskerRight left.hom F') = CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.Functor.whiskerRight right.hom G') = CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).inv.left = left.inv
• CategoryTheory.Limits.CatCospanTransform.mkIso_inv_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base) (left_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom (CategoryTheory.Functor.whiskerRight left.hom F') = CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom := by cat_disch) (right_coherence : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom (CategoryTheory.Functor.whiskerRight right.hom G') = CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom) (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom := by cat_disch) : (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).inv.right = right.inv
• CategoryTheory.Limits.CatCospanTransform.pentagon 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} {τ : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} {A'''' : Type u₁₃} {B'''' : Type u₁₄} {C'''' : Type u₁₅} [CategoryTheory.Category.{v₁₃, u₁₃} A''''] [CategoryTheory.Category.{v₁₄, u₁₄} B''''] [CategoryTheory.Category.{v₁₅, u₁₅} C''''] {F'''' : CategoryTheory.Functor A'''' B''''} {G'''' : CategoryTheory.Functor C'''' B''''} {σ : CategoryTheory.Limits.CatCospanTransform F''' G''' F'''' G''''} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (ψ.associator φ τ).hom σ) (CategoryTheory.CategoryStruct.comp (ψ.associator (φ.comp τ) σ).hom (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (φ.associator τ σ).hom)) = CategoryTheory.CategoryStruct.comp ((ψ.comp φ).associator τ σ).hom (ψ.associator φ (τ.comp σ)).hom
• CategoryTheory.Limits.CatCospanTransform.pentagon_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
  {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₉} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} [CategoryTheory.Category.{v₄, u₄} A'] [CategoryTheory.Category.{v₅, u₅} B'] [CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'} [CategoryTheory.Category.{v₇, u₇} A''] [CategoryTheory.Category.{v₈, u₈} B''] [CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''} {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A'''] [CategoryTheory.Category.{v₁₁, u₁₁} B'''] [CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''} {G''' : CategoryTheory.Functor C''' B'''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'} {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} {τ : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''} {A'''' : Type u₁₃} {B'''' : Type u₁₄} {C'''' : Type u₁₅} [CategoryTheory.Category.{v₁₃, u₁₃} A''''] [CategoryTheory.Category.{v₁₄, u₁₄} B''''] [CategoryTheory.Category.{v₁₅, u₁₅} C''''] {F'''' : CategoryTheory.Functor A'''' B''''} {G'''' : CategoryTheory.Functor C'''' B''''} {σ : CategoryTheory.Limits.CatCospanTransform F''' G''' F'''' G''''} {Z : CategoryTheory.Limits.CatCospanTransform F G F'''' G''''} (h : ψ.comp (φ.comp (τ.comp σ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (ψ.associator φ τ).hom σ) (CategoryTheory.CategoryStruct.comp (ψ.associator (φ.comp τ) σ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (φ.associator τ σ).hom) h)) = CategoryTheory.CategoryStruct.comp ((ψ.comp φ).associator τ σ).hom (CategoryTheory.CategoryStruct.comp (ψ.associator φ (τ.comp σ)).hom h)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] : CategoryTheory.Functor (CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (CategoryTheory.Functor (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F₁ G₁ X))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj (CategoryTheory.Limits.CatCospanTransform.id F G) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_fst_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).fst.obj X✝ = ψ.left.obj (S.fst.obj X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_snd_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).snd.obj X✝ = ψ.right.obj (S.snd.obj X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_fst_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {X✝ Y✝ : X} (f : X✝ ⟶ Y✝) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).fst.map f = ψ.left.map (S.fst.map f)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_snd_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) {X✝ Y✝ : X} (f : X✝ ⟶ Y✝) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).snd.map f = ψ.right.map (S.snd.map f)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (U : CategoryTheory.Functor X Y) : CategoryTheory.CatCommSq ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) : CategoryTheory.CatCommSq ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀) [CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj (ψ.comp ψ') ≅ ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).comp ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ')
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_hom_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom.app X✝).fst.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.fst.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom.app X✝).snd.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.snd.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_inv_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).inv.app X✝).fst.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.fst.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄) [CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝¹ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).inv.app X✝).snd.app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.snd.obj X✝¹)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_iso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).iso.hom.app X✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj X✝)) (CategoryTheory.CategoryStruct.comp (ψ.base.map (S.iso.hom.app X✝)) ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G₁).hom.app (S.snd.obj X✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_iso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).iso.inv.app X✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G₁).inv.app (S.snd.obj X✝)) (CategoryTheory.CategoryStruct.comp (ψ.base.map (S.iso.inv.app X✝)) ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F₁).hom.app (S.fst.obj X✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_hom_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀) [CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').hom.app X✝).fst.app x✝ = CategoryTheory.CategoryStruct.id (ψ'.left.obj (ψ.left.obj (X✝.fst.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀) [CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').hom.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ'.right.obj (ψ.right.obj (X✝.snd.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_inv_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀) [CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').inv.app X✝).fst.app x✝ = CategoryTheory.CategoryStruct.id (ψ'.left.obj (ψ.left.obj (X✝.fst.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀) [CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x✝ : X) : ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').inv.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ'.right.obj (ψ.right.obj (X✝.snd.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (U : CategoryTheory.Functor X Y) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).hom.app X✝).fst.app x✝ = CategoryTheory.CategoryStruct.id (ψ.left.obj (X✝.fst.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (U : CategoryTheory.Functor X Y) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).hom.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_inv_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (U : CategoryTheory.Functor X Y) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).inv.app X✝).fst.app x✝ = CategoryTheory.CategoryStruct.id (ψ.left.obj (X✝.fst.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (U : CategoryTheory.Functor X Y) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).inv.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).hom.app X✝).fst.app x✝ = CategoryTheory.CategoryStruct.id (ψ.left.obj (X✝.fst.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).hom.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_inv_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).inv.app X✝).fst.app x✝ = CategoryTheory.CategoryStruct.id (ψ.left.obj (X✝.fst.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_inv_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (X✝ : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x✝ : X) : ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).inv.app X✝).snd.app x✝ = CategoryTheory.CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (f : x ⟶ y) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).map f).fst.app X✝ = ψ.left.map (f.fst.app X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_map_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (f : x ⟶ y) (X✝ : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).map f).snd.app X✝ = ψ.right.map (f.snd.app X✝)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_leftUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map ψ.leftUnitor.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X (CategoryTheory.Limits.CatCospanTransform.id F G) ψ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).leftUnitor.hom)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_rightUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map ψ.rightUnitor.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ (CategoryTheory.Limits.CatCospanTransform.id F₁ G₁)).hom (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).whiskerLeft (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F₁ G₁).hom) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).rightUnitor.hom)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_whiskerLeft 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) {φ φ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂} (α : φ ⟶ φ') : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ α) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ φ).hom (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).whiskerLeft ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map α)) (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ φ').inv)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_whiskerRight 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (α : ψ ⟶ ψ') (φ : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight α φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ φ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map α) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj φ)) (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ' φ).inv)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_naturality₂ 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) {U V : CategoryTheory.Functor X Y} (α : U ⟶ V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map α) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)) (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj V) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj V)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).hom (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ).whiskerLeft ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).map α))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj (CategoryTheory.Limits.CatCospanTransform.id F G)) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj (CategoryTheory.Limits.CatCospanTransform.id F G))).hom (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).whiskerLeft (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId Y F G).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).leftUnitor.hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).rightUnitor.inv)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_naturality₂ 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).map η) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)) (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ') ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ')).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).hom (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).whiskerLeft ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map η))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj (CategoryTheory.Functor.id X)) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj (CategoryTheory.Functor.id X))).hom (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).whiskerLeft (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F₁ G₁ X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).leftUnitor.hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).rightUnitor.inv)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_associator 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} {A₃ : Type u₁₀} {B₃ : Type u₁₁} {C₃ : Type u₁₂} [CategoryTheory.Category.{v₁₀, u₁₀} A₃] [CategoryTheory.Category.{v₁₁, u₁₁} B₃] [CategoryTheory.Category.{v₁₂, u₁₂} C₃] {F₃ : CategoryTheory.Functor A₃ B₃} {G₃ : CategoryTheory.Functor C₃ B₃} (X : Type u₁₃) [CategoryTheory.Category.{v₁₃, u₁₃} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (φ : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) (τ : CategoryTheory.Limits.CatCospanTransform F₂ G₂ F₃ G₃) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map (ψ.associator φ τ).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X (ψ.comp φ) τ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ φ).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj τ)) (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).associator ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj φ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj τ)).hom (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).whiskerLeft (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X φ τ).inv) (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ (φ.comp τ)).inv)))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u₇} {Y : Type u₈} {Z : Type u₉} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] [CategoryTheory.Category.{v₉, u₉} Z] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (U : CategoryTheory.Functor X Y) (V : CategoryTheory.Functor Y Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj (U.comp V)) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Z).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj (U.comp V))).hom (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Z).obj ψ).whiskerLeft (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F₁ G₁ U V).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U V).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)) (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj V).associator ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).hom (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj V).whiskerLeft (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).hom) (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj V).associator ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj V) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Z).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj V)).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)) (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Z).obj ψ).associator ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj V) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).hom))))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformPrecomposeObjSquare_iso_hom_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [CategoryTheory.Category.{v₇, u₇} A₂] [CategoryTheory.Category.{v₈, u₈} B₂] [CategoryTheory.Category.{v₉, u₉} C₂] {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} {X : Type u₁₀} {Y : Type u₁₁} [CategoryTheory.Category.{v₁₀, u₁₀} X] [CategoryTheory.Category.{v₁₁, u₁₁} Y] (U : CategoryTheory.Functor X Y) (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj (ψ.comp ψ')) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₂ G₂).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj (ψ.comp ψ'))).hom (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).whiskerLeft (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp Y ψ ψ').hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₂ G₂).obj U)) (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ).associator ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ') ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₂ G₂).obj U)).hom (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ).whiskerLeft (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ') ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₂ G₂).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ')).hom) (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ).associator ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ')).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ')) (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).associator ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ')).hom))))
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ') (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (y : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map η).app S).fst.app y = η.left.app (S.fst.obj y)
• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_snd_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
  {A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ') (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (y : X) : (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map η).app S).snd.app y = η.right.app (S.snd.obj y)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c