Library HoTT.WildCat.Products

Require Import Basics.Equivalences Basics.Overture Basics.Tactics.
Require Import Types.Bool Types.Prod Types.Forall.
Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd
               WildCat.Forall WildCat.NatTrans WildCat.Opposite
               WildCat.Universe WildCat.Yoneda WildCat.ZeroGroupoid
               WildCat.Monoidal.

Categories with products


Definition cat_prod_corec_inv {I A : Type} `{Is1Cat A}
  (prod : A) (x : I → A) (z : A) (pr : ∀ i, prod $-> x i)
  : yon_0gpd prod z $-> prod_0gpd I (fun i ⇒ yon_0gpd (x i) z).
Proof.
  snrapply equiv_prod_0gpd_corec.
  intros i.
  exact (fmap (fun x ⇒ yon_0gpd x z) (pr i)).
Defined.

(* A product of an I-indexed family of objects of a category is an object of the category with an I-indexed family of projections such that the induced map is an equivalence. *)
Class Product (I : Type) {A : Type} `{Is1Cat A} {x : I → A} := Build_Product' {
  cat_prod : A;
  cat_pr : ∀ i : I, cat_prod $-> x i;
  cat_isequiv_cat_prod_corec_inv
    :: ∀ z : A, CatIsEquiv (cat_prod_corec_inv cat_prod x z cat_pr);
}.

Arguments Product I {A _ _ _ _} x.
Arguments cat_prod I {A _ _ _ _} x {product} : rename.

A convenience wrapper for building products
Definition Build_Product (I : Type) {A : Type} `{Is1Cat A} {x : I → A}
  (cat_prod : A) (cat_pr : ∀ i : I, cat_prod $-> x i)
  (cat_prod_corec : ∀ z : A,
    (∀ i : I, z $-> x i) → (z $-> cat_prod))
  (cat_prod_beta_pr : ∀ (z : A) (f : ∀ i, z $-> x i) (i : I),
    cat_pr i $o cat_prod_corec z f $== f i)
  (cat_prod_eta_pr : ∀ (z : A) (f g : z $-> cat_prod),
    (∀ i : I, cat_pr i $o f $== cat_pr i $o g) → f $== g)
  : Product I x.
Proof.
  snrapply (Build_Product' I A _ _ _ _ _ cat_prod cat_pr).
  intros z.
  nrapply isequiv_0gpd_issurjinj.
  nrapply Build_IsSurjInj.
  - intros f.
    ∃ (cat_prod_corec z f).
    intros i.
    nrapply cat_prod_beta_pr.
  - intros f g p.
    by nrapply cat_prod_eta_pr.
Defined.

Section Lemmata.

  Context (I : Type) {A : Type} {x : I → A} `{Product I _ x}.

  Definition cate_cat_prod_corec_inv {z : A}
    : (yon_0gpd (cat_prod I x) z) $<~> prod_0gpd I (fun i ⇒ yon_0gpd (x i) z)
    := Build_CatEquiv (cat_prod_corec_inv (cat_prod I x) x z cat_pr).

  Definition cate_cat_prod_corec {z : A}
    : prod_0gpd I (fun i ⇒ yon_0gpd (x i) z) $<~> (yon_0gpd (cat_prod I x) z)
    := cate_cat_prod_corec_inv^-1$.

  Definition cat_prod_corec {z : A}
    : (∀ i, z $-> x i) → (z $-> cat_prod I x).
  Proof.
    apply cate_cat_prod_corec.
  Defined.

Applying the ith projection after a tuple of maps gives the ith map.
  Lemma cat_prod_beta {z : A} (f : ∀ i, z $-> x i)
    : ∀ i, cat_pr i $o cat_prod_corec f $== f i.
  Proof.
    exact (cate_isretr cate_cat_prod_corec_inv f).
  Defined.

