; centralmor_second : forall `(g:c~>d), (g ⋉ _ >>> _ ⋊ f) ~~ (_ ⋊ f >>> g ⋉ _)
}.
-(* the central morphisms of a category constitute a subcategory *)
-Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
- apply Build_SubCategory; intros; apply Build_CentralMorphism; intros.
- abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
- setoid_rewrite (fmor_preserves_id(bin_first d));
- setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
- abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
- setoid_rewrite (fmor_preserves_id(bin_second d));
- setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
+ : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
+ intros.
+ apply Build_CentralMorphism; intros.
abstract (setoid_rewrite <- (fmor_preserves_comp(bin_first c0));
setoid_rewrite associativity;
setoid_rewrite centralmor_first;
reflexivity).
Qed.
+(* the central morphisms of a category constitute a subcategory *)
+Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
+ apply Build_SubCategory; intros.
+ apply Build_CentralMorphism; intros.
+ abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
+ setoid_rewrite (fmor_preserves_id(bin_first d));
+ setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+ abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
+ setoid_rewrite (fmor_preserves_id(bin_second d));
+ setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
+ apply central_morphisms_compose; auto.
+ Qed.
+
Class CommutativeCat `(BinoidalCat) :=
{ commutative_central : forall `(f:a~>b), CentralMorphism f
; commutative_morprod := fun `(f:a~>b)`(g:a~>b) => f ⋉ _ >>> _ ⋊ g
|}.
Defined.
- (*
- Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat (BinoidalCat_from_Bifunctor F).
+ Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
[ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
| etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
Defined.
- *)
+
End BinoidalCat_from_Bifunctor.
(* not in Awodey *)
(* FIXME *)
Admitted.
-(* Formalized Definition 3.10 *)
Class PreMonoidalFunctor
`(PM1:PreMonoidalCat(C:=C1)(I:=I1))
`(PM2:PreMonoidalCat(C:=C2)(I:=I2))
(* Braided and Symmetric Categories *)
Class BraidedCat `(mc:PreMonoidalCat) :=
-{ br_swap : forall a b, a⊗b ≅ b⊗a
-; triangleb : forall a:C, #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
-; hexagon1 : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
- ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
-; hexagon2 : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
- ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
+{ br_niso : forall a, bin_first a <~~~> bin_second a
+; br_swap := fun a b => ni_iso (br_niso b) a
+; triangleb : forall a:C, #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
+; hexagon1 : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
+ ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
+; hexagon2 : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
+ ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
}.
Class SymmetricCat `(bc:BraidedCat) :=
{ symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
}.
-Class DiagonalCat `(BinoidalCat) :=
-{ copy : forall a, a ~> (a⊗a)
-(* copy >> swap == copy -- only necessary for non-cartesian braided diagonal categories *)
-}.
-
(* Definition 7.23 *)
Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C Fobj}(I:C) :=
{ mon_f := F
; mon_i := I
; mon_c := C
-(*; mon_bin := BinoidalCat_from_Bifunctor mon_f*)
; mon_first := fun a b c (f:a~>b) => F \ pair_mor (pair_obj a c) (pair_obj b c) f (id c)
; mon_second := fun a b c (f:a~>b) => F \ pair_mor (pair_obj c a) (pair_obj c b) (id c) f
; mon_cancelr : (func_rlecnac I >>>> F) <~~~> functor_id C
; mon_triangle : Triangle mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
(fun a => #(mon_cancell a)) (fun a => #(mon_cancelr a))
}.
-
-(* FIXME: show that the endofunctors on any given category form a monoidal category *)
-
(* Coq manual on coercions: ... only the oldest one is valid and the
* others are ignored. So the order of declaration of coercions is
* important. *)
Coercion mon_c : MonoidalCat >-> Category.
-(*Coercion mon_bin : MonoidalCat >-> BinoidalCat.*)
Coercion mon_f : MonoidalCat >-> Functor.
Implicit Arguments mon_f [Ob Hom C Fobj F I].
Implicit Arguments mon_i [Ob Hom C Fobj F I].
Implicit Arguments mon_c [Ob Hom C Fobj F I].
-(*Implicit Arguments mon_bin [Ob Hom C Fobj F I].*)
Implicit Arguments MonoidalCat [Ob Hom ].
Section MonoidalCat_is_PreMonoidal.
Hint Extern 1 => apply MonoidalCat_all_central.
Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
-(*Lemma CommutativePreMonoidalCategoriesAreMonoidal `(pm:PreMonoidalCat)(cc:CommutativeCat pm) : MonoidalCat pm.*)
+(* Later: generalize to premonoidal categories *)
+Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
+{ copy_nt : forall a, functor_id _ ~~~> func_diagonal >>>> F
+; copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
+ := fun a => nt_component _ _ (copy_nt a) a
+(* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
+}.
+
+(* TO DO: show that the endofunctors on any given category form a monoidal category *)
Section MonoidalFunctor.
Context `(m1:MonoidalCat(C:=C1)) `(m2:MonoidalCat(C:=C2)).
Class MonoidalFunctor {Mobj:C1->C2} (mf_F:Functor C1 C2 Mobj) :=
apply ni_inv.
apply mc1.
apply ni_id.
- Qed.
+ Defined.
Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
{ mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
; mf_coherence := mf_compose_coherence
}.
- Admitted.
+ admit.
+ admit.
+ admit.
+ Defined.
End MonoidalFunctorsCompose.
{ car_terminal : Terminal mc
; car_one : (@one _ _ _ car_terminal) ≅ (mon_i mc)
; car_diagonal : DiagonalCat mc
-; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) _) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
-; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) _) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
+; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
+; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
; car_mn := mc
}.
Coercion car_diagonal : CartesianCat >-> DiagonalCat.
Coercion car_terminal : CartesianCat >-> Terminal.
Coercion car_mn : CartesianCat >-> MonoidalCat.
+
+Section CenterMonoidal.
+
+ Context `(mc:PreMonoidalCat(I:=pI)).
+
+ Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc.
+ intro.
+ destruct X as [a b].
+ destruct a as [a apf].
+ destruct b as [b bpf].
+ exists (a ⊗ b); auto.
+ Defined.
+
+ Definition CenterMonoidal_F_fmor (a b:(Center mc) ×× (Center mc)) :
+ (a~~{(Center mc) ×× (Center mc)}~~>b) ->
+ ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)).
+ destruct a as [[a1 a1'] [a2 a2']].
+ destruct b as [[b1 b1'] [b2 b2']].
+ intro f.
+ destruct f as [[f1 f1'] [f2 f2']].
+ simpl in *.
+ unfold hom.
+ simpl.
+ exists (f1 ⋉ a2 >>> b1 ⋊ f2).
+ apply central_morphisms_compose.
+ admit.
+ admit.
+ Defined.
+
+ Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
+ refine {| fmor := CenterMonoidal_F_fmor |}.
+ intros.
+ destruct a as [[a1 a1'] [a2 a2']].
+ destruct b as [[b1 b1'] [b2 b2']].
+ destruct f as [[f1 f1'] [f2 f2']].
+ destruct f' as [[g1 g1'] [g2 g2']].
+ simpl in *.
+ destruct H.
+ apply comp_respects.
+ set (fmor_respects(-⋉a2)) as q; apply q; auto.
+ set (fmor_respects(b1⋊-)) as q; apply q; auto.
+ intros.
+ destruct a as [[a1 a1'] [a2 a2']].
+ simpl in *.
+ setoid_rewrite (fmor_preserves_id (-⋉a2)).
+ setoid_rewrite (fmor_preserves_id (a1⋊-)).
+ apply left_identity.
+ intros.
+ destruct a as [[a1 a1'] [a2 a2']].
+ destruct b as [[b1 b1'] [b2 b2']].
+ destruct c as [[c1 c1'] [c2 c2']].
+ destruct f as [[f1 f1'] [f2 f2']].
+ destruct g as [[g1 g1'] [g2 g2']].
+ simpl in *.
+ setoid_rewrite juggle3.
+ setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
+ setoid_rewrite <- juggle3.
+ setoid_rewrite <- fmor_preserves_comp.
+ reflexivity.
+ Defined.
+
+ Definition CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I).
+ admit.
+ Defined.
+
+End CenterMonoidal.
+
projects / coq-categories.git / blobdiff