[Merged by Bors] - feat(order/category/omega-complete): omega-complete partial orders form a complete category

src/order/category/omega_complete_partial_order.lean

@@ -55,17 +55,12 @@ section
 open category_theory.limits
 
 def make_product {J : Type v} (f : J → ωCPO.{v}) : fan f :=
-@fan.mk _ _ _ _ (of (Π j, f j))
-begin
-  intro j,
-  exact continuous_hom.of_mono (pi.monotone_apply j) (λ c, rfl),
-end
+@fan.mk _ _ _ _ (of (Π j, f j)) (λ j, continuous_hom.of_mono (pi.monotone_apply j : _) (λ c, rfl))
 
 def is_prod (J : Type v) (f : J → ωCPO) : is_limit (make_product f) :=
 { lift := λ s,
-  begin
-    refine ⟨λ t j, s.π.app j t, λ x y h j, (s.π.app j).monotone h, λ x, funext (λ j, (s.π.app j).continuous x)⟩,
-  end,
+    ⟨λ t j, s.π.app j t, λ x y h j, (s.π.app j).monotone h,
+     λ x, funext (λ j, (s.π.app j).continuous x)⟩,
   uniq' := λ s m w,
   begin
     ext t j,
@@ -74,7 +69,7 @@ def is_prod (J : Type v) (f : J → ωCPO) : is_limit (make_product f) :=
     refl,
   end }.
 
-instance has_prod (J : Type v) (f : J → ωCPO.{v}) : has_product f :=
+instance has_product (J : Type v) (f : J → ωCPO.{v}) : has_product f :=
 has_limit.mk ⟨_, is_prod _ f⟩
 
 instance : has_products ωCPO.{v} :=
@@ -93,27 +88,27 @@ omega_complete_partial_order.lift
   (λ x y h, h)
   (λ c, rfl)
 
-instance kernel_cpo {α β : Type*} [omega_complete_partial_order α] [omega_complete_partial_order β]
+instance omega_complete_partial_order_equalizer
+  {α β : Type*} [omega_complete_partial_order α] [omega_complete_partial_order β]
   (f g : α →𝒄 β) : omega_complete_partial_order {a : α // f a = g a} :=
 subtype_order _ $ λ c hc,
 begin
   rw [f.continuous, g.continuous],
   congr' 1,
-  apply preorder_hom.ext,
-  intro a,
+  ext,
   apply hc _ ⟨_, rfl⟩,
 end
 
-def include_kernel {α β : Type*} [omega_complete_partial_order α] [omega_complete_partial_order β]
+def equalizer_ι {α β : Type*} [omega_complete_partial_order α] [omega_complete_partial_order β]
   (f g : α →𝒄 β) :
   {a : α // f a = g a} →𝒄 α :=
 continuous_hom.of_mono (subtype_monotone _) (λ c, rfl)
 
-def make_equalizer {X Y : ωCPO.{v}} (f g : X ⟶ Y) :
+def equalizer {X Y : ωCPO.{v}} (f g : X ⟶ Y) :
   fork f g :=
-@fork.of_ι _ _ _ _ _ _ (ωCPO.of {a // f a = g a}) (include_kernel f g) (continuous_hom.ext _ _ (λ x, x.2))
+@fork.of_ι _ _ _ _ _ _ (ωCPO.of {a // f a = g a}) (equalizer_ι f g) (continuous_hom.ext _ _ (λ x, x.2))
 
-def is_equalizer {X Y : ωCPO.{v}} (f g : X ⟶ Y) : is_limit (make_equalizer f g) :=
+def is_equalizer {X Y : ωCPO.{v}} (f g : X ⟶ Y) : is_limit (equalizer f g) :=
 fork.is_limit.mk' _ $ λ s,
 ⟨{ to_fun := λ x, ⟨s.ι x, by { apply congr_fun (congr_arg continuous_hom.to_fun s.condition : _ = _) }⟩,
     monotone' := λ x y h, s.ι.monotone h,
@@ -125,9 +120,9 @@ fork.is_limit.mk' _ $ λ s,
     apply congr_fun (congr_arg continuous_hom.to_fun hm : _ = _),
   end⟩
 
-instance has_eq : has_equalizers ωCPO.{v} :=
+instance : has_equalizers ωCPO.{v} :=
 @has_equalizers_of_has_limit_parallel_pair _ _ $
-λ X Y f g, has_limit.mk ⟨make_equalizer f g, is_equalizer f g⟩
+λ X Y f g, has_limit.mk ⟨equalizer f g, is_equalizer f g⟩
 
 instance : has_limits ωCPO.{v} := limits_from_equalizers_and_products