The pairing map is the unique map that makes the following diagram commute.
  Lemma cat_prod_eta {z : A} (f : z $-> cat_prod I x)
    : cat_prod_corec (fun i ⇒ cat_pr i $o f) $== f.
  Proof.
    exact (cate_issect cate_cat_prod_corec_inv f).
  Defined.

  Local Instance is0functor_prod_0gpd_helper
    : Is0Functor (fun z : A^op ⇒ prod_0gpd I (fun i ⇒ yon_0gpd (x i) z)).
  Proof.
    snrapply Build_Is0Functor.
    intros a b f.
    snrapply Build_Morphism_0Gpd.
    - intros g i.
      exact (f $o g i).
    - snrapply Build_Is0Functor.
      intros g h p i.
      exact (f $@L p i).
  Defined.

  Local Instance is1functor_prod_0gpd_helper
    : Is1Functor (fun z : A^op ⇒ prod_0gpd I (fun i ⇒ yon_0gpd (x i) z)).
  Proof.
    snrapply Build_Is1Functor.
    - intros a b f g p r i.
      refine (_ $@L _).
      exact p.
    - intros a r i.
      nrapply cat_idl; exact _.
    - intros a b c f g r i.
      nrapply cat_assoc; exact _.
  Defined.

  Definition natequiv_cat_prod_corec_inv
    : NatEquiv (yon_0gpd (cat_prod I x))
      (fun z : A^op ⇒ prod_0gpd I (fun i ⇒ yon_0gpd (x i) z)).
  Proof.
    snrapply Build_NatEquiv.
    1: intro; nrapply cate_cat_prod_corec_inv.
    exact (is1natural_yoneda_0gpd
      (cat_prod I x)
      (fun z ⇒ prod_0gpd I (fun i ⇒ yon_0gpd (x i) z))
      cat_pr).
  Defined.

  Lemma cat_prod_corec_eta {z : A} {f f' : ∀ i, z $-> x i}
    : (∀ i, f i $== f' i) → cat_prod_corec f $== cat_prod_corec f'.
  Proof.
    intros p.
    unfold cat_prod_corec.
    nrapply (moveL_equiv_V_0gpd cate_cat_prod_corec_inv).
    nrefine (cate_isretr cate_cat_prod_corec_inv _ $@ _).
    exact p.
  Defined.

  Lemma cat_prod_pr_eta {z : A} {f f' : z $-> cat_prod I x}
    : (∀ i, cat_pr i $o f $== cat_pr i $o f') → f $== f'.
  Proof.
    intros p.
    refine ((cat_prod_eta _)^$ $@ _ $@ cat_prod_eta _).
    by nrapply cat_prod_corec_eta.
  Defined.

End Lemmata.

Diagonal map


Definition cat_prod_diag {I : Type} {A : Type} (x : A)
  `{Product I _ (fun _ ⇒ x)}
  : x $-> cat_prod I (fun _ ⇒ x)
  := cat_prod_corec I (fun _ ⇒ Id x).

Uniqueness of products


Definition cate_cat_prod {I J : Type} (ie : I <~> J) {A : Type} `{HasEquivs A}
  (x : I → A) `{!Product I x} (y : J → A) `{!Product J y}
  (e : ∀ i : I, x i $<~> y (ie i))
  : cat_prod I x $<~> cat_prod J y.
Proof.
  nrapply yon_equiv_0gpd.
  nrefine (natequiv_compose _ (natequiv_cat_prod_corec_inv _)).
  nrefine (natequiv_compose
            (natequiv_inverse (natequiv_cat_prod_corec_inv _)) _).
  snrapply Build_NatEquiv.
  - intros z.
    nrapply (cate_prod_0gpd ie).
    intros i.
    exact (natequiv_yon_equiv_0gpd (e i) _).
  - intros a b f g j.
    cbn.
    destruct (eisretr ie j).
    exact (cat_assoc_opp _ _ _).
Defined.

I-indexed products are unique no matter how they are constructed.
Definition cat_prod_unique {I A : Type} `{HasEquivs A}
  (x : I → A) `{!Product I x} (y : I → A) `{!Product I y}
  (e : ∀ i : I, x i $<~> y i)
  : cat_prod I x $<~> cat_prod I y.
Proof.
  exact (cate_cat_prod 1 x y e).
Defined.

Existence of products


Class HasProducts (I A : Type) `{Is1Cat A}
  := has_products :: ∀ x : I → A, Product I x.

Class HasAllProducts (A : Type) `{Is1Cat A}
  := has_all_products :: ∀ I : Type, HasProducts I A.

Product functor


Global Instance is0functor_cat_prod (I : Type) (A : Type) `{HasProducts I A}
  : Is0Functor (fun x : I → A ⇒ cat_prod I x).
Proof.
  nrapply Build_Is0Functor.
  intros x y f.
  exact (cat_prod_corec I (fun i ⇒ f i $o cat_pr i)).
Defined.

Global Instance is1functor_cat_prod (I : Type) (A : Type) `{HasProducts I A}
  : Is1Functor (fun x : I → A ⇒ cat_prod I x).
Proof.
  nrapply Build_Is1Functor.
  - intros x y f g p.
    exact (cat_prod_corec_eta I (fun i ⇒ p i $@R cat_pr i)).
  - intros x.
    nrefine (_ $@ (cat_prod_eta I (Id _))).
    exact (cat_prod_corec_eta I (fun i ⇒ cat_idl _ $@ (cat_idr _)^$)).
  - intros x y z f g.
    nrapply cat_prod_pr_eta.
    intros i.
    nrefine (cat_prod_beta _ _ _ $@ _).
    nrefine (_ $@ cat_assoc _ _ _).
    symmetry.
    nrefine (cat_prod_beta _ _ _ $@R _ $@ _).
    nrefine (cat_assoc _ _ _ $@ _).
    nrefine (_ $@L cat_prod_beta _ _ _ $@ _).
    nrapply cat_assoc_opp.
Defined.

Categories with specific kinds of products


Definition isterminal_prodempty {A : Type} {z : A}
  `{Product Empty A (fun _ ⇒ z)}
  : IsTerminal (cat_prod Empty (fun _ ⇒ z)).
Proof.
  intros a.
  snrefine (cat_prod_corec _ _; fun f ⇒ cat_prod_pr_eta _ _); intros [].
Defined.

Binary products


Class BinaryProduct {A : Type} `{Is1Cat A} (x y : A)
  := binary_product :: Product Bool (fun b ⇒ if b then x else y).

A category with binary products is a category with a binary product for each pair of objects.
Class HasBinaryProducts (A : Type) `{Is1Cat A}
  := has_binary_products :: ∀ x y : A, BinaryProduct x y.

Global Instance hasbinaryproducts_hasproductsbool {A : Type} `{HasProducts Bool A}
  : HasBinaryProducts A
  := fun x y ⇒ has_products (fun b : Bool ⇒ if b then x else y).

Section BinaryProducts.

  Context {A : Type} `{Is1Cat A} {x y : A} `{!BinaryProduct x y}.

  Definition cat_binprod : A
    := cat_prod Bool (fun b : Bool ⇒ if b then x else y).

  Definition cat_pr1 : cat_binprod $-> x := cat_pr true.

  Definition cat_pr2 : cat_binprod $-> y := cat_pr false.

  Definition cat_binprod_corec {z : A} (f : z $-> x) (g : z $-> y)
    : z $-> cat_binprod.
  Proof.
    nrapply (cat_prod_corec Bool).
    intros [|].
    - exact f.
    - exact g.
  Defined.

  Definition cat_binprod_beta_pr1 {z : A} (f : z $-> x) (g : z $-> y)
    : cat_pr1 $o cat_binprod_corec f g $== f
    := cat_prod_beta _ _ true.

  Definition cat_binprod_beta_pr2 {z : A} (f : z $-> x) (g : z $-> y)
    : cat_pr2 $o cat_binprod_corec f g $== g
    := cat_prod_beta _ _ false.

  Definition cat_binprod_eta {z : A} (f : z $-> cat_binprod)
    : cat_binprod_corec (cat_pr1 $o f) (cat_pr2 $o f) $== f.
  Proof.
    unfold cat_binprod_corec.
    nrapply cat_prod_pr_eta.
    intros [|].
    - exact (cat_binprod_beta_pr1 _ _).
    - exact (cat_binprod_beta_pr2 _ _).
  Defined.

  Definition cat_binprod_eta_pr {z : A} (f g : z $-> cat_binprod)
    : cat_pr1 $o f $== cat_pr1 $o g → cat_pr2 $o f $== cat_pr2 $o g → f $== g.
  Proof.
    intros p q.
    rapply cat_prod_pr_eta.
    intros [|].
    - exact p.
    - exact q.
  Defined.

  Definition cat_binprod_corec_eta {z : A} (f f' : z $-> x) (g g' : z $-> y)
    : f $== f' → g $== g' → cat_binprod_corec f g $== cat_binprod_corec f' g'.
  Proof.
    intros p q.
    rapply cat_prod_corec_eta.
    intros [|].
    - exact p.
    - exact q.
  Defined.

End BinaryProducts.

Arguments cat_binprod {A _ _ _ _} x y {_}.

A convenience wrapper for building binary products
Definition Build_BinaryProduct {A : Type} `{Is1Cat A} {x y : A}
  (cat_binprod : A) (cat_pr1 : cat_binprod $-> x) (cat_pr2 : cat_binprod $-> y)
  (cat_binprod_corec : ∀ z : A, z $-> x → z $-> y → z $-> cat_binprod)
  (cat_binprod_beta_pr1 : ∀ (z : A) (f : z $-> x) (g : z $-> y),
    cat_pr1 $o cat_binprod_corec z f g $== f)
  (cat_binprod_beta_pr2 : ∀ (z : A) (f : z $-> x) (g : z $-> y),
    cat_pr2 $o cat_binprod_corec z f g $== g)
  (cat_binprod_eta_pr : ∀ (z : A) (f g : z $-> cat_binprod),
    cat_pr1 $o f $== cat_pr1 $o g → cat_pr2 $o f $== cat_pr2 $o g → f $== g)
  : Product Bool (fun b ⇒ if b then x else y).
Proof.
  snrapply (Build_Product _ cat_binprod).
  - intros [|].
    + exact cat_pr1.
    + exact cat_pr2.
  - intros z f.
    nrapply cat_binprod_corec.
    + exact (f true).
    + exact (f false).
  - intros z f [|].
    + nrapply cat_binprod_beta_pr1.
    + nrapply cat_binprod_beta_pr2.
  - intros z f g p.
    nrapply cat_binprod_eta_pr.
    + exact (p true).
    + exact (p false).
Defined.

Definition cat_binprod_eta_pr_x_xx {A : Type} `{HasBinaryProducts A} {w x y z : A}
  (f g : w $-> cat_binprod x (cat_binprod y z))
  : cat_pr1 $o f $== cat_pr1 $o g
  → cat_pr1 $o cat_pr2 $o f $== cat_pr1 $o cat_pr2 $o g
  → cat_pr2 $o cat_pr2 $o f $== cat_pr2 $o cat_pr2 $o g
  → f $== g.
Proof.
  intros p q r.
  snrapply cat_binprod_eta_pr.
  - exact p.
  - snrapply cat_binprod_eta_pr.
    + exact (cat_assoc_opp _ _ _ $@ q $@ cat_assoc _ _ _).
    + exact (cat_assoc_opp _ _ _ $@ r $@ cat_assoc _ _ _).
Defined.

Definition cat_binprod_eta_pr_xx_x {A : Type} `{HasBinaryProducts A} {w x y z : A}
  (f g : w $-> cat_binprod (cat_binprod x y) z)
  : cat_pr1 $o cat_pr1 $o f $== cat_pr1 $o cat_pr1 $o g
  → cat_pr2 $o cat_pr1 $o f $== cat_pr2 $o cat_pr1 $o g
  → cat_pr2 $o f $== cat_pr2 $o g
  → f $== g.
Proof.
  intros p q r.
  snrapply cat_binprod_eta_pr.
  2: exact r.
  snrapply cat_binprod_eta_pr.
  1,2: refine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
  - exact p.
  - exact q.
Defined.

Definition cat_binprod_eta_pr_x_xx_id {A : Type} `{HasBinaryProducts A} {x y z : A}
  (f : cat_binprod x (cat_binprod y z) $-> cat_binprod x (cat_binprod y z))
  : cat_pr1 $o f $== cat_pr1
  → cat_pr1 $o cat_pr2 $o f $== cat_pr1 $o cat_pr2
  → cat_pr2 $o cat_pr2 $o f $== cat_pr2 $o cat_pr2
  → f $== Id _.
Proof.
  intros p q r.
  snrapply cat_binprod_eta_pr_x_xx.
  - exact (p $@ (cat_idr _)^$).
  - exact (q $@ (cat_idr _)^$).
  - exact (r $@ (cat_idr _)^$).
Defined.

From binary products, all Bool-shaped products can be constructed. This should not be an instance to avoid a cycle with hasbinaryproducts_hasproductsbool.
Definition hasproductsbool_hasbinaryproducts {A : Type} `{HasBinaryProducts A}
  : HasProducts Bool A.
Proof.
  intros x.
  snrapply Build_Product.
  - exact (cat_binprod (x true) (x false)).
  - intros [|].
    + exact cat_pr1.
    + exact cat_pr2.
  - intros z f.
    exact (cat_binprod_corec (f true) (f false)).
  - intros z f [|].
    + exact (cat_binprod_beta_pr1 (f true) (f false)).
    + exact (cat_binprod_beta_pr2 (f true) (f false)).
  - intros z f g p.
    nrapply cat_binprod_eta_pr.
    + exact (p true).
    + exact (p false).
Defined.

Operations on indexed products

We can take the disjoint union of the index set of an indexed product if we have all binary products. This is useful for associating products in a canonical way. This leads to symmetry and associativity of binary products.

Definition cat_prod_index_sum {I J : Type} {A : Type} `{HasBinaryProducts A}
  (x : I → A) (y : J → A)
  : Product I x → Product J y → Product (I + J) (sum_ind _ x y).
Proof.
  intros p q.
  snrapply Build_Product.
  - exact (cat_binprod (cat_prod I x) (cat_prod J y)).
  - intros [i | j].
    + exact (cat_pr _ $o cat_pr1).
    + exact (cat_pr _ $o cat_pr2).
  - intros z f.
    nrapply cat_binprod_corec.
    + nrapply cat_prod_corec.
      exact (f o inl).
    + nrapply cat_prod_corec.
      exact (f o inr).
  - intros z f [i | j].
    + nrefine (cat_assoc _ _ _ $@ _).
      nrefine ((_ $@L cat_binprod_beta_pr1 _ _) $@ _).
      rapply cat_prod_beta.
    + nrefine (cat_assoc _ _ _ $@ _).
      nrefine ((_ $@L cat_binprod_beta_pr2 _ _) $@ _).
      rapply cat_prod_beta.
  - intros z f g r.
    rapply cat_binprod_eta_pr.
    + rapply cat_prod_pr_eta.
      intros i.
      exact ((cat_assoc _ _ _)^$ $@ r (inl i) $@ cat_assoc _ _ _).
    + rapply cat_prod_pr_eta.
      intros j.
      exact ((cat_assoc _ _ _)^$ $@ r (inr j) $@ cat_assoc _ _ _).
Defined.

Binary product functor

We prove bifunctoriality of cat_binprod : A → A → A by factoring it as cat_prod Bool o Bool_rec A. First, we prove that Bool_rec A : A → A → (Bool → A) is a bifunctor.
Local Instance is0bifunctor_boolrec {A : Type} `{Is1Cat A}
  : Is0Bifunctor (Bool_rec A).
Proof.
  snrapply Build_Is0Bifunctor'.
  1,2: exact _.
  snrapply Build_Is0Functor.
  intros [a b] [a' b'] [f g] [ | ].
  - exact f.
  - exact g.
Defined.

Local Instance is1bifunctor_boolrec {A : Type} `{Is1Cat A}
  : Is1Bifunctor (Bool_rec A).
Proof.
  snrapply Build_Is1Bifunctor'.
  snrapply Build_Is1Functor.
  - intros [a b] [a' b'] [f g] [f' g'] [p q] [ | ].
    + exact p.
    + exact q.
  - intros [a b] [ | ]; reflexivity.
  - intros [a b] [a' b'] [a'' b''] [f f'] [g g'] [ | ]; reflexivity.
Defined.

As a special case of the product functor, restriction along Bool_rec A yields bifunctoriality of cat_binprod.
Global Instance is0bifunctor_cat_binprod {A : Type} `{HasBinaryProducts A}
  : Is0Bifunctor (fun x y ⇒ cat_binprod x y).
Proof.
  pose (p:=@has_products _ _ _ _ _ _ hasproductsbool_hasbinaryproducts).
  exact (is0bifunctor_postcompose
          (Bool_rec A) (fun x ⇒ cat_prod Bool x (product:=p x))).
Defined.

Global Instance is1bifunctor_cat_binprod {A : Type} `{HasBinaryProducts A}
  : Is1Bifunctor (fun x y ⇒ cat_binprod x y).
Proof.
  pose (p:=@has_products _ _ _ _ _ _ hasproductsbool_hasbinaryproducts).
  exact (is1bifunctor_postcompose
          (Bool_rec A) (fun x ⇒ cat_prod Bool x (product:=p x))).
Defined.

Binary products are functorial in each argument.
Global Instance is0functor_cat_binprod_l {A : Type} `{HasBinaryProducts A}
  (y : A)
  : Is0Functor (fun x ⇒ cat_binprod x y).
Proof.
  exact (is0functor10_bifunctor y).
Defined.

Global Instance is1functor_cat_binprod_l {A : Type} `{HasBinaryProducts A}
  (y : A)
  : Is1Functor (fun x ⇒ cat_binprod x y).
Proof.
  exact (is1functor10_bifunctor y).
Defined.

Global Instance is0functor_cat_binprod_r {A : Type} `{HasBinaryProducts A}
  (x : A)
  : Is0Functor (fun y ⇒ cat_binprod x y).
Proof.
  exact (is0functor01_bifunctor x).
Defined.

Global Instance is1functor_cat_binprod_r {A : Type} `{HasBinaryProducts A}
  (x : A)
  : Is1Functor (fun y ⇒ cat_binprod x y).
Proof.
  exact (is1functor01_bifunctor x).
Defined.

cat_binprod_corec is also functorial in each morphsism.

Global Instance is0functor_cat_binprod_corec_l {A : Type}
  `{HasBinaryProducts A} {x y z : A} (g : z $-> y)
  : Is0Functor (fun f : z $-> y ⇒ cat_binprod_corec f g).
Proof.
  snrapply Build_Is0Functor.
  intros f f' p.
  by nrapply cat_binprod_corec_eta.
Defined.

Global Instance is0functor_cat_binprod_corec_r {A : Type}
  `{HasBinaryProducts A} {x y z : A} (f : z $-> x)
  : Is0Functor (fun g : z $-> x ⇒ cat_binprod_corec f g).
Proof.
  snrapply Build_Is0Functor.
  intros g h p.
  by nrapply cat_binprod_corec_eta.
Defined.

Definition cat_pr1_fmap01_binprod {A : Type} `{HasBinaryProducts A}
  (a : A) {x y : A} (g : x $-> y)
  : cat_pr1 $o fmap01 (fun x y ⇒ cat_binprod x y) a g $== cat_pr1
  := cat_binprod_beta_pr1 _ _ $@ cat_idl _.

Definition cat_pr1_fmap10_binprod {A : Type} `{HasBinaryProducts A}
  {x y : A} (f : x $-> y) (a : A)
  : cat_pr1 $o fmap10 (fun x y ⇒ cat_binprod x y) f a $== f $o cat_pr1
  := cat_binprod_beta_pr1 _ _.

Definition cat_pr1_fmap11_binprod {A : Type} `{HasBinaryProducts A}
  {w x y z : A} (f : w $-> y) (g : x $-> z)
  : cat_pr1 $o fmap11 (fun x y ⇒ cat_binprod x y) f g $== f $o cat_pr1
  := cat_binprod_beta_pr1 _ _.

Definition cat_pr2_fmap01_binprod {A : Type} `{HasBinaryProducts A}
  (a : A) {x y : A} (g : x $-> y)
  : cat_pr2 $o fmap01 (fun x y ⇒ cat_binprod x y) a g $== g $o cat_pr2
  := cat_binprod_beta_pr2 _ _.

Definition cat_pr2_fmap10_binprod {A : Type} `{HasBinaryProducts A}
  {x y : A} (f : x $-> y) (a : A)
  : cat_pr2 $o fmap10 (fun x y ⇒ cat_binprod x y) f a $== cat_pr2
  := cat_binprod_beta_pr2 _ _ $@ cat_idl _.

Definition cat_pr2_fmap11_binprod {A : Type} `{HasBinaryProducts A}
  {w x y z : A} (f : w $-> y) (g : x $-> z)
  : cat_pr2 $o fmap11 (fun x y ⇒ cat_binprod x y) f g $== g $o cat_pr2
  := cat_binprod_beta_pr2 _ _.

Symmetry of binary products


Section Symmetry.

The requirement of having all binary products can be weakened further to having specific binary products, but it is not clear this is a useful generality.
  Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}.

  Definition cat_binprod_swap (x y : A) : cat_binprod x y $-> cat_binprod y x
    := cat_binprod_corec cat_pr2 cat_pr1.

  Lemma cat_binprod_swap_cat_binprod_swap (x y : A)
    : cat_binprod_swap x y $o cat_binprod_swap y x $== Id _.
  Proof.
    nrapply cat_binprod_eta_pr.
    - refine ((cat_assoc _ _ _)^$ $@ _).
      nrefine (cat_binprod_beta_pr1 _ _ $@R _ $@ _).
      exact (cat_binprod_beta_pr2 _ _ $@ (cat_idr _)^$).
    - refine ((cat_assoc _ _ _)^$ $@ _).
      nrefine (cat_binprod_beta_pr2 _ _ $@R _ $@ _).
      exact (cat_binprod_beta_pr1 _ _ $@ (cat_idr _)^$).
  Defined.

  Lemma cate_binprod_swap (x y : A)
    : cat_binprod x y $<~> cat_binprod y x.
  Proof.
    snrapply cate_adjointify.
    1,2: nrapply cat_binprod_swap.
    all: nrapply cat_binprod_swap_cat_binprod_swap.
  Defined.

  Definition cat_binprod_swap_nat {a b c d : A} (f : a $-> c) (g : b $-> d)
    : cat_binprod_swap c d $o fmap11 (fun x y : A ⇒ cat_binprod x y) f g
    $== fmap11 (fun x y : A ⇒ cat_binprod x y) g f $o cat_binprod_swap a b.
  Proof.
    nrapply cat_binprod_eta_pr.
    - nrefine (cat_assoc_opp _ _ _ $@ _).
      nrefine ((cat_binprod_beta_pr1 _ _ $@R _) $@ _).
      nrefine (cat_pr2_fmap11_binprod _ _ $@ _).
      nrefine (_ $@ cat_assoc _ _ _).
      refine (_ $@ (_^$ $@R _)).
      2: nrapply cat_pr1_fmap11_binprod.
      refine ((_ $@L _^$) $@ (cat_assoc _ _ _)^$).
      nrapply cat_binprod_beta_pr1.
    - refine ((cat_assoc _ _ _)^$ $@ _).
      nrefine ((cat_binprod_beta_pr2 _ _ $@R _) $@ _).
      nrefine (cat_pr1_fmap11_binprod _ _ $@ _).
      nrefine (_ $@ cat_assoc _ _ _).
      refine (_ $@ (_^$ $@R _)).
      2: nrapply cat_pr2_fmap11_binprod.
      refine ((_ $@L _^$) $@ cat_assoc_opp _ _ _).
      nrapply cat_binprod_beta_pr2.
  Defined.

  Local Instance symmetricbraiding_binprod
    : SymmetricBraiding (fun x y ⇒ cat_binprod x y).
  Proof.
    snrapply Build_SymmetricBraiding.
    - snrapply Build_Braiding.
      + exact cat_binprod_swap.
      + intros [a b] [c d] [f g]; cbn in f, g.
        exact(cat_binprod_swap_nat f g).
    - exact cat_binprod_swap_cat_binprod_swap.
  Defined.

End Symmetry.

Associativity of binary products


Section Associativity.

  Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}.

  Definition cat_binprod_twist (x y z : A)
    : cat_binprod x (cat_binprod y z) $-> cat_binprod y (cat_binprod x z).
  Proof.
    nrapply cat_binprod_corec.
    - exact (cat_pr1 $o cat_pr2).
    - exact (fmap01 (fun x y ⇒ cat_binprod x y) x cat_pr2).
  Defined.

  Definition cat_binprod_pr1_twist (x y z : A)
    : cat_pr1 $o cat_binprod_twist x y z $== cat_pr1 $o cat_pr2
    := cat_binprod_beta_pr1 _ _.

  Definition cat_binprod_pr1_pr2_twist (x y z : A)
    : cat_pr1 $o cat_pr2 $o cat_binprod_twist x y z $== cat_pr1.
  Proof.
    nrefine (cat_assoc _ _ _ $@ _).
    nrefine ((_ $@L cat_binprod_beta_pr2 _ _) $@ _).
    nrapply cat_pr1_fmap01_binprod.
  Defined.

  Definition cat_binprod_pr2_pr2_twist (x y z : A)
    : cat_pr2 $o cat_pr2 $o cat_binprod_twist x y z $== cat_pr2 $o cat_pr2.
  Proof.
    nrefine (cat_assoc _ _ _ $@ _).
    nrefine ((_ $@L cat_binprod_beta_pr2 _ _) $@ _).
    nrapply cat_pr2_fmap01_binprod.
  Defined.

  Lemma cat_binprod_twist_cat_binprod_twist (x y z : A)
    : cat_binprod_twist x y z $o cat_binprod_twist y x z $== Id _.
  Proof.
    nrapply cat_binprod_eta_pr_x_xx_id.
    - nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_pr1_twist _ _ _ $@R _) $@ _).
      nrapply cat_binprod_pr1_pr2_twist.
    - nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_pr1_pr2_twist _ _ _ $@R _) $@ _).
      nrapply cat_binprod_pr1_twist.
    - nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_pr2_pr2_twist _ _ _ $@R _) $@ _).
      nrapply cat_binprod_pr2_pr2_twist.
  Defined.

  Definition cate_binprod_twist (x y z : A)
    : cat_binprod x (cat_binprod y z) $<~> cat_binprod y (cat_binprod x z).
  Proof.
    snrapply cate_adjointify.
    1,2: nrapply cat_binprod_twist.
    1,2: nrapply cat_binprod_twist_cat_binprod_twist.
  Defined.

  Definition cat_binprod_twist_nat {a a' b b' c c' : A}
    (f : a $-> a') (g : b $-> b') (h : c $-> c')
    : cat_binprod_twist a' b' c'
        $o fmap11 (fun x y ⇒ cat_binprod x y) f (fmap11 (fun x y ⇒ cat_binprod x y) g h)
      $== fmap11 (fun x y ⇒ cat_binprod x y) g (fmap11 (fun x y ⇒ cat_binprod x y) f h)
        $o cat_binprod_twist a b c.
  Proof.
    nrapply cat_binprod_eta_pr.
    - refine (cat_assoc_opp _ _ _ $@ _).
      nrefine ((cat_binprod_beta_pr1 _ _ $@R _) $@ _).
      nrefine (cat_assoc _ _ _ $@ _).
      nrefine ((_ $@L _) $@ _).
      1: nrapply cat_pr2_fmap11_binprod.
      nrefine (cat_assoc_opp _ _ _ $@ _).
      nrefine ((_ $@R _) $@ _).
      1: nrapply cat_pr1_fmap11_binprod.
      nrefine (_ $@ cat_assoc _ _ _).
      refine (_ $@ (_^$ $@R _)).
      2: nrapply cat_pr1_fmap11_binprod.
      refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$).
      nrapply cat_binprod_beta_pr1.
    - nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_beta_pr2 _ _ $@R _) $@ _).
      nrefine (_ $@ cat_assoc _ _ _).
      refine (_ $@ (_^$ $@R _)).
      2: nrapply cat_pr2_fmap11_binprod.
      refine (_ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$).
      2: nrapply cat_binprod_beta_pr2.
      refine (_^$ $@ _ $@ _).
      1,3: rapply fmap11_comp.
      rapply fmap22.
      1: exact (cat_idl _ $@ (cat_idr _)^$).
      nrapply cat_binprod_beta_pr2.
  Defined.

  Local Existing Instance symmetricbraiding_binprod.

  Local Instance associator_binprod : Associator (fun x y ⇒ cat_binprod x y).
  Proof.
    snrapply associator_twist.
    - exact _.
    - exact cat_binprod_twist.
    - exact cat_binprod_twist_cat_binprod_twist.
    - intros ? ? ? ? ? ?; exact cat_binprod_twist_nat.
  Defined.

  Definition cat_pr1_pr1_associator_binprod x y z
    : cat_pr1 $o cat_pr1 $o associator_binprod x y z $== cat_pr1.
  Proof.
    nrefine ((_ $@L Monoidal.associator_twist'_unfold _ _ _ _ _ _ _ _) $@ _).
    nrefine (cat_assoc _ _ _ $@ (_ $@L (cat_assoc_opp _ _ _ $@ (_ $@R _))) $@ _).
    1: nrapply cat_binprod_beta_pr1.
    do 2 nrefine (cat_assoc_opp _ _ _ $@ _).
    nrefine ((cat_binprod_pr1_pr2_twist _ _ _ $@R _) $@ _).
    nrapply cat_pr1_fmap01_binprod.
  Defined.

  Definition cat_pr2_pr1_associator_binprod x y z
    : cat_pr2 $o cat_pr1 $o associator_binprod x y z $== cat_pr1 $o cat_pr2.
  Proof.
    nrefine ((_ $@L Monoidal.associator_twist'_unfold _ _ _ _ _ _ _ _) $@ _).
    nrefine (cat_assoc _ _ _ $@ (_ $@L (cat_assoc_opp _ _ _ $@ (_ $@R _))) $@ _).
    1: nrapply cat_binprod_beta_pr1.
    do 2 nrefine (cat_assoc_opp _ _ _ $@ _).
    nrefine ((cat_binprod_pr2_pr2_twist _ _ _ $@R _) $@ _).
    nrefine (cat_assoc _ _ _ $@ (_ $@L cat_pr2_fmap01_binprod _ _) $@ _).
    exact (cat_assoc_opp _ _ _ $@ (cat_binprod_beta_pr2 _ _ $@R _)).
  Defined.

  Definition cat_pr2_associator_binprod x y z
    : cat_pr2 $o associator_binprod x y z $== cat_pr2 $o cat_pr2.
  Proof.
    nrefine ((_ $@L Monoidal.associator_twist'_unfold _ _ _ _ _ _ _ _) $@ _).
    nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_beta_pr2 _ _ $@R _) $@ _).
    nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_pr1_twist _ _ _ $@R _) $@ _).
    nrefine (cat_assoc _ _ _ $@ (_ $@L cat_pr2_fmap01_binprod _ _) $@ _).
    exact (cat_assoc_opp _ _ _ $@ (cat_binprod_beta_pr1 _ _ $@R _)).
  Defined.

  Context (unit : A) `{!IsTerminal unit}.

  Local Instance right_unitor_binprod
    : RightUnitor (fun x y ⇒ cat_binprod x y) unit.
  Proof.
    snrapply Build_NatEquiv.
    - intros a; unfold flip.
      snrapply cate_adjointify.
      + exact cat_pr1.
      + exact (cat_binprod_corec (Id _) (mor_terminal _ _)).
      + exact (cat_binprod_beta_pr1 _ _).
      + nrapply cat_binprod_eta_pr.
        × nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_beta_pr1 _ _ $@R _) $@ _).
          exact (cat_idl _ $@ (cat_idr _)^$).
        × nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_beta_pr2 _ _ $@R _) $@ _).
          exact ((mor_terminal_unique _ _ _)^$ $@ mor_terminal_unique _ _ _).
    - intros a b f.
      refine ((_ $@R _) $@ _ $@ (_ $@L _^$)).
      1,3: nrapply cate_buildequiv_fun.
      nrapply cat_binprod_beta_pr1.
  Defined.

  Local Existing Instance left_unitor_twist.

  Local Instance triangle_binprod
    : TriangleIdentity (fun x y ⇒ cat_binprod x y) unit.
  Proof.
    snrapply triangle_twist.
    intros a b.
    refine (fmap02 _ _ _ $@ _ $@ ((_ $@L fmap02 _ _ _^$) $@R _)).
    1,3: nrapply cate_buildequiv_fun.
    nrapply cat_binprod_eta_pr.
    - nrefine (cat_pr1_fmap01_binprod _ _ $@ _ $@ cat_assoc _ _ _).
      refine (_ $@ (((_^$ $@R _) $@ cat_assoc _ _ _) $@R _)).
      2: nrapply cat_binprod_beta_pr1.
      refine ((_ $@R _) $@ _)^$.
      1: nrapply cat_pr2_fmap01_binprod.
      nrapply cat_binprod_pr1_pr2_twist.
    - nrefine (cat_pr2_fmap01_binprod _ _ $@ _ $@ cat_assoc _ _ _).
      refine (_ $@ (((cat_binprod_beta_pr2 _ _)^$ $@R _) $@ cat_assoc _ _ _ $@R _)).
      refine ((_ $@R _) $@ _)^$.
      1: nrapply cat_pr1_fmap01_binprod.
      nrapply cat_binprod_beta_pr1.
  Defined.

  Local Instance pentagon_binprod
    : PentagonIdentity (fun x y ⇒ cat_binprod x y).
  Proof.
    intros a b c d.
    nrapply cat_binprod_eta_pr_xx_x.
    - nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ _).
      1: nrapply cat_pr1_pr1_associator_binprod.
      refine (_ $@ (_ $@L ((((_^$ $@R _) $@ cat_assoc _ _ _) $@R _)
        $@ cat_assoc _ _ _)) $@ cat_assoc_opp _ _ _).
      2: nrapply cat_pr1_fmap10_binprod.
      do 2 nrefine (_ $@ (_ $@L cat_assoc_opp _ _ _)).
      nrapply cat_binprod_eta_pr.
      + nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
        refine (_ $@ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
        1,3: nrapply cat_pr1_pr1_associator_binprod.
        do 2 nrefine (_ $@ cat_assoc _ _ _).
        refine (_^$ $@ (_^$ $@R _)).
        2: nrapply cat_pr1_pr1_associator_binprod.
        nrapply cat_pr1_fmap01_binprod.
      + nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
        refine (_ $@ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
        1,3: nrapply cat_pr2_pr1_associator_binprod.
        do 2 nrefine (_ $@ cat_assoc _ _ _).
        refine (_ $@ ((cat_assoc _ _ _ $@ (_ $@L (_^$ $@ cat_assoc _ _ _))
          $@ cat_assoc_opp _ _ _ $@ cat_assoc_opp _ _ _) $@R _)).
        2: nrapply cat_pr2_pr1_associator_binprod.
        refine (_^$ $@ (_ $@L _^$) $@ cat_assoc_opp _ _ _).
        2: nrapply cat_pr2_fmap01_binprod.
        nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _)).
        nrapply cat_pr1_pr1_associator_binprod.
    - nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ _).
      1: nrapply cat_pr2_pr1_associator_binprod.
      nrefine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
      nrefine ((_ $@L cat_pr2_associator_binprod _ _ _) $@ _).
      refine (_ $@ (_ $@L ((((_^$ $@R _) $@ cat_assoc _ _ _) $@R _) $@ cat_assoc _ _ _))).
      2: nrapply cat_pr1_fmap10_binprod.
      nrefine (_ $@ (_ $@L (cat_assoc_opp _ _ _ $@ cat_assoc_opp _ _ _))).
      refine (_ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
      2: nrapply cat_pr2_associator_binprod.
      refine (_ $@ (_ $@L ((_^$ $@R _) $@ cat_assoc _ _ _ $@ cat_assoc _ _ _)) $@ cat_assoc_opp _ _ _).
      2: nrapply cat_pr2_pr1_associator_binprod.
      refine (_ $@ (_ $@L ((_ $@L _^$) $@ cat_assoc_opp _ _ _))).
      2: nrapply cat_pr2_fmap01_binprod.
      refine (cat_assoc_opp _ _ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _ $@ cat_assoc _ _ _).
      nrapply cat_pr2_pr1_associator_binprod.
    - nrefine (cat_assoc_opp _ _ _ $@ (cat_pr2_associator_binprod _ _ _ $@R _) $@ _).
      nrefine (cat_assoc _ _ _ $@ (_ $@L (cat_pr2_associator_binprod _ _ _)) $@ _).
      refine (_ $@ (_^$ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L (cat_assoc_opp _ _ _))).
      2: nrapply cat_pr2_fmap10_binprod.
      refine (_ $@ cat_assoc_opp _ _ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
      2: nrapply cat_pr2_associator_binprod.
      refine (cat_assoc_opp _ _ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _
        $@ (_ $@L (cat_pr2_fmap01_binprod _ _)^$)).
      nrapply cat_pr2_associator_binprod.
  Defined.

  Local Instance hexagon_identity
    : HexagonIdentity (fun x y ⇒ cat_binprod x y).
  Proof.
    intros a b c.
    nrefine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
    nrapply cat_binprod_eta_pr.
    { nrefine (cat_assoc_opp _ _ _ $@ (cat_pr1_fmap10_binprod _ _ $@R _) $@ _).
      nrefine (cat_assoc _ _ _ $@ _).
      nrapply cat_binprod_eta_pr.
      { nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _ $@ cat_assoc _ _ _).
        refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
        1: nrapply cat_binprod_beta_pr1.
        2: nrapply cat_pr1_pr1_associator_binprod.
        nrefine (cat_assoc_opp _ _ _ $@ cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
        refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
        1: nrapply cat_pr2_pr1_associator_binprod.
        2: nrapply cat_binprod_beta_pr1.
        refine (cat_assoc _ _ _ $@ (_ $@L _) $@ cat_assoc_opp _ _ _ $@ (_ $@R _) $@ _^$).
        1: nrapply cat_pr2_fmap01_binprod.
        2: nrapply cat_pr2_associator_binprod.
        nrapply cat_binprod_beta_pr1. }
      nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _ $@ cat_assoc _ _ _).
      refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
      1: nrapply cat_binprod_beta_pr2.
      2: nrapply cat_pr2_pr1_associator_binprod.
      nrefine (cat_assoc_opp _ _ _ $@ cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
      refine ((_ $@R _) $@ _ $@ (((_ $@L _^$) $@ cat_assoc_opp _ _ _) $@R _)).
      1: nrapply cat_pr1_pr1_associator_binprod.
      2: nrapply cat_binprod_beta_pr2.
      refine (cat_pr1_fmap01_binprod _ _ $@ _^$).
      nrapply cat_pr1_pr1_associator_binprod. }
    nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _ $@ cat_assoc _ _ _).
    refine ((_ $@R _) $@ _ $@ ((_^$ $@R _) $@R _)).
    1: nrapply cat_pr2_fmap10_binprod.
    2: nrapply cat_pr2_associator_binprod.
    nrefine (cat_assoc_opp _ _ _ $@ (cat_pr2_associator_binprod _ _ _ $@R _) $@ _).
    nrefine (cat_assoc _ _ _ $@ (_ $@L _) $@ _ $@ (cat_assoc_opp _ _ _ $@R _)).
    1: nrapply cat_pr2_fmap01_binprod.
    refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ _^$ $@ ((_ $@L _^$) $@R _)).
    1,3: nrapply cat_binprod_beta_pr2.
    nrapply cat_pr2_pr1_associator_binprod.
  Defined.

  Global Instance ismonoidal_binprod
    : IsMonoidal A (fun x y ⇒ cat_binprod x y) unit
    := {}.

  Global Instance issymmetricmonoidal_binprod
    : IsSymmetricMonoidal A (fun x y ⇒ cat_binprod x y) unit
    := {}.

End Associativity.

Products in Type

Since we use the Yoneda lemma in this file, we therefore depend on WildCat.Universe which means these instances have to live here.
Global Instance hasbinaryproducts_type : HasBinaryProducts Type.
Proof.
  intros X Y.
  snrapply Build_BinaryProduct.
  - exact (X × Y).
  - exact fst.
  - exact snd.
  - intros Z f g z. exact (f z, g z).
  - reflexivity.
  - reflexivity.
  - intros Z f g p q x.
    nrapply path_prod.
    + exact (p x).
    + exact (q x).
Defined.

Assuming Funext, Type has all products.
Global Instance hasallproducts_type `{Funext} : HasAllProducts Type.
Proof.
  intros I x.
  snrapply Build_Product.
  - exact (∀ (i : I), x i).
  - intros i f. exact (f i).
  - intros A f a i. exact (f i a).
  - reflexivity.
  - intros A f g p a.
    exact (path_forall _ _ (fun i ⇒ p i a)).
Defined.