From 3ff9195c49edb634b666da0675cb19ec1b7fb1fa Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 12 Mar 2020 01:34:11 +0900 Subject: [PATCH 1/2] define product functor as a first step towards monoidal category --- closed_category.v | 49 ++++ monoidal_category.v | 589 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 638 insertions(+) create mode 100644 closed_category.v create mode 100644 monoidal_category.v diff --git a/closed_category.v b/closed_category.v new file mode 100644 index 00000000..2b88f593 --- /dev/null +++ b/closed_category.v @@ -0,0 +1,49 @@ +From mathcomp Require Import all_ssreflect. +From mathcomp Require Import boolp. +Require Import monae_lib category. + +(* +In this file: +1. categories with finite products +2. categories with pullbacks +2.99. universal arrow (for defining 3) +3. finitely complete categories (categories with finite limits) +4. categories with morphism comprehension +5. cartesian closed categories + +3 subsumes 1 and 2. +5 = 1 + 4 + exponentiation axiom. + + +In monoidal_category.v: +M1. monoidal cateogories +M2. monoidal closed categories + +M2 subsumes 5. +*) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + + +Module CatWithFinProd. +Section def. +Record mixin_of (C : category) : Type := Mixin { + prod : C -> C -> C; + fst : forall a b, {hom prod a b, a}; + snd : forall a b, {hom prod a b, b}; + univ : forall c a b, {hom c,a} -> {hom c,b} -> {hom c, prod a b}; + _ : forall c a b (f : {hom c,a}) (g : {hom c,b}), + f = [hom of (fst a b) \o (univ f g)]; +}. +Record class_of (T : Type) : Type := Class { + base : Category.mixin_of T; + mixin : mixin_of (Category.Pack base); +}. +Structure t : Type := Pack { T : Type; class : class_of T }. +End def. +Module Exports. +End Exports. +End CatWithFinProd. +Export CatWithFinProd.Exports. diff --git a/monoidal_category.v b/monoidal_category.v new file mode 100644 index 00000000..14f2081c --- /dev/null +++ b/monoidal_category.v @@ -0,0 +1,589 @@ +From mathcomp Require Import all_ssreflect. +From mathcomp Require Import boolp. +Require Import monae_lib category. + +(* +In this file: + +- product category (product of two categories) + +M1. monoidal cateogories +M2. monoidal closed categories +*) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(* A concrete category isomorphic to the product category of C and D *) +(* sum version *) +Module ProductCategory. +Section def. +Variable C D : category. +Definition obj := (C * D)%type. +Definition el (X : obj) : Type := (El X.1 + El X.2)%type. +Definition separated (X Y : obj) (f : el X -> el Y) : Prop := + (forall x : El X.1, exists y : El Y.1, f (inl x) = inl y) /\ + (forall x : El X.2, exists y : El Y.2, f (inr x) = inr y). + +Section sepfstsnd. +Let _sepfst (X Y : obj) (f : el X -> el Y) : separated f -> El X.1 -> El Y.1. +case=> H _ x. +move/cid: (H x)=> [] y _. +exact y. +Defined. +Definition sepfst := Eval hnf in _sepfst. +Let _sepsnd (X Y : obj) (f : el X -> el Y) : separated f -> El X.2 -> El Y.2. +case=> _ H x. +move/cid: (H x)=> [] y _. +exact y. +Defined. +Definition sepsnd := Eval hnf in _sepsnd. +End sepfstsnd. + +Lemma sepfstK X Y (f : el X -> el Y) (Hf : separated f) (x : El X.1) : + inl (sepfst Hf x) = f (inl x). +Proof. +move: f Hf x. +case: X=> X1 X2; case:Y=> Y1 Y2 /= f [] /= Hf1 Hf2 x. +by case: (cid (Hf1 x))=> y ->. +Qed. +Lemma sepsndK X Y (f : el X -> el Y) (Hf : separated f) (x : El X.2) : + inr (sepsnd Hf x) = f (inr x). +Proof. +move: f Hf x. +case: X=> X1 X2; case:Y=> Y1 Y2 /= f [] /= Hf1 Hf2 x. +by case: (cid (Hf2 x))=> y ->. +Qed. +Definition inhom (A B : obj) (f : el A -> el B) : Prop := + exists H : separated f, InHom (sepfst H) /\ InHom (sepsnd H). +Lemma idfun_separated (X : obj) : @separated X X idfun. +Proof. by split; move=> x; exists x. Qed. +Lemma comp_separated (X Y Z : obj) (f :el X -> el Y) (g : el Y -> el Z) : + separated f -> separated g -> separated (g \o f). +Proof. +move: f g. +case: X=> X1 X2; case: Y=> Y1 Y2; case: Z=> Z1 Z2 f g [] /= Hf1 Hf2 [] /= Hg1 Hg2; split. +- by move=> x; case/cid: (Hf1 x)=> y /= ->; case/cid: (Hg1 y)=> z /= ->; exists z. +- by move=> x; case/cid: (Hf2 x)=> y /= ->; case/cid: (Hg2 y)=> z /= ->; exists z. +Qed. +Lemma sepfst_idfun X : sepfst (idfun_separated X) = idfun. +Proof. +apply funext=> x /=. +suff: inl (B:=El X.2) (sepfst (idfun_separated X) x) = inl x by move=> [=]. +by rewrite sepfstK. +Qed. +Lemma sepsnd_idfun X : sepsnd (idfun_separated X) = idfun. +Proof. +apply funext=> x /=. +suff: inr (A:=El X.1) (sepsnd (idfun_separated X) x) = inr x by move=> [=]. +by rewrite sepsndK. +Qed. +Lemma sepfst_comp X Y Z (f : el X -> el Y) (g : el Y -> el Z) + (Hf : separated f) (Hg : separated g) : + sepfst (comp_separated Hf Hg) = sepfst Hg \o sepfst Hf. +Proof. +apply funext=> x /=. +suff: inl (B:=El Z.2) (sepfst (comp_separated Hf Hg) x) = inl (sepfst Hg (sepfst Hf x)) + by move => [=]. +by rewrite 3!sepfstK. +Qed. +Lemma sepsnd_comp X Y Z (f : el X -> el Y) (g : el Y -> el Z) + (Hf : separated f) (Hg : separated g) : + sepsnd (comp_separated Hf Hg) = sepsnd Hg \o sepsnd Hf. +Proof. +apply funext=> x /=. +suff: inr (A:=El Z.1) (sepsnd (comp_separated Hf Hg) x) = inr (sepsnd Hg (sepsnd Hf x)) + by move => [=]. +by rewrite 3!sepsndK. +Qed. +Definition mixin : Category.mixin_of (C * D). +refine (@Category.Mixin obj el inhom _ _). +- by move=> X; exists (idfun_separated X); rewrite sepfst_idfun sepsnd_idfun; split; apply id_in_hom. +- by move=> X Y Z f g [] sf [] homfl homfr [] sg [] homgl homgr ; exists (comp_separated sf sg); rewrite sepfst_comp sepsnd_comp; split; apply funcomp_in_hom. +Defined. +End def. +End ProductCategory. +Definition productCategory (C D : category) := Category.Pack (ProductCategory.mixin C D). + +Canonical productCategory. + +Section prodcat_homfstsnd. +Variables A B : category. +Section homfstsnd. +Let _homfst (x y : A * B) (f : {hom x,y}) : {hom x.1, y.1}. +case:f => f. +case/cid=> sf [] Hf _. +exact: (HomPack Hf). +Defined. +Definition homfst := Eval hnf in _homfst. +Let _homsnd (x y : A * B) (f : {hom x,y}) : {hom x.2, y.2}. +case:f => f. +case/cid=> sf [] _ Hf. +exact: (HomPack Hf). +Defined. +Definition homsnd := Eval hnf in _homsnd. +End homfstsnd. +Lemma homfst_idfun x : homfst (x:=x) [hom of idfun] = [hom of idfun]. +Proof. +apply/hom_ext; rewrite boolp.funeqE => x1 /=. +case: cid => i [i1 i2] /=. +rewrite (_ : i = ProductCategory.idfun_separated _) ?ProductCategory.sepfst_idfun //. +exact/Prop_irrelevance. +Qed. +Lemma homsnd_idfun x : homsnd (x:=x) [hom of idfun] = [hom of idfun]. +Proof. +apply/hom_ext; rewrite boolp.funeqE => x1 /=. +case: cid => i [i1 i2] /=. +rewrite (_ : i = ProductCategory.idfun_separated _) ?ProductCategory.sepsnd_idfun //. +exact/Prop_irrelevance. +Qed. +Lemma homfst_comp (x y z : A * B) (f : {hom x,y}) (g : {hom y,z}) : + homfst [hom of g \o f] = [hom of homfst g \o homfst f]. +Proof. +rewrite /homfst /=. +case: cid => //= gh [gh1 gh2]. +apply/hom_ext => /=. +destruct g as [g g']. +destruct f as [f f']. +case: cid => g_ [g1 g2]. +case: cid => f_ [f1 f2] /=. +rewrite -ProductCategory.sepfst_comp. +congr (ProductCategory.sepfst _ _). +exact/Prop_irrelevance. +Qed. +Lemma homsnd_comp (x y z : A * B) (f : {hom x,y}) (g : {hom y,z}) : + homsnd [hom of g \o f] = [hom of homsnd g \o homsnd f]. +Proof. +rewrite /homsnd /=. +case: cid => //= gh [gh1 gh2]. +apply/hom_ext => /=. +destruct g as [g g']. +destruct f as [f f']. +case: cid => g_ [g1 g2]. +case: cid => f_ [f1 f2] /=. +rewrite -ProductCategory.sepsnd_comp. +congr (ProductCategory.sepsnd _ _). +exact/Prop_irrelevance. +Qed. +Lemma homfstK (x y : A * B) (f : {hom x,y}) (i : El x.1) : inl (homfst f i) = f (inl i). +Proof. +case: f=> /= f Hf. +case: (cid _)=> -[] sf1 sf2 [] Hf1 Hf2 /=. +by case: (cid _)=> j ->. +Qed. +Lemma homsndK (x y : A * B) (f : {hom x,y}) (i : El x.2) : inr (homsnd f i) = f (inr i). +Proof. +case: f=> /= f Hf. +case: (cid _)=> -[] sf1 sf2 [] Hf1 Hf2 /=. +by case: (cid _)=> j ->. +Qed. +End prodcat_homfstsnd. + +Section prodCat_pairhom. +Variables A B : category. +Variables a1 a2 : A. +Variables b1 b2 : B. +Variables (f : {hom a1, a2}) (g : {hom b1, b2}). +Let C := productCategory A B. +Definition pairhom' (ab : El a1 + El b1) : El a2 + El b2 := + match ab with + | inl a => inl (f a) + | inr b => inr (g b) + end. +Lemma pairhom'_in_hom : + @InHom C _ _ (pairhom' : El (a1,b1).1 + El (a1,b1).2 -> + El (a2,b2).1 + El (a2,b2).2). +Proof. +rewrite /InHom /= /ProductCategory.inhom /=. +set s := ProductCategory.separated _. +have [/= s1 s2] : s by split => /= x; [exists (f x) | exists (g x)]. +exists (conj s1 s2); split. +- set h := ProductCategory.sepfst _. + rewrite (_ : h = f); first exact: Hom.class. + by rewrite boolp.funeqE => ?; rewrite /h /=; case: cid => ? []. +- set h := ProductCategory.sepsnd _. + rewrite (_ : h = g); first exact: Hom.class. + by rewrite boolp.funeqE => ?; rewrite /h /=; case: cid => ? []. +Qed. +Definition pairhom : {hom (a1, b1), (a2, b2)} := Hom.Pack _ pairhom'_in_hom. +End prodCat_pairhom. + +Section pairhom_idfun. +Variables (A B : category) (a : A) (b : B). +Lemma pairhom_idfun : pairhom (a1:=a) (b1:=b) [hom of idfun] [hom of idfun] = [hom of idfun]. +Proof. by apply/hom_ext/funext=> -[] x /=. Qed. +End pairhom_idfun. + +Section pairhom_comp. +Variables (A B : category) (a1 a2 a3 : A) (b1 b2 b3 : B). +Variables (fa : {hom a1,a2}) (ga : {hom a2,a3}) (fb : {hom b1,b2}) (gb : {hom b2,b3}). +Lemma pairhom_comp : pairhom [hom of ga \o fa] [hom of gb \o fb] = + [hom of pairhom ga gb \o pairhom fa fb]. +Proof. by apply /hom_ext/funext=> -[] x. Qed. +End pairhom_comp. + +(* couldn't avoid the horrible eq_rect *) +(* +Section pairhomK'. +Variables A B : category. +Variables x y : A * B. +Definition pairhomK'_eq : {hom x,y} = {hom (x.1, x.2), (y.1, y.2)}. +refine (match x with (x1,x2)=> _ end). +refine (match y with (y1,y2)=> _ end). +exact erefl. +Defined. +Lemma pairhomK' (f : {hom x,y}) : pairhom (homfst f) (homsnd f) = + eq_rect _ id f _ pairhomK'_eq. +Proof. +rewrite /pairhomK'_eq. +move: x y f=> [] x1 x2 [] y1 y2 f /=. +apply/hom_ext/funext=> -[] i /=. +by rewrite -homfstK. +by rewrite -homsndK. +Qed. +End pairhomK'. +*) +Section pairhomK. +Variables A B : category. +Variables x1 x2 : A. +Variables y1 y2 : B. +Lemma pairhomK (f : {hom (x1,y1),(x2,y2)}) : pairhom (homfst f) (homsnd f) = f. +Proof. +apply/hom_ext/funext=> -[] i /=. +by rewrite -homfstK. +by rewrite -homsndK. +Qed. +End pairhomK. + +Module papply_left. +Section def. +Variables A B C : category. +Variable F' : functor (productCategory A B) C. +Variable a : A. +Definition F_obj : B -> C := fun b => F' (a, b). +Definition F_mor (b1 b2 : B) (f : {hom b1, b2}) : {hom F_obj b1, F_obj b2} := + F' # pairhom (idfun_hom a) f. +Program Definition mixin_of := @Functor.Mixin _ _ F_obj F_mor _ _. +Next Obligation. +move=> D; rewrite /F_mor; set h := pairhom _ _. +rewrite (_ : h = [hom of idfun]) ?functor_id_hom //. +by apply/hom_ext => /=; rewrite boolp.funeqE; case. +Qed. +Next Obligation. +move=> b b0 b1 g h; rewrite /F_mor; set i := pairhom _ _. +rewrite (_ : i = [hom of [fun of (pairhom (idfun_hom a) g)] \o + [fun of (pairhom (idfun_hom a) h)]]) ?functor_o_hom //. +by apply/hom_ext => /=; rewrite boolp.funeqE; case. +Qed. +Definition F := Functor.Pack mixin_of. +End def. +End papply_left. + +Module papply_right. +Section def. +Variables A B C : category. +Variable F' : functor (productCategory A B) C. +Variable b : B. +Definition F_obj : A -> C := fun a => F' (a, b). +Definition F_mor (a1 a2 : A) (f : {hom a1, a2}) : {hom F_obj a1, F_obj a2} := + F' # pairhom f (idfun_hom b). +Program Definition mixin_of := @Functor.Mixin _ _ F_obj F_mor _ _. +Next Obligation. +move=> D; rewrite /F_mor; set h := pairhom _ _. +rewrite (_ : h = [hom of idfun]) ?functor_id_hom //. +by apply/hom_ext => /=; rewrite boolp.funeqE; case. +Qed. +Next Obligation. +move=> a a0 a1 g h; rewrite /F_mor; set i := pairhom _ _. +rewrite (_ : i = [hom of [fun of (pairhom g (idfun_hom b))] \o + [fun of (pairhom h (idfun_hom b))]]) ?functor_o_hom //. +by apply/hom_ext => /=; rewrite boolp.funeqE; case. +Qed. +Definition F := Functor.Pack mixin_of. +End def. +End papply_right. + +Module ProductFunctor. +(* This notion does not have a proper name in the literature. + "Product functor" is just a tentative naming, + which unfortunately suffers a collision to another notion: + the functor which maps two objects a, b \in C to their product a*b \in C +*) +Section def. +Variables A1 B1 A2 B2 : category. +Variables (F1 : functor A1 B1) (F2 : functor A2 B2). +Local Notation A := (A1 * A2)%type. +Local Notation B := (B1 * B2)%type. +Definition acto (x : A) : B := pair (F1 x.1) (F2 x.2). +Definition actm (x y : A) (f : {hom x,y}) : {hom acto x, acto y} := + pairhom (F1 # homfst f) (F2 # homsnd f). +Program Definition mixin_of := @Functor.Mixin _ _ acto actm _ _. +Next Obligation. +move=> a. +by rewrite /actm homfst_idfun homsnd_idfun 2!functor_id_hom pairhom_idfun. +Qed. +Next Obligation. +move=> [] a1 a2 [] b1 b2 [] c1 c2 g h. +by rewrite /actm homfst_comp homsnd_comp 2!functor_o_hom pairhom_comp. +Qed. +Definition F := Functor.Pack mixin_of. +End def. +End ProductFunctor. + +Module alpha_left. +Section alpha_left. +Variables A B C D : category. +Variable F' : functor (productCategory (productCategory A B) C) D. +Variables (a : A) (b : B). +Definition acto : C -> D := papply_left.F F' (a, b). +Definition actm (c1 c2 : C) (f : {hom c1, c2}) : {hom acto c1, acto c2} := + F' # pairhom (idfun_hom (a, b)) f. +Program Definition mixin_of := @Functor.Mixin _ _ acto actm _ _. +Next Obligation. +move=> c0; rewrite /actm; set h := pairhom _ _. +rewrite (_ : h = [hom of idfun]) ?functor_id_hom //. +by apply/hom_ext => /=; rewrite boolp.funeqE; case. +Qed. +Next Obligation. +move=> c c0 c1 g h; rewrite /actm; set i := pairhom _ _. +rewrite (_ : i = [hom of [fun of (pairhom (idfun_hom (a, b)) g)] \o + [fun of (pairhom (idfun_hom (a, b)) h)]]) ?functor_o_hom //. +by apply/hom_ext => /=; rewrite boolp.funeqE; case. +Qed. +Definition F : functor C D := Functor.Pack mixin_of. +End alpha_left. +End alpha_left. + +Module alpha_right. +Section alpha_right. +Variables A B C D : category. +Variable F' : functor (productCategory A (productCategory B C)) D. +Variables (a : A) (b : B). +Definition acto : C -> D := papply_left.F (papply_left.F F' a) b. +Definition actm (c1 c2 : C) (f : {hom c1, c2}) : {hom acto c1, acto c2}. +Admitted. +Program Definition mixin_of := @Functor.Mixin _ _ acto actm _ _. +Next Obligation. +Admitted. +Next Obligation. +Admitted. +Definition F : functor C D := Functor.Pack mixin_of. +End alpha_right. +End alpha_right. + +Module prod_left. +Section prod_left. +Variable C : category. +Variable F' : functor (productCategory C C) C. +Let CCC := productCategory (productCategory C C) C. +Definition acto : CCC -> C := fun ccc => F' (F' ccc.1, ccc.2). +Definition actm (c1 c2 : CCC) (f : {hom c1, c2}) : {hom acto c1, acto c2}. +Admitted. +Program Definition mixin_of := @Functor.Mixin _ _ acto actm _ _. +Next Obligation. +Admitted. +Next Obligation. +Admitted. +Definition F : functor CCC C := Functor.Pack mixin_of. +End prod_left. +End prod_left. + +Module prod_right. +Section prod_right. +Variable C : category. +Variable F' : functor (productCategory C C) C. +Let CCC := productCategory C (productCategory C C). +Definition acto : CCC -> C := fun ccc => F' (ccc.1, F' ccc.2). +Definition actm (c1 c2 : CCC) (f : {hom c1, c2}) : {hom acto c1, acto c2} := + F' # (pairhom (homfst f) (F' # (homsnd f))). +Program Definition mixin_of := @Functor.Mixin _ _ acto actm _ _. +Next Obligation. +Admitted. +Next Obligation. +Admitted. +Definition F : functor (productCategory C (productCategory C C)) C. +Admitted. +End prod_right. +End prod_right. + +Module ProductCategoryAssoc. +Section def. +Variables A B C : category. +Definition acto (x : A * (B * C)) : A * B * C := match x with (a,(b,c)) => ((a,b),c) end. +Definition actm (x y : A * (B * C)) : {hom x,y} -> {hom acto x, acto y} := +match x with (xa,(xb,xc)) => match y with (ya,(yb,yc)) => fun f => pairhom (pairhom (homfst f) (homfst (homsnd f))) (homsnd (homsnd f)) end end. +Program Definition mixin_of := @Functor.Mixin _ _ acto actm _ _ . +Next Obligation. +case=> a [] b c. +by rewrite /actm 2!homsnd_idfun 2!homfst_idfun 2!pairhom_idfun. +Qed. +Next Obligation. +case=> xa [] xb xc [] ya [] yb yc [] za [] zb zc g h. +by rewrite /actm !homsnd_comp !homfst_comp !pairhom_comp. +Qed. +Definition F := Functor.Pack mixin_of. +End def. +End ProductCategoryAssoc. + +Module MonoidalCategory. +Section def. +Import homcomp_notation. +Record mixin_of (C : category) : Type := Mixin { + I : C; + prod : functor (productCategory C C) C; + lambda : papply_left.F prod I ~> FId ; + rho : papply_right.F prod I ~> FId ; +(* alpha' : forall (x y z : C), El (prod (prod (x,y), z)) -> El (prod (x, prod (y, z))) ;*) + (*alpha : forall a b, alpha_left.F (prod_left.F prod) a b ~> alpha_right.F (prod_right.F prod) a b ;*) + alpha : prod \O (ProductFunctor.F FId prod) ~> prod \O (ProductFunctor.F prod FId) \O ProductCategoryAssoc.F _ _ _ +}. +Section scratch_pad. +Variable C : category. +Variable m : mixin_of C. +Variable x : C. +Variable y : C. +Check (prod m # pairhom (rho m x) (NId FId y)). +Definition h : {hom alpha_right.F (prod_right.F (prod m)) x (I m) y, prod m (FId x, papply_left.F (prod m) (I m) y)}. +have f : El (alpha_right.F (prod_right.F (prod m)) x (I m) y) -> El (prod m (FId x, papply_left.F (prod m) (I m) y)). + rewrite /alpha_right.F /=. + rewrite /alpha_right.acto /=. + rewrite /papply_left.F_obj /=. +Abort. +End scratch_pad. +Record class_of (T : Type) : Type := Class { + base : Category.mixin_of T; + mixin : mixin_of (Category.Pack base); +}. +Structure t : Type := Pack { T : Type; class : class_of T }. +End def. +Module Exports. +End Exports. +End MonoidalCategory. +Export MonoidalCategory.Exports. + + +(* Attic *) +(* +Module BifunctorLaws. +Section def. +Variable (A B C : category). +Variable (M : A * B -> C) (f : forall A B, {hom A,B} -> {hom M A, M B}). +Definition id := forall A, f [hom of idfun] = [hom of idfun] :> {hom M A,M A}. +Definition comp := forall A B C (g : {hom B,C}) (h : {hom A,B}), + f [hom of g \o h] = [hom of f g \o f h] :> {hom M A,M C}. +End def. +End FunctorLaws. + +Module Bifunctor. +Record mixin_of (C D : category) (m : C -> D) : Type := Mixin { + f : forall A B, {hom A, B} -> {hom m A, m B} ; + _ : FunctorLaws.id f ; + _ : FunctorLaws.comp f }. +Structure t (C D : category) : Type := Pack { m : C -> D ; class : mixin_of m }. +Module Exports. +Section exports. +Variables (C D : category). +Definition Fun (F : t C D) : forall A B, {hom A, B} -> {hom m F A, m F B} := + let: Pack _ (Mixin f _ _) := F return forall A B, {hom A, B} -> {hom m F A, m F B} in f. +Arguments Fun _ [A] [B] : simpl never. +End exports. +Notation functor := t. +Coercion m : functor >-> Funclass. +End Exports. +End Functor. +Export Functor.Exports. +Notation "F # f" := (Fun F f). + *) + +(* +(* A similar construction. + Related to another tensor product in Cat, like the funny tensor? *) +Module WeirdProductCategory. +Section def. +Variable C D : category. +Definition obj := (C * D)%type. +Definition el (X : obj) : Type := (El X.1 * El X.2)%type. +Definition independent (X Y : obj) (f : el X -> el Y) : Prop := + (forall (x : El X.1) (y y' : El X.2), fst (f (x,y)) = fst (f (x,y'))) /\ + (forall (x x': El X.1) (y : El X.2), snd (f (x,y)) = snd (f (x',y))). + +Section homfstsnd. +Let _homfst (X Y : obj) (f : el X -> el Y) : independent f -> El X.1 -> El Y.1. +case=> H _ x. +move/cid: (H x)=> [] y _. +exact y. +Defined. +Definition homfst := Eval hnf in _homfst. +Let _homsnd (X Y : obj) (f : el X -> el Y) : separated f -> El X.2 -> El Y.2. +case=> _ H x. +move/cid: (H x)=> [] y _. +exact y. +Defined. +Definition homsnd := Eval hnf in _homsnd. +End homfstsnd. + +Lemma homfstK X Y (f : el X -> el Y) (Hf : separated f) (x : El X.1) : + inl (homfst Hf x) = f (inl x). +Proof. +move: f Hf x. +case: X=> X1 X2; case:Y=> Y1 Y2 /= f [] /= Hf1 Hf2 x. +by case: (cid (Hf1 x))=> y ->. +Qed. +Lemma homsndK X Y (f : el X -> el Y) (Hf : separated f) (x : El X.2) : + inr (homsnd Hf x) = f (inr x). +Proof. +move: f Hf x. +case: X=> X1 X2; case:Y=> Y1 Y2 /= f [] /= Hf1 Hf2 x. +by case: (cid (Hf2 x))=> y ->. +Qed. +Definition inhom (A B : obj) (f : el A -> el B) : Prop := + exists H : separated f, InHom (homfst H) /\ InHom (homsnd H). +Lemma idfun_separated (X : obj) : @separated X X idfun. +Proof. by split; move=> x; exists x. Qed. +Lemma comp_separated (X Y Z : obj) (f :el X -> el Y) (g : el Y -> el Z) : + separated f -> separated g -> separated (g \o f). +Proof. +move: f g. +case: X=> X1 X2; case: Y=> Y1 Y2; case: Z=> Z1 Z2 f g [] /= Hf1 Hf2 [] /= Hg1 Hg2; split. +- by move=> x; case/cid: (Hf1 x)=> y /= ->; case/cid: (Hg1 y)=> z /= ->; exists z. +- by move=> x; case/cid: (Hf2 x)=> y /= ->; case/cid: (Hg2 y)=> z /= ->; exists z. +Qed. +Lemma homfst_idfun X : homfst (idfun_separated X) = idfun. +Proof. +apply funext=> x /=. +suff: inl (B:=El X.2) (homfst (idfun_separated X) x) = inl x by move=> [=]. +by rewrite homfstK. +Qed. +Lemma homsnd_idfun X : homsnd (idfun_separated X) = idfun. +Proof. +apply funext=> x /=. +suff: inr (A:=El X.1) (homsnd (idfun_separated X) x) = inr x by move=> [=]. +by rewrite homsndK. +Qed. +Lemma homfst_comp X Y Z (f : el X -> el Y) (g : el Y -> el Z) + (Hf : separated f) (Hg : separated g) : + homfst (comp_separated Hf Hg) = homfst Hg \o homfst Hf. +Proof. +apply funext=> x /=. +suff: inl (B:=El Z.2) (homfst (comp_separated Hf Hg) x) = inl (homfst Hg (homfst Hf x)) + by move => [=]. +by rewrite 3!homfstK. +Qed. +Lemma homsnd_comp X Y Z (f : el X -> el Y) (g : el Y -> el Z) + (Hf : separated f) (Hg : separated g) : + homsnd (comp_separated Hf Hg) = homsnd Hg \o homsnd Hf. +Proof. +apply funext=> x /=. +suff: inr (A:=El Z.1) (homsnd (comp_separated Hf Hg) x) = inr (homsnd Hg (homsnd Hf x)) + by move => [=]. +by rewrite 3!homsndK. +Qed. +Definition mixin : Category.mixin_of (C * D). +refine (@Category.Mixin obj el inhom _ _). +- by move=> X; exists (idfun_separated X); rewrite homfst_idfun homsnd_idfun; split; apply id_in_hom. +- by move=> X Y Z f g [] sf [] homfl homfr [] sg [] homgl homgr ; exists (comp_separated sf sg); rewrite homfst_comp homsnd_comp; split; apply funcomp_in_hom. +Defined. +End def. +End WeirdProductCategory. +*) From db98f34fd8a6d462f937b029ffdd1bf4b930134c Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Wed, 9 Jun 2021 15:53:13 +0900 Subject: [PATCH 2/2] catch up with master; add monoidal and closed to _CoqProject --- _CoqProject | 2 + closed_category.v | 3 +- monoidal_category.v | 173 ++++++++++++++++++++++---------------------- 3 files changed, 92 insertions(+), 86 deletions(-) diff --git a/_CoqProject b/_CoqProject index 12de38df..abd109c1 100644 --- a/_CoqProject +++ b/_CoqProject @@ -26,5 +26,7 @@ example_array.v example_monty.v smallstep.v example_transformer.v +monoidal_category.v +closed_category.v -R . monae diff --git a/closed_category.v b/closed_category.v index 2b88f593..2ff47b02 100644 --- a/closed_category.v +++ b/closed_category.v @@ -26,6 +26,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Local Open Scope category_scope. Module CatWithFinProd. Section def. @@ -35,7 +36,7 @@ Record mixin_of (C : category) : Type := Mixin { snd : forall a b, {hom prod a b, b}; univ : forall c a b, {hom c,a} -> {hom c,b} -> {hom c, prod a b}; _ : forall c a b (f : {hom c,a}) (g : {hom c,b}), - f = [hom of (fst a b) \o (univ f g)]; + f = [hom (fst a b) \o (univ f g)]; }. Record class_of (T : Type) : Type := Class { base : Category.mixin_of T; diff --git a/monoidal_category.v b/monoidal_category.v index 14f2081c..01438bd0 100644 --- a/monoidal_category.v +++ b/monoidal_category.v @@ -15,25 +15,27 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Local Open Scope category_scope. + (* A concrete category isomorphic to the product category of C and D *) (* sum version *) Module ProductCategory. Section def. Variable C D : category. Definition obj := (C * D)%type. -Definition el (X : obj) : Type := (El X.1 + El X.2)%type. -Definition separated (X Y : obj) (f : el X -> el Y) : Prop := - (forall x : El X.1, exists y : El Y.1, f (inl x) = inl y) /\ - (forall x : El X.2, exists y : El Y.2, f (inr x) = inr y). +Definition el_prod (X : obj) : Type := (el X.1 + el X.2)%type. +Definition separated (X Y : obj) (f : el_prod X -> el_prod Y) : Prop := + (forall x : el X.1, exists y : el Y.1, f (inl x) = inl y) /\ + (forall x : el X.2, exists y : el Y.2, f (inr x) = inr y). Section sepfstsnd. -Let _sepfst (X Y : obj) (f : el X -> el Y) : separated f -> El X.1 -> El Y.1. +Let _sepfst (X Y : obj) (f : el_prod X -> el_prod Y) : separated f -> el X.1 -> el Y.1. case=> H _ x. move/cid: (H x)=> [] y _. exact y. Defined. Definition sepfst := Eval hnf in _sepfst. -Let _sepsnd (X Y : obj) (f : el X -> el Y) : separated f -> El X.2 -> El Y.2. +Let _sepsnd (X Y : obj) (f : el_prod X -> el_prod Y) : separated f -> el X.2 -> el Y.2. case=> _ H x. move/cid: (H x)=> [] y _. exact y. @@ -41,25 +43,25 @@ Defined. Definition sepsnd := Eval hnf in _sepsnd. End sepfstsnd. -Lemma sepfstK X Y (f : el X -> el Y) (Hf : separated f) (x : El X.1) : +Lemma sepfstK X Y (f : el_prod X -> el_prod Y) (Hf : separated f) (x : el X.1) : inl (sepfst Hf x) = f (inl x). Proof. move: f Hf x. case: X=> X1 X2; case:Y=> Y1 Y2 /= f [] /= Hf1 Hf2 x. by case: (cid (Hf1 x))=> y ->. Qed. -Lemma sepsndK X Y (f : el X -> el Y) (Hf : separated f) (x : El X.2) : +Lemma sepsndK X Y (f : el_prod X -> el_prod Y) (Hf : separated f) (x : el X.2) : inr (sepsnd Hf x) = f (inr x). Proof. move: f Hf x. case: X=> X1 X2; case:Y=> Y1 Y2 /= f [] /= Hf1 Hf2 x. by case: (cid (Hf2 x))=> y ->. Qed. -Definition inhom (A B : obj) (f : el A -> el B) : Prop := +Definition inhom (A B : obj) (f : el_prod A -> el_prod B) : Prop := exists H : separated f, InHom (sepfst H) /\ InHom (sepsnd H). Lemma idfun_separated (X : obj) : @separated X X idfun. Proof. by split; move=> x; exists x. Qed. -Lemma comp_separated (X Y Z : obj) (f :el X -> el Y) (g : el Y -> el Z) : +Lemma comp_separated (X Y Z : obj) (f :el_prod X -> el_prod Y) (g : el_prod Y -> el_prod Z) : separated f -> separated g -> separated (g \o f). Proof. move: f g. @@ -70,36 +72,36 @@ Qed. Lemma sepfst_idfun X : sepfst (idfun_separated X) = idfun. Proof. apply funext=> x /=. -suff: inl (B:=El X.2) (sepfst (idfun_separated X) x) = inl x by move=> [=]. +suff: inl (B:=el X.2) (sepfst (idfun_separated X) x) = inl x by move=> [=]. by rewrite sepfstK. Qed. Lemma sepsnd_idfun X : sepsnd (idfun_separated X) = idfun. Proof. apply funext=> x /=. -suff: inr (A:=El X.1) (sepsnd (idfun_separated X) x) = inr x by move=> [=]. +suff: inr (A:=el X.1) (sepsnd (idfun_separated X) x) = inr x by move=> [=]. by rewrite sepsndK. Qed. -Lemma sepfst_comp X Y Z (f : el X -> el Y) (g : el Y -> el Z) +Lemma sepfst_comp X Y Z (f : el_prod X -> el_prod Y) (g : el_prod Y -> el_prod Z) (Hf : separated f) (Hg : separated g) : sepfst (comp_separated Hf Hg) = sepfst Hg \o sepfst Hf. Proof. apply funext=> x /=. -suff: inl (B:=El Z.2) (sepfst (comp_separated Hf Hg) x) = inl (sepfst Hg (sepfst Hf x)) +suff: inl (B:=el Z.2) (sepfst (comp_separated Hf Hg) x) = inl (sepfst Hg (sepfst Hf x)) by move => [=]. by rewrite 3!sepfstK. Qed. -Lemma sepsnd_comp X Y Z (f : el X -> el Y) (g : el Y -> el Z) +Lemma sepsnd_comp X Y Z (f : el_prod X -> el_prod Y) (g : el_prod Y -> el_prod Z) (Hf : separated f) (Hg : separated g) : sepsnd (comp_separated Hf Hg) = sepsnd Hg \o sepsnd Hf. Proof. apply funext=> x /=. -suff: inr (A:=El Z.1) (sepsnd (comp_separated Hf Hg) x) = inr (sepsnd Hg (sepsnd Hf x)) +suff: inr (A:=el Z.1) (sepsnd (comp_separated Hf Hg) x) = inr (sepsnd Hg (sepsnd Hf x)) by move => [=]. by rewrite 3!sepsndK. Qed. Definition mixin : Category.mixin_of (C * D). -refine (@Category.Mixin obj el inhom _ _). -- by move=> X; exists (idfun_separated X); rewrite sepfst_idfun sepsnd_idfun; split; apply id_in_hom. +refine (@Category.Mixin obj el_prod inhom _ _). +- by move=> X; exists (idfun_separated X); rewrite sepfst_idfun sepsnd_idfun; split; apply idfun_in_hom. - by move=> X Y Z f g [] sf [] homfl homfr [] sg [] homgl homgr ; exists (comp_separated sf sg); rewrite sepfst_comp sepsnd_comp; split; apply funcomp_in_hom. Defined. End def. @@ -114,24 +116,24 @@ Section homfstsnd. Let _homfst (x y : A * B) (f : {hom x,y}) : {hom x.1, y.1}. case:f => f. case/cid=> sf [] Hf _. -exact: (HomPack Hf). +exact: (HomPack _ _ _ Hf). Defined. Definition homfst := Eval hnf in _homfst. Let _homsnd (x y : A * B) (f : {hom x,y}) : {hom x.2, y.2}. case:f => f. case/cid=> sf [] _ Hf. -exact: (HomPack Hf). +exact: (HomPack _ _ _ Hf). Defined. Definition homsnd := Eval hnf in _homsnd. End homfstsnd. -Lemma homfst_idfun x : homfst (x:=x) [hom of idfun] = [hom of idfun]. +Lemma homfst_idfun x : homfst (x:=x) [hom idfun] = [hom idfun]. Proof. apply/hom_ext; rewrite boolp.funeqE => x1 /=. case: cid => i [i1 i2] /=. rewrite (_ : i = ProductCategory.idfun_separated _) ?ProductCategory.sepfst_idfun //. exact/Prop_irrelevance. Qed. -Lemma homsnd_idfun x : homsnd (x:=x) [hom of idfun] = [hom of idfun]. +Lemma homsnd_idfun x : homsnd (x:=x) [hom idfun] = [hom idfun]. Proof. apply/hom_ext; rewrite boolp.funeqE => x1 /=. case: cid => i [i1 i2] /=. @@ -139,7 +141,7 @@ rewrite (_ : i = ProductCategory.idfun_separated _) ?ProductCategory.sepsnd_idfu exact/Prop_irrelevance. Qed. Lemma homfst_comp (x y z : A * B) (f : {hom x,y}) (g : {hom y,z}) : - homfst [hom of g \o f] = [hom of homfst g \o homfst f]. + homfst [hom g \o f] = [hom homfst g \o homfst f]. Proof. rewrite /homfst /=. case: cid => //= gh [gh1 gh2]. @@ -153,7 +155,7 @@ congr (ProductCategory.sepfst _ _). exact/Prop_irrelevance. Qed. Lemma homsnd_comp (x y z : A * B) (f : {hom x,y}) (g : {hom y,z}) : - homsnd [hom of g \o f] = [hom of homsnd g \o homsnd f]. + homsnd [hom g \o f] = [hom homsnd g \o homsnd f]. Proof. rewrite /homsnd /=. case: cid => //= gh [gh1 gh2]. @@ -166,13 +168,13 @@ rewrite -ProductCategory.sepsnd_comp. congr (ProductCategory.sepsnd _ _). exact/Prop_irrelevance. Qed. -Lemma homfstK (x y : A * B) (f : {hom x,y}) (i : El x.1) : inl (homfst f i) = f (inl i). +Lemma homfstK (x y : A * B) (f : {hom x,y}) (i : el x.1) : inl (homfst f i) = f (inl i). Proof. case: f=> /= f Hf. case: (cid _)=> -[] sf1 sf2 [] Hf1 Hf2 /=. by case: (cid _)=> j ->. Qed. -Lemma homsndK (x y : A * B) (f : {hom x,y}) (i : El x.2) : inr (homsnd f i) = f (inr i). +Lemma homsndK (x y : A * B) (f : {hom x,y}) (i : el x.2) : inr (homsnd f i) = f (inr i). Proof. case: f=> /= f Hf. case: (cid _)=> -[] sf1 sf2 [] Hf1 Hf2 /=. @@ -186,14 +188,14 @@ Variables a1 a2 : A. Variables b1 b2 : B. Variables (f : {hom a1, a2}) (g : {hom b1, b2}). Let C := productCategory A B. -Definition pairhom' (ab : El a1 + El b1) : El a2 + El b2 := +Definition pairhom' (ab : el a1 + el b1) : el a2 + el b2 := match ab with | inl a => inl (f a) | inr b => inr (g b) end. Lemma pairhom'_in_hom : - @InHom C _ _ (pairhom' : El (a1,b1).1 + El (a1,b1).2 -> - El (a2,b2).1 + El (a2,b2).2). + @InHom C _ _ (pairhom' : el (a1,b1).1 + el (a1,b1).2 -> + el (a2,b2).1 + el (a2,b2).2). Proof. rewrite /InHom /= /ProductCategory.inhom /=. set s := ProductCategory.separated _. @@ -206,20 +208,20 @@ exists (conj s1 s2); split. rewrite (_ : h = g); first exact: Hom.class. by rewrite boolp.funeqE => ?; rewrite /h /=; case: cid => ? []. Qed. -Definition pairhom : {hom (a1, b1), (a2, b2)} := Hom.Pack _ pairhom'_in_hom. +Definition pairhom : {hom (a1, b1), (a2, b2)} := Hom.Pack _ _ pairhom'_in_hom. End prodCat_pairhom. Section pairhom_idfun. Variables (A B : category) (a : A) (b : B). -Lemma pairhom_idfun : pairhom (a1:=a) (b1:=b) [hom of idfun] [hom of idfun] = [hom of idfun]. +Lemma pairhom_idfun : pairhom (a1:=a) (b1:=b) [hom idfun] [hom idfun] = [hom idfun]. Proof. by apply/hom_ext/funext=> -[] x /=. Qed. End pairhom_idfun. Section pairhom_comp. Variables (A B : category) (a1 a2 a3 : A) (b1 b2 b3 : B). Variables (fa : {hom a1,a2}) (ga : {hom a2,a3}) (fb : {hom b1,b2}) (gb : {hom b2,b3}). -Lemma pairhom_comp : pairhom [hom of ga \o fa] [hom of gb \o fb] = - [hom of pairhom ga gb \o pairhom fa fb]. +Lemma pairhom_comp : pairhom [hom ga \o fa] [hom gb \o fb] = + [hom pairhom ga gb \o pairhom fa fb]. Proof. by apply /hom_ext/funext=> -[] x. Qed. End pairhom_comp. @@ -259,48 +261,48 @@ End pairhomK. Module papply_left. Section def. Variables A B C : category. -Variable F' : functor (productCategory A B) C. +Variable F' : {functor (productCategory A B) -> C}. Variable a : A. Definition F_obj : B -> C := fun b => F' (a, b). Definition F_mor (b1 b2 : B) (f : {hom b1, b2}) : {hom F_obj b1, F_obj b2} := - F' # pairhom (idfun_hom a) f. + F' # pairhom (homid0 a) f. Program Definition mixin_of := @Functor.Mixin _ _ F_obj F_mor _ _. Next Obligation. move=> D; rewrite /F_mor; set h := pairhom _ _. -rewrite (_ : h = [hom of idfun]) ?functor_id_hom //. +rewrite (_ : h = [hom idfun]) ?functor_id_hom //. by apply/hom_ext => /=; rewrite boolp.funeqE; case. Qed. Next Obligation. move=> b b0 b1 g h; rewrite /F_mor; set i := pairhom _ _. -rewrite (_ : i = [hom of [fun of (pairhom (idfun_hom a) g)] \o - [fun of (pairhom (idfun_hom a) h)]]) ?functor_o_hom //. +rewrite (_ : i = [hom (pairhom (homid0 a) g) \o + (pairhom (homid0 a) h)]) ?functor_o_hom //. by apply/hom_ext => /=; rewrite boolp.funeqE; case. Qed. -Definition F := Functor.Pack mixin_of. +Definition F := Functor.Pack (Phant _) mixin_of. End def. End papply_left. Module papply_right. Section def. Variables A B C : category. -Variable F' : functor (productCategory A B) C. +Variable F' : {functor (productCategory A B) -> C}. Variable b : B. Definition F_obj : A -> C := fun a => F' (a, b). Definition F_mor (a1 a2 : A) (f : {hom a1, a2}) : {hom F_obj a1, F_obj a2} := - F' # pairhom f (idfun_hom b). + F' # pairhom f (homid0 b). Program Definition mixin_of := @Functor.Mixin _ _ F_obj F_mor _ _. Next Obligation. move=> D; rewrite /F_mor; set h := pairhom _ _. -rewrite (_ : h = [hom of idfun]) ?functor_id_hom //. +rewrite (_ : h = [hom idfun]) ?functor_id_hom //. by apply/hom_ext => /=; rewrite boolp.funeqE; case. Qed. Next Obligation. move=> a a0 a1 g h; rewrite /F_mor; set i := pairhom _ _. -rewrite (_ : i = [hom of [fun of (pairhom g (idfun_hom b))] \o - [fun of (pairhom h (idfun_hom b))]]) ?functor_o_hom //. +rewrite (_ : i = [hom (pairhom g (homid0 b)) \o + (pairhom h (homid0 b))]) ?functor_o_hom //. by apply/hom_ext => /=; rewrite boolp.funeqE; case. Qed. -Definition F := Functor.Pack mixin_of. +Definition F := Functor.Pack (Phant _) mixin_of. End def. End papply_right. @@ -312,7 +314,7 @@ Module ProductFunctor. *) Section def. Variables A1 B1 A2 B2 : category. -Variables (F1 : functor A1 B1) (F2 : functor A2 B2). +Variables (F1 : {functor A1 -> B1}) (F2 : {functor A2 -> B2}). Local Notation A := (A1 * A2)%type. Local Notation B := (B1 * B2)%type. Definition acto (x : A) : B := pair (F1 x.1) (F2 x.2). @@ -327,38 +329,38 @@ Next Obligation. move=> [] a1 a2 [] b1 b2 [] c1 c2 g h. by rewrite /actm homfst_comp homsnd_comp 2!functor_o_hom pairhom_comp. Qed. -Definition F := Functor.Pack mixin_of. +Definition F := Functor.Pack (Phant _) mixin_of. End def. End ProductFunctor. Module alpha_left. Section alpha_left. Variables A B C D : category. -Variable F' : functor (productCategory (productCategory A B) C) D. +Variable F' : {functor (productCategory (productCategory A B) C) -> D}. Variables (a : A) (b : B). Definition acto : C -> D := papply_left.F F' (a, b). Definition actm (c1 c2 : C) (f : {hom c1, c2}) : {hom acto c1, acto c2} := - F' # pairhom (idfun_hom (a, b)) f. + F' # pairhom (homid0 (a, b)) f. Program Definition mixin_of := @Functor.Mixin _ _ acto actm _ _. Next Obligation. move=> c0; rewrite /actm; set h := pairhom _ _. -rewrite (_ : h = [hom of idfun]) ?functor_id_hom //. +rewrite (_ : h = [hom idfun]) ?functor_id_hom //. by apply/hom_ext => /=; rewrite boolp.funeqE; case. Qed. Next Obligation. move=> c c0 c1 g h; rewrite /actm; set i := pairhom _ _. -rewrite (_ : i = [hom of [fun of (pairhom (idfun_hom (a, b)) g)] \o - [fun of (pairhom (idfun_hom (a, b)) h)]]) ?functor_o_hom //. +rewrite (_ : i = [hom (pairhom (homid0 (a, b)) g) \o + (pairhom (homid0 (a, b)) h)]) ?functor_o_hom //. by apply/hom_ext => /=; rewrite boolp.funeqE; case. Qed. -Definition F : functor C D := Functor.Pack mixin_of. +Definition F : {functor C -> D} := Functor.Pack (Phant _) mixin_of. End alpha_left. End alpha_left. Module alpha_right. Section alpha_right. Variables A B C D : category. -Variable F' : functor (productCategory A (productCategory B C)) D. +Variable F' : {functor (productCategory A (productCategory B C)) -> D}. Variables (a : A) (b : B). Definition acto : C -> D := papply_left.F (papply_left.F F' a) b. Definition actm (c1 c2 : C) (f : {hom c1, c2}) : {hom acto c1, acto c2}. @@ -368,14 +370,14 @@ Next Obligation. Admitted. Next Obligation. Admitted. -Definition F : functor C D := Functor.Pack mixin_of. +Definition F : {functor C -> D} := Functor.Pack (Phant _) mixin_of. End alpha_right. End alpha_right. Module prod_left. Section prod_left. Variable C : category. -Variable F' : functor (productCategory C C) C. +Variable F' : {functor (productCategory C C) -> C}. Let CCC := productCategory (productCategory C C) C. Definition acto : CCC -> C := fun ccc => F' (F' ccc.1, ccc.2). Definition actm (c1 c2 : CCC) (f : {hom c1, c2}) : {hom acto c1, acto c2}. @@ -385,14 +387,14 @@ Next Obligation. Admitted. Next Obligation. Admitted. -Definition F : functor CCC C := Functor.Pack mixin_of. +Definition F : {functor CCC -> C} := Functor.Pack (Phant _) mixin_of. End prod_left. End prod_left. Module prod_right. Section prod_right. Variable C : category. -Variable F' : functor (productCategory C C) C. +Variable F' : {functor (productCategory C C) -> C}. Let CCC := productCategory C (productCategory C C). Definition acto : CCC -> C := fun ccc => F' (ccc.1, F' ccc.2). Definition actm (c1 c2 : CCC) (f : {hom c1, c2}) : {hom acto c1, acto c2} := @@ -402,7 +404,7 @@ Next Obligation. Admitted. Next Obligation. Admitted. -Definition F : functor (productCategory C (productCategory C C)) C. +Definition F : {functor (productCategory C (productCategory C C)) -> C}. Admitted. End prod_right. End prod_right. @@ -422,19 +424,19 @@ Next Obligation. case=> xa [] xb xc [] ya [] yb yc [] za [] zb zc g h. by rewrite /actm !homsnd_comp !homfst_comp !pairhom_comp. Qed. -Definition F := Functor.Pack mixin_of. +Definition F := Functor.Pack (Phant _) mixin_of. End def. End ProductCategoryAssoc. Module MonoidalCategory. Section def. -Import homcomp_notation. +Import comps_notation. Record mixin_of (C : category) : Type := Mixin { I : C; - prod : functor (productCategory C C) C; + prod : {functor (productCategory C C) -> C}; lambda : papply_left.F prod I ~> FId ; rho : papply_right.F prod I ~> FId ; -(* alpha' : forall (x y z : C), El (prod (prod (x,y), z)) -> El (prod (x, prod (y, z))) ;*) +(* alpha' : forall (x y z : C), el (prod (prod (x,y), z)) -> el (prod (x, prod (y, z))) ;*) (*alpha : forall a b, alpha_left.F (prod_left.F prod) a b ~> alpha_right.F (prod_right.F prod) a b ;*) alpha : prod \O (ProductFunctor.F FId prod) ~> prod \O (ProductFunctor.F prod FId) \O ProductCategoryAssoc.F _ _ _ }. @@ -445,7 +447,7 @@ Variable x : C. Variable y : C. Check (prod m # pairhom (rho m x) (NId FId y)). Definition h : {hom alpha_right.F (prod_right.F (prod m)) x (I m) y, prod m (FId x, papply_left.F (prod m) (I m) y)}. -have f : El (alpha_right.F (prod_right.F (prod m)) x (I m) y) -> El (prod m (FId x, papply_left.F (prod m) (I m) y)). +have f : el (alpha_right.F (prod_right.F (prod m)) x (I m) y) -> el (prod m (FId x, papply_left.F (prod m) (I m) y)). rewrite /alpha_right.F /=. rewrite /alpha_right.acto /=. rewrite /papply_left.F_obj /=. @@ -463,15 +465,15 @@ End MonoidalCategory. Export MonoidalCategory.Exports. -(* Attic *) +(* TODO *) (* Module BifunctorLaws. Section def. Variable (A B C : category). Variable (M : A * B -> C) (f : forall A B, {hom A,B} -> {hom M A, M B}). -Definition id := forall A, f [hom of idfun] = [hom of idfun] :> {hom M A,M A}. +Definition id := forall A, f [hom idfun] = [hom idfun] :> {hom M A,M A}. Definition comp := forall A B C (g : {hom B,C}) (h : {hom A,B}), - f [hom of g \o h] = [hom of f g \o f h] :> {hom M A,M C}. + f [hom g \o h] = [hom f g \o f h] :> {hom M A,M C}. End def. End FunctorLaws. @@ -497,25 +499,26 @@ Notation "F # f" := (Fun F f). *) (* +(* TODO: figure out what the construction below is *) (* A similar construction. Related to another tensor product in Cat, like the funny tensor? *) Module WeirdProductCategory. Section def. Variable C D : category. Definition obj := (C * D)%type. -Definition el (X : obj) : Type := (El X.1 * El X.2)%type. -Definition independent (X Y : obj) (f : el X -> el Y) : Prop := - (forall (x : El X.1) (y y' : El X.2), fst (f (x,y)) = fst (f (x,y'))) /\ - (forall (x x': El X.1) (y : El X.2), snd (f (x,y)) = snd (f (x',y))). +Definition el_prod (X : obj) : Type := (el X.1 * el X.2)%type. +Definition independent (X Y : obj) (f : el_prod X -> el_prod Y) : Prop := + (forall (x : el X.1) (y y' : el X.2), fst (f (x,y)) = fst (f (x,y'))) /\ + (forall (x x': el X.1) (y : el X.2), snd (f (x,y)) = snd (f (x',y))). Section homfstsnd. -Let _homfst (X Y : obj) (f : el X -> el Y) : independent f -> El X.1 -> El Y.1. +Let _homfst (X Y : obj) (f : el_prod X -> el_prod Y) : independent f -> el X.1 -> el Y.1. case=> H _ x. move/cid: (H x)=> [] y _. exact y. Defined. Definition homfst := Eval hnf in _homfst. -Let _homsnd (X Y : obj) (f : el X -> el Y) : separated f -> El X.2 -> El Y.2. +Let _homsnd (X Y : obj) (f : el_prod X -> el_prod Y) : separated f -> el X.2 -> el Y.2. case=> _ H x. move/cid: (H x)=> [] y _. exact y. @@ -523,25 +526,25 @@ Defined. Definition homsnd := Eval hnf in _homsnd. End homfstsnd. -Lemma homfstK X Y (f : el X -> el Y) (Hf : separated f) (x : El X.1) : +Lemma homfstK X Y (f : el_prod X -> el_prod Y) (Hf : separated f) (x : el X.1) : inl (homfst Hf x) = f (inl x). Proof. move: f Hf x. case: X=> X1 X2; case:Y=> Y1 Y2 /= f [] /= Hf1 Hf2 x. by case: (cid (Hf1 x))=> y ->. Qed. -Lemma homsndK X Y (f : el X -> el Y) (Hf : separated f) (x : El X.2) : +Lemma homsndK X Y (f : el_prod X -> el_prod Y) (Hf : separated f) (x : el X.2) : inr (homsnd Hf x) = f (inr x). Proof. move: f Hf x. case: X=> X1 X2; case:Y=> Y1 Y2 /= f [] /= Hf1 Hf2 x. by case: (cid (Hf2 x))=> y ->. Qed. -Definition inhom (A B : obj) (f : el A -> el B) : Prop := +Definition inhom (A B : obj) (f : el_prod A -> el_prod B) : Prop := exists H : separated f, InHom (homfst H) /\ InHom (homsnd H). Lemma idfun_separated (X : obj) : @separated X X idfun. Proof. by split; move=> x; exists x. Qed. -Lemma comp_separated (X Y Z : obj) (f :el X -> el Y) (g : el Y -> el Z) : +Lemma comp_separated (X Y Z : obj) (f :el_prod X -> el_prod Y) (g : el_prod Y -> el_prod Z) : separated f -> separated g -> separated (g \o f). Proof. move: f g. @@ -552,36 +555,36 @@ Qed. Lemma homfst_idfun X : homfst (idfun_separated X) = idfun. Proof. apply funext=> x /=. -suff: inl (B:=El X.2) (homfst (idfun_separated X) x) = inl x by move=> [=]. +suff: inl (B:=el X.2) (homfst (idfun_separated X) x) = inl x by move=> [=]. by rewrite homfstK. Qed. Lemma homsnd_idfun X : homsnd (idfun_separated X) = idfun. Proof. apply funext=> x /=. -suff: inr (A:=El X.1) (homsnd (idfun_separated X) x) = inr x by move=> [=]. +suff: inr (A:=el X.1) (homsnd (idfun_separated X) x) = inr x by move=> [=]. by rewrite homsndK. Qed. -Lemma homfst_comp X Y Z (f : el X -> el Y) (g : el Y -> el Z) +Lemma homfst_comp X Y Z (f : el_prod X -> el_prod Y) (g : el_prod Y -> el_prod Z) (Hf : separated f) (Hg : separated g) : homfst (comp_separated Hf Hg) = homfst Hg \o homfst Hf. Proof. apply funext=> x /=. -suff: inl (B:=El Z.2) (homfst (comp_separated Hf Hg) x) = inl (homfst Hg (homfst Hf x)) +suff: inl (B:=el Z.2) (homfst (comp_separated Hf Hg) x) = inl (homfst Hg (homfst Hf x)) by move => [=]. by rewrite 3!homfstK. Qed. -Lemma homsnd_comp X Y Z (f : el X -> el Y) (g : el Y -> el Z) +Lemma homsnd_comp X Y Z (f : el_prod X -> el_prod Y) (g : el_prod Y -> el_prod Z) (Hf : separated f) (Hg : separated g) : homsnd (comp_separated Hf Hg) = homsnd Hg \o homsnd Hf. Proof. apply funext=> x /=. -suff: inr (A:=El Z.1) (homsnd (comp_separated Hf Hg) x) = inr (homsnd Hg (homsnd Hf x)) +suff: inr (A:=el Z.1) (homsnd (comp_separated Hf Hg) x) = inr (homsnd Hg (homsnd Hf x)) by move => [=]. by rewrite 3!homsndK. Qed. Definition mixin : Category.mixin_of (C * D). -refine (@Category.Mixin obj el inhom _ _). -- by move=> X; exists (idfun_separated X); rewrite homfst_idfun homsnd_idfun; split; apply id_in_hom. +refine (@Category.Mixin obj el_prod inhom _ _). +- by move=> X; exists (idfun_separated X); rewrite homfst_idfun homsnd_idfun; split; apply idfun_in_hom. - by move=> X Y Z f g [] sf [] homfl homfr [] sg [] homgl homgr ; exists (comp_separated sf sg); rewrite homfst_comp homsnd_comp; split; apply funcomp_in_hom. Defined. End def.