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

Definition two_graph : graph.
Show proof.

exists bool.
exact (λ _ _, empty).

Definition binproduct_diagram (a b : C) : diagram two_graph C.
Show proof.

  exists (λ x : bool , if x then a else b).
  intros u v F.
  induction F.

Definition ProdCone {a b c : C} (ca : C ⟦c ,a ⟧) (cb : C ⟦c ,b ⟧) :
cone (binproduct_diagram a b) c.
Show proof.

use tpair; simpl.
- intro v; induction v.
+ exact ca.
+ exact cb.
- intros u v e; induction e.

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.
Show proof.

intros H c cc.
simpl in *.
set (H' := H c (coneOut cc true) (coneOut cc false)).
use tpair.
- exists (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) ]).

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.
Show proof.

  intros.
  use tpair.
  - exists c.
    apply (ProdCone f g).
  - apply X.

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 ⟧.
Show proof.

apply (limArrow P).
use make_cone.
- intro v; induction v; [ apply f | apply g ].
- intros ? ? e; induction e.

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.
Show proof.

intros c f g.
apply (limArrowCommutes P c (ProdCone f g) true).

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.
Show proof.

intros c f g.
apply (limArrowCommutes P c (ProdCone f g) false).

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.
Show proof.

intros H1 H2.
use limArrowUnique; simpl.
now intro u; induction u; simpl; [ apply H1 | apply H2 ].

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).
Show proof.

now apply BinProductArrowUnique.

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.
Show proof.

now apply BinProductPr1Commutes.

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.
Show proof.

now apply BinProductPr2Commutes.

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).
Show proof.

apply BinProductArrowUnique.
- now rewrite <- assoc, BinProductOfArrowsPr1, assoc, BinProductPr1Commutes.
- now rewrite <- assoc, BinProductOfArrowsPr2, assoc, BinProductPr2Commutes.

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).
Show proof.

apply BinProductArrowUnique.
- now rewrite <- assoc, BinProductPr1Commutes.
- now rewrite <- assoc, BinProductPr2Commutes.

End binproduct_def.

Lemma BinProducts_from_Lims (C : category) :
Lims_of_shape two_graph C -> BinProducts C.
Show proof.

now intros H a b; apply H.