Library UniMath.CategoryTheory.YonedaBinproducts

****************************************************************************
Yoneda commutes with binary products up to iso (iso_yoneda_binproducts).
Written by: Elisabeth Bonnevier, 2019
First we create a natural transformation from Yon(X × Y) to Yon(X) × Yon(Y).
Definition yon_binprod_nat_trans_data :
  nat_trans_data (pr1 (yon (BinProductObject _ (PC X Y))))
                 (pr1 (BinProductObject _ (BinProducts_PreShv (yon X) (yon Y)))).
Show proof.
  intros Z f.
  split; [exact (f · BinProductPr1 _ _) | exact (f · BinProductPr2 _ _)].

Lemma is_nat_trans_yon_binprod : is_nat_trans _ _ yon_binprod_nat_trans_data.
Show proof.
  intros Z W f.
  use funextfun; intro g.
  now apply dirprodeq; use assoc'.

Definition yon_binprod_nat_trans :
  nat_trans (pr1 (yon (BinProductObject _ (_ X Y))))
            (pr1 (BinProductObject _ (BinProducts_PreShv (yon X) (yon Y)))) :=
  make_nat_trans _ _ _ is_nat_trans_yon_binprod.

Second, we create a natural transformation from Yon(X) × Yon(Y) to Yon(X × Y).
Definition yon_binprod_inv_nat_trans_data :
  nat_trans_data (pr1 (BinProductObject _ (BinProducts_PreShv (yon X) (yon Y))))
                 (pr1 (yon (BinProductObject _ (PC X Y)))).
Show proof.
  intros Z [f1 f2].
  exact (BinProductArrow _ (PC X Y) f1 f2).

Lemma is_nat_trans_yon_binprod_inv : is_nat_trans _ _ yon_binprod_inv_nat_trans_data.
Show proof.
  unfold yon_binprod_inv_nat_trans_data.
  intros Z W f.
  use funextfun; intros [g1 g2]; cbn.
  use BinProductArrowsEq; rewrite <- assoc.
  - now rewrite !BinProductPr1Commutes.
  - now rewrite !BinProductPr2Commutes.

Definition yon_binprod_inv_nat_trans :
  nat_trans (pr1 (BinProductObject _ (BinProducts_PreShv (yon X) (yon Y))))
            (pr1 (yon (BinProductObject _ (_ X Y)))) :=
  make_nat_trans _ _ _ is_nat_trans_yon_binprod_inv.

We now show that the first transformation is an isomorphism by showing that the second transformation is its inverse.
The functors Yon(X × Y) and Yon(X) × Yon(Y) are isomorphic.