Library UniMath.CategoryTheory.limits.binproducts
Direct implementation of binary products
Contents
- Definition of binary products
- Definition of binary product functor (binproduct_functor)
- Definition of a binary product structure on a functor category by taking pointwise binary products in the target category (BinProducts_functor_precat)
- Binary products from limits (BinProducts_from_Lims)
- Equivalent universal property: (C --> A) × (C --> B) ≃ (C --> A × B)
- Terminal object as the unit (up to isomorphism) of binary products
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.WeakEquivalences.
Require Import UniMath.CategoryTheory.total2_paths.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.zero.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.FunctorCategory.
Local Open Scope cat.
Section binproduct_def.
Variable C : precategory.
Definition isBinProduct (c d p : C) (p1 : p --> c) (p2 : p --> d) : UU :=
∏ (a : C) (f : a --> c) (g : a --> d),
∃! fg, (fg · p1 = f) × (fg · p2 = g).
Lemma isaprop_isBinProduct (c d p : C) (p1 : p --> c) (p2 : p --> d) :
isaprop (isBinProduct c d p p1 p2).
Show proof.
Definition BinProduct (c d : C) : UU :=
∑ pp1p2 : (∑ p : C, (p --> c) × (p --> d)),
isBinProduct c d (pr1 pp1p2) (pr1 (pr2 pp1p2)) (pr2 (pr2 pp1p2)).
Definition BinProducts : UU := ∏ (c d : C), BinProduct c d.
Definition hasBinProducts : UU := ∏ (c d : C), ∥ BinProduct c d ∥.
Definition BinProductObject {c d : C} (P : BinProduct c d) : C := pr1 (pr1 P).
Definition BinProductPr1 {c d : C} (P : BinProduct c d): BinProductObject P --> c :=
pr1 (pr2 (pr1 P)).
Definition BinProductPr2 {c d : C} (P : BinProduct c d) : BinProductObject P --> d :=
pr2 (pr2 (pr1 P)).
Definition isBinProduct_BinProduct {c d : C} (P : BinProduct c d) :
isBinProduct c d (BinProductObject P) (BinProductPr1 P) (BinProductPr2 P).
Show proof.
Definition BinProductArrow {c d : C} (P : BinProduct c d) {a : C} (f : a --> c) (g : a --> d) :
a --> BinProductObject P.
Show proof.
Lemma BinProductPr1Commutes (c d : C) (P : BinProduct c d):
∏ (a : C) (f : a --> c) g, BinProductArrow P f g · BinProductPr1 P = f.
Show proof.
Lemma BinProductPr2Commutes (c d : C) (P : BinProduct c d):
∏ (a : C) (f : a --> c) g, BinProductArrow P f g · BinProductPr2 P = g.
Show proof.
Lemma BinProductArrowUnique (c d : C) (P : BinProduct c d) (x : C)
(f : x --> c) (g : x --> d) (k : x --> BinProductObject P) :
k · BinProductPr1 P = f -> k · BinProductPr2 P = g ->
k = BinProductArrow P f g.
Show proof.
Lemma BinProductArrowsEq (c d : C) (P : BinProduct c d) (x : C)
(k1 k2 : x --> BinProductObject P) :
k1 · BinProductPr1 P = k2 · BinProductPr1 P ->
k1 · BinProductPr2 P = k2 · BinProductPr2 P ->
k1 = k2.
Show proof.
Definition mk_BinProduct (a b : C) :
∏ (c : C) (f : C⟦c,a⟧) (g : C⟦c,b⟧),
isBinProduct _ _ _ f g -> BinProduct a b.
Show proof.
Definition mk_isBinProduct (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) ->
isBinProduct a b p pa pb.
Show proof.
Lemma BinProductArrowEta (c d : C) (P : BinProduct c d) (x : C)
(f : x --> BinProductObject P) :
f = BinProductArrow P (f · BinProductPr1 P) (f · BinProductPr2 P).
Show proof.
Definition BinProductOfArrows {c d : C} (Pcd : BinProduct c d) {a b : C}
(Pab : BinProduct a b) (f : a --> c) (g : b --> d) :
BinProductObject Pab --> BinProductObject Pcd :=
BinProductArrow Pcd (BinProductPr1 Pab · f) (BinProductPr2 Pab · g).
Lemma BinProductOfArrowsPr1 {c d : C} (Pcd : BinProduct c d) {a b : C}
(Pab : BinProduct a b) (f : a --> c) (g : b --> d) :
BinProductOfArrows Pcd Pab f g · BinProductPr1 Pcd = BinProductPr1 Pab · f.
Show proof.
Lemma BinProductOfArrowsPr2 {c d : C} (Pcd : BinProduct c d) {a b : C}
(Pab : BinProduct a b) (f : a --> c) (g : b --> d) :
BinProductOfArrows Pcd Pab f g · BinProductPr2 Pcd = BinProductPr2 Pab · g.
Show proof.
Lemma postcompWithBinProductArrow {c d : C} (Pcd : BinProduct c d) {a b : C}
(Pab : BinProduct a b) (f : a --> c) (g : b --> d)
{x : C} (k : x --> a) (h : x --> b) :
BinProductArrow Pab k h · BinProductOfArrows Pcd Pab f g =
BinProductArrow Pcd (k · f) (h · g).
Show proof.
Lemma precompWithBinProductArrow {c d : C} (Pcd : BinProduct c d) {a : C}
(f : a --> c) (g : a --> d) {x : C} (k : x --> a) :
k · BinProductArrow Pcd f g = BinProductArrow Pcd (k · f) (k · g).
Show proof.
End binproduct_def.
Section BinProducts.
Variable C : precategory.
Variable CC : BinProducts C.
Variables a b c d x y : C.
Definition BinProductOfArrows_comp (f : a --> c) (f' : b --> d) (g : c --> x) (g' : d --> y)
: BinProductOfArrows _ (CC c d) (CC a b) f f' ·
BinProductOfArrows _ (CC _ _) (CC _ _) g g'
=
BinProductOfArrows _ (CC _ _) (CC _ _)(f · g) (f' · g').
Show proof.
Definition BinProductOfArrows_eq (f f' : a --> c) (g g' : b --> d)
: f = f' → g = g' →
BinProductOfArrows _ _ _ f g = BinProductOfArrows _ (CC _ _) (CC _ _) f' g'.
Show proof.
End BinProducts.
Section BinProduct_unique.
Variable C : precategory.
Variable CC : BinProducts C.
Variables a b : C.
Lemma BinProduct_endo_is_identity (P : BinProduct _ a b)
(k : BinProductObject _ P --> BinProductObject _ P)
(H1 : k · BinProductPr1 _ P = BinProductPr1 _ P)
(H2 : k · BinProductPr2 _ P = BinProductPr2 _ P)
: identity _ = k.
Show proof.
End BinProduct_unique.
Variable C : precategory.
Definition isBinProduct (c d p : C) (p1 : p --> c) (p2 : p --> d) : UU :=
∏ (a : C) (f : a --> c) (g : a --> d),
∃! fg, (fg · p1 = f) × (fg · p2 = g).
Lemma isaprop_isBinProduct (c d p : C) (p1 : p --> c) (p2 : p --> d) :
isaprop (isBinProduct c d p p1 p2).
Show proof.
do 3 (apply impred_isaprop; intro).
apply isapropiscontr.
apply isapropiscontr.
Definition BinProduct (c d : C) : UU :=
∑ pp1p2 : (∑ p : C, (p --> c) × (p --> d)),
isBinProduct c d (pr1 pp1p2) (pr1 (pr2 pp1p2)) (pr2 (pr2 pp1p2)).
Definition BinProducts : UU := ∏ (c d : C), BinProduct c d.
Definition hasBinProducts : UU := ∏ (c d : C), ∥ BinProduct c d ∥.
Definition BinProductObject {c d : C} (P : BinProduct c d) : C := pr1 (pr1 P).
Definition BinProductPr1 {c d : C} (P : BinProduct c d): BinProductObject P --> c :=
pr1 (pr2 (pr1 P)).
Definition BinProductPr2 {c d : C} (P : BinProduct c d) : BinProductObject P --> d :=
pr2 (pr2 (pr1 P)).
Definition isBinProduct_BinProduct {c d : C} (P : BinProduct c d) :
isBinProduct c d (BinProductObject P) (BinProductPr1 P) (BinProductPr2 P).
Show proof.
exact (pr2 P).
Definition BinProductArrow {c d : C} (P : BinProduct c d) {a : C} (f : a --> c) (g : a --> d) :
a --> BinProductObject P.
Show proof.
exact (pr1 (pr1 (isBinProduct_BinProduct P _ f g))).
Lemma BinProductPr1Commutes (c d : C) (P : BinProduct c d):
∏ (a : C) (f : a --> c) g, BinProductArrow P f g · BinProductPr1 P = f.
Show proof.
intros a f g.
exact (pr1 (pr2 (pr1 (isBinProduct_BinProduct P _ f g)))).
exact (pr1 (pr2 (pr1 (isBinProduct_BinProduct P _ f g)))).
Lemma BinProductPr2Commutes (c d : C) (P : BinProduct c d):
∏ (a : C) (f : a --> c) g, BinProductArrow P f g · BinProductPr2 P = g.
Show proof.
intros a f g.
exact (pr2 (pr2 (pr1 (isBinProduct_BinProduct P _ f g)))).
exact (pr2 (pr2 (pr1 (isBinProduct_BinProduct P _ f g)))).
Lemma BinProductArrowUnique (c d : C) (P : BinProduct c d) (x : C)
(f : x --> c) (g : x --> d) (k : x --> BinProductObject P) :
k · BinProductPr1 P = f -> k · BinProductPr2 P = g ->
k = BinProductArrow P f g.
Show proof.
intros H1 H2.
set (H := tpair (λ h, dirprod _ _ ) k (dirprodpair H1 H2)).
set (H' := (pr2 (isBinProduct_BinProduct P _ f g)) H).
apply (base_paths _ _ H').
set (H := tpair (λ h, dirprod _ _ ) k (dirprodpair H1 H2)).
set (H' := (pr2 (isBinProduct_BinProduct P _ f g)) H).
apply (base_paths _ _ H').
Lemma BinProductArrowsEq (c d : C) (P : BinProduct c d) (x : C)
(k1 k2 : x --> BinProductObject P) :
k1 · BinProductPr1 P = k2 · BinProductPr1 P ->
k1 · BinProductPr2 P = k2 · BinProductPr2 P ->
k1 = k2.
Show proof.
intros H1 H2.
set (p1 := k1 · BinProductPr1 P).
set (p2 := k1 · BinProductPr2 P).
rewrite (BinProductArrowUnique _ _ P _ p1 p2 k1).
apply pathsinv0.
apply BinProductArrowUnique.
unfold p1. apply pathsinv0. apply H1.
unfold p2. apply pathsinv0. apply H2.
apply idpath. apply idpath.
set (p1 := k1 · BinProductPr1 P).
set (p2 := k1 · BinProductPr2 P).
rewrite (BinProductArrowUnique _ _ P _ p1 p2 k1).
apply pathsinv0.
apply BinProductArrowUnique.
unfold p1. apply pathsinv0. apply H1.
unfold p2. apply pathsinv0. apply H2.
apply idpath. apply idpath.
Definition mk_BinProduct (a b : C) :
∏ (c : C) (f : C⟦c,a⟧) (g : C⟦c,b⟧),
isBinProduct _ _ _ f g -> BinProduct a b.
Show proof.
intros.
use tpair.
- exists c.
exists f.
exact g.
- exact X.
use tpair.
- exists c.
exists f.
exact g.
- exact X.
Definition mk_isBinProduct (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) ->
isBinProduct a b p pa pb.
Show proof.
intros H c cc g.
apply H.
apply H.
Lemma BinProductArrowEta (c d : C) (P : BinProduct c d) (x : C)
(f : x --> BinProductObject P) :
f = BinProductArrow P (f · BinProductPr1 P) (f · BinProductPr2 P).
Show proof.
apply BinProductArrowUnique;
apply idpath.
apply idpath.
Definition BinProductOfArrows {c d : C} (Pcd : BinProduct c d) {a b : C}
(Pab : BinProduct a b) (f : a --> c) (g : b --> d) :
BinProductObject Pab --> BinProductObject Pcd :=
BinProductArrow Pcd (BinProductPr1 Pab · f) (BinProductPr2 Pab · g).
Lemma BinProductOfArrowsPr1 {c d : C} (Pcd : BinProduct c d) {a b : C}
(Pab : BinProduct a b) (f : a --> c) (g : b --> d) :
BinProductOfArrows Pcd Pab f g · BinProductPr1 Pcd = BinProductPr1 Pab · f.
Show proof.
unfold BinProductOfArrows.
rewrite BinProductPr1Commutes.
apply idpath.
rewrite BinProductPr1Commutes.
apply idpath.
Lemma BinProductOfArrowsPr2 {c d : C} (Pcd : BinProduct c d) {a b : C}
(Pab : BinProduct a b) (f : a --> c) (g : b --> d) :
BinProductOfArrows Pcd Pab f g · BinProductPr2 Pcd = BinProductPr2 Pab · g.
Show proof.
unfold BinProductOfArrows.
rewrite BinProductPr2Commutes.
apply idpath.
rewrite BinProductPr2Commutes.
apply idpath.
Lemma postcompWithBinProductArrow {c d : C} (Pcd : BinProduct c d) {a b : C}
(Pab : BinProduct a b) (f : a --> c) (g : b --> d)
{x : C} (k : x --> a) (h : x --> b) :
BinProductArrow Pab k h · BinProductOfArrows Pcd Pab f g =
BinProductArrow Pcd (k · f) (h · g).
Show proof.
apply BinProductArrowUnique.
- rewrite <- assoc, BinProductOfArrowsPr1.
rewrite assoc, BinProductPr1Commutes.
apply idpath.
- rewrite <- assoc, BinProductOfArrowsPr2.
rewrite assoc, BinProductPr2Commutes.
apply idpath.
- rewrite <- assoc, BinProductOfArrowsPr1.
rewrite assoc, BinProductPr1Commutes.
apply idpath.
- rewrite <- assoc, BinProductOfArrowsPr2.
rewrite assoc, BinProductPr2Commutes.
apply idpath.
Lemma precompWithBinProductArrow {c d : C} (Pcd : BinProduct c d) {a : C}
(f : a --> c) (g : a --> d) {x : C} (k : x --> a) :
k · BinProductArrow Pcd f g = BinProductArrow Pcd (k · f) (k · g).
Show proof.
apply BinProductArrowUnique.
- rewrite <- assoc, BinProductPr1Commutes;
apply idpath.
- rewrite <- assoc, BinProductPr2Commutes;
apply idpath.
- rewrite <- assoc, BinProductPr1Commutes;
apply idpath.
- rewrite <- assoc, BinProductPr2Commutes;
apply idpath.
End binproduct_def.
Section BinProducts.
Variable C : precategory.
Variable CC : BinProducts C.
Variables a b c d x y : C.
Definition BinProductOfArrows_comp (f : a --> c) (f' : b --> d) (g : c --> x) (g' : d --> y)
: BinProductOfArrows _ (CC c d) (CC a b) f f' ·
BinProductOfArrows _ (CC _ _) (CC _ _) g g'
=
BinProductOfArrows _ (CC _ _) (CC _ _)(f · g) (f' · g').
Show proof.
apply BinProductArrowUnique.
- rewrite <- assoc.
rewrite BinProductOfArrowsPr1.
rewrite assoc.
rewrite BinProductOfArrowsPr1.
apply pathsinv0.
apply assoc.
- rewrite <- assoc.
rewrite BinProductOfArrowsPr2.
rewrite assoc.
rewrite BinProductOfArrowsPr2.
apply pathsinv0.
apply assoc.
- rewrite <- assoc.
rewrite BinProductOfArrowsPr1.
rewrite assoc.
rewrite BinProductOfArrowsPr1.
apply pathsinv0.
apply assoc.
- rewrite <- assoc.
rewrite BinProductOfArrowsPr2.
rewrite assoc.
rewrite BinProductOfArrowsPr2.
apply pathsinv0.
apply assoc.
Definition BinProductOfArrows_eq (f f' : a --> c) (g g' : b --> d)
: f = f' → g = g' →
BinProductOfArrows _ _ _ f g = BinProductOfArrows _ (CC _ _) (CC _ _) f' g'.
Show proof.
induction 1.
induction 1.
apply idpath.
induction 1.
apply idpath.
End BinProducts.
Section BinProduct_unique.
Variable C : precategory.
Variable CC : BinProducts C.
Variables a b : C.
Lemma BinProduct_endo_is_identity (P : BinProduct _ a b)
(k : BinProductObject _ P --> BinProductObject _ P)
(H1 : k · BinProductPr1 _ P = BinProductPr1 _ P)
(H2 : k · BinProductPr2 _ P = BinProductPr2 _ P)
: identity _ = k.
Show proof.
apply pathsinv0.
eapply pathscomp0.
apply BinProductArrowEta.
apply pathsinv0.
apply BinProductArrowUnique; apply pathsinv0.
+ rewrite id_left. exact H1.
+ rewrite id_left. exact H2.
eapply pathscomp0.
apply BinProductArrowEta.
apply pathsinv0.
apply BinProductArrowUnique; apply pathsinv0.
+ rewrite id_left. exact H1.
+ rewrite id_left. exact H2.
End BinProduct_unique.
Section BinProducts_from_Lims.
Variables (C : precategory) (hsC : has_homsets C).
Definition two_graph : graph := (bool,,λ _ _,empty).
Definition binproduct_diagram (a b : C) : diagram two_graph C.
Show proof.
exists (λ x : bool, if x then a else b).
abstract (intros u v F; induction F).
abstract (intros u v F; induction F).
Definition Binproduct {a b c : C} (f : c --> a) (g : c --> b) :
cone (binproduct_diagram a b) c.
Show proof.
use mk_cone; simpl.
+ intros x; induction x; assumption.
+ abstract (intros x y e; destruct e).
+ intros x; induction x; assumption.
+ abstract (intros x y e; destruct e).
Lemma BinProducts_from_Lims : Lims_of_shape two_graph C -> BinProducts C.
Show proof.
intros H a b.
set (LC := H (binproduct_diagram a b)); simpl.
use mk_BinProduct.
+ apply (lim LC).
+ apply (limOut LC true).
+ apply (limOut LC false).
+ apply (mk_isBinProduct _ hsC); simpl; intros c f g.
use unique_exists; simpl.
- apply limArrow, (Binproduct f g).
- abstract (split;
[ apply (limArrowCommutes LC c (Binproduct f g) true)
| apply (limArrowCommutes LC c (Binproduct f g) false) ]).
- abstract (intros h; apply isapropdirprod; apply hsC).
- abstract (now intros h [H1 H2]; apply limArrowUnique; intro x; induction x).
set (LC := H (binproduct_diagram a b)); simpl.
use mk_BinProduct.
+ apply (lim LC).
+ apply (limOut LC true).
+ apply (limOut LC false).
+ apply (mk_isBinProduct _ hsC); simpl; intros c f g.
use unique_exists; simpl.
- apply limArrow, (Binproduct f g).
- abstract (split;
[ apply (limArrowCommutes LC c (Binproduct f g) true)
| apply (limArrowCommutes LC c (Binproduct f g) false) ]).
- abstract (intros h; apply isapropdirprod; apply hsC).
- abstract (now intros h [H1 H2]; apply limArrowUnique; intro x; induction x).
End BinProducts_from_Lims.
Section test.
Variable C : precategory.
Variable H : BinProducts C.
Arguments BinProductObject [C] c d {_}.
Local Notation "c 'x' d" := (BinProductObject c d )(at level 5).
End test.
Section binproduct_functor.
Context {C : precategory} (PC : BinProducts C).
Definition binproduct_functor_data :
functor_data (precategory_binproduct C C) C.
Show proof.
use tpair.
- intros p.
apply (BinProductObject _ (PC (pr1 p) (pr2 p))).
- simpl; intros p q f.
apply (BinProductOfArrows _ (PC (pr1 q) (pr2 q))
(PC (pr1 p) (pr2 p)) (pr1 f) (pr2 f)).
- intros p.
apply (BinProductObject _ (PC (pr1 p) (pr2 p))).
- simpl; intros p q f.
apply (BinProductOfArrows _ (PC (pr1 q) (pr2 q))
(PC (pr1 p) (pr2 p)) (pr1 f) (pr2 f)).
Definition binproduct_functor : functor (precategory_binproduct C C) C.
Show proof.
apply (tpair _ binproduct_functor_data).
abstract (split;
[ intro x; simpl; apply pathsinv0, BinProduct_endo_is_identity;
[ now rewrite BinProductOfArrowsPr1, id_right
| now rewrite BinProductOfArrowsPr2, id_right ]
| now intros x y z f g; simpl; rewrite BinProductOfArrows_comp]).
abstract (split;
[ intro x; simpl; apply pathsinv0, BinProduct_endo_is_identity;
[ now rewrite BinProductOfArrowsPr1, id_right
| now rewrite BinProductOfArrowsPr2, id_right ]
| now intros x y z f g; simpl; rewrite BinProductOfArrows_comp]).
End binproduct_functor.
Definition BinProduct_of_functors_alt {C D : precategory} (HD : BinProducts D)
(F G : functor C D) : functor C D :=
functor_composite (bindelta_functor C)
(functor_composite (pair_functor F G) (binproduct_functor HD)).
In the following section we show that if the morphism to components are
zero, then the unique morphism factoring through the binproduct is the
zero morphism.
Section BinProduct_zeroarrow.
Variable C : precategory.
Variable Z : Zero C.
Lemma BinProductArrowZero {x y z: C} {BP : BinProduct C x y} (f : z --> x) (g : z --> y) :
f = ZeroArrow Z _ _ -> g = ZeroArrow Z _ _ -> BinProductArrow C BP f g = ZeroArrow Z _ _ .
Show proof.
End BinProduct_zeroarrow.
Variable C : precategory.
Variable Z : Zero C.
Lemma BinProductArrowZero {x y z: C} {BP : BinProduct C x y} (f : z --> x) (g : z --> y) :
f = ZeroArrow Z _ _ -> g = ZeroArrow Z _ _ -> BinProductArrow C BP f g = ZeroArrow Z _ _ .
Show proof.
intros X X0. apply pathsinv0.
use BinProductArrowUnique.
rewrite X. apply ZeroArrow_comp_left.
rewrite X0. apply ZeroArrow_comp_left.
use BinProductArrowUnique.
rewrite X. apply ZeroArrow_comp_left.
rewrite X0. apply ZeroArrow_comp_left.
End BinProduct_zeroarrow.
Definition of a binary product structure on a functor category
Section def_functor_pointwise_binprod.
Variable C D : precategory.
Variable HD : BinProducts D.
Variable hsD : has_homsets D.
Section BinProduct_of_functors.
Variables F G : functor C D.
Local Notation "c ⊗ d" := (BinProductObject _ (HD c d)).
Definition BinProduct_of_functors_ob (c : C) : D := F c ⊗ G c.
Definition BinProduct_of_functors_mor (c c' : C) (f : c --> c')
: BinProduct_of_functors_ob c --> BinProduct_of_functors_ob c'
:= BinProductOfArrows _ _ _ (#F f) (#G f).
Definition BinProduct_of_functors_data : functor_data C D.
Show proof.
Lemma is_functor_BinProduct_of_functors_data : is_functor BinProduct_of_functors_data.
Show proof.
Definition BinProduct_of_functors : functor C D :=
tpair _ _ is_functor_BinProduct_of_functors_data.
Lemma BinProduct_of_functors_alt_eq_BinProduct_of_functors :
BinProduct_of_functors_alt HD F G = BinProduct_of_functors.
Show proof.
Definition binproduct_nat_trans_pr1_data : ∏ c, BinProduct_of_functors c --> F c
:= λ c : C, BinProductPr1 _ (HD (F c) (G c)).
Lemma is_nat_trans_binproduct_nat_trans_pr1_data
: is_nat_trans _ _ binproduct_nat_trans_pr1_data.
Show proof.
Definition binproduct_nat_trans_pr1 : nat_trans _ _
:= tpair _ _ is_nat_trans_binproduct_nat_trans_pr1_data.
Definition binproduct_nat_trans_pr2_data : ∏ c, BinProduct_of_functors c --> G c
:= λ c : C, BinProductPr2 _ (HD (F c) (G c)).
Lemma is_nat_trans_binproduct_nat_trans_pr2_data
: is_nat_trans _ _ binproduct_nat_trans_pr2_data.
Show proof.
Definition binproduct_nat_trans_pr2 : nat_trans _ _
:= tpair _ _ is_nat_trans_binproduct_nat_trans_pr2_data.
Section vertex.
Variable C D : precategory.
Variable HD : BinProducts D.
Variable hsD : has_homsets D.
Section BinProduct_of_functors.
Variables F G : functor C D.
Local Notation "c ⊗ d" := (BinProductObject _ (HD c d)).
Definition BinProduct_of_functors_ob (c : C) : D := F c ⊗ G c.
Definition BinProduct_of_functors_mor (c c' : C) (f : c --> c')
: BinProduct_of_functors_ob c --> BinProduct_of_functors_ob c'
:= BinProductOfArrows _ _ _ (#F f) (#G f).
Definition BinProduct_of_functors_data : functor_data C D.
Show proof.
exists BinProduct_of_functors_ob.
exact BinProduct_of_functors_mor.
exact BinProduct_of_functors_mor.
Lemma is_functor_BinProduct_of_functors_data : is_functor BinProduct_of_functors_data.
Show proof.
split; simpl; intros.
- red; intros; simpl in *.
apply pathsinv0.
unfold BinProduct_of_functors_mor.
apply BinProduct_endo_is_identity.
+ rewrite BinProductOfArrowsPr1.
rewrite functor_id.
apply id_right.
+ rewrite BinProductOfArrowsPr2.
rewrite functor_id.
apply id_right.
- red; intros; simpl in *.
unfold BinProduct_of_functors_mor.
do 2 rewrite functor_comp.
apply pathsinv0.
apply BinProductOfArrows_comp.
- red; intros; simpl in *.
apply pathsinv0.
unfold BinProduct_of_functors_mor.
apply BinProduct_endo_is_identity.
+ rewrite BinProductOfArrowsPr1.
rewrite functor_id.
apply id_right.
+ rewrite BinProductOfArrowsPr2.
rewrite functor_id.
apply id_right.
- red; intros; simpl in *.
unfold BinProduct_of_functors_mor.
do 2 rewrite functor_comp.
apply pathsinv0.
apply BinProductOfArrows_comp.
Definition BinProduct_of_functors : functor C D :=
tpair _ _ is_functor_BinProduct_of_functors_data.
Lemma BinProduct_of_functors_alt_eq_BinProduct_of_functors :
BinProduct_of_functors_alt HD F G = BinProduct_of_functors.
Show proof.
now apply (functor_eq _ _ hsD).
Definition binproduct_nat_trans_pr1_data : ∏ c, BinProduct_of_functors c --> F c
:= λ c : C, BinProductPr1 _ (HD (F c) (G c)).
Lemma is_nat_trans_binproduct_nat_trans_pr1_data
: is_nat_trans _ _ binproduct_nat_trans_pr1_data.
Show proof.
red.
intros c c' f.
unfold binproduct_nat_trans_pr1_data.
unfold BinProduct_of_functors. simpl.
unfold BinProduct_of_functors_mor.
apply BinProductOfArrowsPr1.
intros c c' f.
unfold binproduct_nat_trans_pr1_data.
unfold BinProduct_of_functors. simpl.
unfold BinProduct_of_functors_mor.
apply BinProductOfArrowsPr1.
Definition binproduct_nat_trans_pr1 : nat_trans _ _
:= tpair _ _ is_nat_trans_binproduct_nat_trans_pr1_data.
Definition binproduct_nat_trans_pr2_data : ∏ c, BinProduct_of_functors c --> G c
:= λ c : C, BinProductPr2 _ (HD (F c) (G c)).
Lemma is_nat_trans_binproduct_nat_trans_pr2_data
: is_nat_trans _ _ binproduct_nat_trans_pr2_data.
Show proof.
red.
intros c c' f.
unfold binproduct_nat_trans_pr2_data.
unfold BinProduct_of_functors. simpl.
unfold BinProduct_of_functors_mor.
apply BinProductOfArrowsPr2.
intros c c' f.
unfold binproduct_nat_trans_pr2_data.
unfold BinProduct_of_functors. simpl.
unfold BinProduct_of_functors_mor.
apply BinProductOfArrowsPr2.
Definition binproduct_nat_trans_pr2 : nat_trans _ _
:= tpair _ _ is_nat_trans_binproduct_nat_trans_pr2_data.
Section vertex.
The product morphism of a diagram with vertex A
Variable A : functor C D.
Variable f : A ⟹ F.
Variable g : A ⟹ G.
Definition binproduct_nat_trans_data : ∏ c, A c --> BinProduct_of_functors c.
Show proof.
intro c.
apply BinProductArrow.
- exact (f c).
- exact (g c).
apply BinProductArrow.
- exact (f c).
- exact (g c).
Lemma is_nat_trans_binproduct_nat_trans_data : is_nat_trans _ _ binproduct_nat_trans_data.
Show proof.
intros a b k.
simpl.
unfold BinProduct_of_functors_mor.
unfold binproduct_nat_trans_data.
set (XX:=postcompWithBinProductArrow).
set (X1 := XX D _ _ (HD (F b) (G b))).
set (X2 := X1 _ _ (HD (F a) (G a))).
rewrite X2.
clear X2 X1 XX.
set (XX:=precompWithBinProductArrow).
set (X1 := XX D _ _ (HD (F b) (G b))).
rewrite X1.
rewrite (nat_trans_ax f).
rewrite (nat_trans_ax g).
apply idpath.
simpl.
unfold BinProduct_of_functors_mor.
unfold binproduct_nat_trans_data.
set (XX:=postcompWithBinProductArrow).
set (X1 := XX D _ _ (HD (F b) (G b))).
set (X2 := X1 _ _ (HD (F a) (G a))).
rewrite X2.
clear X2 X1 XX.
set (XX:=precompWithBinProductArrow).
set (X1 := XX D _ _ (HD (F b) (G b))).
rewrite X1.
rewrite (nat_trans_ax f).
rewrite (nat_trans_ax g).
apply idpath.
Definition binproduct_nat_trans : nat_trans _ _
:= tpair _ _ is_nat_trans_binproduct_nat_trans_data.
Lemma binproduct_nat_trans_Pr1Commutes :
nat_trans_comp _ _ _ binproduct_nat_trans binproduct_nat_trans_pr1 = f.
Show proof.
apply nat_trans_eq.
- apply hsD.
- intro c; simpl.
apply BinProductPr1Commutes.
- apply hsD.
- intro c; simpl.
apply BinProductPr1Commutes.
Lemma binproduct_nat_trans_Pr2Commutes :
nat_trans_comp _ _ _ binproduct_nat_trans binproduct_nat_trans_pr2 = g.
Show proof.
apply nat_trans_eq.
- apply hsD.
- intro c; simpl.
apply BinProductPr2Commutes.
- apply hsD.
- intro c; simpl.
apply BinProductPr2Commutes.
End vertex.
Lemma binproduct_nat_trans_univ_prop (A : [C, D, hsD])
(f : (A --> (F:[C,D,hsD]))) (g : A --> (G:[C,D,hsD])) :
∏
t : ∑ fg : A --> (BinProduct_of_functors:[C,D,hsD]),
fg · (binproduct_nat_trans_pr1 : (BinProduct_of_functors:[C,D,hsD]) --> F) = f
×
fg · (binproduct_nat_trans_pr2 : (BinProduct_of_functors:[C,D,hsD]) --> G) = g,
t =
tpair
(λ fg : A --> (BinProduct_of_functors:[C,D,hsD]),
fg · (binproduct_nat_trans_pr1 : (BinProduct_of_functors:[C,D,hsD]) --> F) = f
×
fg · (binproduct_nat_trans_pr2 : (BinProduct_of_functors:[C,D,hsD]) --> G) = g)
(binproduct_nat_trans A f g)
(dirprodpair (binproduct_nat_trans_Pr1Commutes A f g)
(binproduct_nat_trans_Pr2Commutes A f g)).
Show proof.
intro t.
simpl in *.
destruct t as [t1 [ta tb]].
simpl in *.
apply subtypeEquality.
- intro.
simpl.
apply isapropdirprod;
apply isaset_nat_trans;
apply hsD.
- simpl.
apply nat_trans_eq.
+ apply hsD.
+ intro c.
unfold binproduct_nat_trans.
simpl.
unfold binproduct_nat_trans_data.
apply BinProductArrowUnique.
* apply (nat_trans_eq_pointwise ta).
* apply (nat_trans_eq_pointwise tb).
simpl in *.
destruct t as [t1 [ta tb]].
simpl in *.
apply subtypeEquality.
- intro.
simpl.
apply isapropdirprod;
apply isaset_nat_trans;
apply hsD.
- simpl.
apply nat_trans_eq.
+ apply hsD.
+ intro c.
unfold binproduct_nat_trans.
simpl.
unfold binproduct_nat_trans_data.
apply BinProductArrowUnique.
* apply (nat_trans_eq_pointwise ta).
* apply (nat_trans_eq_pointwise tb).
Definition functor_precat_binproduct_cone
: BinProduct [C, D, hsD] F G.
Show proof.
use mk_BinProduct.
- apply BinProduct_of_functors.
- apply binproduct_nat_trans_pr1.
- apply binproduct_nat_trans_pr2.
- use mk_isBinProduct.
+ apply functor_category_has_homsets.
+ intros A f g.
exists (tpair _ (binproduct_nat_trans A f g)
(dirprodpair (binproduct_nat_trans_Pr1Commutes _ _ _ )
(binproduct_nat_trans_Pr2Commutes _ _ _ ))).
simpl.
apply binproduct_nat_trans_univ_prop.
- apply BinProduct_of_functors.
- apply binproduct_nat_trans_pr1.
- apply binproduct_nat_trans_pr2.
- use mk_isBinProduct.
+ apply functor_category_has_homsets.
+ intros A f g.
exists (tpair _ (binproduct_nat_trans A f g)
(dirprodpair (binproduct_nat_trans_Pr1Commutes _ _ _ )
(binproduct_nat_trans_Pr2Commutes _ _ _ ))).
simpl.
apply binproduct_nat_trans_univ_prop.
End BinProduct_of_functors.
Definition BinProducts_functor_precat : BinProducts [C, D, hsD].
Show proof.
intros F G.
apply functor_precat_binproduct_cone.
apply functor_precat_binproduct_cone.
End def_functor_pointwise_binprod.
Section BinProduct_from_iso.
Variable C : precategory.
Hypothesis hs : has_homsets C.
Local Lemma iso_to_isBinProduct_comm {x y z : C} (BP : BinProduct C x y)
(i : iso z (BinProductObject C BP)) (w : C) (f : w --> x) (g : w --> y) :
(BinProductArrow C BP f g · inv_from_iso i · (i · BinProductPr1 C BP) = f)
× (BinProductArrow C BP f g · inv_from_iso i · (i · BinProductPr2 C BP) = g).
Show proof.
Local Lemma iso_to_isBinProduct_unique {x y z : C} (BP : BinProduct C x y)
(i : iso z (BinProductObject C BP)) (w : C) (f : C ⟦w, x⟧) (g : C ⟦w, y⟧) (y0 : C ⟦w, z⟧)
(T : y0 · (i · BinProductPr1 C BP) = f × y0 · (i · BinProductPr2 C BP) = g) :
y0 = BinProductArrow C BP f g · iso_inv_from_iso i.
Show proof.
Lemma iso_to_isBinProduct {x y z : C} (BP : BinProduct C x y)
(i : iso z (BinProductObject C BP)) :
isBinProduct C _ _ z (i · (BinProductPr1 C BP)) (i · (BinProductPr2 C BP)).
Show proof.
Definition iso_to_BinProduct {x y z : C} (BP : BinProduct C x y)
(i : iso z (BinProductObject C BP)) :
BinProduct C x y := mk_BinProduct C _ _ z
(i · (BinProductPr1 C BP))
(i · (BinProductPr2 C BP))
(iso_to_isBinProduct BP i).
End BinProduct_from_iso.
Variable C : precategory.
Hypothesis hs : has_homsets C.
Local Lemma iso_to_isBinProduct_comm {x y z : C} (BP : BinProduct C x y)
(i : iso z (BinProductObject C BP)) (w : C) (f : w --> x) (g : w --> y) :
(BinProductArrow C BP f g · inv_from_iso i · (i · BinProductPr1 C BP) = f)
× (BinProductArrow C BP f g · inv_from_iso i · (i · BinProductPr2 C BP) = g).
Show proof.
split.
- rewrite <- assoc. rewrite (assoc _ i).
rewrite (iso_after_iso_inv i). rewrite id_left.
apply BinProductPr1Commutes.
- rewrite <- assoc. rewrite (assoc _ i).
rewrite (iso_after_iso_inv i). rewrite id_left.
apply BinProductPr2Commutes.
- rewrite <- assoc. rewrite (assoc _ i).
rewrite (iso_after_iso_inv i). rewrite id_left.
apply BinProductPr1Commutes.
- rewrite <- assoc. rewrite (assoc _ i).
rewrite (iso_after_iso_inv i). rewrite id_left.
apply BinProductPr2Commutes.
Local Lemma iso_to_isBinProduct_unique {x y z : C} (BP : BinProduct C x y)
(i : iso z (BinProductObject C BP)) (w : C) (f : C ⟦w, x⟧) (g : C ⟦w, y⟧) (y0 : C ⟦w, z⟧)
(T : y0 · (i · BinProductPr1 C BP) = f × y0 · (i · BinProductPr2 C BP) = g) :
y0 = BinProductArrow C BP f g · iso_inv_from_iso i.
Show proof.
apply (post_comp_with_iso_is_inj C _ _ i (pr2 i)).
rewrite <- assoc. cbn. rewrite (iso_after_iso_inv i). rewrite id_right.
apply BinProductArrowUnique.
- rewrite <- assoc. apply (dirprod_pr1 T).
- rewrite <- assoc. apply (dirprod_pr2 T).
rewrite <- assoc. cbn. rewrite (iso_after_iso_inv i). rewrite id_right.
apply BinProductArrowUnique.
- rewrite <- assoc. apply (dirprod_pr1 T).
- rewrite <- assoc. apply (dirprod_pr2 T).
Lemma iso_to_isBinProduct {x y z : C} (BP : BinProduct C x y)
(i : iso z (BinProductObject C BP)) :
isBinProduct C _ _ z (i · (BinProductPr1 C BP)) (i · (BinProductPr2 C BP)).
Show proof.
intros w f g.
use unique_exists.
- exact ((BinProductArrow C BP f g) · (iso_inv_from_iso i)).
- exact (iso_to_isBinProduct_comm BP i w f g).
- intros y0. apply isapropdirprod. apply hs. apply hs.
- intros y0 T. exact (iso_to_isBinProduct_unique BP i w f g y0 T).
Opaque iso_to_isBinProduct.use unique_exists.
- exact ((BinProductArrow C BP f g) · (iso_inv_from_iso i)).
- exact (iso_to_isBinProduct_comm BP i w f g).
- intros y0. apply isapropdirprod. apply hs. apply hs.
- intros y0 T. exact (iso_to_isBinProduct_unique BP i w f g y0 T).
Definition iso_to_BinProduct {x y z : C} (BP : BinProduct C x y)
(i : iso z (BinProductObject C BP)) :
BinProduct C x y := mk_BinProduct C _ _ z
(i · (BinProductPr1 C BP))
(i · (BinProductPr2 C BP))
(iso_to_isBinProduct BP i).
End BinProduct_from_iso.
Section EquivalentDefinition.
Context {C : precategory} {c d p : ob C} (p1 : p --> c) (p2 : p --> d).
Definition postcomp_with_projections (a : ob C) (f : a --> p) :
(a --> c) × (a --> d) := dirprodpair (f · p1) (f · p2).
Definition isBinProduct' : UU := ∏ a : ob C, isweq (postcomp_with_projections a).
Definition isBinProduct'_weq (is : isBinProduct') :
∏ a, (a --> p) ≃ (a --> c) × (a --> d) :=
λ a, weqpair (postcomp_with_projections a) (is a).
Lemma isBinProduct'_to_isBinProduct :
isBinProduct' -> isBinProduct _ _ _ p p1 p2.
Show proof.
intros isBP' ? f g.
apply (@iscontrweqf (hfiber (isBinProduct'_weq isBP' _)
(dirprodpair f g))).
- use weqfibtototal; intro; cbn.
unfold postcomp_with_projections.
apply pathsdirprodweq.
- apply weqproperty.
apply (@iscontrweqf (hfiber (isBinProduct'_weq isBP' _)
(dirprodpair f g))).
- use weqfibtototal; intro; cbn.
unfold postcomp_with_projections.
apply pathsdirprodweq.
- apply weqproperty.
Lemma isBinProduct_to_isBinProduct' :
isBinProduct _ _ _ p p1 p2 -> isBinProduct'.
Show proof.
intros isBP ? fg.
unfold hfiber, postcomp_with_projections.
apply (@iscontrweqf (∑ u : C ⟦ a, p ⟧, u · p1 = pr1 fg × u · p2 = pr2 fg)).
- use weqfibtototal; intro; cbn.
apply invweq, pathsdirprodweq.
- exact (isBP a (pr1 fg) (pr2 fg)).
unfold hfiber, postcomp_with_projections.
apply (@iscontrweqf (∑ u : C ⟦ a, p ⟧, u · p1 = pr1 fg × u · p2 = pr2 fg)).
- use weqfibtototal; intro; cbn.
apply invweq, pathsdirprodweq.
- exact (isBP a (pr1 fg) (pr2 fg)).
End EquivalentDefinition.
Match non-implicit arguments of isBinProduct
Arguments isBinProduct' _ _ _ _ _ : clear implicits.
Local Lemma f_equal_2 :
forall {A B C : UU} (f : A -> B -> C) (a a' : A) (b b' : B),
a = a' -> b = b' -> f a b = f a' b'.
Show proof.
do 8 intro; intros eq1 eq2.
abstract (now rewrite eq1; rewrite eq2).
abstract (now rewrite eq1; rewrite eq2).
Lemma terminal_binprod_unit_l {C : precategory}
(T : Terminal C) (BC : BinProducts C) :
∏ x : C, is_iso (BinProductPr2 C (BC T x)).
Show proof.
(T : Terminal C) (BC : BinProducts C) :
∏ x : C, is_iso (BinProductPr2 C (BC T x)).
Show proof.
intros x.
use is_iso_qinv.
apply BinProductArrow.
-
use is_iso_qinv.
apply BinProductArrow.
-
apply TerminalArrow.
- apply identity.
-
- apply identity.
-
These are inverses
unfold is_inverse_in_precat.
split; [|apply BinProductPr2Commutes].
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
apply f_equal_2.
+ apply TerminalArrowEq.
+ exact (id_right _ @ !id_left _).
split; [|apply BinProductPr2Commutes].
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
apply f_equal_2.
+ apply TerminalArrowEq.
+ exact (id_right _ @ !id_left _).
Lemma terminal_binprod_unit_r {C : precategory}
(T : Terminal C) (BC : BinProducts C) :
∏ x : C, is_iso (BinProductPr1 C (BC x T)).
Show proof.
intros x.
use is_iso_qinv.
apply BinProductArrow.
- apply identity.
-
use is_iso_qinv.
apply BinProductArrow.
- apply identity.
-
apply TerminalArrow.
-
-
These are inverses
unfold is_inverse_in_precat.
split; [|apply BinProductPr1Commutes].
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
apply f_equal_2.
+ exact (id_right _ @ !id_left _).
+ apply TerminalArrowEq.
split; [|apply BinProductPr1Commutes].
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
apply f_equal_2.
+ exact (id_right _ @ !id_left _).
+ apply TerminalArrowEq.