Theorems · Definition · category theory

CategoryTheory.Limits.isLimitOfReflects

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              (F : CategoryTheory.Functor C D) →
                {c : CategoryTheory.Limits.Cone K} →
                  CategoryTheory.Limits.IsLimit (F.mapCone c) →
                    [CategoryTheory.Limits.ReflectsLimit K F] → CategoryTheory.Limits.IsLimit c

A convenience function for ReflectsLimit, which takes the functor as an explicit argument to guide typeclass resolution.

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Basic

Cited by

18 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.ReflectsLimit