@[instance]
def
category_theory.limits.has_finite_limits_of_semilattice_inf_top
{α : Type u}
[semilattice_inf_top α] :
Equations
- category_theory.limits.has_finite_limits_of_semilattice_inf_top = λ (J : Type u) (𝒥₁ : category_theory.small_category J) (𝒥₂ : category_theory.fin_category J), {has_limit := λ (F : J ⥤ α), {cone := {X := finset.univ.inf F.obj, π := {app := λ (j : J), {down := {down := _}}, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone F), {down := {down := _}}, fac' := _, uniq' := _}}}
@[instance]
def
category_theory.limits.has_finite_colimits_of_semilattice_sup_bot
{α : Type u}
[semilattice_sup_bot α] :
Equations
- category_theory.limits.has_finite_colimits_of_semilattice_sup_bot = λ (J : Type u) (𝒥₁ : category_theory.small_category J) (𝒥₂ : category_theory.fin_category J), {has_colimit := λ (F : J ⥤ α), {cocone := {X := finset.univ.sup F.obj, ι := {app := λ (i : J), {down := {down := _}}, naturality' := _}}, is_colimit := {desc := λ (s : category_theory.limits.cocone F), {down := {down := _}}, fac' := _, uniq' := _}}}
@[instance]
Equations
- category_theory.limits.has_limits_of_complete_lattice = {has_limits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ α), {cone := {X := has_Inf.Inf (set.range F.obj), π := {app := λ (j : J), {down := {down := _}}, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone F), {down := {down := _}}, fac' := _, uniq' := _}}}}
@[instance]
Equations
- category_theory.limits.has_colimits_of_complete_lattice = {has_colimits_of_shape := λ (J : Type u) (𝒥 : category_theory.small_category J), {has_colimit := λ (F : J ⥤ α), {cocone := {X := has_Sup.Sup (set.range F.obj), ι := {app := λ (j : J), {down := {down := _}}, naturality' := _}}, is_colimit := {desc := λ (s : category_theory.limits.cocone F), {down := {down := _}}, fac' := _, uniq' := _}}}}