import category_theory.universal.limits
import category_theory.functor_category

universes u v

namespace category_theory.universal
open category_theory

variables {C : Type u} [𝒞 : category.{u v} C] [has_limits.{u v} C]
include 𝒞

def lim {J : Type v} [small_category J] : (J ↝ C) ↝ C :=
{ obj := limit,
  map' := λ F F' t, (limit.universal_property F').lift $
    { X := limit F, π := λ j, limit.π F j ≫ t.app j },
  map_id' := assume F,
    by apply limit.hom_characterisation; simp [limit.π, -limit.cone_π],
  map_comp' := assume F F' F'' t t', begin
    apply limit.hom_characterisation; simp [limit.π, -limit.cone_π],
    intro j, rw [←category.assoc, is_limit.fac], simp
  end }

end category_theory.universal