Theorems · Theorem · category theory

CategoryTheory.Cat.freeMapCompIso_inv_app

∀ {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} [inst : Quiver V₁] [inst_1 : Quiver V₂] [inst_2 : Quiver V₃]
  (F : V₁ ⥤q V₂) (G : V₂ ⥤q V₃) (X : CategoryTheory.Paths V₁),
  (CategoryTheory.Cat.freeMapCompIso F G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj (F.obj X))

Defined in

Mathlib.CategoryTheory.Category.Quiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

QuiverQuiverQuiver