Skip to content

Commit

Permalink
Insubstantial change; in-progress portions of RigCategory commented o…
Browse files Browse the repository at this point in the history 
…ut to let the core build. Examples are still non-building.
  • Loading branch information
@wjbs
wjbs committed Mar 17, 2024
1 parent 0341245 commit 7321534
Show file tree
Hide file tree
Showing 3 changed files with 64 additions and 28 deletions.
70 changes: 53 additions & 17 deletions ViCaR/Classes/RigCategory.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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).

Expand Down Expand Up @@ -284,7 +283,7 @@ Definition condition_XV `{@BraidedMonoidalCategory DD cC MulC} :=




(*
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -664,6 +663,8 @@ Proof.
apply distributive_hexagon_2.
Qed.
Lemma equivalence_3_helper_2 {BMul : BraidedMonoidalCategory MulC} :
forall (A B C D : DD),
Expand Down Expand Up @@ -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) :
Expand Down Expand Up @@ -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.
20 changes: 10 additions & 10 deletions ViCaR/GeneralLemmas.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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).
Expand All @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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).
Expand All @@ -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).
Expand All @@ -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).
Expand All @@ -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).
Expand Down
2 changes: 1 addition & 1 deletion examples/TypesExample.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 7321534

Please sign in to comment.