Theorems · Definition · category theory

CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor

{C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        CategoryTheory.Functor (CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y))
          (CategoryTheory.Limits.BinaryBicone X Y)

Convert a Bicone over a function on WalkingPair to a BinaryBicone.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms