Theorems · Definition · category theory

CategoryTheory.IsCofiltered.cone

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofiltered C] →
      {J : Type w} →
        [inst_2 : CategoryTheory.SmallCategory J] →
          [CategoryTheory.FinCategory J] → (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.Cone F

An arbitrary choice of cone over F : J ⥤ C, for FinCategory J and IsCofiltered C.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredCategoryTheory.SmallCategoryCategoryTheory.FinCategory