Theorems · Definition · category theory

CategoryTheory.Paths.liftNatIso

{V : Type u₁} →
  [inst : Quiver V] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} →
          (α_app : (v : V) → F.obj v ≅ G.obj v) →
            (∀ {X Y : V} (f : X ⟶ Y),
                CategoryTheory.CategoryStruct.comp (F.map f.toPath) (α_app Y).hom =
                  CategoryTheory.CategoryStruct.comp (α_app X).hom (G.map f.toPath)) →
              (F ≅ G)

A natural isomorphism between F G : Paths V ⥤ C is defined by its components and its unary naturality squares.

Defined in

Mathlib.CategoryTheory.PathCategory.MorphismProperty

Cited by

2 results in Mathlib

Foundations

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

Assumes

QuiverCategoryTheory.Category