Theorems · Inductive type · category theory

CategoryTheory.Limits.Bicone

{J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [CategoryTheory.Limits.HasZeroMorphisms C] → (J → C) → Type (max (max uC uC') w)

A c : Bicone F is: * an object c.pt and * morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j, * such that ι j ≫ π j' is the identity when j = j' and zero otherwise.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Cited by

75 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms