Library UniMath.CategoryTheory.Limits.BinProducts

Direct implementation of binary products

Written by: Benedikt Ahrens, Ralph Matthes Extended by: Anders Mörtberg and Tomi Pannila Extended by: Langston Barrett (@siddharthist), 2018

Contents

  • Definition of binary products
  • Definition of binary product functor (binproduct_functor)
  • Definition of a binary product structure on a functor category by taking pointwise binary products in the target category (BinProducts_functor_precat)
  • Binary products from limits (BinProducts_from_Lims)
  • Equivalent universal property: (C --> A) × (C --> B) (C --> A × B)
  • Terminal object as the unit (up to isomorphism) of binary products
  • Definition of the "associative" z-isomorphism BinProduct_assoc
  • Definition of the diagonal map diagonalMap

Definition of binary products

Section binproduct_def.

Context (C : category).

Definition isBinProduct (c d p : C) (p1 : p --> c) (p2 : p --> d) : UU :=
   (a : C) (f : a --> c) (g : a --> d),
  ∃! fg, (fg · p1 = f) × (fg · p2 = g).

Lemma isaprop_isBinProduct (c d p : C) (p1 : p --> c) (p2 : p --> d) :
  isaprop (isBinProduct c d p p1 p2).
Show proof.
  do 3 (apply impred_isaprop; intro).
  apply isapropiscontr.

Definition BinProduct (c d : C) : UU :=
   pp1p2 : ( p : C, (p --> c) × (p --> d)),
    isBinProduct c d (pr1 pp1p2) (pr1 (pr2 pp1p2)) (pr2 (pr2 pp1p2)).

Definition BinProducts : UU := (c d : C), BinProduct c d.
Definition hasBinProducts : UU := (c d : C), BinProduct c d .

Definition BinProductObject {c d : C} (P : BinProduct c d) : C := pr1 (pr1 P).
Coercion BinProductObject : BinProduct >-> ob.

Definition BinProductPr1 {c d : C} (P : BinProduct c d): BinProductObject P --> c :=
  pr1 (pr2 (pr1 P)).
Definition BinProductPr2 {c d : C} (P : BinProduct c d) : BinProductObject P --> d :=
   pr2 (pr2 (pr1 P)).

Definition isBinProduct_BinProduct {c d : C} (P : BinProduct c d) :
   isBinProduct c d (BinProductObject P) (BinProductPr1 P) (BinProductPr2 P).
Show proof.
  exact (pr2 P).

Definition BinProductArrow {c d : C} (P : BinProduct c d) {a : C} (f : a --> c) (g : a --> d) :
       a --> BinProductObject P.
Show proof.
  exact (pr1 (pr1 (isBinProduct_BinProduct P _ f g))).

Lemma BinProductPr1Commutes (c d : C) (P : BinProduct c d):
      (a : C) (f : a --> c) g, BinProductArrow P f g · BinProductPr1 P = f.
Show proof.
  intros a f g.
  exact (pr1 (pr2 (pr1 (isBinProduct_BinProduct P _ f g)))).

Lemma BinProductPr2Commutes (c d : C) (P : BinProduct c d):
      (a : C) (f : a --> c) g, BinProductArrow P f g · BinProductPr2 P = g.
Show proof.
  intros a f g.
  exact (pr2 (pr2 (pr1 (isBinProduct_BinProduct P _ f g)))).

Lemma BinProductArrowUnique (c d : C) (P : BinProduct c d) (x : C)
    (f : x --> c) (g : x --> d) (k : x --> BinProductObject P) :
    k · BinProductPr1 P = f -> k · BinProductPr2 P = g ->
      k = BinProductArrow P f g.
Show proof.
  intros; apply path_to_ctr; split; assumption.

Lemma BinProductArrowsEq (c d : C) (P : BinProduct c d) (x : C)
      (k1 k2 : x --> BinProductObject P) :
  k1 · BinProductPr1 P = k2 · BinProductPr1 P ->
  k1 · BinProductPr2 P = k2 · BinProductPr2 P ->
  k1 = k2.
Show proof.
  intros H1 H2.
  set (p1 := k1 · BinProductPr1 P).
  set (p2 := k1 · BinProductPr2 P).
  rewrite (BinProductArrowUnique _ _ P _ p1 p2 k1).
  apply pathsinv0.
  apply BinProductArrowUnique.
  unfold p1. apply pathsinv0. apply H1.
  unfold p2. apply pathsinv0. apply H2.
  apply idpath. apply idpath.

Definition make_BinProduct (a b : C) :
   (c : C) (f : Cc,a) (g : Cc,b),
   isBinProduct _ _ _ f g -> BinProduct a b.
Show proof.
  intros.
  use tpair.
  - exists c.
    exists f.
    exact g.
  - exact X.

Definition make_isBinProduct (a b p : C)
  (pa : Cp,a) (pb : Cp,b) :
  ( (c : C) (f : Cc,a) (g : Cc,b),
    ∃! k : Cc,p, k · pa = f × k · pb = g) ->
  isBinProduct a b p pa pb.
Show proof.
  intros H c cc g.
  apply H.

Lemma BinProductArrowEta (c d : C) (P : BinProduct c d) (x : C)
    (f : x --> BinProductObject P) :
    f = BinProductArrow P (f · BinProductPr1 P) (f · BinProductPr2 P).
Show proof.
  apply BinProductArrowUnique;
  apply idpath.

Definition BinProductOfArrows {c d : C} (Pcd : BinProduct c d) {a b : C}
    (Pab : BinProduct a b) (f : a --> c) (g : b --> d) :
          BinProductObject Pab --> BinProductObject Pcd :=
    BinProductArrow Pcd (BinProductPr1 Pab · f) (BinProductPr2 Pab · g).

Lemma BinProductOfArrowsPr1 {c d : C} (Pcd : BinProduct c d) {a b : C}
    (Pab : BinProduct a b) (f : a --> c) (g : b --> d) :
    BinProductOfArrows Pcd Pab f g · BinProductPr1 Pcd = BinProductPr1 Pab · f.
Show proof.
  unfold BinProductOfArrows.
  rewrite BinProductPr1Commutes.
  apply idpath.

Lemma BinProductOfArrowsPr2 {c d : C} (Pcd : BinProduct c d) {a b : C}
    (Pab : BinProduct a b) (f : a --> c) (g : b --> d) :
    BinProductOfArrows Pcd Pab f g · BinProductPr2 Pcd = BinProductPr2 Pab · g.
Show proof.
  unfold BinProductOfArrows.
  rewrite BinProductPr2Commutes.
  apply idpath.

Lemma postcompWithBinProductArrow {c d : C} (Pcd : BinProduct c d) {a b : C}
    (Pab : BinProduct a b) (f : a --> c) (g : b --> d)
    {x : C} (k : x --> a) (h : x --> b) :
        BinProductArrow Pab k h · BinProductOfArrows Pcd Pab f g =
         BinProductArrow Pcd (k · f) (h · g).
Show proof.
  apply BinProductArrowUnique.
  - rewrite <- assoc, BinProductOfArrowsPr1.
    rewrite assoc, BinProductPr1Commutes.
    apply idpath.
  - rewrite <- assoc, BinProductOfArrowsPr2.
    rewrite assoc, BinProductPr2Commutes.
    apply idpath.

