Theorems · Definition · category theory

CategoryTheory.Limits.diagramIsoParallelPair

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) →
      F ≅
        CategoryTheory.Limits.parallelPair (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
          (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)

Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a parallelPair

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category