Theorems · Definition · category theory

CategoryTheory.StructuredArrow.isoMk

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            {f f' : CategoryTheory.StructuredArrow S T} →
              (g : f.right ≅ f'.right) →
                autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom)
                    CategoryTheory.StructuredArrow.isoMk._auto_1 →
                  (f ≅ f')

To construct an isomorphism of structured arrows, we need an isomorphism of the objects underlying the target, and to check that the triangle commutes.

Defined in

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category