Theorems · Definition · category theory

CategoryTheory.Arrow.isoMk

{T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    {f g : CategoryTheory.Arrow T} →
      (l : f.left ≅ g.left) →
        (r : f.right ≅ g.right) →
          autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom)
              CategoryTheory.Arrow.isoMk._auto_1 →
            (f ≅ g)

Create an isomorphism between arrows, by providing isomorphisms between the domains and codomains, and a proof that the square commutes.

Defined in

Mathlib.CategoryTheory.Comma.Arrow

Cited by

53 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category