Theorems · Definition · category theory

CategoryTheory.CostructuredArrow.isoMk

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

To construct an isomorphism of costructured arrows, we need an isomorphism of the objects underlying the source, 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