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.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.
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 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.
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 subtypeEquality;
              [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 mk_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 mk_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 : precategory) :
Lims_of_shape two_graph C -> BinProducts C.
Show proof.

now intros H a b; apply H.