Theorems · Theorem · category theory

CategoryTheory.ComposableArrows.ext

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C n}
  (h : ∀ (i : Fin (n + 1)), F.obj i = G.obj i),
  (∀ (i : ℕ) (hi : i < n),
      F.map' i (i + 1) ⋯ hi =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (G.map' i (i + 1) ⋯ hi) (CategoryTheory.eqToHom ⋯))) →
    F = G

Defined in

Mathlib.CategoryTheory.ComposableArrows.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category