Library UniMath.CategoryTheory.YonedaBinproducts
****************************************************************************
Yoneda commutes with binary products up to iso (iso_yoneda_binproducts).
Written by: Elisabeth Bonnevier, 2019
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.Presheaf.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.yoneda.
Local Open Scope cat.
Section iso_yoneda_binproducts.
Context {C : category} (PC : BinProducts C) (X Y : C).
Let yon : C ⟶ [C^op, HSET] := yoneda C.
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.
Lemma is_nat_trans_yon_binprod : is_nat_trans _ _ yon_binprod_nat_trans_data.
Show proof.
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.
nat_trans_data (pr1 (yon (BinProductObject _ (PC X Y))))
(pr1 (BinProductObject _ (BinProducts_PreShv (yon X) (yon Y)))).
Show proof.
Lemma is_nat_trans_yon_binprod : is_nat_trans _ _ yon_binprod_nat_trans_data.
Show proof.
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.
Lemma is_nat_trans_yon_binprod_inv : is_nat_trans _ _ yon_binprod_inv_nat_trans_data.
Show proof.
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.
nat_trans_data (pr1 (BinProductObject _ (BinProducts_PreShv (yon X) (yon Y))))
(pr1 (yon (BinProductObject _ (PC X Y)))).
Show proof.
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.
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.
Lemma yon_binprod_is_iso :
@is_iso [C^op, HSET, has_homsets_HSET] _ _ yon_binprod_nat_trans.
Show proof.
@is_iso [C^op, HSET, has_homsets_HSET] _ _ yon_binprod_nat_trans.
Show proof.
use is_iso_from_is_z_iso.
exists yon_binprod_inv_nat_trans.
split; apply (nat_trans_eq has_homsets_HSET); intro Z; use funextfun; intro f.
- cbn; unfold yon_binprod_nat_trans_data, yon_binprod_inv_nat_trans_data.
now rewrite <- (BinProductArrowEta _ _ _ _ _ _).
- use dirprodeq; cbn;
unfold yon_binprod_inv_nat_trans_data;
[use BinProductPr1Commutes | use BinProductPr2Commutes].
exists yon_binprod_inv_nat_trans.
split; apply (nat_trans_eq has_homsets_HSET); intro Z; use funextfun; intro f.
- cbn; unfold yon_binprod_nat_trans_data, yon_binprod_inv_nat_trans_data.
now rewrite <- (BinProductArrowEta _ _ _ _ _ _).
- use dirprodeq; cbn;
unfold yon_binprod_inv_nat_trans_data;
[use BinProductPr1Commutes | use BinProductPr2Commutes].
The functors Yon(X × Y) and Yon(X) × Yon(Y) are isomorphic.
Lemma iso_yoneda_binproducts :
iso (yon (BinProductObject _ (PC X Y)))
(BinProductObject (PreShv _) (BinProducts_PreShv (yon X) (yon Y))).
Show proof.
End iso_yoneda_binproducts.
iso (yon (BinProductObject _ (PC X Y)))
(BinProductObject (PreShv _) (BinProducts_PreShv (yon X) (yon Y))).
Show proof.
End iso_yoneda_binproducts.