Theorems · Inductive type · category theory

CategoryTheory.Limits.WeakLimitCone

{J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] → CategoryTheory.Functor J C → Type (max (max u_1 u_3) v_3)

WeakLimitCone F contains a cone over F together with the information that it is a weak limit.

Defined in

Mathlib.CategoryTheory.Limits.WeakLimits.Basic

Cited by

5 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category