Theorems · Theorem · category theory

CategoryTheory.Join.mkNatIso_hom

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (eₗ : (CategoryTheory.Join.inclLeft C D).comp F ≅ (CategoryTheory.Join.inclLeft C D).comp G)
  (eᵣ : (CategoryTheory.Join.inclRight C D).comp F ≅ (CategoryTheory.Join.inclRight C D).comp G)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
          ((CategoryTheory.Prod.snd C D).isoWhiskerLeft eᵣ).hom =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).isoWhiskerLeft eₗ).hom
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) G))
      CategoryTheory.Join.mkNatIso._auto_1),
  (CategoryTheory.Join.mkNatIso eₗ eᵣ h).hom = CategoryTheory.Join.mkNatTrans eₗ.hom eᵣ.hom h

Defined in

Mathlib.CategoryTheory.Join.Basic

Cited by

0 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category