# Library UniMath.CategoryTheory.limits.graphs.binproducts

Binary products via limits

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.

Local Open Scope cat.

Section binproduct_def.

Variable (C : precategory).

Definition two_graph : graph.
Proof.
bool.
exact (λ _ _, empty).
Defined.

Definition binproduct_diagram (a b : C) : diagram two_graph C.
Proof.
(λ x : bool, if x then a else b).
intros u v F.
induction F.
Defined.

Definition ProdCone {a b c : C} (ca : Cc,a) (cb : Cc,b) :
cone (binproduct_diagram a b) c.
Proof.
use tpair; simpl.
- intro v; induction v.
+ exact ca.
+ exact cb.
- intros u v e; induction e.
Defined.

Definition isBinProductCone (c d p : C) (p1 : Cp,c) (p2 : Cp,d) :=
isLimCone (binproduct_diagram c d) p (ProdCone p1 p2).

Definition make_isBinProductCone (hsC : has_homsets C) (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)
isBinProductCone a b p pa pb.
Proof.
intros H c cc.
simpl in ×.
set (H' := H c (coneOut cc true) (coneOut cc false)).
use tpair.
- (pr1 (pr1 H')).
set (T := pr2 (pr1 H')); simpl in T.
abstract (intro u; induction u; simpl; [exact (pr1 T)|exact (pr2 T)]).
- abstract (simpl; intros; apply subtypePath;
[intro; apply impred;intro; apply hsC|]; simpl;
apply path_to_ctr; split; [ apply (pr2 t true) | apply (pr2 t false) ]).
Defined.

Definition BinProductCone (a b : C) := LimCone (binproduct_diagram a b).

Definition make_BinProductCone (a b : C) :
(c : C) (f : Cc,a) (g : Cc,b),
isBinProductCone _ _ _ f g BinProductCone a b.
Proof.
intros.
use tpair.
- c.
apply (ProdCone f g).
- apply X.
Defined.

Definition BinProducts := (a b : C), BinProductCone a b.
Definition hasBinProducts := (a b : C), BinProductCone a b .

Definition BinProductObject {c d : C} (P : BinProductCone c d) : C := lim P.
Definition BinProductPr1 {c d : C} (P : BinProductCone c d): CBinProductObject P,c :=
limOut P true.

Definition BinProductPr2 {c d : C} (P : BinProductCone c d) : CBinProductObject P,d :=
limOut P false.

Definition BinProductArrow {a b : C} (P : BinProductCone a b) {c : C}
(f : Cc,a) (g : Cc,b) : Cc,BinProductObject P.
Proof.
apply (limArrow P).
use make_cone.
- intro v; induction v; [ apply f | apply g ].
- intros ? ? e; induction e. Defined.

Lemma BinProductPr1Commutes (a b : C) (P : BinProductCone a b):
(c : C) (f : Cc,a) (g : Cc,b), BinProductArrow P f g · BinProductPr1 P = f.
Proof.
intros c f g.
apply (limArrowCommutes P c (ProdCone f g) true).
Qed.

Lemma BinProductPr2Commutes (a b : C) (P : BinProductCone a b):
(c : C) (f : Cc,a) (g : Cc,b), BinProductArrow P f g · BinProductPr2 P = g.
Proof.
intros c f g.
apply (limArrowCommutes P c (ProdCone f g) false).
Qed.

Lemma BinProductArrowUnique (a b : C) (P : BinProductCone a b) (c : C)
(f : Cc,a) (g : Cc,b) (k : Cc,BinProductObject P) :
k · BinProductPr1 P = f k · BinProductPr2 P = g
k = BinProductArrow P f g.
Proof.
intros H1 H2.
use limArrowUnique; simpl.
now intro u; induction u; simpl; [ apply H1 | apply H2 ].
Qed.

Lemma BinProductArrowEta (a b : C) (P : BinProductCone a b) (c : C)
(f : Cc,BinProductObject P) :
f = BinProductArrow P (f · BinProductPr1 P) (f · BinProductPr2 P).
Proof.
now apply BinProductArrowUnique.
Qed.

Definition BinProductOfArrows {c d : C} (Pcd : BinProductCone c d) {a b : C}
(Pab : BinProductCone a b) (f : Ca,c) (g : Cb,d) :
CBinProductObject Pab,BinProductObject Pcd :=
BinProductArrow Pcd (BinProductPr1 Pab · f) (BinProductPr2 Pab · g).

Lemma BinProductOfArrowsPr1 {c d : C} (Pcd : BinProductCone c d) {a b : C}
(Pab : BinProductCone a b) (f : Ca,c) (g : Cb,d) :
BinProductOfArrows Pcd Pab f g · BinProductPr1 Pcd = BinProductPr1 Pab · f.
Proof.
now apply BinProductPr1Commutes.
Qed.

Lemma BinProductOfArrowsPr2 {c d : C} (Pcd : BinProductCone c d) {a b : C}
(Pab : BinProductCone a b) (f : Ca,c) (g : Cb,d) :
BinProductOfArrows Pcd Pab f g · BinProductPr2 Pcd = BinProductPr2 Pab · g.
Proof.
now apply BinProductPr2Commutes.
Qed.

Lemma postcompWithBinProductArrow {c d : C} (Pcd : BinProductCone c d) {a b : C}
(Pab : BinProductCone a b) (f : Ca,c) (g : Cb,d)
{x : C} (k : Cx,a) (h : Cx,b) :
BinProductArrow Pab k h · BinProductOfArrows Pcd Pab f g =
BinProductArrow Pcd (k · f) (h · g).
Proof.
apply BinProductArrowUnique.
- now rewrite <- assoc, BinProductOfArrowsPr1, assoc, BinProductPr1Commutes.
- now rewrite <- assoc, BinProductOfArrowsPr2, assoc, BinProductPr2Commutes.
Qed.

Lemma precompWithBinProductArrow {c d : C} (Pcd : BinProductCone c d) {a : C}
(f : Ca,c) (g : Ca,d) {x : C} (k : Cx,a) :
k · BinProductArrow Pcd f g = BinProductArrow Pcd (k · f) (k · g).
Proof.
apply BinProductArrowUnique.
- now rewrite <- assoc, BinProductPr1Commutes.
- now rewrite <- assoc, BinProductPr2Commutes.
Qed.

End binproduct_def.

Lemma BinProducts_from_Lims (C : precategory) :
Lims_of_shape two_graph C BinProducts C.
Proof.
now intros H a b; apply H.
Defined.