Theorems · Theorem · category theory

CategoryTheory.CatCommSq.vInv_vInv

∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : C₁ ≌ C₃) (R : C₂ ≌ C₄)
  (B : CategoryTheory.Functor C₃ C₄) (h : CategoryTheory.CatCommSq T L.functor R.functor B),
  CategoryTheory.CatCommSq.vInv B L.symm R.symm T (CategoryTheory.CatCommSq.vInv T L R B h) = h

Defined in

Mathlib.CategoryTheory.CatCommSq

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category