Theorems · Definition · category theory

CategoryTheory.Limits.reflexiveCoforkEquivCofork

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) →
      CategoryTheory.Limits.ReflexiveCofork F ≌
        CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
          (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)

Forgetting the reflexion yields an equivalence between cocones over a bundled reflexive pair and coforks on the underlying parallel pair.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category