diff --git a/ViCaR/Classes/RigCategory.v b/ViCaR/Classes/RigCategory.v index b16f1f3..4558883 100644 --- a/ViCaR/Classes/RigCategory.v +++ b/ViCaR/Classes/RigCategory.v @@ -174,11 +174,10 @@ Notation "'[×]'" := (addC) (at level 0) : Rig_scope. *) Section CoherenceConditions. -Variables (DD : Type). -Context {cC : Category DD} +Context {DD : Type} {cC : Category DD} {mAddC : MonoidalCategory cC} {bAddC : BraidedMonoidalCategory mAddC} - (AddC : SymmetricMonoidalCategory bAddC) - (MulC : MonoidalCategory cC) + {AddC : SymmetricMonoidalCategory bAddC} + {MulC : MonoidalCategory cC} (pdC : PreDistributiveBimonoidalCategory AddC MulC) (rC : DistributiveBimonoidalCategory pdC). @@ -284,7 +283,7 @@ Definition condition_XV `{@BraidedMonoidalCategory DD cC MulC} := - +(* @@ -624,7 +623,7 @@ Proof. apply stack_distr_pushout_l_top. Qed. -Lemma distributive_hexagon_1 `{BMulC: @BraidedMonoidalCategory DD cC MulC} : +Lemma distributive_hexagon_1 {BMulC : BraidedMonoidalCategory MulC} : forall (A B C D : DD), id_ A ⊠ γ_ B, C ⊞ id_ A ⊠ γ_ B, D ∘ γ_ A,(C×B) ⊞ γ_ A, (D×B) ∘ α^-1_ C,B,A ⊞ α^-1_ D,B,A ∘ id_ C ⊠ (γ_ A, B)^-1 ⊞ id_ D ⊠ (γ_ A, B)^-1 @@ -635,7 +634,7 @@ Proof. apply morphism_bicompat; apply hexagon_resultant_1. Qed. -Lemma distributive_hexagon_2 `{BMulC: @BraidedMonoidalCategory DD cC MulC} : +Lemma distributive_hexagon_2 {BMulC : BraidedMonoidalCategory MulC} : forall (A B C D : DD), id_ A ⊠ γ_ B,(C+D) ∘ γ_ A,((C+D)×B) ∘ α^-1_ (C+D), B, A ∘ id_(C+D) ⊠ (γ_ A,B)^-1 @@ -645,7 +644,7 @@ Proof. apply hexagon_resultant_1. Qed. -Lemma equivalence_3_helper_1 `{BMul: @BraidedMonoidalCategory DD cC MulC} : +Lemma equivalence_3_helper_1 {BMul : BraidedMonoidalCategory MulC} : forall (A B C D : DD), α^-1_ (C+D), B, A ≃ (γ_ A,((C+D)×B)) ^-1 ∘ id_ A ⊠ (γ_ B, (C+D)) ^-1 @@ -664,6 +663,8 @@ Proof. apply distributive_hexagon_2. Qed. +Lemma equivalence_3_helper_2 {BMul : BraidedMonoidalCategory MulC} : + forall (A B C D : DD), @@ -886,11 +887,39 @@ Proof. rewrite e; clear e. Admitted. -. - +. *) +End CoherenceConditions. -Class SemiCoherent_DistributiveBimonoidalCategory {DD : Type} `(rC : DistributiveBimonoidalCategory DD) := { - condition_I (A B C : DD) : +Class SemiCoherent_DistributiveBimonoidalCategory {DD : Type} {cC : Category DD} + {mAddC : MonoidalCategory cC} {bAddC : BraidedMonoidalCategory mAddC} + {AddC : SymmetricMonoidalCategory bAddC} + {MulC : MonoidalCategory cC} + {pdC : PreDistributiveBimonoidalCategory AddC MulC} + (rC : DistributiveBimonoidalCategory pdC) := { + cond_I : condition_I _; + cond_III : condition_III _; + cond_IV : condition_IV _; + cond_V : condition_V _; + cond_VI : condition_VI _; + cond_VII : condition_VII _; + cond_VIII : condition_VIII _; + cond_IX : condition_IX _; + cond_X : condition_X _ _; + cond_XI : condition_XI _ _; + cond_XII : condition_XII _ _; + cond_XIII : condition_XIII _ _; + cond_XIV : condition_XIV _ _; + cond_XVI : condition_XVI _ _; + cond_XVII : condition_XVII _ _; + cond_XVIII : condition_XVIII _ _; + cond_XIX : condition_XIX _ _; + cond_XX : condition_XX _ _; + cond_XXI : condition_XXI _ _; + cond_XXII : condition_XXII _ _; + cond_XXIII : condition_XXIII _; + cond_XXIV : condition_XXIV _; + +(* condition_I (A B C : DD) : δ_ A,B,C ∘ γ'_ (A×B), (A×C) ≃ id_ A ⊠ γ'_ B, C ∘ δ_ A, C, B; condition_III (A B C : DD) : @@ -957,21 +986,28 @@ Class SemiCoherent_DistributiveBimonoidalCategory {DD : Type} `(rC : Distributiv condition_XXIV (A B : DD) : δ#_ A,B,c1 ∘ (ρ_ A ⊞ ρ_ B) ≃ ρ_ (A+B); +*) }. -Class SemiCoherent_BraidedDistributiveBimonoidalCategory {DD : Type} {cD} - {H1 H2} - {AddC} - {MulC} `(rC : @DistributiveBimonoidalCategory DD cD H1 H2 AddC MulC) - `(@BraidedMonoidalCategory DD cD MulC) := { +Class SemiCoherent_BraidedDistributiveBimonoidalCategory {DD : Type} {cC : Category DD} + {mAddC : MonoidalCategory cC} {bAddC : BraidedMonoidalCategory mAddC} + {AddC : SymmetricMonoidalCategory bAddC} + {MulC : MonoidalCategory cC} + {pdC : PreDistributiveBimonoidalCategory AddC MulC} + (rC : DistributiveBimonoidalCategory pdC) + (bMulC : BraidedMonoidalCategory MulC) := { + cond_II : condition_II _; + cond_XV : condition_XV _ _; +(* condition_II (A B C : DD) : (δ#_ A, B, C) ∘ (γ_ A,C ⊞ γ_ B,C) ≃ γ_ A+B, C ∘ δ_ C,A,B; condition_XV (A : DD) : ρ*_ A ≃ γ_ A,c0 ∘ λ*_A; +*) }. Close Scope Rig_scope. diff --git a/ViCaR/GeneralLemmas.v b/ViCaR/GeneralLemmas.v index 8e69fc3..3bb68cd 100644 --- a/ViCaR/GeneralLemmas.v +++ b/ViCaR/GeneralLemmas.v @@ -4,7 +4,7 @@ Require Import Setoid. Local Open Scope Cat. -Lemma compose_simplify_general : forall {C : Type} {Cat : Category C} +Lemma compose_simplify_general : forall {C : Type} {cC : Category C} {A B M : C} (f1 f3 : A ~> B) (f2 f4 : B ~> M), f1 ≃ f3 -> f2 ≃ f4 -> (f1 ∘ f2) ≃ (f3 ∘ f4). Proof. @@ -14,7 +14,7 @@ Proof. Qed. Lemma stack_simplify_general : forall {C : Type} - {Cat : Category C} {MonCat : MonoidalCategory C} + {cC : Category C} {mC : MonoidalCategory cC} {A B M N : C} (f1 f3 : A ~> B) (f2 f4 : M ~> N), f1 ≃ f3 -> f2 ≃ f4 -> (f1 ⊗ f2) ≃ (f3 ⊗ f4). Proof. @@ -24,7 +24,7 @@ Proof. Qed. Lemma stack_compose_distr_test : forall {C : Type} - `{Cat : Category C} `{MonCat : MonoidalCategory C} + {cC : Category C} {mC : MonoidalCategory cC} {A B D M N P : C} (f : A ~> B) (g : B ~> D) (h : M ~> N) (i : N ~> P), (f ∘ g) ⊗ (h ∘ i) ≃ (f ⊗ h) ∘ (g ⊗ i). @@ -38,9 +38,9 @@ Qed. Lemma stack_distr_pushout_r_bot : forall {C : Type} - `{Cat : Category C} `{MonCat : MonoidalCategory C} + `{cC : Category C} `{mC : MonoidalCategory C} {a b d m n} (f : a ~> b) (g : b ~> d) (h : m ~> n), - f ∘ g ⊗ h ≃ f ⊗ h ∘ (g ⊗ (id_ n)). + (f ∘ g) ⊗ h ≃ f ⊗ h ∘ (g ⊗ (id_ n)). Proof. intros. rewrite <- compose_bimap, right_unit. @@ -50,7 +50,7 @@ Qed. (* TODO: the other two; _l_bot and _l_top *) Lemma stack_distr_pushout_r_top : forall {C : Type} - `{Cat : Category C} `{MonCat : MonoidalCategory C} + {cC : Category C} {mC : MonoidalCategory cC} {a b m n o} (f : a ~> b) (g : m ~> n) (h : n ~> o), f ⊗ (g ∘ h) ≃ f ⊗ g ∘ (id_ b ⊗ h). Proof. @@ -110,7 +110,7 @@ Qed. Lemma nwire_stack_compose_topleft_general : forall {C : Type} - {Cat : Category C} {MonCat : MonoidalCategory C} + {cC : Category C} {mC : MonoidalCategory cC} {topIn botIn topOut botOut : C} (f0 : botIn ~> botOut) (f1 : topIn ~> topOut), ((c_identity topIn) ⊗ f0) ∘ (f1 ⊗ (c_identity botOut)) ≃ (f1 ⊗ f0). @@ -122,7 +122,7 @@ Proof. Qed. Lemma nwire_stackcompose_topright_general : forall {C : Type} - {Cat: Category C} {MonCat : MonoidalCategory C} + {cC : Category C} {mC : MonoidalCategory cC} {topIn botIn topOut botOut : C} (f0 : topIn ~> topOut) (f1 : botIn ~> botOut), (f0 ⊗ (c_identity botIn)) ∘ ((c_identity topOut) ⊗ f1) ≃ (f0 ⊗ f1). @@ -134,7 +134,7 @@ Proof. Qed. Lemma stack_id_compose_split_top : forall {C : Type} - {Cat: Category C} {MonCat : MonoidalCategory C} + {cC : Category C} {mC : MonoidalCategory cC} {topIn topMid topOut bot : C} (f0 : topIn ~> topMid) (f1 : topMid ~> topOut), (f0 ∘ f1) ⊗ (id_ bot) ≃ f0 ⊗ id_ bot ∘ (f1 ⊗ id_ bot). @@ -145,7 +145,7 @@ Proof. Qed. Lemma stack_id_compose_split_bot : forall {C : Type} - {Cat: Category C} {MonCat : MonoidalCategory C} + {cC : Category C} {mC : MonoidalCategory cC} {top botIn botMid botOut : C} (f0 : botIn ~> botMid) (f1 : botMid ~> botOut), (id_ top) ⊗ (f0 ∘ f1) ≃ id_ top ⊗ f0 ∘ (id_ top ⊗ f1). diff --git a/examples/TypesExample.v b/examples/TypesExample.v index 4a75660..4d06621 100644 --- a/examples/TypesExample.v +++ b/examples/TypesExample.v @@ -1018,7 +1018,7 @@ Class Category_with_Limits {C} (cC : Category C) := { Definition typ_limit_obj {D} {cD : Category D} (F : Functor cD Typ) : Type := { s : big_prod F.(obj_map) | - forall (d d' : D) (f : d ~> d'), (F @ f) (s d) = s d'}. + forall (d d' : D) (f : d ~> d'), (F @ f) (s d) = s d' }. Definition typ_limit_obj_cone_mor {D} {cD : Category D} (F : Functor cD Typ) : forall (d : D), typ_limit_obj F ~> F d