Lemma precompWithBinProductArrow {c d : C} (Pcd : BinProduct c d) {a : C}
    (f : a --> c) (g : a --> d) {x : C} (k : x --> a) :
       k · BinProductArrow Pcd f g = BinProductArrow Pcd (k · f) (k · g).
Show proof.
  apply BinProductArrowUnique.
  - rewrite <- assoc, BinProductPr1Commutes;
     apply idpath.
  - rewrite <- assoc, BinProductPr2Commutes;
     apply idpath.

End binproduct_def.

Section BinProducts.

Context (C : category) (CC : BinProducts C).

Definition BinProductOfArrows_comp (a b c d x y : C) (f : a --> c) (f' : b --> d) (g : c --> x) (g' : d --> y)
  : BinProductOfArrows _ (CC c d) (CC a b) f f' ·
    BinProductOfArrows _ (CC _ _) (CC _ _) g g'
    =
    BinProductOfArrows _ (CC _ _) (CC _ _)(f · g) (f' · g').
Show proof.
  apply BinProductArrowUnique.
  - rewrite <- assoc.
    rewrite BinProductOfArrowsPr1.
    rewrite assoc.
    rewrite BinProductOfArrowsPr1.
    apply pathsinv0.
    apply assoc.
  - rewrite <- assoc.
    rewrite BinProductOfArrowsPr2.
    rewrite assoc.
    rewrite BinProductOfArrowsPr2.
    apply pathsinv0.
    apply assoc.

Lemma BinProductOfArrows_idxcomp {a b c d : C} (f:C b, c ) (g:C c, d )
  : BinProductOfArrows _ (CC a c) (CC a b) (identity a) f ·
      BinProductOfArrows _ (CC _ _) (CC _ _) (identity a) g
  =
  BinProductOfArrows _ (CC _ _) (CC _ _)(identity a) (f·g).
Show proof.
  now rewrite BinProductOfArrows_comp, id_right.

Lemma BinProductOfArrows_compxid {a b c d : C} (f:C b, c ) (g:C c, d )
  : BinProductOfArrows _ (CC c a) (CC b a) f (identity a) ·
      BinProductOfArrows _ (CC _ _) (CC _ _) g (identity a)
      =
      BinProductOfArrows _ (CC _ _) (CC _ _) (f·g) (identity a).
Show proof.
  now rewrite BinProductOfArrows_comp, id_right.

Lemma BinProductOfArrows_id (a b:C)
  : BinProductOfArrows _ (CC a b) (CC a b) (identity a) (identity b)
    = identity _ .
Show proof.
  unfold BinProductOfArrows.
  use pathsinv0.
  use BinProductArrowUnique.
  + now rewrite id_left, id_right.
  + now rewrite id_left, id_right.

End BinProducts.

Section BinProduct_unique.

Context (C : category) (CC : BinProducts C) (a b : C).

Lemma BinProduct_endo_is_identity (P : BinProduct _ a b)
  (k : BinProductObject _ P --> BinProductObject _ P)
  (H1 : k · BinProductPr1 _ P = BinProductPr1 _ P)
  (H2 : k · BinProductPr2 _ P = BinProductPr2 _ P)
  : identity _ = k.
Show proof.
  apply pathsinv0.
  eapply pathscomp0.
  apply BinProductArrowEta.
  apply pathsinv0.
  apply BinProductArrowUnique; apply pathsinv0.
  + rewrite id_left. exact H1.
  + rewrite id_left. exact H2.

End BinProduct_unique.

Binary products from limits (BinProducts_from_Lims)


Section BinProducts_from_Lims.

Context (C : category).

Definition two_graph : graph := (bool,,λ _ _,empty).

Definition binproduct_diagram (a b : C) : diagram two_graph C.
Show proof.
exists (λ x : bool, if x then a else b).
abstract (intros u v F; induction F).

Definition Binproduct {a b c : C} (f : c --> a) (g : c --> b) :
  cone (binproduct_diagram a b) c.
Show proof.
use make_cone.
+ intros x; induction x; assumption.
+ abstract (intros x y e; destruct e).

Lemma BinProducts_from_Lims : Lims_of_shape two_graph C -> BinProducts C.
Show proof.
intros H a b.
set (LC := H (binproduct_diagram a b)).
use make_BinProduct.
+ apply (lim LC).
+ apply (limOut LC true).
+ apply (limOut LC false).
+ apply (make_isBinProduct C); intros c f g.
  use unique_exists.
  - apply limArrow, (Binproduct f g).
  - abstract (split;
      [ apply (limArrowCommutes LC c (Binproduct f g) true)
      | apply (limArrowCommutes LC c (Binproduct f g) false) ]).
  - abstract (intros h; apply isapropdirprod; apply C).
  - abstract (now intros h [H1 H2]; apply limArrowUnique; intro x; induction x).

End BinProducts_from_Lims.

Section test.

  Context (C : category) (H : BinProducts C).

Arguments BinProductObject [C] c d {_}.

Local Notation "c 'x' d" := (BinProductObject c d )(at level 5).
End test.

Definition of binary product functor (binproduct_functor)


Section binproduct_functor.

Context {C : category} (PC : BinProducts C).

Definition binproduct_functor_data :
  functor_data (category_binproduct C C) C.
Show proof.
use tpair.
- intros p.
  apply (BinProductObject _ (PC (pr1 p) (pr2 p))).
- intros p q f.
  apply (BinProductOfArrows _ (PC (pr1 q) (pr2 q))
                           (PC (pr1 p) (pr2 p)) (pr1 f) (pr2 f)).

Definition binproduct_functor : functor (category_binproduct C C) C.
Show proof.
apply (tpair _ binproduct_functor_data).
abstract (split;
  [ intro x; simpl; apply pathsinv0, BinProduct_endo_is_identity;
    [ now rewrite BinProductOfArrowsPr1, id_right
    | now rewrite BinProductOfArrowsPr2, id_right ]
  | now intros x y z f g; simpl; rewrite BinProductOfArrows_comp]).

End binproduct_functor.

Definition BinProduct_of_functors_alt {C D : category} (HD : BinProducts D)
  (F G : functor C D) : functor C D :=
  functor_composite (bindelta_functor C)
     (functor_composite (pair_functor F G) (binproduct_functor HD)).

In the following section we show that if the morphism to components are zero, then the unique morphism factoring through the binproduct is the zero morphism.
Section BinProduct_zeroarrow.

  Context (C : category) (Z : Zero C).

  Lemma BinProductArrowZero {x y z: C} {BP : BinProduct C x y} (f : z --> x) (g : z --> y) :
    f = ZeroArrow Z _ _ -> g = ZeroArrow Z _ _ -> BinProductArrow C BP f g = ZeroArrow Z _ _ .
  Show proof.
    intros X X0. apply pathsinv0.
    use BinProductArrowUnique.
    rewrite X. apply ZeroArrow_comp_left.
    rewrite X0. apply ZeroArrow_comp_left.

End BinProduct_zeroarrow.

Definition of a binary product structure on a functor category

Goal: lift binary products from the target (pre)category to the functor (pre)category
Section def_functor_pointwise_binprod.

Context (C D : category) (HD : BinProducts D).

Section BinProduct_of_functors.

Context (F G : functor C D).

Local Notation "c ⊗ d" := (BinProductObject _ (HD c d)).

Definition BinProduct_of_functors_ob (c : C) : D := F c G c.

