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
- Definition of the "associative" z-isomorphism BinProduct_assoc
- Definition of the diagonal map diagonalMap
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
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.Monics.
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.
Context (C : category).
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).
Coercion BinProductObject : BinProduct >-> ob.
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 make_BinProduct (a b : C) :
∏ (c : C) (f : C⟦c,a⟧) (g : C⟦c,b⟧),
isBinProduct _ _ _ f g -> BinProduct a b.
Show proof.
Definition make_isBinProduct (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.
Context (C : category) (CC : BinProducts C).
Definition BinProductOfArrows_comp (a b c d x y : C) (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.
Lemma BinProductOfArrows_idxcomp {a b c d : C} (f:C⟦ b, c ⟧) (g:C⟦ c, d ⟧)
: BinProductOfArrows _ (CC a c) (CC a b) (identity a) f ·
BinProductOfArrows _ (CC _ _) (CC _ _) (identity a) g
=
BinProductOfArrows _ (CC _ _) (CC _ _)(identity a) (f·g).
Show proof.
Lemma BinProductOfArrows_compxid {a b c d : C} (f:C⟦ b, c ⟧) (g:C⟦ c, d ⟧)
: BinProductOfArrows _ (CC c a) (CC b a) f (identity a) ·
BinProductOfArrows _ (CC _ _) (CC _ _) g (identity a)
=
BinProductOfArrows _ (CC _ _) (CC _ _) (f·g) (identity a).
Show proof.
Lemma BinProductOfArrows_id (a b:C)
: BinProductOfArrows _ (CC a b) (CC a b) (identity a) (identity b)
= identity _ .
Show proof.
End BinProducts.
Section BinProduct_unique.
Context (C : category) (CC : BinProducts C) (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.
Context (C : category).
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).
Coercion BinProductObject : BinProduct >-> ob.
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.
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 make_BinProduct (a b : C) :
∏ (c : C) (f : C⟦c,a⟧) (g : C⟦c,b⟧),
isBinProduct _ _ _ f g -> BinProduct a b.
Show proof.
Definition make_isBinProduct (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.
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.
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.
Context (C : category) (CC : BinProducts C).
Definition BinProductOfArrows_comp (a b c d x y : C) (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.
Lemma BinProductOfArrows_idxcomp {a b c d : C} (f:C⟦ b, c ⟧) (g:C⟦ c, d ⟧)
: BinProductOfArrows _ (CC a c) (CC a b) (identity a) f ·
BinProductOfArrows _ (CC _ _) (CC _ _) (identity a) g
=
BinProductOfArrows _ (CC _ _) (CC _ _)(identity a) (f·g).
Show proof.
Lemma BinProductOfArrows_compxid {a b c d : C} (f:C⟦ b, c ⟧) (g:C⟦ c, d ⟧)
: BinProductOfArrows _ (CC c a) (CC b a) f (identity a) ·
BinProductOfArrows _ (CC _ _) (CC _ _) g (identity a)
=
BinProductOfArrows _ (CC _ _) (CC _ _) (f·g) (identity a).
Show proof.
Lemma BinProductOfArrows_id (a b:C)
: BinProductOfArrows _ (CC a b) (CC a b) (identity a) (identity b)
= identity _ .
Show proof.
unfold BinProductOfArrows.
use pathsinv0.
use BinProductArrowUnique.
+ now rewrite id_left, id_right.
+ now rewrite id_left, id_right.
use pathsinv0.
use BinProductArrowUnique.
+ now rewrite id_left, id_right.
+ now rewrite id_left, id_right.
End BinProducts.
Section BinProduct_unique.
Context (C : category) (CC : BinProducts C) (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.
Binary products from limits (BinProducts_from_Lims)
Section BinProducts_from_Lims.
Context (C : category).
Definition two_graph : graph := (bool,,λ _ _,empty).
Definition binproduct_diagram (a b : C) : diagram two_graph C.
Show proof.
Definition Binproduct {a b c : C} (f : c --> a) (g : c --> b) :
cone (binproduct_diagram a b) c.
Show proof.
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)).
use make_BinProduct.
+ apply (lim LC).
+ apply (limOut LC true).
+ apply (limOut LC false).
+ apply (make_isBinProduct C); intros c f g.
use unique_exists.
- 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 C).
- abstract (now intros h [H1 H2]; apply limArrowUnique; intro x; induction x).
set (LC := H (binproduct_diagram a b)).
use make_BinProduct.
+ apply (lim LC).
+ apply (limOut LC true).
+ apply (limOut LC false).
+ apply (make_isBinProduct C); intros c f g.
use unique_exists.
- 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 C).
- abstract (now intros h [H1 H2]; apply limArrowUnique; intro x; induction x).
End BinProducts_from_Lims.
Section test.
Context (C : category) (H : BinProducts C).
Arguments BinProductObject [C] c d {_}.
Local Notation "c 'x' d" := (BinProductObject c d )(at level 5).
End test.
Definition of binary product functor (binproduct_functor)
Section binproduct_functor.
Context {C : category} (PC : BinProducts C).
Definition binproduct_functor_data :
functor_data (category_binproduct C C) C.
Show proof.
use tpair.
- intros p.
apply (BinProductObject _ (PC (pr1 p) (pr2 p))).
- 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))).
- intros p q f.
apply (BinProductOfArrows _ (PC (pr1 q) (pr2 q))
(PC (pr1 p) (pr2 p)) (pr1 f) (pr2 f)).
Definition binproduct_functor : functor (category_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 : category} (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.
Context (C : category) (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.
Context (C : category) (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.
Context (C D : category) (HD : BinProducts D).
Section BinProduct_of_functors.
Context (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.
Context (C D : category) (HD : BinProducts D).
Section BinProduct_of_functors.
Context (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.
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.
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
Context (A : functor C D) (f : A ⟹ F) (g : A ⟹ G).
Definition binproduct_nat_trans_data : ∏ c, A c --> BinProduct_of_functors c.
Show proof.
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.
Lemma binproduct_nat_trans_Pr2Commutes :
nat_trans_comp _ _ _ binproduct_nat_trans binproduct_nat_trans_pr2 = g.
Show proof.
End vertex.
Lemma binproduct_nat_trans_univ_prop (A : [C, D])
(f : A --> (F:[C,D])) (g : A --> (G:[C,D])) :
∏
t : ∑ fg : A --> (BinProduct_of_functors:[C,D]),
fg · (binproduct_nat_trans_pr1 : (BinProduct_of_functors:[C,D]) --> F) = f
×
fg · (binproduct_nat_trans_pr2 : (BinProduct_of_functors:[C,D]) --> G) = g,
t =
tpair
(λ fg : A --> (BinProduct_of_functors:[C,D]),
fg · (binproduct_nat_trans_pr1 : (BinProduct_of_functors:[C,D]) --> F) = f
×
fg · (binproduct_nat_trans_pr2 : (BinProduct_of_functors:[C,D]) --> G) = g)
(binproduct_nat_trans A f g)
(make_dirprod (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 subtypePath.
- intro.
simpl.
apply isapropdirprod;
apply isaset_nat_trans;
apply D.
- simpl.
apply nat_trans_eq.
+ apply D.
+ 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 subtypePath.
- intro.
simpl.
apply isapropdirprod;
apply isaset_nat_trans;
apply D.
- simpl.
apply nat_trans_eq.
+ apply D.
+ 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] F G.
Show proof.
use make_BinProduct.
- apply BinProduct_of_functors.
- apply binproduct_nat_trans_pr1.
- apply binproduct_nat_trans_pr2.
- use make_isBinProduct.
+ intros A f g.
exists (tpair _ (binproduct_nat_trans A f g)
(make_dirprod (binproduct_nat_trans_Pr1Commutes _ _ _ )
(binproduct_nat_trans_Pr2Commutes _ _ _ ))).
apply binproduct_nat_trans_univ_prop.
- apply BinProduct_of_functors.
- apply binproduct_nat_trans_pr1.
- apply binproduct_nat_trans_pr2.
- use make_isBinProduct.
+ intros A f g.
exists (tpair _ (binproduct_nat_trans A f g)
(make_dirprod (binproduct_nat_trans_Pr1Commutes _ _ _ )
(binproduct_nat_trans_Pr2Commutes _ _ _ ))).
apply binproduct_nat_trans_univ_prop.
End BinProduct_of_functors.
Definition BinProducts_functor_precat : BinProducts [C, D].
Show proof.
End def_functor_pointwise_binprod.
Section BinProduct_of_functors_commutative.
Context (C D : category) (BD : BinProducts D) (F G : functor C D).
Definition BinProduct_of_functors_commutes_data :
nat_trans_data (BinProduct_of_functors C D BD F G) (BinProduct_of_functors C D BD G F).
Show proof.
Definition BinProduct_of_functors_commutes_invdata :
nat_trans_data (BinProduct_of_functors C D BD G F) (BinProduct_of_functors C D BD F G).
Show proof.
Lemma BinProduct_of_functors_commutes_is_inverse (c: C) :
is_inverse_in_precat (BinProduct_of_functors_commutes_data c) (BinProduct_of_functors_commutes_invdata c).
Show proof.
split.
- apply BinProductArrowsEq.
+ rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr1Commutes. }
etrans.
{ apply BinProductPr2Commutes. }
apply pathsinv0, id_left.
+ rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr2Commutes. }
etrans.
{ apply BinProductPr1Commutes. }
apply pathsinv0, id_left.
- apply BinProductArrowsEq.
+ rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr1Commutes. }
etrans.
{ apply BinProductPr2Commutes. }
apply pathsinv0, id_left.
+ rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr2Commutes. }
etrans.
{ apply BinProductPr1Commutes. }
apply pathsinv0, id_left.
- apply BinProductArrowsEq.
+ rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr1Commutes. }
etrans.
{ apply BinProductPr2Commutes. }
apply pathsinv0, id_left.
+ rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr2Commutes. }
etrans.
{ apply BinProductPr1Commutes. }
apply pathsinv0, id_left.
- apply BinProductArrowsEq.
+ rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr1Commutes. }
etrans.
{ apply BinProductPr2Commutes. }
apply pathsinv0, id_left.
+ rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr2Commutes. }
etrans.
{ apply BinProductPr1Commutes. }
apply pathsinv0, id_left.
Lemma BinProduct_of_functors_commutes_law : is_nat_trans _ _ BinProduct_of_functors_commutes_data.
Show proof.
intros c c' f.
cbn.
unfold BinProduct_of_functors_mor.
etrans.
2: { apply pathsinv0, postcompWithBinProductArrow. }
apply BinProductArrowUnique.
- rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr1Commutes. }
etrans.
{ apply BinProductOfArrowsPr2. }
apply idpath.
- rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr2Commutes. }
etrans.
{ apply BinProductOfArrowsPr1. }
apply idpath.
cbn.
unfold BinProduct_of_functors_mor.
etrans.
2: { apply pathsinv0, postcompWithBinProductArrow. }
apply BinProductArrowUnique.
- rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr1Commutes. }
etrans.
{ apply BinProductOfArrowsPr2. }
apply idpath.
- rewrite assoc'.
etrans.
{ apply maponpaths.
apply BinProductPr2Commutes. }
etrans.
{ apply BinProductOfArrowsPr1. }
apply idpath.
Definition BinProduct_of_functors_commutes :
nat_z_iso (BinProduct_of_functors C D BD F G) (BinProduct_of_functors C D BD G F).
Show proof.
use make_nat_z_iso.
- use make_nat_trans.
+ exact BinProduct_of_functors_commutes_data.
+ exact BinProduct_of_functors_commutes_law.
- intro c.
use make_is_z_isomorphism.
{ apply BinProduct_of_functors_commutes_invdata. }
apply BinProduct_of_functors_commutes_is_inverse.
- use make_nat_trans.
+ exact BinProduct_of_functors_commutes_data.
+ exact BinProduct_of_functors_commutes_law.
- intro c.
use make_is_z_isomorphism.
{ apply BinProduct_of_functors_commutes_invdata. }
apply BinProduct_of_functors_commutes_is_inverse.
End BinProduct_of_functors_commutative.
Section PairNatTrans.
Context {C₁ C₂ C₃ : category}
{F : C₁ ⟶ C₂}
{G₁ G₂ G₃ : C₂ ⟶ C₃}
(H : BinProducts C₃)
(η₁ : F ∙ G₁ ⟹ F ∙ G₂)
(η₂ : F ∙ G₁ ⟹ F ∙ G₃).
Local Definition pair_nat_trans_data
: nat_trans_data (F ∙ G₁) (F ∙ BinProduct_of_functors C₂ C₃ H G₂ G₃).
Show proof.
Definition pair_nat_trans_is_nat_trans
: is_nat_trans
(F ∙ G₁)
(F ∙ BinProduct_of_functors C₂ C₃ H G₂ G₃)
pair_nat_trans_data.
Show proof.
intros x y f ; cbn.
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
pose (pr2 η₁ x y f) as p.
pose (pr2 η₂ x y f) as q.
cbn in p, q.
refine (_ @ _).
{
apply maponpaths.
exact q.
}
refine (_ @ _).
{
apply maponpaths_2.
exact p.
}
unfold BinProduct_of_functors_mor, BinProductOfArrows, BinProductPr1, BinProductPr2.
exact (!(postcompWithBinProductArrow _ _ _ _ _ _ _)).
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
pose (pr2 η₁ x y f) as p.
pose (pr2 η₂ x y f) as q.
cbn in p, q.
refine (_ @ _).
{
apply maponpaths.
exact q.
}
refine (_ @ _).
{
apply maponpaths_2.
exact p.
}
unfold BinProduct_of_functors_mor, BinProductOfArrows, BinProductPr1, BinProductPr2.
exact (!(postcompWithBinProductArrow _ _ _ _ _ _ _)).
Definition pair_nat_trans
: F ∙ G₁ ⟹ F ∙ (BinProduct_of_functors _ _ H G₂ G₃).
Show proof.
End PairNatTrans.
Section BinProduct_from_iso.
Context (C : category).
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 := make_BinProduct C _ _ z
(i · (BinProductPr1 C BP))
(i · (BinProductPr2 C BP))
(iso_to_isBinProduct BP i).
End BinProduct_from_iso.
Context (C : category).
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 _ _ 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)).
- abstract (exact (iso_to_isBinProduct_comm BP i w f g)).
- abstract (intro; apply isapropdirprod; apply C).
- abstract (intros y0 T; exact (iso_to_isBinProduct_unique BP i w f g y0 T)).
use unique_exists.
- exact ((BinProductArrow C BP f g) · (iso_inv_from_iso i)).
- abstract (exact (iso_to_isBinProduct_comm BP i w f g)).
- abstract (intro; apply isapropdirprod; apply C).
- abstract (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 := make_BinProduct C _ _ z
(i · (BinProductPr1 C BP))
(i · (BinProductPr2 C BP))
(iso_to_isBinProduct BP i).
End BinProduct_from_iso.
Section EquivalentDefinition.
Context {C : category} {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) := make_dirprod (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, make_weq (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' _)
(make_dirprod f g))).
- use weqfibtototal; intro; cbn.
unfold postcomp_with_projections.
apply pathsdirprodweq.
- apply weqproperty.
apply (@iscontrweqf (hfiber (isBinProduct'_weq isBP' _)
(make_dirprod 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
Lemma terminal_binprod_unit_l_z_aux {C : category} (T : Terminal C) (BC : BinProducts C) (x : C) :
is_inverse_in_precat (BinProductPr2 C (BC T x))
(BinProductArrow C (BC T x) (TerminalArrow T x) (identity x)).
Show proof.
Lemma terminal_binprod_unit_l_z {C : category}
(T : Terminal C) (BC : BinProducts C) (x : C) :
is_z_isomorphism (BinProductPr2 C (BC T x)).
Show proof.
is_inverse_in_precat (BinProductPr2 C (BC T x))
(BinProductArrow C (BC T x) (TerminalArrow T x) (identity x)).
Show proof.
unfold is_inverse_in_precat.
split; [|apply BinProductPr2Commutes].
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
apply maponpaths_12.
- apply TerminalArrowEq.
- exact (id_right _ @ !id_left _).
split; [|apply BinProductPr2Commutes].
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
apply maponpaths_12.
- apply TerminalArrowEq.
- exact (id_right _ @ !id_left _).
Lemma terminal_binprod_unit_l_z {C : category}
(T : Terminal C) (BC : BinProducts C) (x : C) :
is_z_isomorphism (BinProductPr2 C (BC T x)).
Show proof.
Lemma terminal_binprod_unit_r_z_aux {C : category} (T : Terminal C) (BC : BinProducts C) (x : C) :
is_inverse_in_precat (BinProductPr1 C (BC x T)) (BinProductArrow C (BC x T) (identity x)
(TerminalArrow T x)).
Show proof.
Lemma terminal_binprod_unit_r_z {C : category}
(T : Terminal C) (BC : BinProducts C) (x : C) :
is_z_isomorphism (BinProductPr1 C (BC x T)).
Show proof.
Section BinProduct_of_functors_with_terminal.
Context (C D : category) (HD : BinProducts D) (TD : Terminal D) (F : functor C D).
Definition terminal_BinProduct_of_functors_unit_l_data :
nat_trans_data (BinProduct_of_functors C D HD (constant_functor C D TD) F) F.
Show proof.
Lemma terminal_BinProduct_of_functors_unit_l_law :
is_nat_trans _ _ terminal_BinProduct_of_functors_unit_l_data.
Show proof.
Definition terminal_BinProduct_of_functors_unit_l :
nat_z_iso (BinProduct_of_functors _ _ HD (constant_functor _ _ TD) F) F.
Show proof.
Definition terminal_BinProduct_of_functors_unit_r_data :
nat_trans_data (BinProduct_of_functors C D HD F (constant_functor C D TD)) F.
Show proof.
Lemma terminal_BinProduct_of_functors_unit_r_law :
is_nat_trans _ _ terminal_BinProduct_of_functors_unit_r_data.
Show proof.
Definition terminal_BinProduct_of_functors_unit_r :
nat_z_iso (BinProduct_of_functors _ _ HD F (constant_functor _ _ TD)) F.
Show proof.
End BinProduct_of_functors_with_terminal.
is_inverse_in_precat (BinProductPr1 C (BC x T)) (BinProductArrow C (BC x T) (identity x)
(TerminalArrow T x)).
Show proof.
unfold is_inverse_in_precat.
split; [|apply BinProductPr1Commutes].
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
apply maponpaths_12.
- exact (id_right _ @ !id_left _).
- apply TerminalArrowEq.
split; [|apply BinProductPr1Commutes].
refine (precompWithBinProductArrow _ _ _ _ _ @ _).
refine (_ @ !BinProductArrowEta _ _ _ _ _ (identity _)).
apply maponpaths_12.
- exact (id_right _ @ !id_left _).
- apply TerminalArrowEq.
Lemma terminal_binprod_unit_r_z {C : category}
(T : Terminal C) (BC : BinProducts C) (x : C) :
is_z_isomorphism (BinProductPr1 C (BC x T)).
Show proof.
Section BinProduct_of_functors_with_terminal.
Context (C D : category) (HD : BinProducts D) (TD : Terminal D) (F : functor C D).
Definition terminal_BinProduct_of_functors_unit_l_data :
nat_trans_data (BinProduct_of_functors C D HD (constant_functor C D TD) F) F.
Show proof.
Lemma terminal_BinProduct_of_functors_unit_l_law :
is_nat_trans _ _ terminal_BinProduct_of_functors_unit_l_data.
Show proof.
Definition terminal_BinProduct_of_functors_unit_l :
nat_z_iso (BinProduct_of_functors _ _ HD (constant_functor _ _ TD) F) F.
Show proof.
use make_nat_z_iso.
- use make_nat_trans.
+ exact terminal_BinProduct_of_functors_unit_l_data.
+ exact terminal_BinProduct_of_functors_unit_l_law.
- intro c. apply terminal_binprod_unit_l_z.
- use make_nat_trans.
+ exact terminal_BinProduct_of_functors_unit_l_data.
+ exact terminal_BinProduct_of_functors_unit_l_law.
- intro c. apply terminal_binprod_unit_l_z.
Definition terminal_BinProduct_of_functors_unit_r_data :
nat_trans_data (BinProduct_of_functors C D HD F (constant_functor C D TD)) F.
Show proof.
Lemma terminal_BinProduct_of_functors_unit_r_law :
is_nat_trans _ _ terminal_BinProduct_of_functors_unit_r_data.
Show proof.
Definition terminal_BinProduct_of_functors_unit_r :
nat_z_iso (BinProduct_of_functors _ _ HD F (constant_functor _ _ TD)) F.
Show proof.
use make_nat_z_iso.
- use make_nat_trans.
+ exact terminal_BinProduct_of_functors_unit_r_data.
+ exact terminal_BinProduct_of_functors_unit_r_law.
- intro c. apply terminal_binprod_unit_r_z.
- use make_nat_trans.
+ exact terminal_BinProduct_of_functors_unit_r_data.
+ exact terminal_BinProduct_of_functors_unit_r_law.
- intro c. apply terminal_binprod_unit_r_z.
End BinProduct_of_functors_with_terminal.
In a univalent category, the type of binary products on a given diagram
is a proposition
Definition eq_BinProduct
{C : category}
{x y : C}
(prod₁ prod₂ : BinProduct C x y)
(q : BinProductObject _ prod₁ = BinProductObject _ prod₂)
(e₁ : BinProductPr1 _ prod₁ = idtoiso q · BinProductPr1 _ prod₂)
(e₂ : BinProductPr2 _ prod₁ = idtoiso q · BinProductPr2 _ prod₂)
: prod₁ = prod₂.
Show proof.
Section IsoBinProduct.
Context {C : category}
{x y : C}
(p₁ p₂ : BinProduct C x y).
Let f : BinProductObject C p₁ --> BinProductObject C p₂
:= BinProductArrow _ _ (BinProductPr1 _ p₁) (BinProductPr2 _ p₁).
Let g : BinProductObject C p₂ --> BinProductObject C p₁
:= BinProductArrow _ _ (BinProductPr1 _ p₂) (BinProductPr2 _ p₂).
Local Lemma iso_between_BinProduct_eq
: is_inverse_in_precat f g.
Show proof.
Definition iso_between_BinProduct
: z_iso (BinProductObject C p₁) (BinProductObject C p₂).
Show proof.
End IsoBinProduct.
Definition isaprop_BinProduct
{C : category}
(HC : is_univalent C)
(x y : C)
: isaprop (BinProduct C x y).
Show proof.
{C : category}
{x y : C}
(prod₁ prod₂ : BinProduct C x y)
(q : BinProductObject _ prod₁ = BinProductObject _ prod₂)
(e₁ : BinProductPr1 _ prod₁ = idtoiso q · BinProductPr1 _ prod₂)
(e₂ : BinProductPr2 _ prod₁ = idtoiso q · BinProductPr2 _ prod₂)
: prod₁ = prod₂.
Show proof.
use subtypePath.
{
intro.
repeat (use impred ; intro).
use isapropiscontr.
}
use total2_paths_f.
- exact q.
- rewrite transportf_dirprod.
rewrite <- !idtoiso_precompose.
rewrite !idtoiso_inv.
use pathsdirprod ; cbn ; use z_iso_inv_on_right.
+ exact e₁.
+ exact e₂.
{
intro.
repeat (use impred ; intro).
use isapropiscontr.
}
use total2_paths_f.
- exact q.
- rewrite transportf_dirprod.
rewrite <- !idtoiso_precompose.
rewrite !idtoiso_inv.
use pathsdirprod ; cbn ; use z_iso_inv_on_right.
+ exact e₁.
+ exact e₂.
Section IsoBinProduct.
Context {C : category}
{x y : C}
(p₁ p₂ : BinProduct C x y).
Let f : BinProductObject C p₁ --> BinProductObject C p₂
:= BinProductArrow _ _ (BinProductPr1 _ p₁) (BinProductPr2 _ p₁).
Let g : BinProductObject C p₂ --> BinProductObject C p₁
:= BinProductArrow _ _ (BinProductPr1 _ p₂) (BinProductPr2 _ p₂).
Local Lemma iso_between_BinProduct_eq
: is_inverse_in_precat f g.
Show proof.
unfold f, g.
split.
- use BinProductArrowsEq.
+ rewrite assoc'.
rewrite !BinProductPr1Commutes.
rewrite id_left.
apply idpath.
+ rewrite assoc'.
rewrite !BinProductPr2Commutes.
rewrite id_left.
apply idpath.
- use BinProductArrowsEq.
+ rewrite assoc'.
rewrite !BinProductPr1Commutes.
rewrite id_left.
apply idpath.
+ rewrite assoc'.
rewrite !BinProductPr2Commutes.
rewrite id_left.
apply idpath.
split.
- use BinProductArrowsEq.
+ rewrite assoc'.
rewrite !BinProductPr1Commutes.
rewrite id_left.
apply idpath.
+ rewrite assoc'.
rewrite !BinProductPr2Commutes.
rewrite id_left.
apply idpath.
- use BinProductArrowsEq.
+ rewrite assoc'.
rewrite !BinProductPr1Commutes.
rewrite id_left.
apply idpath.
+ rewrite assoc'.
rewrite !BinProductPr2Commutes.
rewrite id_left.
apply idpath.
Definition iso_between_BinProduct
: z_iso (BinProductObject C p₁) (BinProductObject C p₂).
Show proof.
End IsoBinProduct.
Definition isaprop_BinProduct
{C : category}
(HC : is_univalent C)
(x y : C)
: isaprop (BinProduct C x y).
Show proof.
use invproofirrelevance.
intros p₁ p₂.
use eq_BinProduct.
- refine (isotoid _ HC _).
apply iso_between_BinProduct.
- rewrite idtoiso_isotoid ; cbn.
rewrite BinProductPr1Commutes.
apply idpath.
- rewrite idtoiso_isotoid ; cbn.
rewrite BinProductPr2Commutes.
apply idpath.
intros p₁ p₂.
use eq_BinProduct.
- refine (isotoid _ HC _).
apply iso_between_BinProduct.
- rewrite idtoiso_isotoid ; cbn.
rewrite BinProductPr1Commutes.
apply idpath.
- rewrite idtoiso_isotoid ; cbn.
rewrite BinProductPr2Commutes.
apply idpath.
Products when the projections are equal
Definition isBinProduct_eq_arrow
{C : category}
{x y z : C}
{π₁ π₁' : z --> x}
(p₁ : π₁ = π₁')
{π₂ π₂' : z --> y}
(p₂ : π₂ = π₂')
(H : isBinProduct C x y z π₁ π₂)
: isBinProduct C x y z π₁' π₂'.
Show proof.
{C : category}
{x y z : C}
{π₁ π₁' : z --> x}
(p₁ : π₁ = π₁')
{π₂ π₂' : z --> y}
(p₂ : π₂ = π₂')
(H : isBinProduct C x y z π₁ π₂)
: isBinProduct C x y z π₁' π₂'.
Show proof.
pose (P := make_BinProduct _ _ _ _ _ _ H).
use make_isBinProduct.
intros w f g.
use iscontraprop1.
- abstract
(induction p₁, p₂ ;
apply isapropifcontr ;
apply H).
- simple refine (_ ,, _ ,, _).
+ exact (BinProductArrow _ P f g).
+ abstract
(induction p₁ ;
exact (BinProductPr1Commutes _ _ _ P _ f g)).
+ abstract
(induction p₂ ;
exact (BinProductPr2Commutes _ _ _ P _ f g)).
use make_isBinProduct.
intros w f g.
use iscontraprop1.
- abstract
(induction p₁, p₂ ;
apply isapropifcontr ;
apply H).
- simple refine (_ ,, _ ,, _).
+ exact (BinProductArrow _ P f g).
+ abstract
(induction p₁ ;
exact (BinProductPr1Commutes _ _ _ P _ f g)).
+ abstract
(induction p₂ ;
exact (BinProductPr2Commutes _ _ _ P _ f g)).
Products of isos
Section BinProductOfIsos.
Context {C : category}
{a b c d : C}
(Pab : BinProduct C a b)
(Pcd : BinProduct C c d)
(f : z_iso a c)
(g : z_iso b d).
Let fg : BinProductObject _ Pab --> BinProductObject _ Pcd
:= BinProductOfArrows _ _ _ f g.
Let fg_inv : BinProductObject _ Pcd --> BinProductObject _ Pab
:= BinProductOfArrows _ _ _ (inv_from_z_iso f) (inv_from_z_iso g).
Definition binproduct_of_z_iso_inv
: is_inverse_in_precat fg fg_inv.
Show proof.
Definition binproduct_of_z_iso
: z_iso (BinProductObject _ Pab) (BinProductObject _ Pcd).
Show proof.
End BinProductOfIsos.
Section BinProduct_assoc_z_iso.
Context {C : category}
(P : BinProducts C)
(a b c : C).
Let Pbc := P b c.
Let Pa_bc := P a (BinProductObject _ Pbc).
Let Pab := P a b.
Let Pab_c := P (BinProductObject _ Pab) c.
Definition BinProduct_assoc_mor : C ⟦ BinProductObject C Pa_bc , BinProductObject C Pab_c ⟧.
Show proof.
Definition BinProduct_assoc_invmor : C ⟦ BinProductObject C Pab_c , BinProductObject C Pa_bc ⟧.
Show proof.
Lemma BinProduct_assoc_is_inverse : is_inverse_in_precat BinProduct_assoc_mor BinProduct_assoc_invmor.
Show proof.
Definition BinProduct_assoc_is_z_iso : is_z_isomorphism (BinProduct_assoc_mor).
Show proof.
Definition BinProduct_assoc : z_iso (BinProductObject C Pa_bc) (BinProductObject C Pab_c).
Show proof.
End BinProduct_assoc_z_iso.
Section BinProduct_OfArrows_assoc.
Context {C : category}
(P : BinProducts C)
{a a' b b' c c' : C}
(f : C ⟦ a', a ⟧) (g : C ⟦ b', b ⟧) (h : C ⟦ c', c ⟧).
Let Pbc := P b c.
Let Pa_bc := P a (BinProductObject _ Pbc).
Let Pab := P a b.
Let Pab_c := P (BinProductObject _ Pab) c.
Let Pbc' := P b' c'.
Let Pa_bc' := P a' (BinProductObject _ Pbc').
Let Pab' := P a' b'.
Let Pab_c' := P (BinProductObject _ Pab') c'.
Lemma BinProduct_OfArrows_assoc
: BinProductOfArrows _ Pa_bc Pa_bc' f (BinProductOfArrows _ Pbc Pbc' g h) · (BinProduct_assoc P a b c) =
(BinProduct_assoc P a' b' c') · BinProductOfArrows _ Pab_c Pab_c' (BinProductOfArrows _ Pab Pab' f g) h.
Show proof.
End BinProduct_OfArrows_assoc.
Section diagonalMap.
Context {C:category} (P : BinProducts C) (B:C).
Definition diagonalMap' : C ⟦ B, BinProductObject C (P B B) ⟧.
Show proof.
Lemma diagonalMap_isMonic : isMonic (diagonalMap').
Show proof.
Definition diagonalMap : Monic _ B (BinProductObject C (P B B)).
Show proof.
End diagonalMap.
Section ProductFunctions.
Context {C : category}
(prodC : BinProducts C).
Definition prod_swap
(x y : C)
: prodC x y --> prodC y x.
Show proof.
Definition prod_lwhisker
{x₁ x₂ : C}
(f : x₁ --> x₂)
(y : C)
: prodC x₁ y --> prodC x₂ y.
Show proof.
Definition prod_rwhisker
(x : C)
{y₁ y₂ : C}
(g : y₁ --> y₂)
: prodC x y₁ --> prodC x y₂.
Show proof.
Proposition prod_lwhisker_rwhisker
{x₁ x₂ : C}
{y₁ y₂ : C}
(f : x₁ --> x₂)
(g : y₁ --> y₂)
: prod_lwhisker f _ · prod_rwhisker _ g
=
BinProductOfArrows _ _ _ f g.
Show proof.
Proposition prod_swap_swap
(x y : C)
: prod_swap x y · prod_swap y x = identity _.
Show proof.
Proposition BinProductOfArrows_swap
{x₁ x₂ : C}
{y₁ y₂ : C}
(f : x₁ --> x₂)
(g : y₁ --> y₂)
: BinProductOfArrows C (prodC _ _) (prodC _ _) f g · prod_swap x₂ y₂
=
prod_swap x₁ y₁ · BinProductOfArrows C _ _ g f.
Show proof.
Context {C : category}
{a b c d : C}
(Pab : BinProduct C a b)
(Pcd : BinProduct C c d)
(f : z_iso a c)
(g : z_iso b d).
Let fg : BinProductObject _ Pab --> BinProductObject _ Pcd
:= BinProductOfArrows _ _ _ f g.
Let fg_inv : BinProductObject _ Pcd --> BinProductObject _ Pab
:= BinProductOfArrows _ _ _ (inv_from_z_iso f) (inv_from_z_iso g).
Definition binproduct_of_z_iso_inv
: is_inverse_in_precat fg fg_inv.
Show proof.
split ; use BinProductArrowsEq ; unfold fg, fg_inv.
- rewrite !assoc'.
rewrite BinProductOfArrowsPr1.
rewrite !assoc.
rewrite BinProductOfArrowsPr1.
rewrite !assoc'.
rewrite z_iso_inv_after_z_iso.
rewrite id_left, id_right.
apply idpath.
- rewrite !assoc'.
rewrite BinProductOfArrowsPr2.
rewrite !assoc.
rewrite BinProductOfArrowsPr2.
rewrite !assoc'.
rewrite z_iso_inv_after_z_iso.
rewrite id_left, id_right.
apply idpath.
- rewrite !assoc'.
rewrite BinProductOfArrowsPr1.
rewrite !assoc.
rewrite BinProductOfArrowsPr1.
rewrite !assoc'.
rewrite z_iso_after_z_iso_inv.
rewrite id_left, id_right.
apply idpath.
- rewrite !assoc'.
rewrite BinProductOfArrowsPr2.
rewrite !assoc.
rewrite BinProductOfArrowsPr2.
rewrite !assoc'.
rewrite z_iso_after_z_iso_inv.
rewrite id_left, id_right.
apply idpath.
- rewrite !assoc'.
rewrite BinProductOfArrowsPr1.
rewrite !assoc.
rewrite BinProductOfArrowsPr1.
rewrite !assoc'.
rewrite z_iso_inv_after_z_iso.
rewrite id_left, id_right.
apply idpath.
- rewrite !assoc'.
rewrite BinProductOfArrowsPr2.
rewrite !assoc.
rewrite BinProductOfArrowsPr2.
rewrite !assoc'.
rewrite z_iso_inv_after_z_iso.
rewrite id_left, id_right.
apply idpath.
- rewrite !assoc'.
rewrite BinProductOfArrowsPr1.
rewrite !assoc.
rewrite BinProductOfArrowsPr1.
rewrite !assoc'.
rewrite z_iso_after_z_iso_inv.
rewrite id_left, id_right.
apply idpath.
- rewrite !assoc'.
rewrite BinProductOfArrowsPr2.
rewrite !assoc.
rewrite BinProductOfArrowsPr2.
rewrite !assoc'.
rewrite z_iso_after_z_iso_inv.
rewrite id_left, id_right.
apply idpath.
Definition binproduct_of_z_iso
: z_iso (BinProductObject _ Pab) (BinProductObject _ Pcd).
Show proof.
End BinProductOfIsos.
Section BinProduct_assoc_z_iso.
Context {C : category}
(P : BinProducts C)
(a b c : C).
Let Pbc := P b c.
Let Pa_bc := P a (BinProductObject _ Pbc).
Let Pab := P a b.
Let Pab_c := P (BinProductObject _ Pab) c.
Definition BinProduct_assoc_mor : C ⟦ BinProductObject C Pa_bc , BinProductObject C Pab_c ⟧.
Show proof.
use BinProductArrow.
+ use BinProductOfArrows.
- exact (identity a).
- use BinProductPr1.
+ use (compose (b := BinProductObject C Pbc)).
- use BinProductPr2.
- use BinProductPr2.
+ use BinProductOfArrows.
- exact (identity a).
- use BinProductPr1.
+ use (compose (b := BinProductObject C Pbc)).
- use BinProductPr2.
- use BinProductPr2.
Definition BinProduct_assoc_invmor : C ⟦ BinProductObject C Pab_c , BinProductObject C Pa_bc ⟧.
Show proof.
use BinProductArrow.
+ use (compose (b := BinProductObject C Pab)).
- use BinProductPr1.
- use BinProductPr1.
+ use BinProductOfArrows.
- use BinProductPr2.
- exact (identity c).
+ use (compose (b := BinProductObject C Pab)).
- use BinProductPr1.
- use BinProductPr1.
+ use BinProductOfArrows.
- use BinProductPr2.
- exact (identity c).
Lemma BinProduct_assoc_is_inverse : is_inverse_in_precat BinProduct_assoc_mor BinProduct_assoc_invmor.
Show proof.
use make_is_inverse_in_precat.
- unfold BinProduct_assoc_mor, BinProduct_assoc_invmor.
use BinProductArrowsEq.
* now rewrite
id_left,
assoc',
BinProductPr1Commutes,
assoc,
BinProductPr1Commutes,
BinProductOfArrowsPr1,
id_right.
* now rewrite
id_left,
assoc',
BinProductPr2Commutes,
postcompWithBinProductArrow,
id_right,
BinProductOfArrowsPr2,
<-precompWithBinProductArrow,
<-(id_left (BinProductPr1 C Pbc)),
<-(id_left (BinProductPr2 C Pbc)),
<-BinProductArrowEta,
id_right.
- unfold BinProduct_assoc_mor, BinProduct_assoc_invmor.
use BinProductArrowsEq.
* now rewrite
id_left,
assoc',
BinProductPr1Commutes,
postcompWithBinProductArrow,
id_right,
BinProductOfArrowsPr1,
<-precompWithBinProductArrow,
<-(id_left (BinProductPr1 C Pab)),
<-(id_left (BinProductPr2 C Pab)),
<-BinProductArrowEta, id_right.
* now rewrite
id_left,
assoc',
BinProductPr2Commutes,
assoc,
BinProductPr2Commutes,
BinProductOfArrowsPr2,
id_right.
- unfold BinProduct_assoc_mor, BinProduct_assoc_invmor.
use BinProductArrowsEq.
* now rewrite
id_left,
assoc',
BinProductPr1Commutes,
assoc,
BinProductPr1Commutes,
BinProductOfArrowsPr1,
id_right.
* now rewrite
id_left,
assoc',
BinProductPr2Commutes,
postcompWithBinProductArrow,
id_right,
BinProductOfArrowsPr2,
<-precompWithBinProductArrow,
<-(id_left (BinProductPr1 C Pbc)),
<-(id_left (BinProductPr2 C Pbc)),
<-BinProductArrowEta,
id_right.
- unfold BinProduct_assoc_mor, BinProduct_assoc_invmor.
use BinProductArrowsEq.
* now rewrite
id_left,
assoc',
BinProductPr1Commutes,
postcompWithBinProductArrow,
id_right,
BinProductOfArrowsPr1,
<-precompWithBinProductArrow,
<-(id_left (BinProductPr1 C Pab)),
<-(id_left (BinProductPr2 C Pab)),
<-BinProductArrowEta, id_right.
* now rewrite
id_left,
assoc',
BinProductPr2Commutes,
assoc,
BinProductPr2Commutes,
BinProductOfArrowsPr2,
id_right.
Definition BinProduct_assoc_is_z_iso : is_z_isomorphism (BinProduct_assoc_mor).
Show proof.
Definition BinProduct_assoc : z_iso (BinProductObject C Pa_bc) (BinProductObject C Pab_c).
Show proof.
End BinProduct_assoc_z_iso.
Section BinProduct_OfArrows_assoc.
Context {C : category}
(P : BinProducts C)
{a a' b b' c c' : C}
(f : C ⟦ a', a ⟧) (g : C ⟦ b', b ⟧) (h : C ⟦ c', c ⟧).
Let Pbc := P b c.
Let Pa_bc := P a (BinProductObject _ Pbc).
Let Pab := P a b.
Let Pab_c := P (BinProductObject _ Pab) c.
Let Pbc' := P b' c'.
Let Pa_bc' := P a' (BinProductObject _ Pbc').
Let Pab' := P a' b'.
Let Pab_c' := P (BinProductObject _ Pab') c'.
Lemma BinProduct_OfArrows_assoc
: BinProductOfArrows _ Pa_bc Pa_bc' f (BinProductOfArrows _ Pbc Pbc' g h) · (BinProduct_assoc P a b c) =
(BinProduct_assoc P a' b' c') · BinProductOfArrows _ Pab_c Pab_c' (BinProductOfArrows _ Pab Pab' f g) h.
Show proof.
unfold BinProduct_assoc, BinProduct_assoc_mor.
simpl.
use BinProductArrowsEq.
+ rewrite !assoc', (BinProductPr1Commutes), BinProductOfArrowsPr1, assoc, BinProductPr1Commutes.
use BinProductArrowsEq.
- now rewrite !assoc',
!BinProductOfArrowsPr1,
!assoc,
!BinProductOfArrowsPr1,
id_right, !assoc', id_left.
- now rewrite !assoc',
!BinProductOfArrowsPr2,
!assoc,
!BinProductOfArrowsPr2,
!assoc',
!BinProductOfArrowsPr1.
+ now rewrite !assoc',
!BinProductOfArrowsPr2, !BinProductPr2Commutes,
!assoc,
!BinProductOfArrowsPr2, !BinProductPr2Commutes,
!assoc',
!BinProductOfArrowsPr2.
simpl.
use BinProductArrowsEq.
+ rewrite !assoc', (BinProductPr1Commutes), BinProductOfArrowsPr1, assoc, BinProductPr1Commutes.
use BinProductArrowsEq.
- now rewrite !assoc',
!BinProductOfArrowsPr1,
!assoc,
!BinProductOfArrowsPr1,
id_right, !assoc', id_left.
- now rewrite !assoc',
!BinProductOfArrowsPr2,
!assoc,
!BinProductOfArrowsPr2,
!assoc',
!BinProductOfArrowsPr1.
+ now rewrite !assoc',
!BinProductOfArrowsPr2, !BinProductPr2Commutes,
!assoc,
!BinProductOfArrowsPr2, !BinProductPr2Commutes,
!assoc',
!BinProductOfArrowsPr2.
End BinProduct_OfArrows_assoc.
Section diagonalMap.
Context {C:category} (P : BinProducts C) (B:C).
Definition diagonalMap' : C ⟦ B, BinProductObject C (P B B) ⟧.
Show proof.
Lemma diagonalMap_isMonic : isMonic (diagonalMap').
Show proof.
use make_isMonic.
intros x g h p.
assert (p' :=
(maponpaths (λ f, compose f (BinProductPr1 C (P B B))) p)).
unfold diagonalMap' in p'.
rewrite !assoc', BinProductPr1Commutes , !id_right in p'.
exact p'.
intros x g h p.
assert (p' :=
(maponpaths (λ f, compose f (BinProductPr1 C (P B B))) p)).
unfold diagonalMap' in p'.
rewrite !assoc', BinProductPr1Commutes , !id_right in p'.
exact p'.
Definition diagonalMap : Monic _ B (BinProductObject C (P B B)).
Show proof.
End diagonalMap.
Section ProductFunctions.
Context {C : category}
(prodC : BinProducts C).
Definition prod_swap
(x y : C)
: prodC x y --> prodC y x.
Show proof.
Definition prod_lwhisker
{x₁ x₂ : C}
(f : x₁ --> x₂)
(y : C)
: prodC x₁ y --> prodC x₂ y.
Show proof.
Definition prod_rwhisker
(x : C)
{y₁ y₂ : C}
(g : y₁ --> y₂)
: prodC x y₁ --> prodC x y₂.
Show proof.
Proposition prod_lwhisker_rwhisker
{x₁ x₂ : C}
{y₁ y₂ : C}
(f : x₁ --> x₂)
(g : y₁ --> y₂)
: prod_lwhisker f _ · prod_rwhisker _ g
=
BinProductOfArrows _ _ _ f g.
Show proof.
unfold prod_lwhisker, prod_rwhisker.
rewrite BinProductOfArrows_comp.
rewrite id_left, id_right.
apply idpath.
rewrite BinProductOfArrows_comp.
rewrite id_left, id_right.
apply idpath.
Proposition prod_swap_swap
(x y : C)
: prod_swap x y · prod_swap y x = identity _.
Show proof.
use BinProductArrowsEq.
- unfold prod_swap.
rewrite !assoc'.
rewrite !id_left.
rewrite BinProductPr1Commutes.
rewrite BinProductPr2Commutes.
apply idpath.
- unfold prod_swap.
rewrite !assoc'.
rewrite !id_left.
rewrite BinProductPr2Commutes.
rewrite BinProductPr1Commutes.
apply idpath.
- unfold prod_swap.
rewrite !assoc'.
rewrite !id_left.
rewrite BinProductPr1Commutes.
rewrite BinProductPr2Commutes.
apply idpath.
- unfold prod_swap.
rewrite !assoc'.
rewrite !id_left.
rewrite BinProductPr2Commutes.
rewrite BinProductPr1Commutes.
apply idpath.
Proposition BinProductOfArrows_swap
{x₁ x₂ : C}
{y₁ y₂ : C}
(f : x₁ --> x₂)
(g : y₁ --> y₂)
: BinProductOfArrows C (prodC _ _) (prodC _ _) f g · prod_swap x₂ y₂
=
prod_swap x₁ y₁ · BinProductOfArrows C _ _ g f.
Show proof.
use BinProductArrowsEq.
- unfold prod_swap.
rewrite !assoc'.
rewrite BinProductPr1Commutes.
rewrite BinProductOfArrowsPr2.
rewrite BinProductOfArrowsPr1.
rewrite !assoc.
rewrite BinProductPr1Commutes.
apply idpath.
- unfold prod_swap.
rewrite !assoc'.
rewrite BinProductPr2Commutes.
rewrite BinProductOfArrowsPr2.
rewrite BinProductOfArrowsPr1.
rewrite !assoc.
rewrite BinProductPr2Commutes.
apply idpath.
End ProductFunctions.- unfold prod_swap.
rewrite !assoc'.
rewrite BinProductPr1Commutes.
rewrite BinProductOfArrowsPr2.
rewrite BinProductOfArrowsPr1.
rewrite !assoc.
rewrite BinProductPr1Commutes.
apply idpath.
- unfold prod_swap.
rewrite !assoc'.
rewrite BinProductPr2Commutes.
rewrite BinProductOfArrowsPr2.
rewrite BinProductOfArrowsPr1.
rewrite !assoc.
rewrite BinProductPr2Commutes.
apply idpath.
Binary products are closed under iso
Definition isBinProduct_z_iso
{C : category}
{x y a₁ a₂ : C}
{p₁ : a₁ --> x}
{q₁ : a₁ --> y}
{p₂ : a₂ --> x}
{q₂ : a₂ --> y}
(H : isBinProduct C x y a₁ p₁ q₁)
(f : z_iso a₂ a₁)
(r₁ : p₂ = f · p₁)
(r₂ : q₂ = f · q₁)
: isBinProduct C x y a₂ p₂ q₂.
Show proof.
{C : category}
{x y a₁ a₂ : C}
{p₁ : a₁ --> x}
{q₁ : a₁ --> y}
{p₂ : a₂ --> x}
{q₂ : a₂ --> y}
(H : isBinProduct C x y a₁ p₁ q₁)
(f : z_iso a₂ a₁)
(r₁ : p₂ = f · p₁)
(r₂ : q₂ = f · q₁)
: isBinProduct C x y a₂ p₂ q₂.
Show proof.
intros w h₁ h₂.
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ;
use (cancel_z_iso _ _ f) ;
use (BinProductArrowsEq _ _ _ (make_BinProduct _ _ _ _ _ _ H)) ;
[ cbn ;
rewrite !assoc' ;
rewrite <- !r₁ ;
exact (pr12 φ₁ @ !(pr12 φ₂))
| cbn ;
rewrite !assoc' ;
rewrite <- !r₂ ;
exact (pr22 φ₁ @ !(pr22 φ₂)) ]).
- simple refine (_ ,, _ ,, _).
+ exact (BinProductArrow _ (make_BinProduct _ _ _ _ _ _ H) h₁ h₂ · inv_from_z_iso f).
+ abstract
(rewrite r₁ ;
rewrite !assoc' ;
rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)) ;
rewrite z_iso_after_z_iso_inv ;
rewrite id_left ;
apply BinProductPr1Commutes).
+ abstract
(cbn ;
rewrite r₂ ;
rewrite !assoc' ;
rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)) ;
rewrite z_iso_after_z_iso_inv ;
rewrite id_left ;
apply (BinProductPr2Commutes _ _ _ (make_BinProduct _ _ _ _ _ _ H))).
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ;
use (cancel_z_iso _ _ f) ;
use (BinProductArrowsEq _ _ _ (make_BinProduct _ _ _ _ _ _ H)) ;
[ cbn ;
rewrite !assoc' ;
rewrite <- !r₁ ;
exact (pr12 φ₁ @ !(pr12 φ₂))
| cbn ;
rewrite !assoc' ;
rewrite <- !r₂ ;
exact (pr22 φ₁ @ !(pr22 φ₂)) ]).
- simple refine (_ ,, _ ,, _).
+ exact (BinProductArrow _ (make_BinProduct _ _ _ _ _ _ H) h₁ h₂ · inv_from_z_iso f).
+ abstract
(rewrite r₁ ;
rewrite !assoc' ;
rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)) ;
rewrite z_iso_after_z_iso_inv ;
rewrite id_left ;
apply BinProductPr1Commutes).
+ abstract
(cbn ;
rewrite r₂ ;
rewrite !assoc' ;
rewrite (maponpaths (λ z, _ · z) (assoc _ _ _)) ;
rewrite z_iso_after_z_iso_inv ;
rewrite id_left ;
apply (BinProductPr2Commutes _ _ _ (make_BinProduct _ _ _ _ _ _ H))).