diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v index 3edd6877a43..9d4f3eab82d 100644 --- a/theories/Algebra/AbGroups/AbHom.v +++ b/theories/Algebra/AbGroups/AbHom.v @@ -1,6 +1,8 @@ Require Import Basics Types. Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse. Require Import AbelianGroup Biproduct. +Require Import Algebra.Groups.Group. +Require Import Algebra.Homological.Additive. (** * Homomorphisms from a group to an abelian group form an abelian group. *) @@ -117,3 +119,27 @@ Proof. rapply (conn_map_elim (Tr (-1)) f). exact (equiv_path_grouphomomorphism^-1 p). Defined. + +(** ** Additivity of AbGroup *) + +(** The group operation that is induced from the semiadditive structure agrees with the handcrafted operation on hom at the level of the underlying functions. *) +Definition ab_homo_add_is_semiadditive_add `{Funext} + {A B : AbGroup} (f g : A $-> B) + : ab_homo_add f g = sgop_hom A B f g :> (A -> B) + := 1. + +(** AbGroup is an additive category. *) +Global Instance additive_ab `{Funext} : IsAdditive AbGroup. +Proof. + snrapply Build_IsAdditive. + - exact _. + - exact _. + - intros A B f. + snrapply equiv_path_grouphomomorphism. + intros x. + exact (left_inverse (f x)). + - intros A B f. + snrapply equiv_path_grouphomomorphism. + intros x. + exact (right_inverse (f x)). +Defined. diff --git a/theories/Algebra/AbGroups/Biproduct.v b/theories/Algebra/AbGroups/Biproduct.v index 536f2785df8..a42bf877445 100644 --- a/theories/Algebra/AbGroups/Biproduct.v +++ b/theories/Algebra/AbGroups/Biproduct.v @@ -3,6 +3,8 @@ Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse. +Require Import Algebra.Homological.Biproducts. +Require Import Algebra.Homological.Additive. Local Open Scope mc_add_scope. @@ -313,3 +315,30 @@ Proof. refine (abgroup_commutative _ _ _ @ _). exact (ap (fun a => a + snd x) (abgroup_commutative _ _ _)). Defined. + +(** ** AbGroup has binary biproducts *) + +Global Instance hasbinarybiproducts_ab : HasBinaryBiproducts AbGroup. +Proof. + intros A B. + snrapply Build_BinaryBiproduct. + - exact (ab_biprod A B). + - exact ab_biprod_pr1. + - exact ab_biprod_pr2. + - exact (fun _ => ab_biprod_corec). + - exact (fun _ f _ => Id f). + - exact (fun _ _ g => Id g). + - exact (fun _ _ _ p q a => path_prod' (p a) (q a)). + - exact ab_biprod_inl. + - exact ab_biprod_inr. + - exact (fun _ => ab_biprod_rec). + - exact (fun _ => ab_biprod_rec_inl_beta). + - exact (fun _ => ab_biprod_rec_inr_beta). + - exact (fun _ => ab_biprod_corec_eta'). + - cbn; reflexivity. + - cbn; reflexivity. + - cbn; reflexivity. + - cbn; reflexivity. +Defined. + +Global Instance issemiadditive_ab `{Funext} : IsSemiAdditive AbGroup := {}. diff --git a/theories/Algebra/Categorical/MonoidObject.v b/theories/Algebra/Categorical/MonoidObject.v index 65dcbb15283..56ff2d163d2 100644 --- a/theories/Algebra/Categorical/MonoidObject.v +++ b/theories/Algebra/Categorical/MonoidObject.v @@ -98,7 +98,7 @@ Section ComonoidObject. (** Coassociativity *) Definition co_coassoc {x : A} `{!IsComonoidObject x} : associator x x x $o fmap01 tensor x co_comult $o co_comult - $== fmap10 tensor co_comult x $o co_comult. + $== fmap10 tensor co_comult x $o co_comult. Proof. refine (cat_assoc _ _ _ $@ _). apply cate_moveR_Me. @@ -146,11 +146,12 @@ Section ComonoidObject. - exact cco_cocomm. Defined. - Global Instance co_cco {x : A} `{!IsCocommutativeComonoidObject x} + Definition co_cco {x : A} `{!IsCocommutativeComonoidObject x} : IsComonoidObject x. Proof. apply cmo_mo. Defined. + Hint Immediate co_cco : typeclass_instances. (** Cocommutativity *) Definition cco_cocomm {x : A} `{!IsCocommutativeComonoidObject x} @@ -200,7 +201,7 @@ Defined. (** ** Monoid enrichment *) -(** A hom [x $-> y] in a cartesian category where [y] is a monoid object has the structure of a monoid. Equivalently, a hom [x $-> y] in a cartesian category where [x] is a comonoid object has the structure of a monoid. *) +(** A hom [x $-> y] in a cartesian category where [y] is a monoid object has the structure of a monoid. *) Section MonoidEnriched. Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A} @@ -210,28 +211,29 @@ Section MonoidEnriched. Section Monoid. Context `{!IsMonoidObject _ _ y}. - Local Instance sgop_hom : SgOp (x $-> y) + Local Instance sgop_hom_mo : SgOp (x $-> y) := fun f g => mo_mult $o cat_binprod_corec f g. - Local Instance monunit_hom : MonUnit (x $-> y) := mo_unit $o mor_terminal _ _. + Local Instance monunit_hom_mo : MonUnit (x $-> y) + := mo_unit $o mor_terminal _ _. - Local Instance associative_hom : Associative sgop_hom. + Local Instance associative_hom_mo : Associative sgop_hom_mo. Proof. intros f g h. - unfold sgop_hom. + unfold sgop_hom_mo. rapply path_hom. refine ((_ $@L cat_binprod_fmap01_corec _ _ _)^$ $@ _). nrefine (cat_assoc_opp _ _ _ $@ _). - refine ((mo_assoc $@R _)^$ $@ _). nrefine (_ $@ (_ $@L cat_binprod_fmap10_corec _ _ _)). + refine ((mo_assoc $@R _)^$ $@ _). refine (cat_assoc _ _ _ $@ (_ $@L _) $@ cat_assoc _ _ _). nrapply cat_binprod_associator_corec. Defined. - Local Instance leftidentity_hom : LeftIdentity sgop_hom mon_unit. + Local Instance leftidentity_hom_mo : LeftIdentity sgop_hom_mo mon_unit. Proof. intros f. - unfold sgop_hom, mon_unit. + unfold sgop_hom_mo, mon_unit. rapply path_hom. refine ((_ $@L (cat_binprod_fmap10_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _). nrefine (((mo_left_unit $@ _) $@R _) $@ _). @@ -243,29 +245,30 @@ Section MonoidEnriched. nrapply cat_binprod_beta_pr2. Defined. - Local Instance rightidentity_hom : RightIdentity sgop_hom mon_unit. + Local Instance rightidentity_hom_mo : RightIdentity sgop_hom_mo mon_unit. Proof. intros f. - unfold sgop_hom, mon_unit. + unfold sgop_hom_mo, mon_unit. rapply path_hom. - refine ((_ $@L (cat_binprod_fmap01_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _). + refine ((_ $@L (cat_binprod_fmap01_corec _ _ _)^$) + $@ cat_assoc_opp _ _ _ $@ _). nrefine (((mo_right_unit $@ _) $@R _) $@ _). 1: nrapply cate_buildequiv_fun. nrapply cat_binprod_beta_pr1. Defined. - Local Instance issemigroup_hom : IsSemiGroup (x $-> y) := {}. - Local Instance ismonoid_hom : IsMonoid (x $-> y) := {}. + Local Instance issemigroup_hom_mo : IsSemiGroup (x $-> y) := {}. + Local Instance ismonoid_hom_mo : IsMonoid (x $-> y) := {}. End Monoid. Context `{!IsCommutativeMonoidObject _ _ y}. - Local Existing Instances sgop_hom monunit_hom ismonoid_hom. + Local Existing Instances sgop_hom_mo monunit_hom_mo ismonoid_hom_mo. - Local Instance commutative_hom : Commutative sgop_hom. + Local Instance commutative_hom : Commutative sgop_hom_mo. Proof. intros f g. - unfold sgop_hom. + unfold sgop_hom_mo. rapply path_hom. refine ((_ $@L _^$) $@ cat_assoc_opp _ _ _ $@ (cmo_comm $@R _)). nrapply cat_binprod_swap_corec. diff --git a/theories/Algebra/Homological/Abelian.v b/theories/Algebra/Homological/Abelian.v new file mode 100644 index 00000000000..6ba9ae0fd67 --- /dev/null +++ b/theories/Algebra/Homological/Abelian.v @@ -0,0 +1,143 @@ +Require Import Basics.Overture Basics.Tactics Basics.Equivalences. +Require Import WildCat.Core WildCat.Equiv WildCat.PointedCat WildCat.Opposite. +Require Import Algebra.AbGroups.AbelianGroup Algebra.Rings.Ring. +Require Import Algebra.Homological.Additive. +Require Import canonical_names. + +(** * Abelian Categories *) + +Local Open Scope mc_scope. +Local Open Scope mc_add_scope. + +(** ** Kernels and cokernels *) + +(** *** Kernels *) + +Class Kernel {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b) := { + cat_ker_obj : A; + cat_ker : cat_ker_obj $-> a; + + cat_ker_zero : f $o cat_ker $== zero_morphism; + + cat_ker_corec {x} (g : x $-> a) : f $o g $== zero_morphism -> x $-> cat_ker_obj; + + cat_ker_corec_beta {x} (g : x $-> a) (p : f $o g $== zero_morphism) + : cat_ker $o cat_ker_corec g p $== g; + + monic_cat_ker : Monic cat_ker; +}. + +Arguments cat_ker_obj {A _ _ _ _ _ a b} f {_}. +Arguments cat_ker_corec {A _ _ _ _ _ a b f _ x} g p. +Arguments cat_ker {A _ _ _ _ _ a b} f {_}. +Arguments cat_ker_zero {A _ _ _ _ _ a b} f {_}. +Arguments monic_cat_ker {A _ _ _ _ _ a b} f {_}. + +(** Kernels of monomorphisms are zero. *) +Definition ker_zero_monic {A : Type} `{IsPointedCat A} + {a b : A} (f : a $-> b) `{!Kernel f} + : Monic f -> cat_ker f $== zero_morphism. +Proof. + intros monic. + nrapply monic. + refine (cat_ker_zero f $@ _^$). + apply cat_zero_r. +Defined. + +(** Maps with zero kernel are monic. *) +Definition monic_ker_zero {A : Type} `{IsAdditive A} + {a b : A} (f : a $-> b) `{!Kernel f} + : cat_ker f $== zero_morphism -> Monic f. +Proof. + intros ker_zero c g h p. + nrapply GpdHom_path. + apply path_hom in p. + change (@paths (AbHom c a) g h). + change (@paths (AbHom c b) (f $o g) (f $o h)) in p. + apply grp_moveL_1M. + apply grp_moveL_1M in p. + apply GpdHom_path in p. + apply path_hom. + refine ((cat_ker_corec_beta (g + (-h)) _)^$ $@ (ker_zero $@R _) $@ cat_zero_l _). + refine (addcat_dist_l _ _ _ $@ _ $@ p). + apply GpdHom_path. + f_ap. + apply path_hom. + symmetry. + nrapply addcat_comp_negate_r. +Defined. + +(** *** Cokernels *) + +Class Cokernel {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b) + := cokernel_kernel_op :: Kernel (A := A^op) (f : Hom (A:= A^op) b a). + +Arguments Cokernel {A _ _ _ _ _ a b} f. + +Definition cat_coker_obj {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b) + `{!Cokernel f} : A + := cat_ker_obj (A:=A^op) (a:=b) f. + +Definition cat_coker {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b) + `{!Cokernel f} : b $-> cat_coker_obj f + := cat_ker (A:=A^op) (a:=b) (b:=a) f. + +Definition cat_coker_zero {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b) + `{!Cokernel f} : cat_coker f $o f $== zero_morphism + := cat_ker_zero (A:=A^op) (a:=b) f. + +Definition cat_coker_rec {A : Type} `{IsPointedCat A} {a b : A} {f : a $-> b} + `{!Cokernel f} {x} (g : b $-> x) + : g $o f $== zero_morphism -> cat_coker_obj f $-> x + := cat_ker_corec (A:=A^op) (a:=b) (b:=a) g. + +Definition cat_coker_rec_beta {A : Type} `{IsPointedCat A} {a b : A} (f : a $-> b) + `{!Cokernel f} {x} (g : b $-> x) (p : g $o f $== zero_morphism) + : cat_coker_rec g p $o cat_coker f $== g + := cat_ker_corec_beta (A:=A^op) (a:=b) (b:=a) g p. + +Definition epic_cat_coker {A : Type} `{IsPointedCat A} + {a b : A} (f : a $-> b) `{!Cokernel f} + : Epic (cat_coker f) + := monic_cat_ker (A:=A^op) (a:=b) (b:=a) f. + +Definition coker_zero_epic {A : Type} `{IsPointedCat A} + {a b : A} (f : a $-> b) `{!Cokernel f} + : Epic f -> cat_coker f $== zero_morphism + := ker_zero_monic (A:=A^op) (a:=b) f. + +Definition epic_coker_zero {A : Type} `{IsAdditive A} + {a b : A} (f : a $-> b) {k : Cokernel f} + : cat_coker f $== zero_morphism -> Epic f + := monic_ker_zero (A:=A^op) (a:=b) (b:=a) f. + +(** ** Preabelian categories *) + +Class IsPreAbelian {A : Type} `{IsAdditive A} := { + preabelian_has_kernels :: forall {a b : A} (f : a $-> b), Kernel f; + preabelian_has_cokernels :: forall {a b : A} (f : a $-> b), Cokernel f; +}. + +Definition cat_coker_ker_ker_coker {A : Type} `{IsPreAbelian A} + {a b : A} (f : a $-> b) + : cat_coker_obj (cat_ker f) $-> cat_ker_obj (cat_coker f). +Proof. + snrapply cat_coker_rec. + - snrapply cat_ker_corec. + + exact f. + + nrapply cat_coker_zero. + - snrapply monic_cat_ker. + refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: nrapply cat_ker_corec_beta. + refine (_ $@ (cat_zero_r _)^$). + nrapply cat_ker_zero. +Defined. + +(** ** Abelian categories *) + +Class IsAbelian {A : Type} `{IsPreAbelian A} := { + catie_preabelian_canonical_map : forall a b (f : a $-> b), + CatIsEquiv (cat_coker_ker_ker_coker f); +}. + diff --git a/theories/Algebra/Homological/Additive.v b/theories/Algebra/Homological/Additive.v new file mode 100644 index 00000000000..e55b43391dd --- /dev/null +++ b/theories/Algebra/Homological/Additive.v @@ -0,0 +1,517 @@ +Require Import Basics.Overture. +Require Import WildCat.Core WildCat.Equiv WildCat.PointedCat WildCat.Bifunctor. +Require Import WildCat.Square WildCat.Opposite WildCat.Monoidal NatTrans WildCat.Products WildCat.Coproducts. +Require Import Algebra.Homological.Biproducts. +Require Import Algebra.Groups.Group. +Require Import Algebra.AbGroups.AbelianGroup. +Require Import canonical_names. +Require Import MonoidObject. + +(** * Semiadditive and Additive Categories *) + + +(** ** Semiadditive Categories *) + +(** As semiadditive category is a wild category with equivalences and the following data: *) +Class IsSemiAdditive (A : Type) `{HasEquivs A} := { + (** It is a pointed category. *) + semiadditive_pointed :: IsPointedCat A; + (** It has binary biproducts. *) + semiadditive_hasbiproducts :: HasBinaryBiproducts A; + (** We have morphism extensionality. *) + semiadditive_hasmorext :: HasMorExt A; + (** The homs are sets. *) + semiadditive_ishset_hom :: forall (a b : A), IsHSet (a $-> b); +}. + +(** The final two conditions in the definition of a semiadditive category ensure that the hom types can become commutative monoids. This is an essential characteristic of semiadditive categories making it equivalent to alternate definitions where the category is semiadditive if it is enriched in commutative monoids. The machinery of encriched categories however is a bit heavy so we use this more lightweight definition where the commutative monoid structure appears naturally. *) + +Local Existing Instance issymmetricmonoidal_cat_binbiprod. + +Global Instance iscocommutativecomonoidobject_semiadditive + {A : Type} `{IsSemiAdditive A} (x : A) + : IsCocommutativeComonoidObject (fun x y => cat_binprod x y) zero_object x. +Proof. + snrapply Build_IsCocommutativeComonoidObject. + { snrapply Build_IsComonoidObject. + - exact (cat_binbiprod_diag x). + - exact zero_morphism. + - refine (_ $@ (cat_binbiprod_fmap10_corec _ _ _)^$). + nrefine (cat_assoc _ _ _ $@ (_ $@L cat_binbiprod_fmap01_corec _ _ _) $@ _). + refine ((_ $@L (cat_binbiprod_corec_eta' (Id _) (cat_idr _))) $@ _ + $@ cat_binbiprod_corec_eta' (cat_idr _)^$ (Id _)). + nrapply Products.cat_binprod_associator_corec. + - refine (cat_assoc _ _ _ $@ (_ $@L cat_binbiprod_fmap10_corec _ _ _) $@ _). + nrefine ((cate_buildequiv_fun _ $@R _) $@ _). + unfold trans_nattrans. + nrefine (cat_assoc _ _ _ $@ (_ $@L cat_binprod_swap_corec _ _) $@ _). + nrefine ((cate_buildequiv_fun _ $@R _) $@ _). + nrapply cat_binbiprod_corec_beta_pr1. + - refine (cat_assoc _ _ _ $@ (_ $@L cat_binbiprod_fmap01_corec _ _ _) $@ _). + nrefine ((cate_buildequiv_fun _ $@R _) $@ _). + nrapply cat_binbiprod_corec_beta_pr1. } + rapply cat_binprod_swap_corec. +Defined. + +Section CMonHom. + + Context {A : Type} `{IsSemiAdditive A} (a b : A). + + (** We can show that the hom-types of a semiadditive category are commutative monoids. *) + + Local Instance zero_hom : Zero (a $-> b). + Proof. + snrapply MonoidObject.monunit_hom_co. + 1-5: exact _. + 1: exact zero_object. + 1: exact _. + (* Set Printing All. *) + (* Check ( cco_co (iscocommutativecomonoidobject_semiadditive a)). *) + unfold cat_bincoprod. + snrefine (transport (fun x => @IsComonoidObject _ _ _ _ _ _ _ _ _ x _ _ _ a) _ _). + 3:{ + (* TODO: we need to redefine biproducts so that the coproduct strucutre is emergent from the birpoduct structure rather than being part of the structure. Hopefully this is enough for the following term to be accepted. *) + pose (i := cco_co (iscocommutativecomonoidobject_semiadditive a)). + exact i. + (* Arguments IsComonoidObject : clear implicits. + Arguments IsCocommutativeComonoidObject : clear implicits. + pose proof (i := cco_co (iscocommutativecomonoidobject_semiadditive a)). + unfold cat_bincoprod. + unfold is1bifunctor_cat_bincoprod. + Arguments is1bifunctor_op' : clear implicits. + unfold is1bifunctor_op'. + unfold is1bifunctor_op. + + exact i. + + unfold Coproducts.is1bifunctor_cat_bincoprod. + unfold Coproducts.is1bifunctor_cat_bincoprod. + + exact i. + exact _. + + + + + change (MonUnit (Hom (A:=A^op) b a)). + snrapply ( (A:=A^op) (zero_object (A:=A^op)) (x := b) (y := a)). + 1-11: exact _. + (* change (IsMonoidObject (A:=A^op) ?F ?z ?x) with (IsComonoidObject (A:=A) F z x). + (IsComonoidObject (fun x y => cat_binbiprod x y) _ b). *) + pose proof (iscocommutativecomonoidobject_semiadditive a). + unfold IsCocommutativeComonoidObject in X. + rapply cmo_mo. + *) + Admitted. + + (** TODO: explain a bit more: diagonal duplicates and codiagonal sums. *) + (** The operation is given by the biproduct structure. *) + Global Instance sgop_hom : Plus (a $-> b) := fun f g => + cat_binbiprod_codiag b + $o fmap11 (fun x y => cat_binbiprod x y) f g + $o cat_binbiprod_diag a. + + Local Instance left_identity_hom : LeftIdentity sgop_hom zero_hom. + Proof. + intros g. + apply path_hom. + unfold sgop_hom. + nrefine (cat_assoc _ _ _ $@ (_ $@L (_ $@ _)) $@ _). + 1: nrapply cat_binbiprod_fmap11_corec. + 1: nrapply (cat_binbiprod_corec_eta' (cat_idr _) (cat_idr _) $@ _). + 1: exact (cat_binbiprod_corec_zero_inr g). + nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_idl _). + nrapply cat_binbiprod_rec_beta_inr. + Defined. + + Local Existing Instance symmetricbraiding_cat_binbiprod. + + (** Using the naturality of swap we can show that the operation is commutative. *) + Local Instance commutative_hom : Commutative sgop_hom. + Proof. + intros f g. + apply path_hom. + refine (cat_assoc _ _ _ $@ _). + refine ((_^$ $@R _) $@ _). + 1: nrapply cat_binbiprod_swap_codiag. + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$). + refine (_ $@ (_ $@L _)). + 2: nrapply cat_binbiprod_swap_diag. + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ cat_assoc _ _ _). + rapply Monoidal.braid_nat. + Defined. + + Local Instance right_identity_ab_hom : RightIdentity sgop_hom zero_hom. + Proof. + intros f. + refine (commutativity _ _ @ _). + nrapply left_identity_hom. + Defined. + + Local Instance associative_ab_hom : Associative sgop_hom. + Proof. + (** There is a lot to unfold here. But drawing out the diagram we can split this into 5 separate diagrams that all commute. Much of the work here will be applying associativity and functor laws to get this diagram in the correct shape. *) + (* intros f g h. + apply path_hom. + refine (((_ $@L (_ $@R _)) $@R _) $@ _ $@ ((_ $@L (_ $@L _)^$) $@R _)). + 1,3: refine (_ $@ ((_ $@ (_ $@L _)) $@R _)). + 1-3: rapply fmap01_comp. + 1-3: rapply fmap10_comp. + Local Notation "a ⊕L g" := (fmap01 (fun x y => cat_binbiprod x y) a g) (at level 99). + Local Notation "f ⊕R b" := (fmap10 (fun x y => cat_binbiprod x y) f b) (at level 99). + Local Notation "'Δ' x" := (cat_binbiprod_diag x) (at level 10). + Local Notation "'∇' x" := (cat_binbiprod_codiag x) (at level 10). + change (?w $o ?x $== ?y $o ?z) with (Square z w x y). + nrapply move_right_top. + (** The following associativity rewrites are specially chosen so that the diagram can be decomposed easily. *) + rapply vconcatL. + 1: do 2 refine (cat_assoc _ _ _ $@ _). + 1: refine (((cat_assoc _ _ _)^$ $@R _)). + rapply vconcatR. + 2: do 2 refine ((cat_assoc _ _ _)^$ $@ (_ $@L (cat_assoc _ _ _)) $@ _). + 2: refine (cat_assoc _ _ _)^$. + srapply hconcat. + (** We now have to specify the morphism that we are composing along, i.e. the common edge of the two squares where they meet. This is chosen to be the associativity equivalence for biproducts. *) + 1: nrapply cate_binbiprod_assoc. + { nrefine ((_ $@R _) $@ _). + 1: rapply Monoidal.associator_twist'_unfold. + nrapply cat_binbiprod_pr_eta. + - srefine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: exact (fmap01 (fun x y => cat_binbiprod x y) b cat_binbiprod_pr1). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr1. + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr2. + refine (_^$ $@ _). + 1: rapply fmap01_comp. + refine (fmap02 _ _ _). + nrapply cat_binbiprod_corec_beta_pr2. } + refine ((cat_assoc _ _ _)^$ $@ _). + refine ((((fmap02 _ _ _ $@ fmap01_id _ _ _)^$ $@ fmap01_comp _ _ _ _)^$ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr1. + nrefine (cat_idl _ $@ _). + refine (_ $@ (_ $@L (cat_assoc _ _ _)^$)). + nrefine (_ $@ cat_assoc _ _ _). + refine (_ $@ (_^$ $@R _)). + 2: rapply cat_binbiprod_corec_beta_pr1. + refine ((_ $@L _) $@ (cat_assoc _ _ _)^$). + nrefine (_ $@ cat_assoc _ _ _). + refine (_ $@ (_^$ $@R _)). + 2: rapply cat_binbiprod_corec_beta_pr1. + refine (_ $@ (cat_assoc _ _ _)^$). + refine (_ $@ (_ $@L _^$)). + 2: rapply cat_binbiprod_corec_beta_pr1. + symmetry. + nrapply cat_idr. + - nrefine ((_ $@L (cat_assoc _ _ _)) $@ _). + refine ((cat_assoc _ _ _)^$ $@ _). + nrefine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr2. + nrefine ((_ $@L (cat_assoc _ _ _)) $@ _). + refine ((cat_assoc _ _ _)^$ $@ _). + nrefine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr1. + nrefine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + nrapply cat_binbiprod_corec_beta_pr2. } + nrefine ((_ $@L (cat_assoc _ _ _)) $@ _). + refine ((cat_assoc _ _ _)^$ $@ _). + nrefine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr1. + nrefine ((_ $@L _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + nrapply cat_binbiprod_corec_beta_pr2. } + nrefine ((_ $@L (cat_assoc _ _ _)) $@ _). + refine ((cat_assoc _ _ _)^$ $@ _). + nrefine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr2. + nrefine (cat_idl _ $@ _). + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr2. + nrefine (cat_assoc _ _ _ $@ _). + nrefine (cat_idl _ $@ _). + nrefine (cat_binbiprod_corec_beta_pr2 _ _ $@ _). + refine (_ $@ (_ $@L (cat_assoc _ _ _)^$)). + nrefine (_ $@ cat_assoc _ _ _). + refine (_ $@ (_^$ $@R _)). + 2: nrapply cat_binbiprod_corec_beta_pr2. + refine (_ $@ (cat_assoc _ _ _)^$). + refine (_ $@ (cat_idl _)^$). + refine (_ $@ (_^$ $@R _) $@ cat_assoc _ _ _). + 2: nrapply cat_binbiprod_corec_beta_pr2. + refine (_ $@ (cat_assoc _ _ _)^$). + refine (_ $@ (cat_idl _)^$). + symmetry. + nrapply cat_binbiprod_corec_beta_pr2. } + (** We split the square again, this time by picking yet another associativity map as the common edge. This leaves us with a naturality square for associativity. *) + srapply hconcat. + 1: nrapply cate_binbiprod_assoc. + 1: nrapply Monoidal.associator_nat_m. + (** Finally we are left with another polygon which we resolve by brute force. *) + refine ((cat_assoc _ _ _)^$ $@ _). + nrapply cat_binbiprod_in_eta. + - nrefine (cat_assoc _ _ _ $@ _). + nrefine ((_ $@L _) $@ _). + { nrefine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + nrapply cat_binbiprod_rec_beta_inl. } + refine ((cat_assoc _ _ _)^$ $@ _). + refine (cat_idr _ $@ _). + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). + { refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + nrapply cat_binbiprod_rec_beta_inl. } + refine ((cat_assoc _ _ _)^$ $@ _). + refine (cat_idr _ $@ _). + refine (_ $@ _). + 1: nrapply cat_binbiprod_rec_beta_inl. + symmetry. + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L _) $@ _). + 1: nrapply cate_binbiprod_assoc_inl. + refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + { refine (cat_assoc _ _ _ $@ (_ $@L _)). + refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + nrapply cat_binbiprod_rec_beta_inl. } + simpl. + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L _) $@ _). + { refine (cat_assoc _ _ _ $@ (_ $@L _)). + nrapply cat_binbiprod_rec_beta_inl. } + refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + { refine (cat_assoc _ _ _ $@ (_ $@L _)). + refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ (_ $@ _)). + 1: nrapply cat_binbiprod_rec_beta_inl. + nrapply cat_idr. } + refine (cat_idr _ $@ _). + nrapply cat_binbiprod_rec_beta_inl. + - nrefine (cat_assoc _ _ _ $@ _). + nrefine ((_ $@L _) $@ _). + { nrefine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + nrapply cat_binbiprod_rec_beta_inr. } + refine ((cat_assoc _ _ _)^$ $@ _). + simpl. + refine ((_ $@R _) $@ _). + { refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). + 1: refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inr. + refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inr. + nrapply cat_idl. } + simpl. + refine (_ $@ (cat_assoc _ _ _)^$). + nrapply cat_binbiprod_in_eta. + + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L _) $@ _). + { refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + nrapply cat_binbiprod_rec_beta_inl. } + refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inl. + refine (cat_idr _ $@ _). + refine (_ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$). + 2: nrapply cate_binbiprod_assoc_inr_inl. + refine (_ $@ (cat_assoc _ _ _)^$). + refine (_ $@ (_ $@L _^$)). + 2: { refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inl. + simpl. + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inr. + nrapply cat_idr. } + simpl. + refine (_ $@ (cat_assoc _ _ _)^$). + refine (_^$ $@ (_ $@L _^$)). + 2: { refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ (_ $@ _)). + 1: nrapply cat_binbiprod_rec_beta_inl. + nrapply cat_idr. } + nrapply cat_binbiprod_rec_beta_inl. + + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L _) $@ _). + { refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + nrapply cat_binbiprod_rec_beta_inr. } + refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inr. + refine (cat_idl _ $@ _). + refine (_ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$). + 2: nrapply cate_binbiprod_assoc_inr_inr. + simpl. + refine (_ $@ (cat_assoc _ _ _)^$). + refine (_^$ $@ (_ $@L _^$)). + 2: { refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ (_ $@ _)). + 1: nrapply cat_binbiprod_rec_beta_inr. + nrapply cat_idr. } + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). + { refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inr. } + refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inr. + nrapply cat_idl. *) + Admitted. + + Local Instance issemigroup_hom : IsSemiGroup (a $-> b) := {}. + Local Instance ismonoid_hom : IsMonoid (a $-> b) := {}. + +End CMonHom. + +(** ** Additive Categories *) + +(** *** Definition *) + +Class IsAdditive (A : Type) `{HasEquivs A} := { + additive_semiadditive :: IsSemiAdditive A; + additive_negate_hom :: forall (a b : A), Negate (a $-> b); + additive_left_inverse_hom :: forall (a b : A), + LeftInverse (sgop_hom a b) (additive_negate_hom a b) (zero_hom a b); + additive_right_inverse_hom :: forall (a b : A), + RightInverse (sgop_hom a b) (additive_negate_hom a b) (zero_hom a b); +}. + +(** *** Abelian Group structure on Hom *) + +(** Homs in an additive category form abelian groups. *) +Definition AbHom {A : Type} `{IsAdditive A} : A -> A -> AbGroup. +Proof. + intros a b. + snrapply Build_AbGroup. + 1: snrapply Build_Group. + 5: split. + - exact (a $-> b). + - exact (sgop_hom a b). + - exact (zero_hom a b). + - exact (additive_negate_hom a b). + - exact (ismonoid_hom a b). + - exact (additive_left_inverse_hom a b). + - exact (additive_right_inverse_hom a b). + - exact (commutative_hom a b). +Defined. + +(** *** Distributivity of composition over addition *) + +Definition addcat_dist_l {A : Type} `{IsAdditive A} {a b c : A} + (f : b $-> c) (g h : a $-> b) + : f $o (g + h) $== (f $o g) + (f $o h). +Proof. + (* refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _ $@ cat_assoc _ _ _). + 1: nrapply cat_binbiprod_codiag_fmap11. + refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$). + rapply fmap11_comp. *) +Admitted. + +(** Note that this is more general than the distributive law in the endomorphism ring. *) +Global Instance left_heterodistribute_hom {A : Type} `{IsAdditive A} {a b c : A} + : LeftHeteroDistribute cat_comp (sgop_hom a b) (sgop_hom a c). +Proof. + intros f g h. + apply path_hom. + nrapply addcat_dist_l. +Defined. + +Definition addcat_dist_r {A : Type} `{IsAdditive A} {a b c : A} + (f g : b $-> c) (h : a $-> b) + : (f + g) $o h $== (f $o h) + (g $o h). +Proof. + refine (cat_assoc _ _ _ $@ _). + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$). + refine ((_ $@L _) $@ _). + 1: nrapply cat_binbiprod_diag_fmap11. + refine ((cat_assoc _ _ _)^$ $@ (_^$ $@R _)). + rapply fmap11_comp. +Defined. + +Global Instance right_heterodistribute_hom {A : Type} `{IsAdditive A} {a b c : A} + : RightHeteroDistribute cat_comp (sgop_hom a c) (sgop_hom b c). +Proof. + intros f g h. + apply path_hom. + nrapply addcat_dist_r. +Defined. + +Definition addcat_comp_negate_id_l {A : Type} `{IsAdditive A} {a b : A} + (f : a $-> b) + : (- Id _) $o f $== -f. +Proof. + nrapply GpdHom_path. + change (@paths (Hom a b) ?x ?y) with (@paths (AbHom a b : Type) x y). + rapply grp_moveL_1V. + transitivity ((-Id b $o f) + (Id b $o f)). + - f_ap; symmetry; apply path_hom, cat_idl. + - lhs_V rapply right_heterodistribute_hom. + transitivity (zero_morphism (b := b) $o f). + + f_ap; nrapply (grp_inv_l (Id b : AbHom b b)). + + apply path_hom. + nrapply cat_zero_l. +Defined. + +Definition addcat_comp_negate_id_r {A : Type} `{IsAdditive A} {a b : A} + (f : a $-> b) + : f $o (- Id _) $== -f. +Proof. + nrapply GpdHom_path. + change (@paths (Hom a b) ?x ?y) with (@paths (AbHom a b : Type) x y). + rapply grp_moveL_1V. + transitivity ((f $o -Id a) + (f $o Id a)). + - f_ap; symmetry; apply path_hom, cat_idr. + - lhs_V rapply left_heterodistribute_hom. + transitivity (f $o zero_morphism (a := a)). + + f_ap; nrapply (grp_inv_l (Id a : AbHom a a)). + + apply path_hom. + nrapply cat_zero_r. +Defined. + +Definition addcat_comp_negate_l {A : Type} `{IsAdditive A} {a b c : A} + (f : b $-> c) (g : a $-> b) + : - (f $o g) $== (- f) $o g. +Proof. + refine ((addcat_comp_negate_id_l _)^$ $@ _). + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + nrapply addcat_comp_negate_id_l. +Defined. + +Definition addcat_comp_negate_r {A : Type} `{IsAdditive A} {a b c : A} + (f : b $-> c) (g : a $-> b) + : - (f $o g) $== f $o (- g). +Proof. + refine ((addcat_comp_negate_id_r _)^$ $@ _). + refine (cat_assoc _ _ _ $@ (_ $@L _)). + nrapply addcat_comp_negate_id_r. +Defined. + +(** ** Properties of additive categories *) + +(** The opposite of a semiadditive category is semiadditive. *) +Global Instance issemiadditive_op {A : Type} `{IsSemiAdditive A} + : IsSemiAdditive A^op. +Proof. + snrapply Build_IsSemiAdditive. + 1-3: exact _. + intros a b. + change A in a, b. + change (IsHSet (b $-> a)). + exact _. +Defined. + +Axiom sorry : Empty. +Ltac sorry := apply Empty_rect; apply sorry. + +(** The opposite of an additive category is additive. *) +Global Instance isadditive_op {A : Type} `{H : IsAdditive A} + : IsAdditive A^op. +Proof. + snrapply Build_IsAdditive. + - exact _. + - intros a b. + change A in a, b. + change (Negate (b $-> a)). + exact _. + - sorry. + - sorry. +Defined. + +(** TODO: Additive functors *) diff --git a/theories/Algebra/Homological/Biproducts.v b/theories/Algebra/Homological/Biproducts.v new file mode 100644 index 00000000000..fb8ec756544 --- /dev/null +++ b/theories/Algebra/Homological/Biproducts.v @@ -0,0 +1,963 @@ +Require Import Basics.Overture Basics.Decidable Basics.Tactics Basics.Trunc Basics.Equivalences. +Require Import Types.Forall Types.Bool Types.Paths Types.Empty Types.Equiv Types.Sigma. +Require Import WildCat.Core WildCat.Products WildCat.Coproducts WildCat.Equiv. +Require Import WildCat.PointedCat WildCat.Bifunctor WildCat.Square. +Require Import WildCat.Opposite WildCat.Monoidal. + +(** * Categories with biproducts *) + +(** ** Biproducts *) + +Class Biproduct (I : Type) `{DecidablePaths I} {A : Type} + `{HasEquivs A, !IsPointedCat A} {x : I -> A} + := Build_Biproduct' { + biproduct_product :: Product I x; + biproduct_coproduct :: Coproduct I x; + catie_cat_coprod_prod :: CatIsEquiv (cat_coprod_prod x); +}. + +Arguments Biproduct I {_ A _ _ _ _ _ _} x. +Arguments Build_Biproduct' I {_ A _ _ _ _ _ _} x _ _ _. + +Section Biproducts. + Context {I : Type} {A : Type} (x : I -> A) `{Biproduct I A x}. + + Definition cate_coprod_prod : cat_coprod I x $<~> cat_prod I x + := Build_CatEquiv (cat_coprod_prod x). + + Definition cat_biprod : A + := cat_prod I x. + + Definition cat_biprod_pr : forall (i : I), cat_biprod $-> x i + := cat_pr. + + Definition cat_biprod_corec {z : A} + : (forall i, z $-> x i) -> z $-> cat_biprod + := cat_prod_corec I. + + Definition cat_biprod_corec_beta {z : A} (f : forall i, z $-> x i) + : forall i, cat_biprod_pr i $o cat_biprod_corec f $== f i + := cat_prod_beta I f. + + Definition cat_biprod_corec_eta {z : A} (f : z $-> cat_biprod) + : cat_biprod_corec (fun i => cat_biprod_pr i $o f) $== f + := cat_prod_eta I f. + + Definition cat_biprod_corec_eta' {z : A} {f f' : forall i, z $-> x i} + : (forall i, f i $== f' i) -> cat_biprod_corec f $== cat_biprod_corec f' + := cat_prod_corec_eta I. + + Definition cat_biprod_pr_eta {z : A} {f f' : z $-> cat_biprod} + : (forall i, cat_biprod_pr i $o f $== cat_biprod_pr i $o f') -> f $== f' + := cat_prod_pr_eta I. + + Definition cat_biprod_in : forall (i : I), x i $-> cat_biprod + := fun i => cate_coprod_prod $o cat_in i. + + Definition cat_biprod_rec {z : A} + : (forall i, x i $-> z) -> cat_biprod $-> z + := fun f => cat_coprod_rec I f $o cate_coprod_prod^-1$. + + Definition cat_biprod_rec_beta {z : A} (f : forall i, x i $-> z) + : forall i, cat_biprod_rec f $o cat_biprod_in i $== f i. + Proof. + intros i. + unfold cat_biprod_rec, cat_biprod_in. + refine (_ $@ cat_coprod_beta I f i). + nrefine (cat_assoc _ _ _ $@ (_ $@L _)). + nrapply compose_V_hh. + Defined. + + Definition cat_biprod_rec_eta {z : A} (f : cat_biprod $-> z) + : cat_biprod_rec (fun i => f $o cat_biprod_in i) $== f. + Proof. + unfold cat_biprod_rec. + nrapply cate_moveR_eV. + nrapply cat_coprod_in_eta. + intros i. + refine (cat_coprod_beta I _ i $@ _^$). + nrapply cat_assoc; exact _. + Defined. + + Definition cat_biprod_rec_eta' {z : A} {f f' : forall i, x i $-> z} + : (forall i, f i $== f' i) -> cat_biprod_rec f $== cat_biprod_rec f'. + Proof. + intros p. + unfold cat_biprod_rec. + exact (cat_coprod_rec_eta I p $@R _). + Defined. + + Definition cat_biprod_in_eta {z : A} {f f' : cat_biprod $-> z} + : (forall i, f $o cat_biprod_in i $== f' $o cat_biprod_in i) -> f $== f'. + Proof. + intros p. + nrapply (cate_epic_equiv cate_coprod_prod). + nrapply cat_coprod_in_eta. + intros i. + exact (cat_assoc _ _ _ $@ p i $@ (cat_assoc _ _ _)^$). + Defined. + +End Biproducts. + +Arguments cat_biprod I {A} x {_ _ _ _ _ _ _ _}. +Arguments cat_biprod_pr {I A x _ _ _ _ _ _ _ _} i. +Arguments cat_biprod_in {I A x _ _ _ _ _ _ _ _} i. +Arguments cate_coprod_prod {I A} x {_ _ _ _ _ _ _ _}. + +(** A smart constructor for biproducts. Note that compared to a typical definition of a biproduct, we have not asked for the sum of inclusions composed with projections to be the identity. There are a few reasons for this: In our general setting [I] may be infinite, so it doesn't make sense to ask for an infinite sum; Even if we somehow axiomatized something about the sum, we later show in [Additive.v] that the sum is in fact an emergent property; Finally, it doesn't seem necessary to produce an isomorphism since we take that to be the identity in this lemma. We should also note that we require [A] to be a pointed category. In theory this requirement could be dropped. To do this we would weaken the equation showing [cat_pr j $o cat_in i] for different [i] and [j], to postulate that [cat_pr j $o cat_in i] is a split idempotent. This doesn't seem particularly useful however as the finite biproduct case implies the existence of zero objects. *) +Definition Build_Biproduct (I : Type) `{DecidablePaths I} + {A : Type} `{HasEquivs A, !IsPointedCat A} (x : I -> A) + (cat_biprod : A) + (** A biproduct is a product. *) + (cat_pr : forall i, cat_biprod $-> x i) + (corec : forall z, (forall i, z $-> x i) -> z $-> cat_biprod) + (corec_beta : forall z f i, cat_pr i $o corec z f $== f i) + (corec_eta : forall z (f g : z $-> cat_biprod), + (forall i, cat_pr i $o f $== cat_pr i $o g) -> f $== g) + (** A biproduct is a coproduct. *) + (cat_in : forall i, x i $-> cat_biprod) + (rec : forall z, (forall i, x i $-> z) -> cat_biprod $-> z) + (rec_beta : forall z f i, rec z f $o cat_in i $== f i) + (rec_eta : forall z (f g : cat_biprod $-> z), + (forall i, f $o cat_in i $== g $o cat_in i) -> f $== g) + (** The projections and inclusion maps satisfy some further properties. *) + (cat_pr_in : forall i, cat_pr i $o cat_in i $== Id _) + (cat_pr_in_ne : forall i j, i <> j -> cat_pr j $o cat_in i $== zero_morphism) + : Biproduct I x. +Proof. + (** We can show these directly when building the biproduct, however we would like to refer to them between goals so we prove them here first. *) + transparent assert (product : (Product I x)). + { snrapply Build_Product. + - exact cat_biprod. + - exact cat_pr. + - exact corec. + - exact corec_beta. + - exact corec_eta. } + transparent assert (coproduct : (Coproduct I x)). + { snrapply Build_Coproduct. + - exact cat_biprod. + - exact cat_in. + - exact rec. + - exact rec_beta. + - exact rec_eta. } + assert (r : (cat_coprod_prod x $== Id cat_biprod)). + { nrapply rec_eta. + intros i. + refine (rec_beta _ _ _ $@ _ $@ (cat_idl _)^$). + nrapply corec_eta. + intros j. + refine (corec_beta _ _ _ $@ _^$). + destruct (dec_paths i j) as [p|np]. + * destruct p. + exact (cat_pr_in i). + * exact (cat_pr_in_ne i j np). } + snrapply Build_Biproduct'. + - exact product. + - exact coproduct. + - exact (catie_homotopic _ r^$). +Defined. + +(** An inclusion followed by a projection of the same index is the identity. *) +Definition cat_biprod_pr_in (I : Type) {A : Type} (x : I -> A) + `{Biproduct I A x} (i : I) + : cat_biprod_pr i $o cat_biprod_in i $== Id _. +Proof. + unfold cat_biprod_pr, cat_biprod_in. + refine ((_ $@L _) $@ _). + { refine ((cate_buildequiv_fun _ $@R _) $@ _). + nrapply cat_coprod_beta. } + refine (cat_prod_beta _ _ _ $@ _). + simpl. + generalize (dec_paths i i). + by nrapply decidable_paths_refl. +Defined. + +(** An inclusion followed by a projection of a different index is zero. *) +Definition cat_biprod_pr_in_ne (I : Type) {A : Type} (x : I -> A) + `{Biproduct I A x} {i j : I} (p : i <> j) + : cat_biprod_pr j $o cat_biprod_in i $== zero_morphism. +Proof. + unfold cat_biprod_pr, cat_biprod_in. + refine ((_ $@L _) $@ _). + { refine ((cate_buildequiv_fun _ $@R _) $@ _). + nrapply cat_coprod_beta. } + refine (cat_prod_beta _ _ _ $@ _). + decidable_false (dec_paths i j) p. + simpl. + reflexivity. +Defined. + +Definition cat_biprod_diag I {A} (x : A) `{Biproduct I A (fun _ => x)} + : x $-> cat_biprod I (fun _ => x) + := cat_prod_diag x. + +Definition cat_biprod_codiag I {A} (x : A) `{Biproduct I A (fun _ => x)} + : cat_biprod I (fun _ => x) $-> x + := cat_coprod_codiag x $o (cate_coprod_prod (fun _ => x))^-1$. + +(** Compatability of [cat_biprod_rec] and [cat_biprod_corec]. *) +Definition cat_biprod_corec_rec I `{DecidablePaths I} {A : Type} + `{HasEquivs A, !IsPointedCat A} {x y : I -> A} + `{!Biproduct I x, !Biproduct I y} + (f : forall i, x i $-> y i) + : cat_biprod_corec y (fun i => f i $o cat_biprod_pr i) + $== cat_biprod_rec x (fun i => cat_biprod_in i $o f i). +Proof. + nrapply cat_biprod_pr_eta. + intros i. + refine (cat_biprod_corec_beta _ _ i $@ _). + nrapply cat_biprod_in_eta. + intros j. + refine (_ $@ (_ $@L (cat_biprod_rec_beta _ _ _)^$) $@ (cat_assoc _ _ _)^$). + refine (cat_assoc _ _ _ $@ _ $@ cat_assoc _ _ _). + destruct (dec_paths j i) as [p | np]. + - destruct p. + refine ((_ $@L _) $@ cat_idr _ $@ (cat_idl _)^$ $@ (_^$ $@R _)). + 1,2: nrapply cat_biprod_pr_in. + - refine ((_ $@L _) $@ cat_zero_r _ $@ (cat_zero_l _)^$ $@ (_^$ $@R _)). + 1,2: nrapply cat_biprod_pr_in_ne; assumption. +Defined. + +(** *** Existence of biproducts *) + +Class HasBiproducts (I A : Type) + `{DecidablePaths I, HasEquivs A, !IsPointedCat A} + := has_biproducts :: forall (x : I -> A), Biproduct I x. + +(** *** Binary biproducts *) + +Class BinaryBiproduct {A : Type} `{HasEquivs A, !IsPointedCat A} (x y : A) + := binary_biproduct :: Biproduct Bool (fun b => if b then x else y). + +Definition Build_BinaryBiproduct' {A : Type} `{HasEquivs A, !IsPointedCat A} + {x y : A} {p : BinaryProduct x y} {c : BinaryCoproduct x y} + {ie : CatIsEquiv (cat_bincoprod_binprod x y)} + : BinaryBiproduct x y + := Build_Biproduct' _ _ p c ie. + +(** Smart constructor for binary biproducts. *) +Definition Build_BinaryBiproduct {A : Type} `{HasEquivs A, !IsPointedCat A} + {x y : A} (cat_biprod : A) + (** A binary biproduct is a product. *) + (cat_pr1 : cat_biprod $-> x) (cat_pr2 : cat_biprod $-> y) + (corec : forall z, (z $-> x) -> (z $-> y) -> z $-> cat_biprod) + (corec_beta_pr1 : forall z f g, cat_pr1 $o corec z f g $== f) + (corec_beta_pr2 : forall z f g, cat_pr2 $o corec z f g $== g) + (corec_eta : forall z (f g : z $-> cat_biprod), + cat_pr1 $o f $== cat_pr1 $o g -> cat_pr2 $o f $== cat_pr2 $o g -> f $== g) + (** A biproduct is a coproduct. *) + (cat_inl : x $-> cat_biprod) (cat_inr : y $-> cat_biprod) + (rec : forall z, (x $-> z) -> (y $-> z) -> cat_biprod $-> z) + (rec_beta_inl : forall z f g, rec z f g $o cat_inl $== f) + (rec_beta_inr : forall z f g, rec z f g $o cat_inr $== g) + (rec_eta : forall z (f g : cat_biprod $-> z), + f $o cat_inl $== g $o cat_inl -> f $o cat_inr $== g $o cat_inr -> f $== g) + (** The projections and inclusion maps satisfy some further properties. *) + (cat_pr1_inl : cat_pr1 $o cat_inl $== Id _) + (cat_pr2_inr : cat_pr2 $o cat_inr $== Id _) + (cat_pr1_inr : cat_pr1 $o cat_inr $== zero_morphism) + (cat_pr2_inl : cat_pr2 $o cat_inl $== zero_morphism) + : BinaryBiproduct x y. +Proof. + snrapply Build_Biproduct. + - exact cat_biprod. + - intros [ | ]. + + exact cat_pr1. + + exact cat_pr2. + - intros z f. + exact (corec z (f true) (f false)). + - intros z f [ | ]. + + exact (corec_beta_pr1 z (f true) (f false)). + + exact (corec_beta_pr2 z (f true) (f false)). + - intros z f g p. + exact (corec_eta z _ _ (p true) (p false)). + - intros [ | ]. + + exact cat_inl. + + exact cat_inr. + - intros z f. + exact (rec z (f true) (f false)). + - intros z f [ | ]. + + exact (rec_beta_inl z (f true) (f false)). + + exact (rec_beta_inr z (f true) (f false)). + - intros z f g p. + exact (rec_eta z _ _ (p true) (p false)). + - intros [ | ]. + + exact cat_pr1_inl. + + exact cat_pr2_inr. + - intros i j ne. + destruct (negb_ne' ne), i as [ | ]. + + exact cat_pr2_inl. + + exact cat_pr1_inr. +Defined. + +Class HasBinaryBiproducts (A : Type) `{HasEquivs A, !IsPointedCat A} + := has_binary_biproducts :: forall (x y : A), BinaryBiproduct x y. + +Global Instance hasbinarybiproducts_hasbiproductsbool {A : Type} + `{HasEquivs A, !IsPointedCat A, !HasBiproducts Bool A} + : HasBinaryBiproducts A + := fun x y => has_biproducts (fun b : Bool => if b then x else y). + +Global Instance hasbinaryproducts_hasbinarybiproducts {A : Type} + `{H : HasBinaryBiproducts A} + : HasBinaryProducts A. +Proof. + intros x y. + apply biproduct_product. +Defined. + +Global Instance hasbinarycoproducts_hasbinarybiproducts {A : Type} + `{H : HasBinaryBiproducts A} + : HasBinaryCoproducts A. +Proof. + intros x y. + nrapply biproduct_coproduct. + nrapply H. +Defined. + +Section BinaryBiproducts. + + Context {A : Type} `{HasEquivs A, !IsPointedCat A} {x y : A} + `{!BinaryBiproduct x y}. + + Definition cat_binbiprod : A + := cat_biprod Bool (fun b => if b then x else y). + + Definition cat_binbiprod_pr1 : cat_binbiprod $-> x := cat_biprod_pr true. + Definition cat_binbiprod_pr2 : cat_binbiprod $-> y := cat_biprod_pr false. + + Definition cat_binbiprod_corec {z : A} (f : z $-> x) (g : z $-> y) + : z $-> cat_binbiprod. + Proof. + nrapply cat_biprod_corec. + intros [|]. + - exact f. + - exact g. + Defined. + + Definition cat_binbiprod_corec_beta_pr1 {z : A} (f : z $-> x) (g : z $-> y) + : cat_binbiprod_pr1 $o cat_binbiprod_corec f g $== f + := cat_biprod_corec_beta _ _ true. + + Definition cat_binbiprod_corec_beta_pr2 {z : A} (f : z $-> x) (g : z $-> y) + : cat_binbiprod_pr2 $o cat_binbiprod_corec f g $== g + := cat_biprod_corec_beta _ _ false. + + Definition cat_binbiprod_corec_eta {z : A} (f : z $-> cat_binbiprod) + : cat_binbiprod_corec (cat_binbiprod_pr1 $o f) (cat_binbiprod_pr2 $o f) + $== f. + Proof. + nrapply cat_biprod_pr_eta. + intros [|]. + - exact (cat_binbiprod_corec_beta_pr1 _ _). + - exact (cat_binbiprod_corec_beta_pr2 _ _). + Defined. + + Definition cat_binbiprod_corec_eta' {z : A} {f f' : z $-> x} {g g' : z $-> y} + : f $== f' -> g $== g' + -> cat_binbiprod_corec f g $== cat_binbiprod_corec f' g'. + Proof. + intros p q. + nrapply cat_biprod_corec_eta'. + intros [|]. + - exact p. + - exact q. + Defined. + + Definition cat_binbiprod_pr_eta {z : A} {f f' : z $-> cat_binbiprod} + : cat_binbiprod_pr1 $o f $== cat_binbiprod_pr1 $o f' + -> cat_binbiprod_pr2 $o f $== cat_binbiprod_pr2 $o f' + -> f $== f'. + Proof. + intros p q. + nrapply cat_biprod_pr_eta. + intros [|]. + - exact p. + - exact q. + Defined. + + Definition cat_binbiprod_inl : x $-> cat_binbiprod := cat_biprod_in true. + Definition cat_binbiprod_inr : y $-> cat_binbiprod := cat_biprod_in false. + + Definition cat_binbiprod_rec {z : A} (f : x $-> z) (g : y $-> z) + : cat_binbiprod $-> z. + Proof. + nrapply cat_biprod_rec. + intros [|]. + - exact f. + - exact g. + Defined. + + Definition cat_binbiprod_rec_beta_inl {z : A} (f : x $-> z) (g : y $-> z) + : cat_binbiprod_rec f g $o cat_binbiprod_inl $== f + := cat_biprod_rec_beta _ _ true. + + Definition cat_binbiprod_rec_beta_inr {z : A} (f : x $-> z) (g : y $-> z) + : cat_binbiprod_rec f g $o cat_binbiprod_inr $== g + := cat_biprod_rec_beta _ _ false. + + Definition cat_binbiprod_rec_eta {z : A} (f : cat_binbiprod $-> z) + : cat_binbiprod_rec (f $o cat_binbiprod_inl) (f $o cat_binbiprod_inr) $== f. + Proof. + nrapply cat_biprod_in_eta. + intros [|]. + - exact (cat_binbiprod_rec_beta_inl _ _). + - exact (cat_binbiprod_rec_beta_inr _ _). + Defined. + + Definition cat_binbiprod_rec_eta' {z : A} {f f' : x $-> z} {g g' : y $-> z} + : f $== f' -> g $== g' + -> cat_binbiprod_rec f g $== cat_binbiprod_rec f' g'. + Proof. + intros p q. + nrapply cat_biprod_rec_eta'. + intros [|]. + - exact p. + - exact q. + Defined. + + Definition cat_binbiprod_in_eta {z : A} {f f' : cat_binbiprod $-> z} + : f $o cat_binbiprod_inl $== f' $o cat_binbiprod_inl + -> f $o cat_binbiprod_inr $== f' $o cat_binbiprod_inr + -> f $== f'. + Proof. + intros p q. + nrapply cat_biprod_in_eta. + intros [|]. + - exact p. + - exact q. + Defined. + + Definition cat_binbiprod_pr1_inl + : cat_binbiprod_pr1 $o cat_binbiprod_inl $== Id _ + := cat_biprod_pr_in Bool _ true. + + Definition cat_binbiprod_pr2_inr + : cat_binbiprod_pr2 $o cat_binbiprod_inr $== Id _ + := cat_biprod_pr_in Bool _ false. + + Definition cat_binbiprod_pr2_inl + : cat_binbiprod_pr2 $o cat_binbiprod_inl $== zero_morphism. + Proof. + snrapply (cat_biprod_pr_in_ne Bool _ (i := true) (j := false)). + nrapply (not_fixed_negb false). + Defined. + + Definition cat_binbiprod_pr1_inr + : cat_binbiprod_pr1 $o cat_binbiprod_inr $== zero_morphism. + Proof. + snrapply (cat_biprod_pr_in_ne Bool _ (i := false) (j := true)). + nrapply (not_fixed_negb true). + Defined. + + Definition cat_binbiprod_corec_zero_inl {z} (f : z $-> x) + : cat_binbiprod_corec f zero_morphism $== cat_binbiprod_inl $o f. + Proof. + snrapply cat_binbiprod_pr_eta. + - refine (cat_binbiprod_corec_beta_pr1 _ _ $@ _^$). + exact ((cat_assoc _ _ _)^$ $@ (cat_binbiprod_pr1_inl $@R _) $@ cat_idl _). + - refine (cat_binbiprod_corec_beta_pr2 _ _ $@ _^$). + exact ((cat_assoc _ _ _)^$ $@ (cat_binbiprod_pr2_inl $@R _) $@ cat_zero_l _). + Defined. + + Definition cat_binbiprod_corec_zero_inr {z} (f : z $-> y) + : cat_binbiprod_corec zero_morphism f $== cat_binbiprod_inr $o f. + Proof. + snrapply cat_binbiprod_pr_eta. + - refine (cat_binbiprod_corec_beta_pr1 _ _ $@ _^$). + exact ((cat_assoc _ _ _)^$ $@ (cat_binbiprod_pr1_inr $@R _) $@ cat_zero_l _). + - refine (cat_binbiprod_corec_beta_pr2 _ _ $@ _^$). + exact ((cat_assoc _ _ _)^$ $@ (cat_binbiprod_pr2_inr $@R _) $@ cat_idl _). + Defined. + +End BinaryBiproducts. + +Arguments cat_binbiprod {A _ _ _ _ _ _} x y {_}. + +(** Annoyingly this doesn't follow directly from the general diagonal since [fun b => if b then x else x] is not definitionally equal to [fun _ => x]. *) +Definition cat_binbiprod_diag {A : Type} + `{HasEquivs A, !IsPointedCat A} (x : A) `{!BinaryBiproduct x x} + : x $-> cat_binbiprod x x. +Proof. + snrapply cat_binbiprod_corec; exact (Id _). +Defined. + +Definition cat_binbiprod_codiag {A : Type} + `{HasEquivs A, !IsPointedCat A} (x : A) `{!BinaryBiproduct x x} + : cat_binbiprod x x $-> x. +Proof. + snrapply cat_binbiprod_rec; exact (Id _). +Defined. + +(** Compatability of [cat_binprod_rec] and [cat_binprod_corec]. *) +Definition cat_binbiprod_corec_rec {A : Type} + `{HasEquivs A, !IsPointedCat A} {w x y z : A} + `{!BinaryBiproduct w x, !BinaryBiproduct y z} + (f : w $-> y) (g : x $-> z) + : cat_binbiprod_corec (f $o cat_binbiprod_pr1) (g $o cat_binbiprod_pr2) + $== cat_binbiprod_rec (cat_binbiprod_inl $o f) (cat_binbiprod_inr $o g). +Proof. + unfold cat_binbiprod_corec, cat_binbiprod_rec. + nrefine (_ $@ _ $@ _). + 2: snrapply cat_biprod_corec_rec; by intros [|]. + 1: snrapply cat_biprod_corec_eta'; by intros [|]. + snrapply cat_biprod_rec_eta'; by intros [|]. +Defined. + +(** *** Binary biproduct bifunctor *) + +Global Instance is0bifunctor_cat_binbiprod {A : Type} + `{HasBinaryBiproducts A} + : Is0Bifunctor (fun x y : A => cat_binbiprod x y) + := is0bifunctor_cat_binprod. + +Global Instance is1bifunctor_cat_binbiprod {A : Type} + `{HasBinaryBiproducts A} + : Is1Bifunctor (fun x y : A => cat_binbiprod x y) + := is1bifunctor_cat_binprod. + +(** Binary biproducts are functorial in each argument. *) +Global Instance is0functor_cat_binbiprod_l {A : Type} + `{HasBinaryBiproducts A} (y : A) + : Is0Functor (fun x => cat_binbiprod x y) + := is0functor10_bifunctor _ y. + +Global Instance is1functor_cat_binbiprod_l {A : Type} + `{HasBinaryBiproducts A} (y : A) + : Is1Functor (fun x => cat_binbiprod x y) + := is1functor10_bifunctor _ y. + +Global Instance is0functor_cat_binbiprod_r {A : Type} + `{HasBinaryBiproducts A} (x : A) + : Is0Functor (fun y => cat_binbiprod x y) + := is0functor01_bifunctor _ x. + +Global Instance is1functor_cat_binbiprod_r {A : Type} + `{HasBinaryBiproducts A} (x : A) + : Is1Functor (fun y => cat_binbiprod x y) + := is1functor01_bifunctor _ x. + +(** *** Functor lemmas *) + +Definition cat_binbiprod_fmap01_corec {A : Type} + `{HasEquivs A, !IsPointedCat A, !HasBinaryBiproducts A} {w x y z : A} + (f : w $-> z) (g : x $-> y) (h : w $-> x) + : fmap01 (fun x y => cat_binbiprod x y) z g $o cat_binbiprod_corec f h + $== cat_binbiprod_corec f (g $o h). +Proof. + rapply cat_binprod_fmap01_corec. +Defined. + +Definition cat_binbiprod_fmap10_corec {A : Type} + `{HasEquivs A, !IsPointedCat A, !HasBinaryBiproducts A} {w x y z : A} + (f : x $-> y) (g : w $-> x) (h : w $-> z) + : fmap10 (fun x y => cat_binbiprod x y) f z $o cat_binbiprod_corec g h + $== cat_binbiprod_corec (f $o g) h. +Proof. + rapply cat_binprod_fmap10_corec. +Defined. + +Definition cat_binbiprod_fmap11_corec {A : Type} + `{HasEquivs A, !IsPointedCat A, !HasBinaryBiproducts A} {v w x y z : A} + (f : w $-> y) (g : x $-> z) (h : v $-> w) (i : v $-> x) + : fmap11 (fun x y => cat_binbiprod x y) f g $o cat_binbiprod_corec h i + $== cat_binbiprod_corec (f $o h) (g $o i). +Proof. + rapply cat_binprod_fmap11_corec. +Defined. + +Definition cat_binbiprod_diag_fmap11 {A : Type} + `{HasEquivs A, !IsPointedCat A, !HasBinaryBiproducts A} {x y : A} (f : x $-> y) + : cat_binbiprod_diag y $o f + $== fmap11 (fun x y => cat_binbiprod x y) f f $o cat_binbiprod_diag x. +Proof. + refine (_ $@ _^$). + 2: nrapply cat_binbiprod_fmap11_corec. + nrapply cat_binbiprod_pr_eta. + - refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ cat_idl _ $@ (cat_idr _)^$ $@ _^$). + 1,2: rapply cat_binbiprod_corec_beta_pr1. + - refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ cat_idl _ $@ (cat_idr _)^$ $@ _^$). + 1,2: rapply cat_binbiprod_corec_beta_pr2. +Defined. + +Definition cat_binbiprod_codiag_fmap11 {A : Type} + `{HasEquivs A, !IsPointedCat A, !HasBinaryBiproducts A} {x y : A} (f : x $-> y) + : f $o cat_binbiprod_codiag x + $== cat_binbiprod_codiag y $o fmap11 (fun x y => cat_binbiprod x y) f f. +Proof. + (* nrapply cat_binbiprod_in_eta. + - refine (cat_assoc _ _ _ $@ (_ $@L _) $@ cat_idr _ $@ _). + 1: nrapply cat_binbiprod_rec_beta_inl. + refine (_ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$). + 2: { + (* refine ((_ $@L _) $@ (cat_assoc _ _ _)^$). *) + refine (_^$ $@ (cat_binbiprod_corec_rec _ _ $@R _)^$). + nrapply cat_binbiprod_rec_beta_inl. } + refine (_ $@ (_ $@L _)). + 2: { + (* refine ((_ $@R _) $@ cat_assoc _ _ _). *) + refine ((_ $@ _)^$ $@ (cat_binbiprod_corec_rec _ _ $@R _)^$). + 1: nrapply cat_binbiprod_rec_beta_inl. + nrapply cat_idr. } + refine (_^$ $@ (_^$ $@R _) $@ cat_assoc _ _ _). + 2: nrapply cat_binbiprod_rec_beta_inl. + nrapply cat_idl; exact _. + - refine (cat_assoc _ _ _ $@ (_ $@L _) $@ cat_idr _ $@ _). + 1: nrapply cat_binbiprod_rec_beta_inr. + refine (_ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$). + 2: { refine ((_ $@L _) $@ (cat_assoc _ _ _)^$). + refine ((_ $@ _)^$ $@ (cat_binbiprod_corec_rec _ _ $@R _)^$). + 1: nrapply cat_binbiprod_rec_beta_inr. + nrapply cat_idr. } + refine (_ $@ (_ $@L _)). + 2: { refine ((_ $@R _) $@ _)^$. + 1: rapply cat_binbiprod_corec_rec. + nrapply cat_binbiprod_rec_beta_inr. } + refine (_^$ $@ (_^$ $@R _) $@ cat_assoc _ _ _). + 2: nrapply cat_binbiprod_rec_beta_inr. + nrapply cat_idl; exact _. *) +Admitted. + +(** *** Symmetry *) + +Section Symmetry. + Context {A : Type} `{HasBinaryBiproducts A}. + + Definition cat_binbiprod_swap (x y : A) + : cat_binbiprod x y $-> cat_binbiprod y x + := cat_binbiprod_corec cat_binbiprod_pr2 cat_binbiprod_pr1. + + Lemma cat_binbiprod_swap_swap (x y : A) + : cat_binbiprod_swap x y $o cat_binbiprod_swap y x $== Id _. + Proof. + rapply cat_binprod_swap_cat_binprod_swap. + Defined. + + Local Instance symmetricbraiding_cat_binbiprod + : SymmetricBraiding (fun x y => cat_binbiprod x y). + Proof. + rapply symmetricbraiding_binprod. + Defined. + + Lemma cat_binbiprod_swap_inl (x y : A) + : cat_binbiprod_swap x y $o cat_binbiprod_inl + $== cat_binbiprod_inr. + Proof. + nrapply cat_binbiprod_pr_eta. + - refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr1. + refine (_ $@ _^$). + 1: nrapply cat_binbiprod_pr2_inl. + nrapply cat_binbiprod_pr1_inr. + - refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr2. + refine (_ $@ _^$). + 1: nrapply cat_binbiprod_pr1_inl. + nrapply cat_binbiprod_pr2_inr. + Defined. + + Lemma cat_binbiprod_swap_inr (x y : A) + : cat_binbiprod_swap x y $o cat_binbiprod_inr + $== cat_binbiprod_inl. + Proof. + nrapply cat_binbiprod_pr_eta. + - refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr1. + refine (_ $@ _^$). + 1: nrapply cat_binbiprod_pr2_inr. + nrapply cat_binbiprod_pr1_inl. + - refine ((cat_assoc _ _ _)^$ $@ _). + refine ((_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr2. + refine (_ $@ _^$). + 1: nrapply cat_binbiprod_pr1_inr. + nrapply cat_binbiprod_pr2_inl. + Defined. + + (** The swap map preserves the diagonal. *) + Lemma cat_binbiprod_swap_diag (x : A) + : cat_binbiprod_swap x x $o cat_binbiprod_diag x $== cat_binbiprod_diag x. + Proof. + nrapply cat_binbiprod_pr_eta. + - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr1. + refine (cat_binbiprod_corec_beta_pr2 _ _ $@ _^$). + nrapply cat_binbiprod_corec_beta_pr1. + - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr2. + refine (cat_binbiprod_corec_beta_pr1 _ _ $@ _^$). + nrapply cat_binbiprod_corec_beta_pr2. + Defined. + + (** The swap map preserves the codiagonal. *) + Lemma cat_binbiprod_swap_codiag (x : A) + : cat_binbiprod_codiag x $o cat_binbiprod_swap x x $== cat_binbiprod_codiag x. + Proof. + nrapply cat_binbiprod_in_eta. + - refine (_ $@ (cat_binbiprod_rec_beta_inl _ _)^$). + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). + 1: nrapply cat_binbiprod_swap_inl. + nrapply cat_binbiprod_rec_beta_inr. + - refine (_ $@ (cat_binbiprod_rec_beta_inr _ _)^$). + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). + 1: nrapply cat_binbiprod_swap_inr. + nrapply cat_binbiprod_rec_beta_inl. + Defined. + +End Symmetry. + +(** *** Associativity of binary products *) + +Section Associativity. + + Context {A : Type} `{HasBinaryBiproducts A}. + + Local Instance associator_binbiprod + : Associator (fun x y => cat_binbiprod x y) + := associator_binprod. + + Lemma cate_binbiprod_assoc (x y z : A) + : cat_binbiprod x (cat_binbiprod y z) + $<~> cat_binbiprod (cat_binbiprod x y) z. + Proof. + rapply associator_binbiprod. + Defined. + + Definition cat_binbiprod_twist (x y z : A) + : cat_binbiprod x (cat_binbiprod y z) + $-> cat_binbiprod y (cat_binbiprod x z) + := cat_binprod_twist x y z. + + Lemma cat_binbiprod_twist_inl (x y z : A) + : cat_binbiprod_twist x y z $o cat_binbiprod_inl + $== cat_binbiprod_inr $o cat_binbiprod_inl. + Proof. + nrapply cat_binbiprod_pr_eta. + - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr1. + refine (cat_assoc _ _ _ $@ _ $@ cat_assoc _ _ _). + refine ((_ $@L _) $@ _ $@ (_^$ $@R _)). + 1: nrapply cat_binbiprod_pr2_inl. + 2: nrapply cat_binbiprod_pr1_inr. + refine (_ $@ _^$). + 1: nrapply cat_zero_r. + nrapply cat_zero_l. + - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_beta_pr2. + refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + refine (cat_binbiprod_rec_beta_inl _ _ $@ cat_idr _ $@ _). + refine ((cat_idl _)^$ $@ (_^$ $@R _) $@ cat_assoc _ _ _). + nrapply cat_binbiprod_pr2_inr. + Defined. + + Lemma cat_binbiprod_twist_inr_inl (x y z : A) + : cat_binbiprod_twist x y z $o cat_binbiprod_inr $o cat_binbiprod_inl + $== cat_binbiprod_inl. + Proof. + nrapply cat_binbiprod_pr_eta. + - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + 1: nrapply cat_binbiprod_corec_beta_pr1. } + refine (cat_assoc _ _ _ $@ _). + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_pr2_inr. + nrapply cat_idl. } + refine (_ $@ _^$). + 1,2: nrapply cat_binbiprod_pr1_inl. + - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + 1: nrapply cat_binbiprod_corec_beta_pr2. } + refine (cat_assoc _ _ _ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_rec. + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inr. + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). + 1: nrapply cat_binbiprod_pr2_inl. + refine (_ $@ _^$). + 1: nrapply cat_zero_r. + nrapply cat_binbiprod_pr2_inl. + Defined. + + Lemma cat_binbiprod_twist_inr_inr (x y z : A) + : cat_binbiprod_twist x y z $o cat_binbiprod_inr $o cat_binbiprod_inr + $== cat_binbiprod_inr $o cat_binbiprod_inr. + Proof. + nrapply cat_binbiprod_pr_eta. + - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + 1: nrapply cat_binbiprod_corec_beta_pr1. } + refine (cat_assoc _ _ _ $@ _). + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_pr2_inr. + nrapply cat_idl. } + refine (_ $@ _^$). + 1: nrapply cat_binbiprod_pr1_inr. + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_pr1_inr. + nrapply cat_zero_l. + - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + 1: nrapply cat_binbiprod_corec_beta_pr2. } + refine (cat_assoc _ _ _ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_corec_rec. + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_rec_beta_inr. + refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). + 1: nrapply cat_binbiprod_pr2_inr. + refine (cat_idr _ $@ _^$). + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _). + 1: nrapply cat_binbiprod_pr2_inr. + nrapply cat_idl. + Defined. + + Lemma cate_binbiprod_assoc_inl (x y z : A) + : cate_binbiprod_assoc x y z $o cat_binbiprod_inl + $== cat_binbiprod_inl $o cat_binbiprod_inl. + Proof. + refine ((_ $@R _) $@ _). + 1: nrapply Monoidal.associator_twist'_unfold. + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L (cat_assoc _ _ _ $@ (_ $@L _))) $@ _). + { refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ (_ $@ _)). + 1: nrapply cat_binbiprod_rec_beta_inl. + nrapply cat_idr. } + simpl. + refine ((_ $@L _) $@ _). + 1: nrapply cat_binbiprod_twist_inl. + refine ((cat_assoc _ _ _)^$ $@ _). + refine (_ $@R _). + nrapply cat_binbiprod_swap_inr. + Defined. + + Lemma cate_binbiprod_assoc_inr_inl (x y z : A) + : cate_binbiprod_assoc x y z $o cat_binbiprod_inr $o cat_binbiprod_inl + $== cat_binbiprod_inl $o cat_binbiprod_inr. + Proof. + refine (((_ $@R _) $@R _) $@ _). + 1: nrapply Monoidal.associator_twist'_unfold. + refine (cat_assoc _ _ _ $@ _). + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L (cat_assoc _ _ _ $@ (_ $@L _))) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + nrapply cat_binbiprod_rec_beta_inr. } + refine ((_ $@L _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ _). + refine (((cat_assoc _ _ _)^$ $@R _) $@ _). + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L _) $@ _). + 1: nrapply cat_binbiprod_swap_inl. + nrapply cat_binbiprod_twist_inr_inr. } + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + nrapply cat_binbiprod_swap_inr. + Defined. + + Lemma cate_binbiprod_assoc_inr_inr (x y z : A) + : cate_binbiprod_assoc x y z $o cat_binbiprod_inr $o cat_binbiprod_inr + $== cat_binbiprod_inr. + Proof. + refine (((_ $@R _) $@R _) $@ _). + 1: nrapply Monoidal.associator_twist'_unfold. + refine (cat_assoc _ _ _ $@ _). + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L (cat_assoc _ _ _ $@ (_ $@L _))) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)). + refine ((cat_binbiprod_corec_rec _ _ $@R _) $@ _). + nrapply cat_binbiprod_rec_beta_inr. } + refine ((_ $@L _) $@ _). + { refine ((cat_assoc _ _ _)^$ $@ _). + refine (((cat_assoc _ _ _)^$ $@R _) $@ _). + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L _) $@ _). + 1: nrapply cat_binbiprod_swap_inr. + nrapply cat_binbiprod_twist_inr_inl. } + nrapply cat_binbiprod_swap_inl. + Defined. + + Definition issymmetricmonoidal_cat_binbiprod + : IsSymmetricMonoidal A (fun x y => cat_binbiprod x y) zero_object. + Proof. + change (IsSymmetricMonoidal A (fun x y => cat_binprod x y) zero_object). + exact _. + Defined. + +End Associativity. + +(** *** Biproducts in the opposite category *) + +(** Biproducts exist in the opposite category if they exist in the original category. *) +Global Instance biproduct_op {I A : Type} {x : I -> A} `{Biproduct I A x} + : Biproduct (A:=A^op) I x. +Proof. + snrapply Build_Biproduct'. + (** Products in the opposite category are coproducts in the original category. *) + - exact _. + (** Coproducts in the opposite category are products in the original category. *) + - nrapply coproduct_op. + exact _. + - snrapply catie_homotopic. + + simpl; exact (cat_coprod_prod (A:=A) x). + + simpl; exact _. + + (** Showing that these two maps are homotopic is a bit tricky. *) + nrapply cat_coprod_in_eta. + intros i. + nrapply cat_prod_pr_eta. + intros j. + simpl. + refine (cat_assoc _ _ _ $@ _). + refine ((_ $@L _) $@ _). + 1: nrapply cat_coprod_beta. + refine (_ $@ _). + 1: nrapply cat_prod_beta. + symmetry. + refine ((_ $@R _) $@ _). + 1: nrapply cat_prod_beta. + refine (_ $@ _). + 1: nrapply cat_coprod_beta. + simpl. + generalize (dec_paths j i). + generalize (dec_paths i j). + intros p q. + destruct p as [p|np]. + * decidable_true q p^. + assert (r : p^ = x0) by apply path_ishprop. + destruct r. + destruct p. + reflexivity. + * destruct q. + 1: by destruct (np p^). + reflexivity. +Defined. + +Global Instance hasbiproducts_op {I A : Type} `{DecidablePaths I, HasEquivs A, !IsPointedCat A, !HasBiproducts I A} + : HasBiproducts I (A^op). +Proof. + intros x. + by rapply biproduct_op. +Defined. + +Global Instance binarybiproduct_op {A : Type} + `{HasEquivs A, !IsPointedCat A} {x y : A} {bb : BinaryBiproduct x y} + : BinaryBiproduct (A:=A^op) x y. +Proof. + nrapply biproduct_op. + exact bb. +Defined. + +Global Instance hasbinarybiproducts_op {A : Type} + `{HasEquivs A, !IsPointedCat A} {hbb : HasBinaryBiproducts A} + : HasBinaryBiproducts (A^op). +Proof. + intros x y. + rapply biproduct_op. + exact (hbb x y). +Defined. diff --git a/theories/Algebra/Homological/End.v b/theories/Algebra/Homological/End.v new file mode 100644 index 00000000000..4f5f07ece85 --- /dev/null +++ b/theories/Algebra/Homological/End.v @@ -0,0 +1,29 @@ +Require Import Basics.Overture. +Require Import WildCat.Core. +Require Import Algebra.AbGroups.AbelianGroup Algebra.Rings.Ring. +Require Import canonical_names. + +Require Import Algebra.Homological.Additive. + +(** * Endomorphism Rings *) + +Definition End {A : Type} `{IsAdditive A} (X : A) : Ring. +Proof. + snrapply Build_Ring; repeat split. + - exact (AbHom X X). + - exact (fun f g => f $o g). + - exact (Id _). + - exact left_heterodistribute_hom. + - exact right_heterodistribute_hom. + - exact _. + - intros f g h. + apply path_hom. + symmetry. + nrapply cat_assoc. + - intros f. + apply path_hom. + nrapply cat_idl. + - intros g. + apply path_hom. + nrapply cat_idr. +Defined. diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v index 865f8ceb6b6..f6625ba4560 100644 --- a/theories/WildCat/Bifunctor.v +++ b/theories/WildCat/Bifunctor.v @@ -355,6 +355,15 @@ Proof. exact _. Defined. +Global Instance is1functor_uncurry_uncurry_left {A B C D E} + (F : A -> B -> C) (G : C -> D -> E) + `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D, Is1Cat E, + !Is0Bifunctor F, !Is1Bifunctor F, !Is0Bifunctor G, !Is1Bifunctor G} + : Is1Functor (uncurry (uncurry (fun x y z => G (F x y) z))). +Proof. + exact _. +Defined. + Global Instance is0functor_uncurry_uncurry_right {A B C D E} (F : A -> B -> D) (G : C -> D -> E) `{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E, @@ -366,6 +375,21 @@ Proof. exact (fmap11 G h (fmap11 F f g)). Defined. +Global Instance is1functor_uncurry_uncurry_right {A B C D E} + (F : A -> B -> D) (G : C -> D -> E) + `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D, Is1Cat E, + !Is0Bifunctor F, !Is1Bifunctor F, !Is0Bifunctor G, !Is1Bifunctor G} + : Is1Functor (uncurry (uncurry (fun x y z => G x (F y z)))). +Proof. + snrapply Build_Is1Functor. + - intros cab cab' [[h f] g] [[h' f'] g'] [[q p] r]. + exact (fmap22 G q (fmap22 F p r)). + - intros cab. + exact (fmap12 G _ (fmap11_id F _ _) $@ fmap11_id G _ _). + - intros cab cab' cab'' [[h f] g] [[h' f'] g']. + exact (fmap12 G _ (fmap11_comp F _ _ _ _) $@ fmap11_comp G _ _ _ _). +Defined. + Definition fmap11_square {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} {a00 a20 a02 a22 : A} {f10 : a00 $-> a20} {f12 : a02 $-> a22} diff --git a/theories/WildCat/Coproducts.v b/theories/WildCat/Coproducts.v index 2c700a69b75..2f7dc029063 100644 --- a/theories/WildCat/Coproducts.v +++ b/theories/WildCat/Coproducts.v @@ -3,7 +3,7 @@ Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans WildCat.Opposite WildCat.Products WildCat.Universe WildCat.Yoneda WildCat.ZeroGroupoid WildCat.PointedCat - WildCat.Monoidal. + WildCat.Monoidal WildCat.Bifunctor. (** * Categories with coproducts *) @@ -51,7 +51,7 @@ Section Lemmata. : yon_0gpd z (cat_coprod I x) $<~> prod_0gpd I (fun i => yon_0gpd z (x i)) := cate_cat_prod_corec_inv I (A:=A^op) (x:=x). - Definition cate_cate_coprod_rec {z : A} + Definition cate_cat_coprod_rec {z : A} : prod_0gpd I (fun i => yon_0gpd z (x i)) $<~> yon_0gpd z (cat_coprod I x) := cate_cat_prod_corec I (A:=A^op) (x:=x). @@ -83,7 +83,7 @@ End Lemmata. (** *** Codiagonal / fold map *) -Definition cat_coprod_fold {I : Type} {A : Type} (x : A) `{Coproduct I _ (fun _ => x)} +Definition cat_coprod_codiag {I : Type} {A : Type} (x : A) `{Coproduct I _ (fun _ => x)} : cat_coprod I (fun _ => x) $-> x := cat_prod_diag (A:=A^op) x. @@ -141,9 +141,9 @@ Defined. (** *** Binary coproducts *) Class BinaryCoproduct {A : Type} `{Is1Cat A} (x y : A) - := prod_co_bincoprod :: BinaryProduct (x : A^op) (y : A^op). + := prod_co_bincoprod :: BinaryProduct (A:=A^op) x y. -Definition cat_bincoprod {A : Type} `{Is1Cat A} (x y : A) `{!BinaryCoproduct x y} : A +Definition cat_bincoprod {A : Type} `{Is1Cat A} (x y : A) `{!BinaryCoproduct x y} : A := cat_binprod (x : A^op) y. Definition cat_inl {A : Type} `{Is1Cat A} {x y : A} `{!BinaryCoproduct x y} @@ -211,25 +211,6 @@ Section Lemmata. := @cat_binprod_corec_eta A^op _ _ _ _ x y _ _ f f' g g'. End Lemmata. -(** *** Symmetry of coproducts *) - -Definition cate_bincoprod_swap {A : Type} `{HasEquivs A} - {e : HasBinaryCoproducts A} (x y : A) - : cat_bincoprod x y $<~> cat_bincoprod y x. -Proof. - exact (@cate_binprod_swap A^op _ _ _ _ _ e _ _). -Defined. - -(** *** Associativity of coproducts *) - -Lemma cate_coprod_assoc {A : Type} `{HasEquivs A} - {e : HasBinaryCoproducts A} (x y z : A) - : cat_bincoprod x (cat_bincoprod y z) - $<~> cat_bincoprod (cat_bincoprod x y) z. -Proof. - exact (@associator_binprod A^op _ _ _ _ _ e x y z)^-1$. -Defined. - (** *** Binary coproduct functor *) (** Hint: Use [Set Printing Implicit] to see the implicit arguments in the following proofs. *) @@ -266,6 +247,156 @@ Proof. exact (is1functor_cat_binprod_r (A:=A^op) (H0:=H0) x). Defined. +Global Instance is0bifunctor_cat_bincoprod {A : Type} + `{H0 : HasBinaryCoproducts A} + : Is0Bifunctor (fun x y => cat_bincoprod x y). +Proof. + nrapply is0bifunctor_op'. + exact (is0bifunctor_cat_binprod (A:=A^op) (H0:=H0)). +Defined. + +Global Instance is1bifunctor_cat_bincoprod {A : Type} + `{H0 : HasBinaryCoproducts A} + : Is1Bifunctor (fun x y => cat_bincoprod x y). +Proof. + nrapply is1bifunctor_op'. + exact (is1bifunctor_cat_binprod (A:=A^op) (H0:=H0)). +Defined. + +(** *** Products and coproducts in the opposite category *) + +Definition hasbinarycoproducts_op_hasbinaryproducts {A : Type} + `{H : HasBinaryProducts A} + : HasBinaryCoproducts A^op + := H. +Hint Immediate hasbinarycoproducts_op_hasbinaryproducts : typeclass_instances. + +Definition hasbinarycoproducts_hasbinaryproducts_op {A : Type} + `{HasEquivs A, H' : !HasBinaryProducts A^op} + : HasBinaryCoproducts A + := H'. +Hint Immediate hasbinarycoproducts_hasbinaryproducts_op : typeclass_instances. + +Definition hasbinaryproducts_op_hasbinarycoproducts {A : Type} + `{H : HasBinaryCoproducts A} + : HasBinaryProducts A^op + := H. +Hint Immediate hasbinarycoproducts_op_hasbinaryproducts : typeclass_instances. + +Definition hasbinaryproducts_hasbinarycoproducts_op {A : Type} + `{HasEquivs A, H' : !HasBinaryCoproducts A^op} + : HasBinaryProducts A + := H'. +Hint Immediate hasbinaryproducts_hasbinarycoproducts_op : typeclass_instances. + +(** *** Symmetry of coproducts *) + +Definition cat_bincoprod_swap {A : Type} `{HasEquivs A} + {e : HasBinaryCoproducts A} (x y : A) + : cat_bincoprod x y $-> cat_bincoprod y x. +Proof. + exact (@cat_binprod_swap A^op _ _ _ _ e _ _). +Defined. + +Definition cate_bincoprod_swap {A : Type} `{HasEquivs A} + {e : HasBinaryCoproducts A} (x y : A) + : cat_bincoprod x y $<~> cat_bincoprod y x. +Proof. + exact (@cate_binprod_swap A^op _ _ _ _ _ e _ _). +Defined. + +(** *** Associativity of coproducts *) + +Lemma cate_coprod_assoc {A : Type} `{HasEquivs A} + {e : HasBinaryCoproducts A} (x y z : A) + : cat_bincoprod x (cat_bincoprod y z) + $<~> cat_bincoprod (cat_bincoprod x y) z. +Proof. + exact (@associator_binprod A^op _ _ _ _ _ e x y z)^-1$. +Defined. + +Definition associator_cat_bincoprod {A : Type} `{HasEquivs A} + {e : HasBinaryCoproducts A} + : Associator (fun x y => cat_bincoprod x y). +Proof. + unfold Associator. + snrapply associator_op'. + 1: exact _. + nrapply associator_binprod. +Defined. + +(** *** Codiagonal *) + +Definition cat_bincoprod_codiag {A : Type} + `{HasEquivs A} (x : A) `{!BinaryCoproduct x x} + : cat_bincoprod x x $-> x + := cat_binprod_diag (A:=A^op) x. + +(** *** Lemmas about [cat_bincoprod_rec] *) + +Definition cat_bincoprod_fmap01_rec {A : Type} + `{Is1Cat A, !HasBinaryCoproducts A} {w x y z : A} + (f : z $-> w) (g : y $-> x) (h : x $-> w) + : cat_bincoprod_rec f h $o fmap01 (fun x y => cat_bincoprod x y) z g + $== cat_bincoprod_rec f (h $o g) + := @cat_binprod_fmap01_corec A^op _ _ _ _ + hasbinaryproducts_op_hasbinarycoproducts _ _ _ _ f g h. + +Definition cat_bincoprod_fmap10_rec {A : Type} + `{Is1Cat A, !HasBinaryCoproducts A} {w x y z : A} + (f : y $-> x) (g : x $-> w) (h : z $-> w) + : cat_bincoprod_rec g h $o fmap10 (fun x y => cat_bincoprod x y) f z + $== cat_bincoprod_rec (g $o f) h + := @cat_binprod_fmap10_corec A^op _ _ _ _ + hasbinaryproducts_op_hasbinarycoproducts _ _ _ _ f g h. + +Definition cat_bincoprod_fmap11_rec {A : Type} + `{Is1Cat A, !HasBinaryCoproducts A} {v w x y z : A} + (f : y $-> w) (g : z $-> x) (h : w $-> v) (i : x $-> v) + : cat_bincoprod_rec h i $o fmap11 (fun x y => cat_binprod x y) f g + $== cat_bincoprod_rec (h $o f) (i $o g) + := @cat_binprod_fmap11_corec A^op _ _ _ _ + hasbinaryproducts_op_hasbinarycoproducts _ _ _ _ _ f g h i. + +Definition cat_bincoprod_rec_associator {A : Type} `{HasEquivs A} + `{!HasBinaryCoproducts A} {w x y z : A} (f : w $-> z) (g : x $-> z) (h : y $-> z) + : cat_bincoprod_rec (cat_bincoprod_rec f g) h $o associator_cat_bincoprod w x y + $== cat_bincoprod_rec f (cat_bincoprod_rec g h). +Proof. + nrapply cate_moveR_eV. + symmetry. + (** TODO not sure why this can't be inlined *) + pose (X := @cat_binprod_associator_corec A^op _ _ _ _ _ + hasbinaryproducts_op_hasbinarycoproducts _ _ _ _ f g h). + exact X. +Defined. + +Definition cat_bincoprod_swap_rec {A : Type} `{HasEquivs A} + `{!HasBinaryCoproducts A} {a b c : A} (f : a $-> c) (g : b $-> c) + : cat_bincoprod_rec f g $o cat_bincoprod_swap b a $== cat_bincoprod_rec g f + := @cat_binprod_swap_corec A^op _ _ _ _ + hasbinaryproducts_op_hasbinarycoproducts _ _ _ _ _. + +(** *** Cocartesian Monoidal Structure *) + +Global Instance ismonoidal_cat_bincoprod {A : Type} `{HasEquivs A} + {e : HasBinaryCoproducts A} (zero : A) `{!IsInitial zero} + : IsMonoidal A (fun x y => cat_bincoprod x y) zero. +Proof. + nrapply ismonoidal_op'. + nrapply (ismonoidal_binprod (A:=A^op) zero). + by nrapply isterminal_op_isinitial. +Defined. + +Global Instance issymmetricmonoidal_cat_bincoprod {A : Type} `{HasEquivs A} + {e : HasBinaryCoproducts A} (zero : A) `{!IsInitial zero} + : IsSymmetricMonoidal A (fun x y => cat_bincoprod x y) zero. +Proof. + nrapply issymmetricmonoidal_op'. + nrapply (issymmetricmonoidal_binprod (A :=A^op) zero). + by nrapply isterminal_op_isinitial. +Defined. + (** *** Coproducts in Type *) (** [Type] has all coproducts. *) @@ -303,3 +434,19 @@ Proof. exact (Id _). - apply zero_morphism. Defined. + +Definition cat_bincoprod_binprod {A : Type} `{Is1Cat A, !IsPointedCat A} + (x y : A) `{!BinaryCoproduct x y, !BinaryProduct x y} + : cat_bincoprod x y $-> cat_binprod x y. +Proof. + nrapply cat_coprod_prod; exact _. +Defined. + +(** *** Coproducts in the opposite category *) + +Definition coproduct_op {I A : Type} (x : I -> A) + `{Is1Cat A} {H' : Product I x} + : Coproduct I (A:=A^op) x + := H'. + +Hint Immediate coproduct_op : typeclass_instances. diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v index bdbbce2df1d..cb39ac4d3ae 100644 --- a/theories/WildCat/Monoidal.v +++ b/theories/WildCat/Monoidal.v @@ -124,8 +124,8 @@ Class IsMonoidal (A : Type) `{HasEquivs A} (** These all satisfy the following properties: *) := { (** A [cat_tensor] is a 1-bifunctor. *) - is0bifunctor_cat_tensor :: Is0Bifunctor cat_tensor; - is1bifunctor_cat_tensor :: Is1Bifunctor cat_tensor; + is0bifunctor_cat_tensor : Is0Bifunctor cat_tensor; + is1bifunctor_cat_tensor : Is1Bifunctor cat_tensor; (** A natural isomorphism [associator] witnessing the associativity of the tensor product. *) cat_tensor_associator :: Associator cat_tensor; (** A natural isomorphism [left_unitor] witnessing the left unit law. *) @@ -138,6 +138,9 @@ Class IsMonoidal (A : Type) `{HasEquivs A} cat_tensor_pentagon_identity :: PentagonIdentity cat_tensor; }. +Existing Instance is0bifunctor_cat_tensor | 10. +Existing Instance is1bifunctor_cat_tensor | 10. + (** TODO: Braided monoidal categories *) (** ** Symmetric Monoidal Categories *) @@ -207,6 +210,11 @@ Section Associator. End Associator. +Definition associator_op' {A : Type} `{HasEquivs A} {F : A -> A -> A} + `{!Is0Bifunctor F, !Is1Bifunctor F, assoc : !Associator (A:=A^op) F} + : Associator F + := associator_op (A:=A^op) (assoc := assoc). + (** ** Theory about [LeftUnitor] and [RightUnitor] *) Section LeftUnitor. @@ -223,14 +231,15 @@ End LeftUnitor. (** ** Theory about [Braiding] *) -Section Braiding. - Context {A : Type} `{HasEquivs A} {F : A -> A -> A} - `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding F}. - - Global Instance braiding_op : Braiding (A:=A^op) F - := (nattrans_op (nattrans_flip braid)). +Global Instance braiding_op {A : Type} `{HasEquivs A} {F : A -> A -> A} + `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding F} + : Braiding (A:=A^op) F + := (nattrans_op (nattrans_flip braid)). -End Braiding. +Definition braiding_op' {A : Type} `{HasEquivs A} {F : A -> A -> A} + `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding (A:=A^op) F} + : Braiding F + := braiding_op (A:=A^op) (braid := braid). (** ** Theory about [SymmetricBraid] *) @@ -425,6 +434,12 @@ Section SymmetricBraid. End SymmetricBraid. +Definition symmetricbraiding_op' {A : Type} {F : A -> A -> A} + `{HasEquivs A, !Is0Bifunctor F, !Is1Bifunctor F, + H' : !SymmetricBraiding (A:=A^op) F} + : SymmetricBraiding F + := symmetricbraiding_op (A:=A^op) (F := F). + (** ** Opposite Monoidal Categories *) Global Instance ismonoidal_op {A : Type} (tensor : A -> A -> A) (unit : A) @@ -451,8 +466,52 @@ Proof. rapply cat_tensor_pentagon_identity. Defined. -(** ** Further Coherence Conditions *) +Definition ismonoidal_op' {A : Type} (tensor : A -> A -> A) (unit : A) + `{HasEquivs A} `{!IsMonoidal A^op tensor unit} + : IsMonoidal A tensor unit + := ismonoidal_op (A:=A^op) tensor unit. +Global Instance issymmetricmonoidal_op {A : Type} (tensor : A -> A -> A) (unit : A) + `{IsSymmetricMonoidal A tensor unit} + : IsSymmetricMonoidal A^op tensor unit. +Proof. + snrapply Build_IsSymmetricMonoidal. + - rapply ismonoidal_op. + - rapply symmetricbraiding_op. + - intros a b c; unfold op in a, b, c; simpl. + snrefine (_ $@ (_ $@L (_ $@R _))). + 2: exact ((braide _ _)^-1$). + 2: { nrapply cate_moveR_V1. + symmetry. + nrefine ((_ $@R _) $@ _). + 1: nrapply cate_buildequiv_fun. + rapply braid_braid. } + snrefine ((_ $@R _) $@ _). + { refine (emap _ _)^-1$. + rapply braide. } + { symmetry. + refine (cate_inv_adjointify _ _ _ _ $@ fmap2 _ _). + nrapply cate_inv_adjointify. } + snrefine ((_ $@L (_ $@L _)) $@ _). + { refine (emap (flip tensor c) _)^-1$. + rapply braide. } + { symmetry. + refine (cate_inv_adjointify _ _ _ _ $@ fmap2 _ _). + nrapply cate_inv_adjointify. } + refine ((_ $@L _)^$ $@ _^$ $@ cate_inv2 _ $@ _ $@ (_ $@L _)). + 1,2,4,5: rapply cate_inv_compose'. + refine (_ $@ (_ $@@ _) $@ _ $@ (_ $@R _)^$ $@ _^$). + 1-3,5-6: rapply cate_buildequiv_fun. + refine ((fmap02 _ _ _ $@@ ((_ $@ fmap20 _ _ _) $@R _)) $@ cat_symm_tensor_hexagon a b c $@ ((_ $@L _^$) $@R _)). + 1-4: nrapply cate_buildequiv_fun. +Defined. + +Definition issymmetricmonoidal_op' {A : Type} (tensor : A -> A -> A) (unit : A) + `{HasEquivs A} `{H' : !IsSymmetricMonoidal A^op tensor unit} + : IsSymmetricMonoidal A tensor unit + := issymmetricmonoidal_op (A:=A^op) tensor unit. + +(** ** Further Coherence Conditions *) (** In MacLane's original axiomatisation of a monoidal category, 3 extra coherence conditions were given in addition to the pentagon and triangle identities. It was later shown by Kelly that these axioms are redundant and follow from the rest. We reproduce these arguments here. *) (** The left unitor of a tensor can be decomposed as an associator and a functorial action of the tensor on a left unitor. *) @@ -527,7 +586,7 @@ Defined. (** TODO: Kelly also shows that there are redundant coherence conditions for symmetric monoidal categories also, but we leave these out for now. *) -(** ** Building Symmetric Monoidal Categories *) +(** ** The Twist Construction *) (** The following construction is what we call the "twist construction". It is a way to build a symmetric monoidal category from simpler pieces than the axioms ask for. diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v index 1c515862c38..8d26289d5bf 100644 --- a/theories/WildCat/Opposite.v +++ b/theories/WildCat/Opposite.v @@ -127,10 +127,10 @@ Proof. refine (@isequiv_Htpy_path _ _ _ _ _ H0 b a f g). Defined. -Global Instance isinitial_isterminal_op {A : Type} `{Is1Cat A} (x : A) +Global Instance isinitial_op_isterminal {A : Type} `{Is1Cat A} (x : A) {t : IsTerminal x} : IsInitial (A := A^op) x := t. -Global Instance isterminal_isinitial_op {A : Type} `{Is1Cat A} (x : A) +Global Instance isterminal_op_isinitial {A : Type} `{Is1Cat A} (x : A) {i : IsInitial x} : IsTerminal (A := A^op) x := i. diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v index da9236bbb3b..12d186c22ba 100644 --- a/theories/WildCat/Products.v +++ b/theories/WildCat/Products.v @@ -567,6 +567,8 @@ Proof. snrapply cat_binprod_corec; exact (Id _). Defined. +(** *** Lemmas about [cat_binprod_corec] *) + Definition cat_binprod_fmap01_corec {A : Type} `{Is1Cat A, !HasBinaryProducts A} {w x y z : A} (f : w $-> z) (g : x $-> y) (h : w $-> x)