Definition BinProduct_of_functors_mor (c c' : C) (f : c --> c')
  : BinProduct_of_functors_ob c --> BinProduct_of_functors_ob c'
  := BinProductOfArrows _ _ _ (#F f) (#G f).

Definition BinProduct_of_functors_data : functor_data C D.
Show proof.

Lemma is_functor_BinProduct_of_functors_data : is_functor BinProduct_of_functors_data.
Show proof.
  split; simpl; intros.
  - red; intros; simpl in *.
    apply pathsinv0.
    unfold BinProduct_of_functors_mor.
    apply BinProduct_endo_is_identity.
    + rewrite BinProductOfArrowsPr1.
      rewrite functor_id.
      apply id_right.
    + rewrite BinProductOfArrowsPr2.
      rewrite functor_id.
      apply id_right.
  - red; intros; simpl in *.
    unfold BinProduct_of_functors_mor.
    do 2 rewrite functor_comp.
    apply pathsinv0.
    apply BinProductOfArrows_comp.

Definition BinProduct_of_functors : functor C D :=
  tpair _ _ is_functor_BinProduct_of_functors_data.

Lemma BinProduct_of_functors_alt_eq_BinProduct_of_functors :
  BinProduct_of_functors_alt HD F G = BinProduct_of_functors.
Show proof.
now apply (functor_eq _ _ D).

Definition binproduct_nat_trans_pr1_data : c, BinProduct_of_functors c --> F c
  := λ c : C, BinProductPr1 _ (HD (F c) (G c)).

Lemma is_nat_trans_binproduct_nat_trans_pr1_data
  : is_nat_trans _ _ binproduct_nat_trans_pr1_data.
Show proof.
  red.
  intros c c' f.
  unfold binproduct_nat_trans_pr1_data.
  unfold BinProduct_of_functors. simpl.
  unfold BinProduct_of_functors_mor.
  apply BinProductOfArrowsPr1.

Definition binproduct_nat_trans_pr1 : nat_trans _ _
  := tpair _ _ is_nat_trans_binproduct_nat_trans_pr1_data.

Definition binproduct_nat_trans_pr2_data : c, BinProduct_of_functors c --> G c
  := λ c : C, BinProductPr2 _ (HD (F c) (G c)).

Lemma is_nat_trans_binproduct_nat_trans_pr2_data
  : is_nat_trans _ _ binproduct_nat_trans_pr2_data.
Show proof.
  red.
  intros c c' f.
  unfold binproduct_nat_trans_pr2_data.
  unfold BinProduct_of_functors. simpl.
  unfold BinProduct_of_functors_mor.
  apply BinProductOfArrowsPr2.

Definition binproduct_nat_trans_pr2 : nat_trans _ _
  := tpair _ _ is_nat_trans_binproduct_nat_trans_pr2_data.

Section vertex.

The product morphism of a diagram with vertex A

Context (A : functor C D) (f : A F) (g : A G).

Definition binproduct_nat_trans_data : c, A c --> BinProduct_of_functors c.
Show proof.
  intro c.
  apply BinProductArrow.
  - exact (f c).
  - exact (g c).

Lemma is_nat_trans_binproduct_nat_trans_data : is_nat_trans _ _ binproduct_nat_trans_data.
Show proof.
  intros a b k.
  simpl.
  unfold BinProduct_of_functors_mor.
  unfold binproduct_nat_trans_data.
  set (XX:=postcompWithBinProductArrow).
  set (X1 := XX D _ _ (HD (F b) (G b))).
  set (X2 := X1 _ _ (HD (F a) (G a))).
  rewrite X2.
  clear X2 X1 XX.
  set (XX:=precompWithBinProductArrow).
  set (X1 := XX D _ _ (HD (F b) (G b))).
  rewrite X1.
  rewrite (nat_trans_ax f).
  rewrite (nat_trans_ax g).
  apply idpath.

Definition binproduct_nat_trans : nat_trans _ _
  := tpair _ _ is_nat_trans_binproduct_nat_trans_data.

Lemma binproduct_nat_trans_Pr1Commutes :
  nat_trans_comp _ _ _ binproduct_nat_trans binproduct_nat_trans_pr1 = f.
Show proof.
  apply nat_trans_eq.
  - apply D.
  - intro c; simpl.
    apply BinProductPr1Commutes.

Lemma binproduct_nat_trans_Pr2Commutes :
  nat_trans_comp _ _ _ binproduct_nat_trans binproduct_nat_trans_pr2 = g.
Show proof.
  apply nat_trans_eq.
  - apply D.
  - intro c; simpl.
    apply BinProductPr2Commutes.

End vertex.

Lemma binproduct_nat_trans_univ_prop (A : [C, D])
  (f : A --> (F:[C,D])) (g : A --> (G:[C,D])) :
   
   t : fg : A --> (BinProduct_of_functors:[C,D]),
       fg · (binproduct_nat_trans_pr1 : (BinProduct_of_functors:[C,D]) --> F) = f
      ×
       fg · (binproduct_nat_trans_pr2 : (BinProduct_of_functors:[C,D]) --> G) = g,
   t =
   tpair
     (λ fg : A --> (BinProduct_of_functors:[C,D]),
      fg · (binproduct_nat_trans_pr1 : (BinProduct_of_functors:[C,D]) --> F) = f
   ×
      fg · (binproduct_nat_trans_pr2 : (BinProduct_of_functors:[C,D]) --> G) = g)
     (binproduct_nat_trans A f g)
     (make_dirprod (binproduct_nat_trans_Pr1Commutes A f g)
        (binproduct_nat_trans_Pr2Commutes A f g)).
Show proof.
  intro t.
  simpl in *.
  destruct t as [t1 [ta tb]].
  simpl in *.
  apply subtypePath.
  - intro.
    simpl.
    apply isapropdirprod;
    apply isaset_nat_trans;
    apply D.
  - simpl.
    apply nat_trans_eq.
    + apply D.
    + intro c.
      unfold binproduct_nat_trans.
      simpl.
      unfold binproduct_nat_trans_data.
      apply BinProductArrowUnique.
      * apply (nat_trans_eq_pointwise ta).
      * apply (nat_trans_eq_pointwise tb).

Definition functor_precat_binproduct_cone
  : BinProduct [C, D] F G.
Show proof.
use make_BinProduct.
- apply BinProduct_of_functors.
- apply binproduct_nat_trans_pr1.
- apply binproduct_nat_trans_pr2.
- use make_isBinProduct.
  + intros A f g.
    exists (tpair _ (binproduct_nat_trans A f g)
             (make_dirprod (binproduct_nat_trans_Pr1Commutes _ _ _ )
                          (binproduct_nat_trans_Pr2Commutes _ _ _ ))).
    apply binproduct_nat_trans_univ_prop.

End BinProduct_of_functors.

Definition BinProducts_functor_precat : BinProducts [C, D].
Show proof.
  intros F G.
  apply functor_precat_binproduct_cone.

End def_functor_pointwise_binprod.

Section BinProduct_of_functors_commutative.

  Context (C D : category) (BD : BinProducts D) (F G : functor C D).

Definition BinProduct_of_functors_commutes_data :
  nat_trans_data (BinProduct_of_functors C D BD F G) (BinProduct_of_functors C D BD G F).
Show proof.
  intro c.
  use BinProductArrow.
  - apply BinProductPr2.
  - apply BinProductPr1.

Definition BinProduct_of_functors_commutes_invdata :
  nat_trans_data (BinProduct_of_functors C D BD G F) (BinProduct_of_functors C D BD F G).
Show proof.
  intro c.
  use BinProductArrow.
  - apply BinProductPr2.
  - apply BinProductPr1.

Lemma BinProduct_of_functors_commutes_is_inverse (c: C) :
  is_inverse_in_precat (BinProduct_of_functors_commutes_data c) (BinProduct_of_functors_commutes_invdata c).
Show proof.
  split.
  - apply BinProductArrowsEq.
    + rewrite assoc'.
      etrans.
      { apply maponpaths.
        apply BinProductPr1Commutes. }
      etrans.
      { apply BinProductPr2Commutes. }
      apply pathsinv0, id_left.
    + rewrite assoc'.
      etrans.
      { apply maponpaths.
        apply BinProductPr2Commutes. }
      etrans.
      { apply BinProductPr1Commutes. }
      apply pathsinv0, id_left.
  - apply BinProductArrowsEq.
    + rewrite assoc'.
      etrans.
      { apply maponpaths.
        apply BinProductPr1Commutes. }
      etrans.
      { apply BinProductPr2Commutes. }
      apply pathsinv0, id_left.
    + rewrite assoc'.
      etrans.
      { apply maponpaths.
        apply BinProductPr2Commutes. }
      etrans.
      { apply BinProductPr1Commutes. }
      apply pathsinv0, id_left.

Lemma BinProduct_of_functors_commutes_law : is_nat_trans _ _ BinProduct_of_functors_commutes_data.
Show proof.
  intros c c' f.
  cbn.
  unfold BinProduct_of_functors_mor.
  etrans.
  2: { apply pathsinv0, postcompWithBinProductArrow. }
  apply BinProductArrowUnique.
  - rewrite assoc'.
    etrans.
    { apply maponpaths.
      apply BinProductPr1Commutes. }
    etrans.
    { apply BinProductOfArrowsPr2. }
    apply idpath.
  - rewrite assoc'.
    etrans.
    { apply maponpaths.
      apply BinProductPr2Commutes. }
    etrans.
    { apply BinProductOfArrowsPr1. }
    apply idpath.

Definition BinProduct_of_functors_commutes :
  nat_z_iso (BinProduct_of_functors C D BD F G) (BinProduct_of_functors C D BD G F).
Show proof.

End BinProduct_of_functors_commutative.

Section PairNatTrans.
  Context {C₁ C₂ C₃ : category}
          {F : C₁ C₂}
          {G₁ G₂ G₃ : C₂ C₃}
          (H : BinProducts C₃)
          (η₁ : F G₁ F G₂)
          (η₂ : F G₁ F G₃).

  Local Definition pair_nat_trans_data
    : nat_trans_data (F G₁) (F BinProduct_of_functors C₂ C₃ H G₂ G₃).
  Show proof.
    intros x.
    apply (BinProductArrow).
    - exact (η₁ x).
    - exact (η₂ x).

  Definition pair_nat_trans_is_nat_trans
    : is_nat_trans
        (F G₁)
        (F BinProduct_of_functors C₂ C₃ H G₂ G₃)
        pair_nat_trans_data.
  Show proof.
    intros x y f ; cbn.
    refine (precompWithBinProductArrow _ _ _ _ _ @ _).
    pose (pr2 η₁ x y f) as p.
    pose (pr2 η₂ x y f) as q.
    cbn in p, q.
    refine (_ @ _).
    {
      apply maponpaths.
      exact q.
    }
    refine (_ @ _).
    {
      apply maponpaths_2.
      exact p.
    }
    unfold BinProduct_of_functors_mor, BinProductOfArrows, BinProductPr1, BinProductPr2.
    exact (!(postcompWithBinProductArrow _ _ _ _ _ _ _)).

  Definition pair_nat_trans
    : F G₁ F (BinProduct_of_functors _ _ H G₂ G₃).
  Show proof.
    use make_nat_trans.
    - exact pair_nat_trans_data.
    - exact pair_nat_trans_is_nat_trans.
End PairNatTrans.

Construction of BinProduct from an isomorphism to BinProduct.

Section BinProductFromIso.

  Context (C : category).

  Local Lemma iso_to_isBinProduct_comm {x y z : C} (BP : BinProduct C x y)
        (i : iso z (BinProductObject C BP)) (w : C) (f : w --> x) (g : w --> y) :
    (BinProductArrow C BP f g · inv_from_iso i · (i · BinProductPr1 C BP) = f)
      × (BinProductArrow C BP f g · inv_from_iso i · (i · BinProductPr2 C BP) = g).
  Show proof.
    split.
    - rewrite <- assoc. rewrite (assoc _ i).
      rewrite (iso_after_iso_inv i). rewrite id_left.
      apply BinProductPr1Commutes.
    - rewrite <- assoc. rewrite (assoc _ i).
      rewrite (iso_after_iso_inv i). rewrite id_left.
      apply BinProductPr2Commutes.

  Local Lemma iso_to_isBinProduct_unique {x y z : C} (BP : BinProduct C x y)
        (i : iso z (BinProductObject C BP)) (w : C) (f : C w, x) (g : C w, y) (y0 : C w, z)
        (T : y0 · (i · BinProductPr1 C BP) = f × y0 · (i · BinProductPr2 C BP) = g) :
    y0 = BinProductArrow C BP f g · iso_inv_from_iso i.
  Show proof.
    apply (post_comp_with_iso_is_inj _ _ i (pr2 i)).
    rewrite <- assoc. cbn. rewrite (iso_after_iso_inv i). rewrite id_right.
    apply BinProductArrowUnique.
    - rewrite <- assoc. apply (dirprod_pr1 T).
    - rewrite <- assoc. apply (dirprod_pr2 T).

  Lemma iso_to_isBinProduct {x y z : C} (BP : BinProduct C x y)
        (i : iso z (BinProductObject C BP)) :
    isBinProduct C _ _ z (i · (BinProductPr1 C BP)) (i · (BinProductPr2 C BP)).
  Show proof.
    intros w f g.
    use unique_exists.
    - exact ((BinProductArrow C BP f g) · (iso_inv_from_iso i)).
    - abstract (exact (iso_to_isBinProduct_comm BP i w f g)).
    - abstract (intro; apply isapropdirprod; apply C).
    - abstract (intros y0 T; exact (iso_to_isBinProduct_unique BP i w f g y0 T)).

  Definition iso_to_BinProduct {x y z : C} (BP : BinProduct C x y)
             (i : iso z (BinProductObject C BP)) :
    BinProduct C x y := make_BinProduct C _ _ z
                                              (i · (BinProductPr1 C BP))
                                              (i · (BinProductPr2 C BP))
                                              (iso_to_isBinProduct BP i).

End BinProductFromIso.

Equivalent universal property: (C --> A) × (C --> B) (C --> A × B)

Compare to weqfuntoprodtoprod.

Section EquivalentDefinition.
  Context {C : category} {c d p : ob C} (p1 : p --> c) (p2 : p --> d).

  Definition postcomp_with_projections (a : ob C) (f : a --> p) :
    (a --> c) × (a --> d) := make_dirprod (f · p1) (f · p2).

  Definition isBinProduct' : UU := a : ob C, isweq (postcomp_with_projections a).

  Definition isBinProduct'_weq (is : isBinProduct') :
     a, (a --> p) (a --> c) × (a --> d) :=
    λ a, make_weq (postcomp_with_projections a) (is a).

  Lemma isBinProduct'_to_isBinProduct :
    isBinProduct' -> isBinProduct _ _ _ p p1 p2.
  Show proof.
    intros isBP' ? f g.
    apply (@iscontrweqf (hfiber (isBinProduct'_weq isBP' _)
                                (make_dirprod f g))).
    - use weqfibtototal; intro; cbn.
      unfold postcomp_with_projections.
      apply pathsdirprodweq.
    - apply weqproperty.

  Lemma isBinProduct_to_isBinProduct' :
    isBinProduct _ _ _ p p1 p2 -> isBinProduct'.
  Show proof.
    intros isBP ? fg.
    unfold hfiber, postcomp_with_projections.
    apply (@iscontrweqf ( u : C a, p , u · p1 = pr1 fg × u · p2 = pr2 fg)).
    - use weqfibtototal; intro; cbn.
      apply invweq, pathsdirprodweq.
    - exact (isBP a (pr1 fg) (pr2 fg)).


