Library Modules.Prelims.CoproductsComplements
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.ProductCategory.
Require Import UniMath.CategoryTheory.limits.coproducts.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.EpiFacts.
Open Scope cat.
Definition Coproducts_Unit {D : category} : Coproducts unit D .
intro f.
use mk_Coproduct.
- exact (f tt).
- induction i.
exact (identity _).
- intros c g.
use unique_exists.
+ exact (g tt).
+ cbn.
induction i.
apply id_left.
+ intro.
apply impred_isaprop.
intro.
apply homset_property.
+ cbn.
intros u hu.
etrans;[|apply hu].
apply pathsinv0.
apply id_left.
Defined.
Section WEQ.
Context {C : category} {I : UU} (cpC : Coproducts I C).
Variable (a : I -> C).
Definition from_Coproducts_weq c : (∏ i, C ⟦ a i , c ⟧) ≃ C ⟦ CoproductObject _ _ (cpC a) , c ⟧.
use weqpair.
- intro f.
apply CoproductArrow.
exact f.
- intro y.
unfold hfiber.
use unique_exists.
+ intro i.
eapply compose.
* apply CoproductIn.
* exact y.
+ cbn.
apply pathsinv0.
apply CoproductArrowEta.
+ intros h.
apply (homset_property C).
+ cbn.
intro y'.
intro h.
apply funextsec.
intro i.
etrans;[|apply cancel_precomposition;exact h].
apply pathsinv0.
apply CoproductInCommutes.
Defined.
End WEQ.
inspired by bincoproducts.v
Section coproduct_unique.
Context {C : category} {I : UU} (a : I -> C).
Definition from_Coproduct_to_Coproduct (CC CC' : Coproduct I C a)
: CoproductObject _ _ CC --> CoproductObject _ _ CC' :=
CoproductArrow I C CC (CoproductIn I C CC').
Lemma is_iso_from_Coproduct_to_Coproduct (CC CC' : Coproduct I C a)
: is_iso (from_Coproduct_to_Coproduct CC CC').
Proof.
apply is_iso_from_is_z_iso.
exists (from_Coproduct_to_Coproduct CC' CC).
split; simpl.
- apply pathsinv0.
apply Coproduct_endo_is_identity.
intro i.
rewrite assoc. unfold from_Coproduct_to_Coproduct.
rewrite CoproductInCommutes.
rewrite CoproductInCommutes.
apply idpath.
- apply pathsinv0.
apply Coproduct_endo_is_identity.
intro i.
rewrite assoc; unfold from_Coproduct_to_Coproduct.
repeat rewrite CoproductInCommutes; apply idpath.
Defined.
Definition iso_from_Coproduct_to_Coproduct (CC CC' : Coproduct I C a)
: iso (CoproductObject _ _ CC) (CoproductObject _ _ CC')
:= isopair _ (is_iso_from_Coproduct_to_Coproduct CC CC').
End coproduct_unique.
Section CoprodSigma.
Local Notation CPO := (CoproductObject _ _).
Context {C : category} {O : UU} {A : O -> UU}.
Context {B : ∏ (o : O) (a : A o), C} .
Let BS := (fun z => B _ (pr2 z)).
Context (cpF : Coproduct (∑ (o : O), A o) _ BS).
Context (cp1 : ∏ (o : O), Coproduct (A o) _ (B _)).
Context (cp2 : Coproduct O _ (fun o => (CPO (cp1 o)))).
Definition sigma_coprod_In o : C ⟦ BS o , CPO cp2 ⟧ :=
CoproductIn _ C (cp1 (pr1 o)) (pr2 o) · CoproductIn O C cp2 (pr1 o).
Context {C : category} {I : UU} (a : I -> C).
Definition from_Coproduct_to_Coproduct (CC CC' : Coproduct I C a)
: CoproductObject _ _ CC --> CoproductObject _ _ CC' :=
CoproductArrow I C CC (CoproductIn I C CC').
Lemma is_iso_from_Coproduct_to_Coproduct (CC CC' : Coproduct I C a)
: is_iso (from_Coproduct_to_Coproduct CC CC').
Proof.
apply is_iso_from_is_z_iso.
exists (from_Coproduct_to_Coproduct CC' CC).
split; simpl.
- apply pathsinv0.
apply Coproduct_endo_is_identity.
intro i.
rewrite assoc. unfold from_Coproduct_to_Coproduct.
rewrite CoproductInCommutes.
rewrite CoproductInCommutes.
apply idpath.
- apply pathsinv0.
apply Coproduct_endo_is_identity.
intro i.
rewrite assoc; unfold from_Coproduct_to_Coproduct.
repeat rewrite CoproductInCommutes; apply idpath.
Defined.
Definition iso_from_Coproduct_to_Coproduct (CC CC' : Coproduct I C a)
: iso (CoproductObject _ _ CC) (CoproductObject _ _ CC')
:= isopair _ (is_iso_from_Coproduct_to_Coproduct CC CC').
End coproduct_unique.
Section CoprodSigma.
Local Notation CPO := (CoproductObject _ _).
Context {C : category} {O : UU} {A : O -> UU}.
Context {B : ∏ (o : O) (a : A o), C} .
Let BS := (fun z => B _ (pr2 z)).
Context (cpF : Coproduct (∑ (o : O), A o) _ BS).
Context (cp1 : ∏ (o : O), Coproduct (A o) _ (B _)).
Context (cp2 : Coproduct O _ (fun o => (CPO (cp1 o)))).
Definition sigma_coprod_In o : C ⟦ BS o , CPO cp2 ⟧ :=
CoproductIn _ C (cp1 (pr1 o)) (pr2 o) · CoproductIn O C cp2 (pr1 o).
Is it possible to define it without using the homset property ?
Definition sigma_coprod_isCoproduct : isCoproduct _ _ _ _ sigma_coprod_In.
intros c f.
use unique_exists.
- apply CoproductArrow.
intro o.
apply CoproductArrow.
intro i.
apply (f (o ,, i)).
- abstract(intro i;
unfold sigma_coprod_In;
etrans;
[
rewrite <- assoc;
apply cancel_precomposition;
apply (CoproductInCommutes _ _ _ cp2)
|];
etrans;
[
set (CC := cp1 _);
apply (CoproductInCommutes _ _ _ CC)
|];
now induction i).
- intros t.
cbn -[isaprop].
apply impred_isaprop.
intro z.
apply (homset_property C).
- cbn.
intros g hg.
apply CoproductArrowUnique.
intro o.
apply CoproductArrowUnique.
intro i.
etrans;[| exact (hg (o ,, i))].
apply assoc.
Defined.
Definition sigma_Coproduct := mk_Coproduct _ _ _ _ _ sigma_coprod_isCoproduct.
Definition sigma_coprod_iso : iso (CoproductObject _ _ cpF) (CoproductObject _ _ cp2) :=
iso_from_Coproduct_to_Coproduct _ cpF sigma_Coproduct.
End CoprodSigma.
Section CoprodEpis.
Context {C : category} {I : UU} {a b : I -> C}
(cpa : Coproduct _ _ a)
(cpb : Coproduct _ _ b).
Context {ff : ∏ i, C ⟦ a i, b i ⟧} (epif : ∏ i, isEpi (ff i)).
Lemma CoproductOfArrows_isEpi : isEpi (CoproductOfArrows _ _ cpa cpb ff).
Proof.
intros x f g.
intro hfg.
rewrite (CoproductArrowEta _ _ _ _ _ f).
rewrite (CoproductArrowEta _ _ _ _ _ g).
apply maponpaths.
apply funextsec.
intro i.
apply (cancel_precomposition _ _ _ _ _ _ (CoproductIn I C cpa i)) in hfg.
do 2 rewrite assoc in hfg.
rewrite CoproductOfArrowsIn in hfg.
do 2 rewrite <- assoc in hfg.
now use epif.
Qed.
End CoprodEpis.
Section CoprodBinprod.
Local Notation BPO := (BinProductObject _).
Local Notation CPO := (CoproductObject _ _).
Context {C : precategory} {O : UU} .
Context {B : ∏ (o : O) , C} (cpB : Coproduct O _ B).
Context {X : C} (bpBX : ∏ o, BinProduct _ (B o) X)
(bpCX : BinProduct _ (CPO cpB) X)
(cpBX : Coproduct O _ (fun o => BPO (bpBX o))).
Definition bp_coprod_In o : C ⟦ BPO (bpBX o) , BPO bpCX ⟧ :=
BinProductOfArrows C bpCX (bpBX o) (CoproductIn O C cpB o) (identity X).
Definition bp_coprod_mor : C ⟦ CPO (cpBX) , BPO bpCX ⟧ :=
CoproductArrow _ _ _ bp_coprod_In.
End CoprodBinprod.
Definition bp_coprod_isDistributive {C : precategory} {I : UU}
(bp : BinProducts C) (cp : Coproducts I C)
: UU :=
∏ B X, is_iso (bp_coprod_mor (cp B) (fun o => bp _ X) (bp _ _) (cp _) ).
Definition iso_from_isDistributive {C : precategory} {I : UU}
(bp : BinProducts C) (cp : Coproducts I C)
(h : bp_coprod_isDistributive bp cp) B X :
iso _ _ :=
isopair (bp_coprod_mor (cp B) (fun o => bp _ X) (bp _ _) (cp _) )
(h B X).
Section CoprodPwIso.
Local Notation CPO := (CoproductObject _ _).
Context {C : category} {O : UU} .
Context {B B' : ∏ (o : O) , C} (cpB : Coproduct O _ B)(cpB' : Coproduct O _ B')
(pwiso : ∏ o, iso (B o) (B' o)).
Definition coprod_pw_iso_isCoproduct : isCoproduct O _ B (CPO cpB')
(fun i =>
(pwiso i)· (CoproductIn _ _ cpB' i)) .
Proof.
intros c f.
use unique_exists.
- apply CoproductArrow.
intro o.
eapply compose.
+ exact (inv_from_iso (pwiso o)).
+ exact (f o).
- cbn.
intro i.
etrans.
etrans;[eapply pathsinv0;apply assoc|].
apply cancel_precomposition.
apply CoproductInCommutes.
etrans;[apply assoc|].
rewrite iso_inv_after_iso.
apply id_left.
- intro y.
apply impred_isaprop.
intro t.
apply (homset_property C).
- cbn.
intros y h.
apply CoproductArrowUnique.
intro i.
rewrite <- h.
do 2 rewrite assoc.
rewrite iso_after_iso_inv.
apply cancel_postcomposition.
apply pathsinv0.
apply id_left.
Defined.
Let cpB'2 := mk_Coproduct _ _ _ _ _ coprod_pw_iso_isCoproduct.
Definition coprod_pw_iso : iso (CPO cpB) (CPO cpB') :=
(iso_from_Coproduct_to_Coproduct _ cpB cpB'2).
End CoprodPwIso.
intros c f.
use unique_exists.
- apply CoproductArrow.
intro o.
apply CoproductArrow.
intro i.
apply (f (o ,, i)).
- abstract(intro i;
unfold sigma_coprod_In;
etrans;
[
rewrite <- assoc;
apply cancel_precomposition;
apply (CoproductInCommutes _ _ _ cp2)
|];
etrans;
[
set (CC := cp1 _);
apply (CoproductInCommutes _ _ _ CC)
|];
now induction i).
- intros t.
cbn -[isaprop].
apply impred_isaprop.
intro z.
apply (homset_property C).
- cbn.
intros g hg.
apply CoproductArrowUnique.
intro o.
apply CoproductArrowUnique.
intro i.
etrans;[| exact (hg (o ,, i))].
apply assoc.
Defined.
Definition sigma_Coproduct := mk_Coproduct _ _ _ _ _ sigma_coprod_isCoproduct.
Definition sigma_coprod_iso : iso (CoproductObject _ _ cpF) (CoproductObject _ _ cp2) :=
iso_from_Coproduct_to_Coproduct _ cpF sigma_Coproduct.
End CoprodSigma.
Section CoprodEpis.
Context {C : category} {I : UU} {a b : I -> C}
(cpa : Coproduct _ _ a)
(cpb : Coproduct _ _ b).
Context {ff : ∏ i, C ⟦ a i, b i ⟧} (epif : ∏ i, isEpi (ff i)).
Lemma CoproductOfArrows_isEpi : isEpi (CoproductOfArrows _ _ cpa cpb ff).
Proof.
intros x f g.
intro hfg.
rewrite (CoproductArrowEta _ _ _ _ _ f).
rewrite (CoproductArrowEta _ _ _ _ _ g).
apply maponpaths.
apply funextsec.
intro i.
apply (cancel_precomposition _ _ _ _ _ _ (CoproductIn I C cpa i)) in hfg.
do 2 rewrite assoc in hfg.
rewrite CoproductOfArrowsIn in hfg.
do 2 rewrite <- assoc in hfg.
now use epif.
Qed.
End CoprodEpis.
Section CoprodBinprod.
Local Notation BPO := (BinProductObject _).
Local Notation CPO := (CoproductObject _ _).
Context {C : precategory} {O : UU} .
Context {B : ∏ (o : O) , C} (cpB : Coproduct O _ B).
Context {X : C} (bpBX : ∏ o, BinProduct _ (B o) X)
(bpCX : BinProduct _ (CPO cpB) X)
(cpBX : Coproduct O _ (fun o => BPO (bpBX o))).
Definition bp_coprod_In o : C ⟦ BPO (bpBX o) , BPO bpCX ⟧ :=
BinProductOfArrows C bpCX (bpBX o) (CoproductIn O C cpB o) (identity X).
Definition bp_coprod_mor : C ⟦ CPO (cpBX) , BPO bpCX ⟧ :=
CoproductArrow _ _ _ bp_coprod_In.
End CoprodBinprod.
Definition bp_coprod_isDistributive {C : precategory} {I : UU}
(bp : BinProducts C) (cp : Coproducts I C)
: UU :=
∏ B X, is_iso (bp_coprod_mor (cp B) (fun o => bp _ X) (bp _ _) (cp _) ).
Definition iso_from_isDistributive {C : precategory} {I : UU}
(bp : BinProducts C) (cp : Coproducts I C)
(h : bp_coprod_isDistributive bp cp) B X :
iso _ _ :=
isopair (bp_coprod_mor (cp B) (fun o => bp _ X) (bp _ _) (cp _) )
(h B X).
Section CoprodPwIso.
Local Notation CPO := (CoproductObject _ _).
Context {C : category} {O : UU} .
Context {B B' : ∏ (o : O) , C} (cpB : Coproduct O _ B)(cpB' : Coproduct O _ B')
(pwiso : ∏ o, iso (B o) (B' o)).
Definition coprod_pw_iso_isCoproduct : isCoproduct O _ B (CPO cpB')
(fun i =>
(pwiso i)· (CoproductIn _ _ cpB' i)) .
Proof.
intros c f.
use unique_exists.
- apply CoproductArrow.
intro o.
eapply compose.
+ exact (inv_from_iso (pwiso o)).
+ exact (f o).
- cbn.
intro i.
etrans.
etrans;[eapply pathsinv0;apply assoc|].
apply cancel_precomposition.
apply CoproductInCommutes.
etrans;[apply assoc|].
rewrite iso_inv_after_iso.
apply id_left.
- intro y.
apply impred_isaprop.
intro t.
apply (homset_property C).
- cbn.
intros y h.
apply CoproductArrowUnique.
intro i.
rewrite <- h.
do 2 rewrite assoc.
rewrite iso_after_iso_inv.
apply cancel_postcomposition.
apply pathsinv0.
apply id_left.
Defined.
Let cpB'2 := mk_Coproduct _ _ _ _ _ coprod_pw_iso_isCoproduct.
Definition coprod_pw_iso : iso (CPO cpB) (CPO cpB') :=
(iso_from_Coproduct_to_Coproduct _ cpB cpB'2).
End CoprodPwIso.