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 : C ⟦c ,a ⟧) (cb : C ⟦c ,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 : C ⟦p ,c ⟧) (p2 : C ⟦p ,d ⟧) :=
  isLimCone (binproduct_diagram c d) p (ProdCone p1 p2).

Definition mk_isBinProductCone (hsC : has_homsets C) (a b p : C)
  (pa : C ⟦p ,a ⟧) (pb : C ⟦p ,b ⟧) :
  (∏ (c : C) (f : C ⟦c ,a ⟧) (g : C ⟦c ,b ⟧),
    ∃! k : C ⟦c ,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 : C ⟦c ,a ⟧) (g : C ⟦c ,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): C ⟦BinProductObject P ,c ⟧ :=
  limOut P true.

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

Definition BinProductArrow {a b : C} (P : BinProductCone a b) {c : C}
  (f : C ⟦c ,a ⟧) (g : C ⟦c ,b ⟧) : C ⟦c ,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 : C ⟦c ,a ⟧) (g : C ⟦c ,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 : C ⟦c ,a ⟧) (g : C ⟦c ,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 : C ⟦c ,a ⟧) (g : C ⟦c ,b ⟧) (k : C ⟦c ,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 : C ⟦c ,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 : C ⟦a ,c ⟧) (g : C ⟦b ,d ⟧) :
          C ⟦BinProductObject 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 : C ⟦a ,c ⟧) (g : C ⟦b ,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 : C ⟦a ,c ⟧) (g : C ⟦b ,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 : C ⟦a ,c ⟧) (g : C ⟦b ,d ⟧)
    {x : C} (k : C ⟦x ,a ⟧) (h : C ⟦x ,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 : C ⟦a ,c ⟧) (g : C ⟦a ,d ⟧) {x : C} (k : C ⟦x ,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.