End EquivalentDefinition.

Match non-implicit arguments of isBinProduct
Arguments isBinProduct' _ _ _ _ _ : clear implicits.

Terminal object as the unit (up to isomorphism) of binary products

T × x x
Lemma terminal_binprod_unit_l_z_aux {C : category} (T : Terminal C) (BC : BinProducts C) (x : C) :
  is_inverse_in_precat (BinProductPr2 C (BC T x))
    (BinProductArrow C (BC T x) (TerminalArrow T x) (identity x)).
Show proof.
  unfold is_inverse_in_precat.
  split; [|apply BinProductPr2Commutes].
  refine (precompWithBinProductArrow _ _ _ _ _ @ _).
  refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
  apply maponpaths_12.
  - apply TerminalArrowEq.
  - exact (id_right _ @ !id_left _).

Lemma terminal_binprod_unit_l_z {C : category}
      (T : Terminal C) (BC : BinProducts C) (x : C) :
  is_z_isomorphism (BinProductPr2 C (BC T x)).
Show proof.
  use make_is_z_isomorphism.
  - apply BinProductArrow.
    +
The unique x -> T
      apply TerminalArrow.
    + apply identity.
  - apply terminal_binprod_unit_l_z_aux.

x × T x
Lemma terminal_binprod_unit_r_z_aux {C : category} (T : Terminal C) (BC : BinProducts C) (x : C) :
  is_inverse_in_precat (BinProductPr1 C (BC x T)) (BinProductArrow C (BC x T) (identity x)
                                                     (TerminalArrow T x)).
