Loogle!
Result
Found 72 declarations mentioning CategoryTheory.Limits.CatCospanTransform.comp.
- 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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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))))
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:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.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