Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Merge monoidal coherence #4

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Merge monoidal coherence #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
11ca2e7
Merge changes from monoidal-coherence
wjbs Oct 9, 2024
cbba4b4
Clean up MonoidalCoherence
wjbs Oct 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
304 changes: 142 additions & 162 deletions ViCaR/CategoryAutomation.v
View file
Open in desktop

Large diffs are not rendered by default.

10 changes: 4 additions & 6 deletions ViCaR/Classes/BraidedMonoidal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,15 +67,13 @@
id_ B ⊗ β_ M, A ∘ β_ B, (A×M) ∘ associator A M B ∘ id_ A ⊗ (β_ B, M)^-1
≃ associator B M A ^-1 ∘ β_ (B × M), A.
Proof.
(* rewrite <- compose_iso_l. *)
pose proof (hexagon_2 A B M) as hex2.
replace (id_ A) with (IdentityIsomorphism A ^-1) by easy.
rewrite <- (compose_tensor_iso_r' (associator B M A ^-1 ∘ β_ B × M, A) (IdentityIsomorphism A) (β_ B, M)).
rewrite <- (compose_tensor_iso_r' _ (IdentityIsomorphism _)).

Check failure on line 72 in ViCaR/Classes/BraidedMonoidal.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

Found no subterm matching
simpl.
rewrite 2!compose_iso_r.
rewrite !(assoc).
rewrite <- compose_iso_l.
Check compose_tensor_iso_r.
replace (id_ B) with (forward (IdentityIsomorphism B)) by easy.
rewrite (compose_tensor_iso_r _ (IdentityIsomorphism _)).
rewrite (assoc), compose_iso_l'.
symmetry in hex2.
Expand All @@ -87,7 +85,6 @@
apply compose_cancel_r.
pose proof (hexagon_1 B A M) as hex1.
rewrite assoc, <- compose_iso_l'.
replace (id_ M) with (IdentityIsomorphism M ^-1) by easy.
rewrite <- (compose_tensor_iso_l' _ (IdentityIsomorphism _)).
simpl.
rewrite <- 3!(assoc).
Expand All @@ -98,4 +95,5 @@

End BraidedCoherenceRewrites.

Local Close Scope Cat.

Local Close Scope Cat.
20 changes: 15 additions & 5 deletions ViCaR/Classes/Category.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
Reserved Notation "A ≅ B" (at level 70). (* \cong *)
Reserved Notation "'id_' A" (at level 15).

#[universes(polymorphic=yes,cumulative=yes)]
Class Category (C : Type) : Type := {
morphism : C -> C -> Type
where "A ~> B" := (morphism A B);
Expand All @@ -25,10 +26,10 @@
c_identity (A : C) : A ~> A;
}.

Arguments morphism {_} (cC)%Cat (A B)%Cat : rename.

Check warning on line 29 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 29 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Arguments c_equiv {_} (cC)%Cat {A B}%Cat (f g)%Cat : rename.

Check warning on line 30 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 30 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Arguments compose {_} (cC)%Cat {_ _ _}%Cat (f g)%Cat : rename.

Check warning on line 31 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 31 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Arguments c_identity {_} {cC}%Cat (A)%Cat : rename.

Check warning on line 32 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 32 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Notation "'id_' A" := (c_identity A%Cat)
(at level 15, A at next level, no associativity) : Cat_scope.
Expand All @@ -39,6 +40,7 @@
Notation "f ∘ g" := (compose _%Cat f%Cat g%Cat)
(at level 40, g at next level, left associativity) : Cat_scope. (* \circ *)

#[universes(polymorphic=yes,cumulative=yes)]

Check warning on line 43 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

Automatically putting CategoryCoherence in Prop even though it was
Class CategoryCoherence {C} (cC : Category C) : Type := {
(* to_base_struct_cat := cC; *)

Expand All @@ -57,11 +59,11 @@
right_unit {A B : C} (f : A ~> B) : f ∘ id_ B ≃ f;
}.

Arguments c_equiv_rel {_} {cC}%Cat {cCh}%Cat {A B}%Cat : rename.

Check warning on line 62 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 62 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Arguments assoc {_} {cC}%Cat {cCh}%Cat {_ _ _ _}%Cat (f g h)%Cat : rename.

Check warning on line 63 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 63 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Arguments compose_compat {_} {cC}%Cat {cCh}%Cat {_ _ _}%Cat (f g)%Cat _ (h j)%Cat : rename.

Check warning on line 64 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 64 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Arguments left_unit {_} {cC}%Cat {cCh}%Cat {A B}%Cat (f)%Cat : rename.

Check warning on line 65 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 65 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Arguments right_unit {_} {cC}%Cat {cCh}%Cat {A B}%Cat (f)%Cat : rename.

Check warning on line 66 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 66 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (dev, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

(* Coercion to_base_struct_cat : CategoryCoherence >-> Category. *)

Expand Down Expand Up @@ -99,11 +101,13 @@
(** Isomorphism of objects in a category, and equivalent typeclass, with
parametric equivalence *)

#[universes(polymorphic=yes)]
Definition isomorphic {C : Type} {cC : Category C} (A B : C) :=
exists (f : A ~> B) (g : B ~> A), is_inverse f g.

Arguments isomorphic {_} {_}%Cat (_ _)%Cat.

Check warning on line 108 in ViCaR/Classes/Category.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

#[universes(polymorphic=yes,cumulative=yes)]
Class Isomorphism {C : Type} {cC : Category C} (A B : C) := {
forward : A ~> B;
reverse : B ~> A;
Expand Down Expand Up @@ -182,6 +186,7 @@
as isomorphic_equiv_rel.

(** Functors, including instances as equivalence & isomorphism parametric morphisms *)
#[universes(polymorphic=yes,cumulative=yes)]
Class Functor {C D : Type} (cC: Category C) (cD : Category D) : Type := {
obj_map : C -> D;
morphism_map {A B : C} : (A ~> B) -> (obj_map A ~> obj_map B);
Expand Down Expand Up @@ -218,7 +223,7 @@
Qed.



#[universes(polymorphic=yes,cumulative=yes)]
Class Bifunctor {C1 C2 D : Type} (cC1: Category C1)
(cC2 : Category C2) (cD : Category D) := {
obj_bimap : C1 -> C2 -> D;
Expand Down Expand Up @@ -266,6 +271,7 @@
split; apply id_bimap.
Qed.

#[universes(polymorphic=yes)]
Definition CommuteBifunctor {C1 C2 D : Type} `{cC1 : Category C1}
`{cC2 : Category C2} `{cD : Category D} (F : Bifunctor cC1 cC2 cD)
: Bifunctor cC2 cC1 cD := {|
Expand All @@ -281,6 +287,7 @@


(** Natural Transformations & Isomorphisms (and the equivalents for Bifunctors) *)
#[universes(polymorphic=yes,cumulative=yes)]
Class NaturalTransformation {C D : Type} `{cC: Category C} `{cD : Category D}
(F G : Functor cC cD) := {
component_map (A : C) : F A ~> G A;
Expand All @@ -292,6 +299,7 @@
Arguments component_map_natural {_ _} {_ _}%Cat {_ _}%Cat
{N}%Cat {_ _}%Cat (f)%Cat : rename.

#[universes(polymorphic=yes,cumulative=yes)]
Class NaturalIsomorphism {C D : Type} `{cC: Category C} `{cD : Category D}
(F G : Functor cC cD) := {
component_iso (A : C) : F A <~> G A;
Expand All @@ -313,7 +321,7 @@
|}.



#[universes(polymorphic=yes,cumulative=yes)]
Class NaturalBiTransformation {C1 C2 D : Type} `{cC1 : Category C1}
`{cC2 : Category C2} `{cD : Category D} (F G : Bifunctor cC1 cC2 cD) := {
component_bimap (A1 : C1) (A2 : C2) : F A1 A2 ~> G A1 A2;
Expand All @@ -328,6 +336,7 @@
Arguments component_bimap_natural {_ _ _} {_ _ _}%Cat {_ _}%Cat
{N}%Cat {_ _ _ _}%Cat (f1 f2)%Cat : rename.

#[universes(polymorphic=yes,cumulative=yes)]
Class NaturalBiIsomorphism {C1 C2 D : Type} `{cC1 : Category C1}
`{cC2 : Category C2} `{cD : Category D} (F G : Bifunctor cC1 cC2 cD) := {
component_biiso (A1 : C1) (A2 : C2) : F A1 A2 <~> G A1 A2;
Expand Down Expand Up @@ -655,8 +664,8 @@
intros; split; symmetry; apply compose_iso_l; easy.
Qed.


#[program] Definition FunctorIsomorphism {C D} {cC : Category C}
#[universes(polymorphic=yes),
program] Definition FunctorIsomorphism {C D} {cC : Category C}
{cCh : CategoryCoherence cC} {cD : Category D} {cDh : CategoryCoherence cD}
{A B : C} (F : Functor cC cD) (f : A <~> B) : F A <~> F B := {|
forward := F @ f;
Expand All @@ -667,7 +676,8 @@
(proj2 isomorphism_inverse), 2!id_map; easy.
Qed.

#[program] Definition BifunctorIsomorphism {C1 C2 D} {cC1 : Category C1}
#[universes(polymorphic=yes),
program] Definition BifunctorIsomorphism {C1 C2 D} {cC1 : Category C1}
{cC1h : CategoryCoherence cC1} {cC2 : Category C2}
{cC2h : CategoryCoherence cC2} {cD : Category D} {cDh : CategoryCoherence cD}
{A1 B1 : C1} {A2 B2 : C2} (F : Bifunctor cC1 cC2 cD)
Expand Down
59 changes: 58 additions & 1 deletion ViCaR/Classes/Monoidal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Reserved Notation "'λ_' x" (at level 20, no associativity). (* \lambda *)
Reserved Notation "'ρ_' x" (at level 20, no associativity). (* \rho *)
Reserved Notation "'α_' A , B , M" (at level 20, no associativity). (* \alpha *)

#[universes(polymorphic=yes,cumulative=yes)]
Class MonoidalCategory {C : Type} (cC : Category C) : Type := {
obj_tensor : C -> C -> C
where "x × y" := (obj_tensor x y);
Expand Down Expand Up @@ -54,7 +55,7 @@ Notation "'ρ⁻¹_' x" := ((right_unitor x).(reverse))
(at level 20, no associativity) : Cat_scope. (* \rho \^- \^1 *)
*)


#[universes(polymorphic=yes,cumulative=yes)]
Class MonoidalCategoryCoherence {C : Type} {cC : Category C}
{cCh : CategoryCoherence cC} (mC : MonoidalCategory cC) : Type := {
tensor_id (A1 A2 : C) : (id_ A1) ⊗ (id_ A2) ≃ id_ (A1 × A2);
Expand Down Expand Up @@ -149,6 +150,62 @@ Qed.

End TensorBifunctor.

Section InverseCoherences.

Context {C : Type} {cC : Category C} {cCh : CategoryCoherence cC}
{mC : MonoidalCategory cC} {mCh : MonoidalCategoryCoherence mC}.

Lemma invassociator_cohere {A B M N P Q : C} (f : A ~> B)
(g : M ~> N) (h : P ~> Q) :
α_ A, M, P ⁻¹ ∘ ((f ⊗ g) ⊗ h)
≃ (f ⊗ (g ⊗ h)) ∘ α_ B, N, Q ⁻¹.
Proof.
rewrite <- compose_iso_l', <- assoc, <- compose_iso_r.
symmetry.
apply associator_cohere.
Qed.

Lemma invleft_unitor_cohere {A B : C} (f : A ~> B) :
λ_ A ⁻¹ ∘ (id_ I ⊗ f) ≃ f ∘ λ_ B⁻¹.
Proof.
rewrite <- compose_iso_l', <- assoc, <- compose_iso_r.
symmetry.
apply left_unitor_cohere.
Qed.

Lemma invright_unitor_cohere {A B : C} (f : A ~> B) :
ρ_ A ⁻¹ ∘ (f ⊗ id_ I) ≃ f ∘ ρ_ B ⁻¹.
Proof.
rewrite <- compose_iso_l', <- assoc, <- compose_iso_r.
symmetry.
apply right_unitor_cohere.
Qed.

Lemma inv_triangle' (A B : C) :
(id_ A ⊗ λ_ B)
≃ α_ A, I, B ^-1 ∘ ρ_ A ⊗ id_ B.
Proof.
rewrite <- compose_iso_l.
apply triangle.
Qed.

Lemma invpentagon (A B M N : C) :
(id_ A ⊗ α_ B, M, N ^-1) ∘
α_ A, (B × M), N ^-1 ∘ (α_ A, B, M ^-1 ⊗ id_ N)
≃ α_ A, B, (M × N)^-1 ∘ α_ (A × B), M, N ^-1.
Proof.
symmetry. rewrite <- left_unit, <- assoc.
rewrite <- 2!compose_iso_r'.
rewrite assoc, <- pentagon.
rewrite assoc, <- 2!(assoc (_^-1 ⊗ id_ N)), <- tensor_compose.
rewrite iso_inv_l, left_unit, tensor_id, left_unit.
rewrite assoc, <- (assoc (_^-1)), iso_inv_l, left_unit.
now rewrite <- tensor_compose, iso_inv_l, left_unit, tensor_id.
Qed.


End InverseCoherences.

Arguments tensor {_} {_}%Cat (mC)%Cat {_ _}%Cat.
Arguments TensorIsomorphism {_} {_ mC cCh mCh}%Cat {_ _ _ _}%Cat (_ _)%Cat.

Expand Down
Loading
Loading