feat(category_theory/limits): explicit binary product functor in Type (…

…#5043)

Adds `binary_product_functor`, the explicit product functor in Type, and `binary_product_iso_prod` which shows it is isomorphic to the one picked by choice (this is helpful eg to show Type is cartesian closed).

I also edited the definitions a little to use existing machinery instead - this seems to make `simp` and `tidy` stronger when working with the explicit product cone; but they're definitionally the same as the old ones.

src/category_theory/limits/shapes/types.lean

@@ -63,65 +63,98 @@ def initial_limit_cone : limits.colimit_cocone (functor.empty (Type u)) :=
 
 open category_theory.limits.walking_pair
 
-local attribute [tidy] tactic.case_bash
+/-- The product type `X × Y` forms a cone for the binary product of `X` and `Y`. -/
+-- We manually generate the other projection lemmas since the simp-normal form for the legs is
+-- otherwise not created correctly.
+@[simps X {rhs_md := semireducible}]
+def binary_product_cone (X Y : Type u) : binary_fan X Y :=
+binary_fan.mk prod.fst prod.snd
+
+@[simp]
+lemma binary_product_cone_fst (X Y : Type u) :
+  (binary_product_cone X Y).fst = prod.fst :=
+rfl
+@[simp]
+lemma binary_product_cone_snd (X Y : Type u) :
+  (binary_product_cone X Y).snd = prod.snd :=
+rfl
+
+/-- The product type `X × Y` is a binary product for `X` and `Y`. -/
+@[simps]
+def binary_product_limit (X Y : Type u) : is_limit (binary_product_cone X Y) :=
+{ lift := λ (s : binary_fan X Y) x, (s.fst x, s.snd x),
+  fac' := λ s j, walking_pair.cases_on j rfl rfl,
+  uniq' := λ s m w, funext $ λ x, prod.ext (congr_fun (w left) x) (congr_fun (w right) x) }
 
 /--
 The category of types has `X × Y`, the usual cartesian product,
 as the binary product of `X` and `Y`.
 -/
+@[simps]
 def binary_product_limit_cone (X Y : Type u) : limits.limit_cone (pair X Y) :=
-{ cone :=
-  { X := X × Y,
-    π :=
-    { app := by { rintro ⟨_|_⟩, exact prod.fst, exact prod.snd, } }, },
-  is_limit :=
-  { lift := λ s x, (s.π.app left x, s.π.app right x),
-    uniq' := λ s m w,
-    begin
-      ext,
-      exact congr_fun (w left) x,
-      exact congr_fun (w right) x,
-    end }, }
+⟨_, binary_product_limit X Y⟩
+
+/-- The functor which sends `X, Y` to the product type `X × Y`. -/
+@[simps]
+def binary_product_functor : Type u ⥤ Type u ⥤ Type u :=
+{ obj := λ X,
+  { obj := λ Y, X × Y,
+    map := λ Y₁ Y₂ f, (binary_product_limit X Y₂).lift (binary_fan.mk prod.fst (prod.snd ≫ f)) },
+  map := λ X₁ X₂ f,
+  { app := λ Y, (binary_product_limit X₂ Y).lift (binary_fan.mk (prod.fst ≫ f) prod.snd) } }
+
+/--
+The product functor given by the instance `has_binary_products (Type u)` is isomorphic to the
+explicit binary product functor given by the product type.
+-/
+noncomputable def binary_product_iso_prod : binary_product_functor ≅ (prod.functor : Type u ⥤ _) :=
+begin
+  apply nat_iso.of_components (λ X, _) _,
+  { apply nat_iso.of_components (λ Y, _) _,
+    { exact ((limit.is_limit _).cone_point_unique_up_to_iso (binary_product_limit X Y)).symm },
+    { intros Y₁ Y₂ f,
+      ext1;
+      simp } },
+  { intros X₁ X₂ g,
+    ext : 3;
+    simp }
+end
+
+/-- The sum type `X ⊕ Y` forms a cocone for the binary coproduct of `X` and `Y`. -/
+@[simps {rhs_md := semireducible}]
+def binary_coproduct_cocone (X Y : Type u) : cocone (pair X Y) :=
+binary_cofan.mk sum.inl sum.inr
+
+/-- The sum type `X ⊕ Y` is a binary coproduct for `X` and `Y`. -/
+@[simps]
+def binary_coproduct_colimit (X Y : Type u) : is_colimit (binary_coproduct_cocone X Y) :=
+{ desc := λ (s : binary_cofan X Y), sum.elim s.inl s.inr,
+  fac' := λ s j, walking_pair.cases_on j rfl rfl,
+  uniq' := λ s m w, funext $ λ x, sum.cases_on x (congr_fun (w left)) (congr_fun (w right)) }
 
 /--
 The category of types has `X ⊕ Y`,
 as the binary coproduct of `X` and `Y`.
 -/
-def binary_coproduct_limit_cone (X Y : Type u) : limits.colimit_cocone (pair X Y) :=
-{ cocone :=
-  { X := X ⊕ Y,
-    ι :=
-    { app := by { rintro ⟨_|_⟩, exact sum.inl, exact sum.inr, } }, },
-  is_colimit :=
-  { desc := λ s x, sum.elim (s.ι.app left) (s.ι.app right) x,
-    uniq' := λ s m w,
-    begin
-      ext (x|x),
-      exact (congr_fun (w left) x : _),
-      exact (congr_fun (w right) x : _),
-    end }, }
+def binary_coproduct_colimit_cocone (X Y : Type u) : limits.colimit_cocone (pair X Y) :=
+⟨_, binary_coproduct_colimit X Y⟩
 
 /--
 The category of types has `Π j, f j` as the product of a type family `f : J → Type`.
 -/
 def product_limit_cone {J : Type u} (F : J → Type u) : limits.limit_cone (discrete.functor F) :=
 { cone :=
   { X := Π j, F j,
-    π :=
-    { app := λ j f, f j }, },
+    π := { app := λ j f, f j }, },
   is_limit :=
   { lift := λ s x j, s.π.app j x,
-    uniq' := λ s m w,
-    begin
-      ext x j,
-      have := congr_fun (w j) x,
-      exact this,
-    end }, }
+    uniq' := λ s m w, funext $ λ x, funext $ λ j, (congr_fun (w j) x : _) } }
 
 /--
 The category of types has `Σ j, f j` as the coproduct of a type family `f : J → Type`.
 -/
-def coproduct_limit_cone {J : Type u} (F : J → Type u) : limits.colimit_cocone (discrete.functor F) :=
+def coproduct_colimit_cocone {J : Type u} (F : J → Type u) :
+  limits.colimit_cocone (discrete.functor F) :=
 { cocone :=
   { X := Σ j, F j,
     ι :=