Theorems · Definition · category theory

CategoryTheory.CardinalDirectedPoset.cocone

{κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : CategoryTheory.CardinalDirectedPoset κ) →
      CategoryTheory.Limits.Cocone (CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet J.PropSet)

For any object J : CardinalDirectedPoset κ, this is a colimit cocone exhibiting J as the colimit of its subsets that are of cardinality < κ and have a terminal object.

Defined in

Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Cited by

0 results in Mathlib

Foundations

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

Assumes

Fact