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.total2_paths.
Require Import UniMath.CategoryTheory.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 mk_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 subtypeEquality;
              [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 mk_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 mk_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.