Show proof.
  unfold is_inverse_in_precat.
  split; [|apply BinProductPr1Commutes].
  refine (precompWithBinProductArrow _ _ _ _ _ @ _).
  refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
  apply maponpaths_12.
  - exact (id_right _ @ !id_left _).
  - apply TerminalArrowEq.

Lemma terminal_binprod_unit_r_z {C : category}
      (T : Terminal C) (BC : BinProducts C) (x : C) :
  is_z_isomorphism (BinProductPr1 C (BC x T)).
Show proof.
  use make_is_z_isomorphism.
  - apply BinProductArrow.
    + apply identity.
    +
The unique x -> T
      apply TerminalArrow.
  - apply terminal_binprod_unit_r_z_aux.

Section BinProduct_of_functors_with_terminal.

Context (C D : category) (HD : BinProducts D) (TD : Terminal D) (F : functor C D).

Definition terminal_BinProduct_of_functors_unit_l_data :
  nat_trans_data (BinProduct_of_functors C D HD (constant_functor C D TD) F) F.
Show proof.
  intro c. exact (BinProductPr2 D (HD TD (F c))).

Lemma terminal_BinProduct_of_functors_unit_l_law :
  is_nat_trans _ _ terminal_BinProduct_of_functors_unit_l_data.
Show proof.
  intros c c' f.
  apply BinProductOfArrowsPr2.

Definition terminal_BinProduct_of_functors_unit_l :
  nat_z_iso (BinProduct_of_functors _ _ HD (constant_functor _ _ TD) F) F.
Show proof.

Definition terminal_BinProduct_of_functors_unit_r_data :
  nat_trans_data (BinProduct_of_functors C D HD F (constant_functor C D TD)) F.
Show proof.
  intro c. exact (BinProductPr1 D (HD (F c) TD)).

Lemma terminal_BinProduct_of_functors_unit_r_law :
  is_nat_trans _ _ terminal_BinProduct_of_functors_unit_r_data.
Show proof.
  intros c c' f.
  apply BinProductOfArrowsPr1.

Definition terminal_BinProduct_of_functors_unit_r :
  nat_z_iso (BinProduct_of_functors _ _ HD F (constant_functor _ _ TD)) F.
Show proof.

End BinProduct_of_functors_with_terminal.

In a univalent category, the type of binary products on a given diagram is a proposition
Definition eq_BinProduct
           {C : category}
           {x y : C}
           (prod₁ prod₂ : BinProduct C x y)
           (q : BinProductObject _ prod₁ = BinProductObject _ prod₂)
           (e₁ : BinProductPr1 _ prod₁ = idtoiso q · BinProductPr1 _ prod₂)
           (e₂ : BinProductPr2 _ prod₁ = idtoiso q · BinProductPr2 _ prod₂)
  : prod₁ = prod₂.
Show proof.
  use subtypePath.
  {
    intro.
    repeat (use impred ; intro).
    use isapropiscontr.
  }
  use total2_paths_f.
  - exact q.
  - rewrite transportf_dirprod.
    rewrite <- !idtoiso_precompose.
    rewrite !idtoiso_inv.
    use pathsdirprod ; cbn ; use z_iso_inv_on_right.
    + exact e₁.
    + exact e₂.

Section IsoBinProduct.
  Context {C : category}
          {x y : C}
          (p₁ p₂ : BinProduct C x y).

  Let f : BinProductObject C p₁ --> BinProductObject C p₂
      := BinProductArrow _ _ (BinProductPr1 _ p₁) (BinProductPr2 _ p₁).

  Let g : BinProductObject C p₂ --> BinProductObject C p₁
      := BinProductArrow _ _ (BinProductPr1 _ p₂) (BinProductPr2 _ p₂).

  Local Lemma iso_between_BinProduct_eq
    : is_inverse_in_precat f g.
  Show proof.
    unfold f, g.
    split.
    - use BinProductArrowsEq.
      + rewrite assoc'.
        rewrite !BinProductPr1Commutes.
        rewrite id_left.
        apply idpath.
      + rewrite assoc'.
        rewrite !BinProductPr2Commutes.
        rewrite id_left.
        apply idpath.
    - use BinProductArrowsEq.
      + rewrite assoc'.
        rewrite !BinProductPr1Commutes.
        rewrite id_left.
        apply idpath.
      + rewrite assoc'.
        rewrite !BinProductPr2Commutes.
        rewrite id_left.
        apply idpath.

  Definition iso_between_BinProduct
    : z_iso (BinProductObject C p₁) (BinProductObject C p₂).
  Show proof.
    use make_z_iso.
    - exact f.
    - exact g.
    - exact iso_between_BinProduct_eq.

End IsoBinProduct.

