Theorems · Definition · category theory

CategoryTheory.Limits.Cofan

{β : Type w} → {C : Type u} → [CategoryTheory.Category.{v, u} C] → (β → C) → Type (max (max w u) v)

A cofan over f : β → C consists of a collection of maps from every f b to an object P.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Products

Cited by

124 results in Mathlib

Foundations

Depth 13 from the axioms, rests on 71 definitions · uses propext

Assumes

CategoryTheory.Category