failed to synthesize HasFiniteLimits (Type u)

Stream: new members

[Shanghe Chen]

Hi I am doing some exercises related to Yoneda style proof. And it seems currently no instance for showing Type u has finite limits?

import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
import Mathlib.CategoryTheory.Types

open CategoryTheory
open Category
open Limits

universe u

set_option trace.Meta.synthInstance true in
#synth Category (Type u)

#synth HasFiniteLimits (Type u)
-- failed to synthesize
--   HasFiniteLimits (Type u)

[Joël Riou]

You may have to import Mathlib.CategoryTheory.Limits.Types.

[Shanghe Chen]

It works now. Thank you very much Joël :tada: