Library UniMath.CategoryTheory.Limits.Graphs.BinCoproducts
******************************************
Binary coproducts defined as a colimit
Written by: Benedikt Ahrens, March 2015
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.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Local Open Scope cat.
Definition two_graph : graph.
Show proof.
Definition bincoproduct_diagram {C : category} (a b : C) : diagram two_graph C.
Show proof.
Definition CopCocone {C : category} {a b : C} {c : C} (ac : a --> c) (bc : b --> c) :
cocone (bincoproduct_diagram a b) c.
Show proof.
Section bincoproduct_def.
Variable C : category.
Definition isBinCoproductCocone (a b co : C) (ia : a --> co) (ib : b --> co) :=
isColimCocone (bincoproduct_diagram a b) co (CopCocone ia ib).
Definition make_isBinCoproductCocone (hsC : has_homsets C)(a b co : C) (ia : a --> co) (ib : b --> co) :
(∏ (c : C) (f : a --> c) (g : b --> c),
∃! k : C ⟦co, c⟧,
ia · k = f ×
ib · k = g)
→
isBinCoproductCocone a b co ia ib.
Show proof.
intros H c cc.
set (H':= H c (coconeIn cc true) (coconeIn cc false)).
use tpair.
- exists (pr1 (pr1 H')).
set (T := pr2 (pr1 H')). simpl in T.
abstract (intro u; induction u;
[ apply (pr1 T) | apply (pr2 T)]).
- simpl. intros. abstract (intros;
apply subtypePath;
[ intro; apply impred; intro; apply hsC
| apply path_to_ctr; split; [ apply (pr2 t true) | apply (pr2 t false)] ]).
set (H':= H c (coconeIn cc true) (coconeIn cc false)).
use tpair.
- exists (pr1 (pr1 H')).
set (T := pr2 (pr1 H')). simpl in T.
abstract (intro u; induction u;
[ apply (pr1 T) | apply (pr2 T)]).
- simpl. intros. abstract (intros;
apply subtypePath;
[ intro; apply impred; intro; apply hsC
| apply path_to_ctr; split; [ apply (pr2 t true) | apply (pr2 t false)] ]).
Definition BinCoproductCocone (a b : C) :=
ColimCocone (bincoproduct_diagram a b).
Definition make_BinCoproductCocone (a b : C) :
∏ (c : C) (f : a --> c) (g : b --> c),
isBinCoproductCocone _ _ _ f g → BinCoproductCocone a b.
Show proof.
Definition BinCoproducts := ∏ (a b : C), BinCoproductCocone a b.
Definition hasBinCoproducts := ∏ (a b : C), ∥ BinCoproductCocone a b ∥.
Definition BinCoproductObject {a b : C} (CC : BinCoproductCocone a b) : C := colim CC.
Definition BinCoproductIn1 {a b : C} (CC : BinCoproductCocone a b): a --> BinCoproductObject CC
:= colimIn CC true.
Definition BinCoproductIn2 {a b : C} (CC : BinCoproductCocone a b) : b --> BinCoproductObject CC
:= colimIn CC false.
Definition BinCoproductArrow {a b : C} (CC : BinCoproductCocone a b) {c : C} (f : a --> c) (g : b --> c) :
BinCoproductObject CC --> c.
Show proof.
apply (colimArrow CC).
use make_cocone.
+ intro v. induction v.
- apply f.
- apply g.
+ simpl. intros ? ? e; induction e.
use make_cocone.
+ intro v. induction v.
- apply f.
- apply g.
+ simpl. intros ? ? e; induction e.
Lemma BinCoproductIn1Commutes (a b : C) (CC : BinCoproductCocone a b):
∏ (c : C) (f : a --> c) g, BinCoproductIn1 CC · BinCoproductArrow CC f g = f.
Show proof.
intros c f g.
unfold BinCoproductIn1.
set (H:=colimArrowCommutes CC _ (CopCocone f g) true).
apply H.
unfold BinCoproductIn1.
set (H:=colimArrowCommutes CC _ (CopCocone f g) true).
apply H.
Lemma BinCoproductIn2Commutes (a b : C) (CC : BinCoproductCocone a b):
∏ (c : C) (f : a --> c) g, BinCoproductIn2 CC · BinCoproductArrow CC f g = g.
Show proof.
intros c f g.
unfold BinCoproductIn1.
set (H:=colimArrowCommutes CC _ (CopCocone f g) false).
apply H.
unfold BinCoproductIn1.
set (H:=colimArrowCommutes CC _ (CopCocone f g) false).
apply H.
Lemma BinCoproductArrowUnique (a b : C) (CC : BinCoproductCocone a b) (x : C)
(f : a --> x) (g : b --> x) (k : BinCoproductObject CC --> x) :
BinCoproductIn1 CC · k = f → BinCoproductIn2 CC · k = g →
k = BinCoproductArrow CC f g.
Show proof.
Lemma BinCoproductArrowEta (a b : C) (CC : BinCoproductCocone a b) (x : C)
(f : BinCoproductObject CC --> x) :
f = BinCoproductArrow CC (BinCoproductIn1 CC · f) (BinCoproductIn2 CC · f).
Show proof.
Definition BinCoproductOfArrows {a b : C} (CCab : BinCoproductCocone a b) {c d : C}
(CCcd : BinCoproductCocone c d) (f : a --> c) (g : b --> d) :
BinCoproductObject CCab --> BinCoproductObject CCcd :=
BinCoproductArrow CCab (f · BinCoproductIn1 CCcd) (g · BinCoproductIn2 CCcd).
Lemma BinCoproductOfArrowsIn1 {a b : C} (CCab : BinCoproductCocone a b) {c d : C}
(CCcd : BinCoproductCocone c d) (f : a --> c) (g : b --> d) :
BinCoproductIn1 CCab · BinCoproductOfArrows CCab CCcd f g = f · BinCoproductIn1 CCcd.
Show proof.
Lemma BinCoproductOfArrowsIn2 {a b : C} (CCab : BinCoproductCocone a b) {c d : C}
(CCcd : BinCoproductCocone c d) (f : a --> c) (g : b --> d) :
BinCoproductIn2 CCab · BinCoproductOfArrows CCab CCcd f g = g · BinCoproductIn2 CCcd.
Show proof.
Lemma precompWithBinCoproductArrow {a b : C} (CCab : BinCoproductCocone a b) {c d : C}
(CCcd : BinCoproductCocone c d) (f : a --> c) (g : b --> d)
{x : C} (k : c --> x) (h : d --> x) :
BinCoproductOfArrows CCab CCcd f g · BinCoproductArrow CCcd k h =
BinCoproductArrow CCab (f · k) (g · h).
Show proof.
apply BinCoproductArrowUnique.
- rewrite assoc. rewrite BinCoproductOfArrowsIn1.
rewrite <- assoc, BinCoproductIn1Commutes.
apply idpath.
- rewrite assoc, BinCoproductOfArrowsIn2.
rewrite <- assoc, BinCoproductIn2Commutes.
apply idpath.
- rewrite assoc. rewrite BinCoproductOfArrowsIn1.
rewrite <- assoc, BinCoproductIn1Commutes.
apply idpath.
- rewrite assoc, BinCoproductOfArrowsIn2.
rewrite <- assoc, BinCoproductIn2Commutes.
apply idpath.
Lemma postcompWithBinCoproductArrow {a b : C} (CCab : BinCoproductCocone a b) {c : C}
(f : a --> c) (g : b --> c) {x : C} (k : c --> x) :
BinCoproductArrow CCab f g · k = BinCoproductArrow CCab (f · k) (g · k).
Show proof.
apply BinCoproductArrowUnique.
- rewrite assoc, BinCoproductIn1Commutes;
apply idpath.
- rewrite assoc, BinCoproductIn2Commutes;
apply idpath.
- rewrite assoc, BinCoproductIn1Commutes;
apply idpath.
- rewrite assoc, BinCoproductIn2Commutes;
apply idpath.
End bincoproduct_def.
Arguments BinCoproductCocone [_] _ _.
Arguments BinCoproductObject [_ _ _] _ .
Arguments BinCoproductArrow [_ _ _] _ [_] _ _.
Arguments BinCoproductIn1 [_ _ _] _.
Arguments BinCoproductIn2 [_ _ _] _.
Proof that coproducts are unique when the precategory C is a univalent_category
Section coproduct_unique.
Variable C : category.
Hypothesis H : is_univalent C.
Variables a b : C.
Definition from_BinCoproduct_to_BinCoproduct (CC CC' : BinCoproductCocone a b)
: BinCoproductObject CC --> BinCoproductObject CC'.
Show proof.
Lemma BinCoproduct_endo_is_identity (CC : BinCoproductCocone a b)
(k : BinCoproductObject CC --> BinCoproductObject CC)
(H1 : BinCoproductIn1 CC · k = BinCoproductIn1 CC)
(H2 : BinCoproductIn2 CC · k = BinCoproductIn2 CC)
: identity _ = k.
Show proof.
Lemma is_z_iso_from_BinCoproduct_to_BinCoproduct (CC CC' : BinCoproductCocone a b)
: is_z_isomorphism (from_BinCoproduct_to_BinCoproduct CC CC').
Show proof.
exists (from_BinCoproduct_to_BinCoproduct CC' CC).
split; simpl.
- apply pathsinv0.
apply BinCoproduct_endo_is_identity.
+ rewrite assoc. unfold from_BinCoproduct_to_BinCoproduct.
rewrite BinCoproductIn1Commutes.
rewrite BinCoproductIn1Commutes.
apply idpath.
+ rewrite assoc. unfold from_BinCoproduct_to_BinCoproduct.
rewrite BinCoproductIn2Commutes.
rewrite BinCoproductIn2Commutes.
apply idpath.
- apply pathsinv0.
apply BinCoproduct_endo_is_identity.
+ rewrite assoc; unfold from_BinCoproduct_to_BinCoproduct.
repeat rewrite BinCoproductIn1Commutes; apply idpath.
+ rewrite assoc; unfold from_BinCoproduct_to_BinCoproduct.
repeat rewrite BinCoproductIn2Commutes; apply idpath.
split; simpl.
- apply pathsinv0.
apply BinCoproduct_endo_is_identity.
+ rewrite assoc. unfold from_BinCoproduct_to_BinCoproduct.
rewrite BinCoproductIn1Commutes.
rewrite BinCoproductIn1Commutes.
apply idpath.
+ rewrite assoc. unfold from_BinCoproduct_to_BinCoproduct.
rewrite BinCoproductIn2Commutes.
rewrite BinCoproductIn2Commutes.
apply idpath.
- apply pathsinv0.
apply BinCoproduct_endo_is_identity.
+ rewrite assoc; unfold from_BinCoproduct_to_BinCoproduct.
repeat rewrite BinCoproductIn1Commutes; apply idpath.
+ rewrite assoc; unfold from_BinCoproduct_to_BinCoproduct.
repeat rewrite BinCoproductIn2Commutes; apply idpath.
Definition z_iso_from_BinCoproduct_to_BinCoproduct (CC CC' : BinCoproductCocone a b)
: z_iso (BinCoproductObject CC) (BinCoproductObject CC')
:= make_z_iso' _ (is_z_iso_from_BinCoproduct_to_BinCoproduct CC CC').
End coproduct_unique.
Definition limits_isBinCoproductCocone_from_isBinCoproduct (C : category) {a b c}
(u : C ⟦ a, c⟧)(v : C ⟦ b, c⟧) :
Limits.BinCoproducts.isBinCoproduct C a b c u v -> isBinCoproductCocone _ _ _ _ u v :=
make_isBinCoproductCocone _ C _ _ _ _ _.
Lemma limits_isBinCoproduct_from_isBinCoproductCocone (C : category) {a b c}
(u : C ⟦ a, c⟧)(v : C ⟦ b, c⟧) :
isBinCoproductCocone _ _ _ _ u v -> Limits.BinCoproducts.isBinCoproduct C a b c u v.
Show proof.
intro h.
set (CC := make_BinCoproductCocone _ _ _ _ _ _ h); simpl.
intros x f g.
use unique_exists; simpl.
- apply (BinCoproducts.BinCoproductArrow CC f g).
- abstract (split;
[ apply (BinCoproducts.BinCoproductIn1Commutes _ _ _ CC)
| apply (BinCoproducts.BinCoproductIn2Commutes _ _ _ CC)]).
- abstract (intros h'; apply isapropdirprod; apply C).
- intros h' [H1 H2].
eapply (BinCoproducts.BinCoproductArrowUnique _ _ _ CC).
+ exact H1.
+ exact H2.
set (CC := make_BinCoproductCocone _ _ _ _ _ _ h); simpl.
intros x f g.
use unique_exists; simpl.
- apply (BinCoproducts.BinCoproductArrow CC f g).
- abstract (split;
[ apply (BinCoproducts.BinCoproductIn1Commutes _ _ _ CC)
| apply (BinCoproducts.BinCoproductIn2Commutes _ _ _ CC)]).
- abstract (intros h'; apply isapropdirprod; apply C).
- intros h' [H1 H2].
eapply (BinCoproducts.BinCoproductArrowUnique _ _ _ CC).
+ exact H1.
+ exact H2.
Lemma BinCoproducts_from_Colims (C : category) :
Colims_of_shape two_graph C -> BinCoproducts C.
Show proof.
now intros H a b; apply H.
Post-composing a bincoproduct diagram with a functor yields a
bincoproduct diagram.
Lemma mapdiagram_bincoproduct_eq_diag {C : category}{D : category}
(F : functor C D)(a b : C) :
eq_diag (C := D)
(mapdiagram F (BinCoproducts.bincoproduct_diagram a b))
(BinCoproducts.bincoproduct_diagram (F a) (F b)).
Show proof.
(F : functor C D)(a b : C) :
eq_diag (C := D)
(mapdiagram F (BinCoproducts.bincoproduct_diagram a b))
(BinCoproducts.bincoproduct_diagram (F a) (F b)).
Show proof.