Definition isaprop_BinProduct
           {C : category}
           (HC : is_univalent C)
           (x y : C)
  : isaprop (BinProduct C x y).
Show proof.
  use invproofirrelevance.
  intros p₁ p₂.
  use eq_BinProduct.
  - refine (isotoid _ HC _).
    apply iso_between_BinProduct.
  - rewrite idtoiso_isotoid ; cbn.
    rewrite BinProductPr1Commutes.
    apply idpath.
  - rewrite idtoiso_isotoid ; cbn.
    rewrite BinProductPr2Commutes.
    apply idpath.

Products when the projections are equal
Definition isBinProduct_eq_arrow
           {C : category}
           {x y z : C}
           {π π₁' : z --> x}
           (p₁ : π = π₁')
           {π π₂' : z --> y}
           (p₂ : π = π₂')
           (H : isBinProduct C x y z π π)
  : isBinProduct C x y z π₁' π₂'.
Show proof.
  pose (P := make_BinProduct _ _ _ _ _ _ H).
  use make_isBinProduct.
  intros w f g.
  use iscontraprop1.
  - abstract
      (induction p₁, p₂ ;
       apply isapropifcontr ;
       apply H).
  - simple refine (_ ,, _ ,, _).
    + exact (BinProductArrow _ P f g).
    + abstract
        (induction p₁ ;
         exact (BinProductPr1Commutes _ _ _ P _ f g)).
    + abstract
        (induction p₂ ;
         exact (BinProductPr2Commutes _ _ _ P _ f g)).

Products of isos
Section BinProductOfIsos.
  Context {C : category}
          {a b c d : C}
          (Pab : BinProduct C a b)
          (Pcd : BinProduct C c d)
          (f : z_iso a c)
          (g : z_iso b d).

  Let fg : BinProductObject _ Pab --> BinProductObject _ Pcd
    := BinProductOfArrows _ _ _ f g.

  Let fg_inv : BinProductObject _ Pcd --> BinProductObject _ Pab
    := BinProductOfArrows _ _ _ (inv_from_z_iso f) (inv_from_z_iso g).

  Definition binproduct_of_z_iso_inv
    : is_inverse_in_precat fg fg_inv.
  Show proof.
    split ; use BinProductArrowsEq ; unfold fg, fg_inv.
    - rewrite !assoc'.
      rewrite BinProductOfArrowsPr1.
      rewrite !assoc.
      rewrite BinProductOfArrowsPr1.
      rewrite !assoc'.
      rewrite z_iso_inv_after_z_iso.
      rewrite id_left, id_right.
      apply idpath.
    - rewrite !assoc'.
      rewrite BinProductOfArrowsPr2.
      rewrite !assoc.
      rewrite BinProductOfArrowsPr2.
      rewrite !assoc'.
      rewrite z_iso_inv_after_z_iso.
      rewrite id_left, id_right.
      apply idpath.
    - rewrite !assoc'.
      rewrite BinProductOfArrowsPr1.
      rewrite !assoc.
      rewrite BinProductOfArrowsPr1.
      rewrite !assoc'.
      rewrite z_iso_after_z_iso_inv.
      rewrite id_left, id_right.
      apply idpath.
    - rewrite !assoc'.
      rewrite BinProductOfArrowsPr2.
      rewrite !assoc.
      rewrite BinProductOfArrowsPr2.
      rewrite !assoc'.
      rewrite z_iso_after_z_iso_inv.
      rewrite id_left, id_right.
      apply idpath.

  Definition binproduct_of_z_iso
    : z_iso (BinProductObject _ Pab) (BinProductObject _ Pcd).
  Show proof.
    use make_z_iso.
    - exact fg.
    - exact fg_inv.
    - exact binproduct_of_z_iso_inv.

End BinProductOfIsos.

Section BinProduct_assoc_z_iso.

  Context {C : category}
          (P : BinProducts C)
          (a b c : C).

  Let Pbc := P b c.
  Let Pa_bc := P a (BinProductObject _ Pbc).
  Let Pab := P a b.
  Let Pab_c := P (BinProductObject _ Pab) c.

  Definition BinProduct_assoc_mor : C BinProductObject C Pa_bc , BinProductObject C Pab_c .
  Show proof.
    use BinProductArrow.
    + use BinProductOfArrows.
      - exact (identity a).
      - use BinProductPr1.
    + use (compose (b := BinProductObject C Pbc)).
      - use BinProductPr2.
      - use BinProductPr2.

  Definition BinProduct_assoc_invmor : C BinProductObject C Pab_c , BinProductObject C Pa_bc .
  Show proof.
    use BinProductArrow.
    + use (compose (b := BinProductObject C Pab)).
      - use BinProductPr1.
      - use BinProductPr1.
    + use BinProductOfArrows.
      - use BinProductPr2.
      - exact (identity c).

  Lemma BinProduct_assoc_is_inverse : is_inverse_in_precat BinProduct_assoc_mor BinProduct_assoc_invmor.
  Show proof.
    use make_is_inverse_in_precat.
    - unfold BinProduct_assoc_mor, BinProduct_assoc_invmor.
      use BinProductArrowsEq.
      * now rewrite
          id_left,
          assoc',
          BinProductPr1Commutes,
          assoc,
          BinProductPr1Commutes,
          BinProductOfArrowsPr1,
          id_right.
      * now rewrite
          id_left,
          assoc',
          BinProductPr2Commutes,
          postcompWithBinProductArrow,
          id_right,
          BinProductOfArrowsPr2,
          <-precompWithBinProductArrow,
          <-(id_left (BinProductPr1 C Pbc)),
          <-(id_left (BinProductPr2 C Pbc)),
          <-BinProductArrowEta,
          id_right.
    - unfold BinProduct_assoc_mor, BinProduct_assoc_invmor.
      use BinProductArrowsEq.
      * now rewrite
          id_left,
          assoc',
          BinProductPr1Commutes,
          postcompWithBinProductArrow,
          id_right,
          BinProductOfArrowsPr1,
          <-precompWithBinProductArrow,
          <-(id_left (BinProductPr1 C Pab)),
          <-(id_left (BinProductPr2 C Pab)),
          <-BinProductArrowEta, id_right.
      * now rewrite
          id_left,
          assoc',
          BinProductPr2Commutes,
          assoc,
          BinProductPr2Commutes,
          BinProductOfArrowsPr2,
          id_right.

  Definition BinProduct_assoc_is_z_iso : is_z_isomorphism (BinProduct_assoc_mor).
  Show proof.
    use make_is_z_isomorphism.
    + exact BinProduct_assoc_invmor.
    + exact BinProduct_assoc_is_inverse.

  Definition BinProduct_assoc : z_iso (BinProductObject C Pa_bc) (BinProductObject C Pab_c).
  Show proof.
    use make_z_iso'.
    + exact BinProduct_assoc_mor.
    + exact BinProduct_assoc_is_z_iso.

End BinProduct_assoc_z_iso.

Section BinProduct_OfArrows_assoc.

  Context {C : category}
  (P : BinProducts C)
  {a a' b b' c c' : C}
  (f : C a', a ) (g : C b', b ) (h : C c', c ).

  Let Pbc := P b c.
  Let Pa_bc := P a (BinProductObject _ Pbc).
  Let Pab := P a b.
  Let Pab_c := P (BinProductObject _ Pab) c.
  Let Pbc' := P b' c'.
  Let Pa_bc' := P a' (BinProductObject _ Pbc').
  Let Pab' := P a' b'.
  Let Pab_c' := P (BinProductObject _ Pab') c'.

  Lemma BinProduct_OfArrows_assoc
  : BinProductOfArrows _ Pa_bc Pa_bc' f (BinProductOfArrows _ Pbc Pbc' g h) · (BinProduct_assoc P a b c) =
    (BinProduct_assoc P a' b' c') · BinProductOfArrows _ Pab_c Pab_c' (BinProductOfArrows _ Pab Pab' f g) h.
  Show proof.
    unfold BinProduct_assoc, BinProduct_assoc_mor.
    simpl.
    use BinProductArrowsEq.
    + rewrite !assoc', (BinProductPr1Commutes), BinProductOfArrowsPr1, assoc, BinProductPr1Commutes.
      use BinProductArrowsEq.
      - now rewrite !assoc',
          !BinProductOfArrowsPr1,
          !assoc,
          !BinProductOfArrowsPr1,
          id_right, !assoc', id_left.
      - now rewrite !assoc',
          !BinProductOfArrowsPr2,
          !assoc,
          !BinProductOfArrowsPr2,
          !assoc',
          !BinProductOfArrowsPr1.
    + now rewrite !assoc',
        !BinProductOfArrowsPr2, !BinProductPr2Commutes,
        !assoc,
        !BinProductOfArrowsPr2, !BinProductPr2Commutes,
        !assoc',
        !BinProductOfArrowsPr2.

End BinProduct_OfArrows_assoc.

Section diagonalMap.

  Context {C:category} (P : BinProducts C) (B:C).

  Definition diagonalMap' : C B, BinProductObject C (P B B) .
  Show proof.
    use BinProductArrow.
    - exact (identity B).
    - exact (identity B).

  Lemma diagonalMap_isMonic : isMonic (diagonalMap').
  Show proof.
    use make_isMonic.
    intros x g h p.
    assert (p' :=
      (maponpaths (λ f, compose f (BinProductPr1 C (P B B))) p)).
    unfold diagonalMap' in p'.
    rewrite !assoc', BinProductPr1Commutes , !id_right in p'.
    exact p'.

  Definition diagonalMap : Monic _ B (BinProductObject C (P B B)).
  Show proof.
    use make_Monic.
    + exact diagonalMap'.
    + exact diagonalMap_isMonic.

End diagonalMap.

Section ProductFunctions.
  Context {C : category}
          (prodC : BinProducts C).

  Definition prod_swap
             (x y : C)
    : prodC x y --> prodC y x.
  Show proof.
    use BinProductArrow.
    - apply BinProductPr2.
    - apply BinProductPr1.

  Definition prod_lwhisker
             {x₁ x₂ : C}
             (f : x₁ --> x₂)
             (y : C)
    : prodC x₁ y --> prodC x₂ y.
  Show proof.
    use BinProductOfArrows.
    - exact f.
    - exact (identity _).

  Definition prod_rwhisker
             (x : C)
             {y₁ y₂ : C}
             (g : y₁ --> y₂)
    : prodC x y₁ --> prodC x y₂.
  Show proof.
    use BinProductOfArrows.
    - exact (identity _).
    - exact g.

  Proposition prod_lwhisker_rwhisker
              {x₁ x₂ : C}
              {y₁ y₂ : C}
              (f : x₁ --> x₂)
              (g : y₁ --> y₂)
    : prod_lwhisker f _ · prod_rwhisker _ g
      =
      BinProductOfArrows _ _ _ f g.
  Show proof.
    unfold prod_lwhisker, prod_rwhisker.
    rewrite BinProductOfArrows_comp.
    rewrite id_left, id_right.
    apply idpath.

  Proposition prod_swap_swap
              (x y : C)
    : prod_swap x y · prod_swap y x = identity _.
  Show proof.
    use BinProductArrowsEq.
    - unfold prod_swap.
      rewrite !assoc'.
      rewrite !id_left.
      rewrite BinProductPr1Commutes.
      rewrite BinProductPr2Commutes.
      apply idpath.
    - unfold prod_swap.
      rewrite !assoc'.
      rewrite !id_left.
      rewrite BinProductPr2Commutes.
      rewrite BinProductPr1Commutes.
      apply idpath.

  Proposition BinProductOfArrows_swap
              {x₁ x₂ : C}
              {y₁ y₂ : C}
              (f : x₁ --> x₂)
              (g : y₁ --> y₂)
    : BinProductOfArrows C (prodC _ _) (prodC _ _) f g · prod_swap x₂ y₂
      =
      prod_swap x₁ y₁ · BinProductOfArrows C _ _ g f.
  Show proof.
    use BinProductArrowsEq.
    - unfold prod_swap.
      rewrite !assoc'.
      rewrite BinProductPr1Commutes.
      rewrite BinProductOfArrowsPr2.
      rewrite BinProductOfArrowsPr1.
      rewrite !assoc.
      rewrite BinProductPr1Commutes.
      apply idpath.
    - unfold prod_swap.
      rewrite !assoc'.
      rewrite BinProductPr2Commutes.
      rewrite BinProductOfArrowsPr2.
      rewrite BinProductOfArrowsPr1.
      rewrite !assoc.
      rewrite BinProductPr2Commutes.
      apply idpath.
End ProductFunctions.

Binary products are closed under iso
Definition isBinProduct_z_iso
           {C : category}
           {x y a₁ a₂ : C}
           {p₁ : a₁ --> x}
           {q₁ : a₁ --> y}
           {p₂ : a₂ --> x}
           {q₂ : a₂ --> y}
           (H : isBinProduct C x y a₁ p₁ q₁)
           (f : z_iso a₂ a₁)
           (r₁ : p₂ = f · p₁)
           (r₂ : q₂ = f · q₁)
  : isBinProduct C x y a₂ p₂ q₂.
Show proof.
  intros w h₁ h₂.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros φ φ ;
       use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ;
       use (cancel_z_iso _ _ f) ;
       use (BinProductArrowsEq _ _ _ (make_BinProduct _ _ _ _ _ _ H)) ;
       [ cbn ;
         rewrite !assoc' ;
         rewrite <- !r₁ ;
         exact (pr12 φ @ !(pr12 φ))
       | cbn ;
         rewrite !assoc' ;
         rewrite <- !r₂ ;
         exact (pr22 φ @ !(pr22 φ)) ]).
  - simple refine (_ ,, _ ,, _).
    + exact (BinProductArrow _ (make_BinProduct _ _ _ _ _ _ H) h₁ h₂ · inv_from_z_iso f).
    + abstract
        (rewrite r₁ ;
         rewrite !assoc' ;
         rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)) ;
         rewrite z_iso_after_z_iso_inv ;
         rewrite id_left ;
         apply BinProductPr1Commutes).
    + abstract
        (cbn ;
         rewrite r₂ ;
         rewrite !assoc' ;
         rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)) ;
         rewrite z_iso_after_z_iso_inv ;
         rewrite id_left ;
         apply (BinProductPr2Commutes _ _ _ (make_BinProduct _ _ _ _ _ _ H))).

Section BinProductsFromProducts.

Context {C : category}.
Context (c d : C).

Let binproduct_indexed_objects
  (i : bool)
  : C
  := if i then c else d.

Context (P : Product bool C binproduct_indexed_objects).

Definition BinProduct_from_Product
  : BinProduct _ c d.
Show proof.
  use ((_ ,, _ ,, _) ,, (λ p' π π, ((_ ,, _ ,, _) ,, _))).
  - exact (ProductObject _ _ P).
  - exact (ProductPr _ _ P true).
  - exact (ProductPr _ _ P false).
  - apply ProductArrow.
    intro i.
    induction i.
    + exact π.
    + exact π.
  - exact (ProductPrCommutes _ _ _ P _ _ true).
  - exact (ProductPrCommutes _ _ _ P _ _ false).
  - abstract (
      intro t;
      apply subtypePath;
      [ intro;
        apply isapropdirprod;
        apply homset_property | ];
      apply (ProductArrowUnique _ _ _ P);
      intro i;
      induction i;
      [ exact (pr12 t)
      | exact (pr22 t) ]
    ).

End BinProductsFromProducts.

Definition BinProducts_from_Products
  {C : category}
  (P : Products bool C)
  : BinProducts C
  := λ c d, BinProduct_from_Product c d (P _).

Section ProductsFromBinProducts.

  Context {C : category}.
  Context (BP : BinProducts C).
  Context {n : nat}.
  Context {c : C}.
  Context (P : Product (stn n) C (λ _, c)).
  Let stnweq := (weqdnicoprod n lastelement).

  Definition sn_power_object
    : C
    := BP c P.

  Definition sn_power_projection
    (i : stn (S n))
    : C sn_power_object, c .
  Show proof.
    induction (invmap stnweq i) as [i' | i'].
    - exact (
        BinProductPr2 _ _ ·
        ProductPr _ _ _ i'
      ).
    - apply BinProductPr1.

  Section Arrow.

    Context (c' : C).
    Context (cone' : stn (S n) Cc', c).

    Definition sn_power_arrow
      : C c', sn_power_object.
    Show proof.
      use BinProductArrow.
      - apply (cone' (stnweq (inr tt))).
      - apply ProductArrow.
        intro i.
        apply (cone' (stnweq (inl i))).

    Lemma sn_power_arrow_commutes
      (i : stn (S n))
      : sn_power_arrow · sn_power_projection i = cone' i.
    Show proof.
      rewrite <- (homotweqinvweq stnweq i).
      induction (invmap stnweq i) as [i' | i'].
      - refine (maponpaths (λ x, _ · (_ x)) (homotinvweqweq stnweq (inl i')) @ _).
        refine (assoc _ _ _ @ _).
        refine (maponpaths (λ x, x · _) (BinProductPr2Commutes _ _ _ _ _ _ _) @ _).
        apply (ProductPrCommutes _ _ _ P).
      - refine (maponpaths (λ x, _ · (_ x)) (homotinvweqweq stnweq (inr i')) @ _).
        refine (BinProductPr1Commutes _ _ _ (BP c P) _ _ _ @ _).
        apply maponpaths.
        now apply stn_eq.

    Lemma sn_power_arrow_unique
      (t : (f: C c', sn_power_object),
         i, f · sn_power_projection i = cone' i)
      : t = (sn_power_arrow ,, sn_power_arrow_commutes).
    Show proof.
      apply subtypePairEquality.
      {
        intro.
        apply impred_isaprop.
        intro.
        apply homset_property.
      }
      apply BinProductArrowUnique.
      - refine (!_ @ pr2 t _).
        apply maponpaths.
        exact (maponpaths _ (homotinvweqweq _ _)).
      - apply ProductArrowUnique.
        intro i.
        refine (_ @ pr2 t _).
        refine (assoc' _ _ _ @ _).
        refine (maponpaths _ (!_)).
        exact (maponpaths _ (homotinvweqweq _ _)).

  End Arrow.

  Definition sn_power_is_product
    : isProduct _ _ _ sn_power_object sn_power_projection.
  Show proof.
    use (make_isProduct _ _ (homset_property C)).
    intros c' cone'.
    use make_iscontr.
    + exists (sn_power_arrow c' cone').
      exact (sn_power_arrow_commutes c' cone').
    + exact (sn_power_arrow_unique c' cone').

  Definition n_power_to_sn_power
    : Product (stn (S n)) C (λ _, c).
  Show proof.
    use make_Product.
    - exact sn_power_object.
    - exact sn_power_projection.
    - exact sn_power_is_product.

End ProductsFromBinProducts.

Definition bin_product_power
  (C : category)
  (c : C)
  (T : Terminal C)
  (BP : BinProducts C)
  (n : nat)
  : Product (stn n) C (λ _, c).
Show proof.
  induction n as [ | n IHn].
  - exact (Terminal_is_empty_product T _ weqstn0toempty).
  - apply (n_power_to_sn_power BP IHn).

Section BinProductOfIso.

  Lemma isbinproduct_of_isos
        {C : category} {x1 x2 y1 y2 py : C}
        (px : BinProduct _ x1 x2)
        (i1 : z_iso y1 x1) (i2 : z_iso y2 x2)
        (i : z_iso py px)
        (f1 : C py, y1 ) (f2 : C py, y2 )
        (pf1 : i · BinProductPr1 C px = f1 · i1)
        (pf2 : i · BinProductPr2 C px = f2 · i2)
    : isBinProduct _ y1 y2 py f1 f2.
  Show proof.
    use make_isBinProduct.
    intros c g1 g2.
    use iscontraprop1.
    - use invproofirrelevance.
      intros φ φ.
      use subtypePath.
      { intro. apply isapropdirprod ; apply homset_property. }

      use (cancel_z_iso _ _ _ (BinProductArrowsEq _ _ _ px _ (pr1 φ · _) (pr1 φ · _) _ _)).
      + exact i.
      + rewrite ! assoc'.
        rewrite pf1.
        rewrite ! assoc.
        apply maponpaths_2.
        exact (pr12 φ @ ! pr12 φ).
      + rewrite ! assoc'.
        rewrite pf2.
        rewrite ! assoc.
        apply maponpaths_2.
        exact (pr22 φ @ ! pr22 φ).
    - set (t := pr1 (iso_to_isBinProduct _ px (z_iso_to_iso i) c (g1 · i1) (g2 · i2))).
      exists (pr1 t).
      split.
      + refine (_ @ ! z_iso_inv_on_left _ _ _ _ _ _ (pr12 t)).
        rewrite assoc'.
        apply maponpaths.
        use z_iso_inv_on_left.
        exact pf1.
      + refine (_ @ ! z_iso_inv_on_left _ _ _ _ _ _ (pr22 t)).
        rewrite assoc'.
        apply maponpaths.
        use z_iso_inv_on_left.
        exact pf2.

  Lemma binproduct_of_isos {C : category} {x1 x2 y1 y2 : C}
    (p : BinProduct _ x1 x2) (i1 : z_iso x1 y1) (i2 : z_iso x2 y2)
    : BinProduct _ y1 y2.
  Show proof.
    use make_BinProduct.
    - exact p.
    - exact (BinProductPr1 _ p · i1).
    - exact (BinProductPr2 _ p · i2).
    - use (isbinproduct_of_isos p (z_iso_inv i1) (z_iso_inv i2) (identity_z_iso p))
      ; rewrite id_left;
        rewrite assoc';
        rewrite z_iso_inv_after_z_iso;
        now rewrite id_right.

End BinProductOfIso.