Library UniMath.CategoryTheory.limits.graphs.binproducts

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 : category).

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 make_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 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 : 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 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 : 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 : category) :
  Lims_of_shape two_graph C → BinProducts C.
Proof.
now intros H a b; apply H.
Defined.