From c3ac1680c5bd233ecc3c9064f9af0fd98690e159 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 27 May 2024 18:31:16 +0200 Subject: [PATCH 1/5] make opposite Is1Natural definitionally involutive Signed-off-by: Ali Caglayan --- test/WildCat/Opposite.v | 10 +++++-- theories/Homotopy/ClassifyingSpace.v | 4 +-- theories/Homotopy/Join/Core.v | 6 ++-- theories/Homotopy/Join/JoinAssoc.v | 4 +-- theories/Pointed/Core.v | 12 ++++---- theories/Pointed/Loops.v | 2 +- theories/Pointed/pSusp.v | 2 +- theories/WildCat/Adjoint.v | 10 +++---- theories/WildCat/Bifunctor.v | 4 +-- theories/WildCat/Monoidal.v | 4 +-- theories/WildCat/NatTrans.v | 42 +++++++++++++++++----------- theories/WildCat/Paths.v | 10 +++---- theories/WildCat/Products.v | 6 ++-- theories/WildCat/Universe.v | 6 ++-- theories/WildCat/Yoneda.v | 4 +-- 15 files changed, 70 insertions(+), 56 deletions(-) diff --git a/test/WildCat/Opposite.v b/test/WildCat/Opposite.v index b88506ff47f..6ee50a2183e 100644 --- a/test/WildCat/Opposite.v +++ b/test/WildCat/Opposite.v @@ -35,8 +35,14 @@ Definition test9 A B C (F : A -> B -> C) `{x : Is1Bifunctor A B C F} (@is1bifunctor_op _ _ _ F _ _ _ _ _ _ _ _ _ _ _ _ _ x) = x := 1. -(** Opposite natural transformations are *not* definitionally involutive. *) -Fail Definition test10 A `{Is01Cat A} B `{Is1Cat B} (F G : A -> B) +(** Opposite natural transformations are definitionally involutive. *) +Definition test10 A `{Is01Cat A} B `{Is1Cat B} (F G : A -> B) `{!Is0Functor F, !Is0Functor G} (n : NatTrans F G) : nattrans_op (nattrans_op n) = n := 1. + +(** Opposite natural equivalences are definitionally involutive. *) +Definition test11 A `{Is01Cat A} B `{HasEquivs B} (F G : A -> B) + `{!Is0Functor F, !Is0Functor G} (n : NatEquiv F G) + : natequiv_op (natequiv_op n) = n + := 1. diff --git a/theories/Homotopy/ClassifyingSpace.v b/theories/Homotopy/ClassifyingSpace.v index 65974a23bc5..7fdf896df43 100644 --- a/theories/Homotopy/ClassifyingSpace.v +++ b/theories/Homotopy/ClassifyingSpace.v @@ -432,7 +432,7 @@ Definition natequiv_g_loops_bg `{Univalence} Proof. snrapply Build_NatEquiv. 1: intros G; rapply pequiv_g_loops_bg. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros X Y f. symmetry. apply pbloop_natural. @@ -534,7 +534,7 @@ Defined. Global Instance is1natural_grp_homo_pmap_bg_r {U : Univalence} (G : Group) : Is1Natural (opyon G) (opyon (B G) o B) (equiv_grp_homo_pmap_bg G). Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros K H f h. apply path_hom. rapply (fmap_comp B h f). diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v index 48bbe8f2c3a..e0d22f14fd6 100644 --- a/theories/Homotopy/Join/Core.v +++ b/theories/Homotopy/Join/Core.v @@ -627,7 +627,7 @@ Section JoinSym. 1, 2: apply joinrecdata_sym. 1, 2: apply joinrecdata_sym_inv. (* Naturality: *) - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. intros P Q g f; simpl. bundle_joinrecpath. intros b a; simpl. @@ -837,7 +837,7 @@ Section JoinEmpty. Proof. snrapply Build_NatEquiv. - apply equiv_join_empty_right. - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. intros A B f. cbn -[equiv_join_empty_right]. snrapply Join_ind_FlFr. @@ -851,7 +851,7 @@ Section JoinEmpty. Proof. snrapply Build_NatEquiv. - apply equiv_join_empty_left. - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. intros A B f x. cbn -[equiv_join_empty_right]. rhs_V rapply (isnat_natequiv join_right_unitor). diff --git a/theories/Homotopy/Join/JoinAssoc.v b/theories/Homotopy/Join/JoinAssoc.v index aba57567e31..19f07ae8c4b 100644 --- a/theories/Homotopy/Join/JoinAssoc.v +++ b/theories/Homotopy/Join/JoinAssoc.v @@ -60,7 +60,7 @@ Proof. 1, 2: apply trijoinrecdata_twist. 1, 2: apply trijoinrecdata_twist_inv. (* Naturality: *) - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. intros P Q g f; simpl. bundle_trijoinrecpath. all: intros; cbn. @@ -265,7 +265,7 @@ Global Instance join_associator : Associator Join. Proof. snrapply Build_Associator; simpl. - exact join_assoc. - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. intros [[A B] C] [[A' B'] C'] [[f g] h]; cbn. apply join_assoc_nat. Defined. diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v index bfb9d893f33..ec69938b3b9 100644 --- a/theories/Pointed/Core.v +++ b/theories/Pointed/Core.v @@ -661,31 +661,31 @@ Proof. exact (concat_Ap q _)^. + by pelim p f g q h k. - intros A B C D f g. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros r1 r2 s1. srapply Build_pHomotopy. 1: exact (fun _ => concat_p1 _ @ (concat_1p _)^). by pelim f g s1 r1 r2. - intros A B C D f g. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros r1 r2 s1. srapply Build_pHomotopy. 1: exact (fun _ => concat_p1 _ @ (concat_1p _)^). by pelim f s1 r1 r2 g. - intros A B C D f g. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros r1 r2 s1. srapply Build_pHomotopy. 1: cbn; exact (fun _ => concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^). by pelim s1 r1 r2 f g. - intros A B. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros r1 r2 s1. srapply Build_pHomotopy. 1: exact (fun _ => concat_p1 _ @ ap_idmap _ @ (concat_1p _)^). by pelim s1 r1 r2. - intros A B. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros r1 r2 s1. srapply Build_pHomotopy. 1: exact (fun _ => concat_p1 _ @ (concat_1p _)^). @@ -1069,7 +1069,7 @@ Lemma natequiv_pointify_r `{Funext} (A : Type) Proof. snrapply Build_NatEquiv. 1: rapply equiv_pointify_map. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. cbv; reflexivity. Defined. diff --git a/theories/Pointed/Loops.v b/theories/Pointed/Loops.v index 66a4736048a..7feee4dfb31 100644 --- a/theories/Pointed/Loops.v +++ b/theories/Pointed/Loops.v @@ -428,7 +428,7 @@ Defined. (** [loops_inv] is a natural transformation. *) Global Instance is1natural_loops_inv : Is1Natural loops loops loops_inv. Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros A B f. srapply Build_pHomotopy. + intros p. refine (inv_Vp _ _ @ whiskerR _ (point_eq f) @ concat_pp_p _ _ _). diff --git a/theories/Pointed/pSusp.v b/theories/Pointed/pSusp.v index f63286ed73e..b1d302e691c 100644 --- a/theories/Pointed/pSusp.v +++ b/theories/Pointed/pSusp.v @@ -292,7 +292,7 @@ Global Instance is1natural_loop_susp_adjoint_r `{Funext} (A : pType) : Is1Natural (opyon (psusp A)) (opyon A o loops) (loop_susp_adjoint A). Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros B B' g f. refine ( _ @ cat_assoc_strong _ _ _). refine (ap (fun x => x o* loop_susp_unit A) _). diff --git a/theories/WildCat/Adjoint.v b/theories/WildCat/Adjoint.v index eb7775759bb..9e44791f872 100644 --- a/theories/WildCat/Adjoint.v +++ b/theories/WildCat/Adjoint.v @@ -112,7 +112,7 @@ Section AdjunctionData. Proof. snrapply Build_NatEquiv. 1: intros [x y]; exact (equiv_adjunction adj x y). - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros [a b] [a' b'] [f g] K. refine (_ @ ap (fun x : a $-> G b' => x $o f) (is1natural_equiv_adjunction_r adj a b b' g K)). @@ -125,7 +125,7 @@ Section AdjunctionData. snrapply Build_NatTrans. { hnf. intros x. exact (equiv_adjunction adj x (F x) (Id _)). } - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros x x' f. apply GpdHom_path. refine (_^ @ _ @ _). @@ -143,7 +143,7 @@ Section AdjunctionData. snrapply Build_NatTrans. { hnf. intros y. exact ((equiv_adjunction adj (G y) y)^-1 (Id _)). } - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros y y' f. apply GpdHom_path. refine (_^ @ _ @ _). @@ -335,7 +335,7 @@ Proof. - snrapply Build_NatTrans. + intros K. exact (nattrans_prewhisker (adjunction_unit adj) K). - + snrapply Build_Is1Natural'. + + snrapply Build_Is1Natural. intros K K' θ j. apply GpdHom_path. refine (_ @ is1natural_natequiv (natequiv_inverse @@ -348,7 +348,7 @@ Proof. - snrapply Build_NatTrans. + intros K. exact (nattrans_prewhisker (adjunction_counit adj) K). - + snrapply Build_Is1Natural'. + + snrapply Build_Is1Natural. intros K K' θ j. apply GpdHom_path. refine (_ @ is1natural_natequiv diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v index 8fe48b11223..a6708400f36 100644 --- a/theories/WildCat/Bifunctor.v +++ b/theories/WildCat/Bifunctor.v @@ -388,7 +388,7 @@ Global Instance is1natural_uncurry {A B C : Type} (nat_r : forall a, Is1Natural (F a) (G a) (fun y : B => alpha (a, y))) : Is1Natural (uncurry F) (uncurry G) alpha. Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros [a b] [a' b'] [f f']; cbn in *. change (?w $o ?x $== ?y $o ?z) with (Square z w x y). nrapply vconcatL. @@ -409,7 +409,7 @@ Proof. intros [alpha nat]. snrapply Build_NatTrans. - exact (alpha o equiv_prod_symm _ _). - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. intros [b a] [b' a'] [g f]. exact (nat (a, b) (a', b') (f, g)). Defined. diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v index 5d70cb78a8e..fd86dd9d2a8 100644 --- a/theories/WildCat/Monoidal.v +++ b/theories/WildCat/Monoidal.v @@ -682,7 +682,7 @@ Section TwistConstruction. Proof. snrapply Build_Associator. - exact associator_twist'. - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. simpl; intros [[a b] c] [[a' b'] c'] [[f g] h]; simpl in f, g, h. (** To prove naturality it will be easier to reason about squares. *) change (?w $o ?x $== ?y $o ?z) with (Square z w x y). @@ -718,7 +718,7 @@ Section TwistConstruction. snrapply Build_NatEquiv'. - snrapply Build_NatTrans. + exact (fun a => right_unitor a $o braid cat_tensor_unit a). - + snrapply Build_Is1Natural'. + + snrapply Build_Is1Natural. intros a b f. change (?w $o ?x $== ?y $o ?z) with (Square z w x y). nrapply vconcat. diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v index c52a798d17b..e97a96885dd 100644 --- a/theories/WildCat/NatTrans.v +++ b/theories/WildCat/NatTrans.v @@ -57,30 +57,36 @@ Class Is1Natural {A B : Type} `{IsGraph A, Is1Cat B} (F : A -> B) `{!Is0Functor F} (G : A -> B) `{!Is0Functor G} (alpha : F $=> G) := Build_Is1Natural' { isnat {a a'} (f : a $-> a') : alpha a' $o fmap F f $== fmap G f $o alpha a; + (** We also include the transposed naturality square in the definition so that opposite natural transformations are definitionally involutive. In most cases, this will be constructed to be the inverse of the [isnat] field. *) + isnat_tr {a a'} (f : a $-> a') : fmap G f $o alpha a $== alpha a' $o fmap F f; }. Arguments Is1Natural {A B} {isgraph_A} {isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B} F {is0functor_F} G {is0functor_G} alpha : rename. Arguments isnat {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename. +Arguments isnat_tr {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename. (** We coerce naturality proofs to their naturality square as the [isnat] projection can be unwieldy in certain situations where the transformation is difficult to write down. This allows for the naturality proof to be used directly. *) Coercion isnat : Is1Natural >-> Funclass. -(** TODO: make this part of the data for definitional involution of op *) -(** The transposed natural square. *) -Definition isnat_tr {A B : Type} `{IsGraph A} `{Is1Cat B} - {F : A -> B} `{!Is0Functor F} {G : A -> B} `{!Is0Functor G} - (alpha : F $=> G) `{!Is1Natural F G alpha} {a a' : A} (f : a $-> a') - : fmap G f $o alpha a $== alpha a' $o fmap F f - := (isnat alpha f)^$. +Definition Build_Is1Natural {A B : Type} `{IsGraph A} `{Is1Cat B} + {F G : A -> B} `{!Is0Functor F, !Is0Functor G} (alpha : F $=> G) + (isnat : forall a a' (f : a $-> a'), alpha a' $o fmap F f $== fmap G f $o alpha a) + : Is1Natural F G alpha. +Proof. + snrapply Build_Is1Natural'. + - exact isnat. + - intros a a' f. + exact (isnat a a' f)^$. +Defined. (** The identity transformation is 1-natural. *) Global Instance is1natural_id {A B : Type} `{IsGraph A} `{Is1Cat B} (F : A -> B) `{!Is0Functor F} : Is1Natural F F (trans_id F). Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros a b f; cbn. refine (cat_idl _ $@ (cat_idr _)^$). Defined. @@ -92,7 +98,7 @@ Global Instance is1natural_comp {A B : Type} `{IsGraph A} `{Is1Cat B} (alpha : F $=> G) `{!Is1Natural F G alpha} : Is1Natural F K (trans_comp gamma alpha). Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros a b f; unfold trans_comp; cbn. refine (cat_assoc _ _ _ $@ (_ $@L isnat alpha f) $@ _). refine (cat_assoc_opp _ _ _ $@ (isnat gamma f $@R _) $@ _). @@ -105,7 +111,7 @@ Global Instance is1natural_prewhisker {A B C : Type} {F G : B -> C} (K : A -> B) (gamma : F $=> G) `{L : !Is1Natural F G gamma} : Is1Natural (F o K) (G o K) (trans_prewhisker gamma K). Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros x y f; unfold trans_prewhisker; cbn. exact (isnat gamma _). Defined. @@ -117,7 +123,7 @@ Global Instance is1natural_postwhisker {A B C : Type} {F G : A -> B} (K : B -> C (gamma : F $=> G) `{L : !Is1Natural F G gamma} : Is1Natural (K o F) (K o G) (trans_postwhisker K gamma). Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros x y f; unfold trans_postwhisker; cbn. refine (_^$ $@ _ $@ _). 1,3: rapply fmap_comp. @@ -132,7 +138,7 @@ Definition is1natural_homotopic {A B : Type} `{Is01Cat A} `{Is1Cat B} (p : forall a, alpha a $== gamma a) : Is1Natural F G alpha. Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros a b f. exact ((p b $@R _) $@ isnat gamma f $@ (_ $@L (p a)^$)). Defined. @@ -145,8 +151,10 @@ Global Instance is1natural_op A B `{Is01Cat A} `{Is1Cat B} Proof. unfold op. snrapply Build_Is1Natural'. - intros a b f. - srapply isnat_tr. + - intros a b f. + by snrapply isnat_tr. + - intros a b f. + by snrapply isnat. Defined. (** ** Natural transformations *) @@ -250,7 +258,7 @@ Proof. snrapply Build_NatEquiv. - intro a. refine (Build_CatEquiv (alpha a)). - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. intros a a' f. refine (cate_buildequiv_fun _ $@R _ $@ _ $@ (_ $@L cate_buildequiv_fun _)^$). apply (isnat alpha). @@ -301,7 +309,7 @@ Proof. intros [alpha I]. snrapply Build_NatEquiv. 1: intro a; symmetry; apply alpha. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros X Y f. apply vinverse, I. Defined. @@ -315,7 +323,7 @@ Definition natequiv_functor_assoc_ff_f {A B C D : Type} Proof. snrapply Build_NatEquiv. 1: intro; reflexivity. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros X Y f. refine (cat_prewhisker (id_cate_fun _) _ $@ cat_idl _ $@ _^$). refine (cat_postwhisker _ (id_cate_fun _) $@ cat_idr _). diff --git a/theories/WildCat/Paths.v b/theories/WildCat/Paths.v index ac301ecdd24..5d8944c442a 100644 --- a/theories/WildCat/Paths.v +++ b/theories/WildCat/Paths.v @@ -80,25 +80,25 @@ Proof. - intros a b c q r s t h g. exact (concat_whisker q r s t h g)^. - intros a b c d q r. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros s t h. apply concat_p_pp_nat_r. - intros a b c d q r. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros s t h. apply concat_p_pp_nat_m. - intros a b c d q r. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros s t h. apply concat_p_pp_nat_l. - intros a b. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros p q h; cbn. apply moveL_Mp. lhs nrapply concat_p_pp. exact (whiskerR_p1 h). - intros a b. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros p q h. apply moveL_Mp. lhs rapply concat_p_pp. diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v index 1742cfd7dd1..da9236bbb3b 100644 --- a/theories/WildCat/Products.v +++ b/theories/WildCat/Products.v @@ -163,7 +163,7 @@ Proof. nrapply (cate_prod_0gpd ie). intros i. exact (natequiv_yon_equiv_0gpd (e i) _). - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. intros a b f g j. cbn. destruct (eisretr ie j). @@ -666,7 +666,7 @@ Section Symmetry. - snrapply Build_NatTrans. + intros [x y]. exact (cat_binprod_swap x y). - + snrapply Build_Is1Natural'. + + snrapply Build_Is1Natural. intros [a b] [c d] [f g]; cbn in f, g. exact(cat_binprod_swap_nat f g). - exact cat_binprod_swap_cat_binprod_swap. @@ -856,7 +856,7 @@ Section Associativity. exact (cat_idl _ $@ (cat_idr _)^$). * nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_beta_pr2 _ _ $@R _) $@ _). exact ((mor_terminal_unique _ _ _)^$ $@ mor_terminal_unique _ _ _). - - snrapply Build_Is1Natural'. + - snrapply Build_Is1Natural. intros a b f. refine ((_ $@R _) $@ _ $@ (_ $@L _^$)). 1,3: nrapply cate_buildequiv_fun. diff --git a/theories/WildCat/Universe.v b/theories/WildCat/Universe.v index ab54714dbb6..8926c3924a0 100644 --- a/theories/WildCat/Universe.v +++ b/theories/WildCat/Universe.v @@ -155,15 +155,15 @@ Proof. symmetry. apply concat_Ap. - intros a b c d f g. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros h i p x; cbn. exact (concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^). - intros a b. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros f g p x; cbn. exact (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^). - intros a b. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. intros f g p x; cbn. exact (concat_p1 _ @ (concat_1p _)^). - reflexivity. diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v index 4737a58fe73..4af6d842b20 100644 --- a/theories/WildCat/Yoneda.v +++ b/theories/WildCat/Yoneda.v @@ -143,7 +143,7 @@ Global Instance is1natural_opyoneda {A : Type} `{Is1Cat A} (a : A) (F : A -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a) : Is1Natural (opyon a) F (opyoneda a F x). Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. unfold opyon, opyoneda; intros b c f g; cbn in *. exact (fmap_comp F g f x). Defined. @@ -317,7 +317,7 @@ Global Instance is1natural_opyoneda_0gpd {A : Type} `{Is1Cat A} (a : A) (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F} (x : F a) : Is1Natural (opyon_0gpd a) F (opyoneda_0gpd a F x). Proof. - snrapply Build_Is1Natural'. + snrapply Build_Is1Natural. unfold opyon_0gpd, opyoneda_0gpd; intros b c f g; cbn in *. exact (fmap_comp F g f x). Defined. From af11677e582b3faf07aa474317f48c937cc114c4 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 27 May 2024 19:23:38 +0200 Subject: [PATCH 2/5] more tests Signed-off-by: Ali Caglayan --- test/WildCat/Opposite.v | 58 +++++++++++++++++++++++++----------- theories/WildCat/Bifunctor.v | 10 ++++--- 2 files changed, 47 insertions(+), 21 deletions(-) diff --git a/test/WildCat/Opposite.v b/test/WildCat/Opposite.v index 6ee50a2183e..56f59deccf5 100644 --- a/test/WildCat/Opposite.v +++ b/test/WildCat/Opposite.v @@ -1,48 +1,72 @@ From HoTT Require Import Basics WildCat.Core WildCat.Opposite WildCat.Equiv - WildCat.NatTrans WildCat.Bifunctor. + WildCat.NatTrans WildCat.Bifunctor WildCat.Monoidal. (** Opposites are definitionally involutive. *) -Definition test1 A : A = (A^op)^op :> Type := 1. -Definition test2 A `{x : IsGraph A} : x = @isgraph_op A^op (@isgraph_op A x) := 1. -Definition test3 A `{x : Is01Cat A} : x = @is01cat_op A^op _ (@is01cat_op A _ x) := 1. -Definition test4 A `{x : Is2Graph A} : x = @is2graph_op A^op _ (@is2graph_op A _ x) := 1. -Definition test5 A `{x : Is1Cat A} : x = @is1cat_op A^op _ _ _ (@is1cat_op A _ _ _ x) := 1. +Succeed Definition t A : A = (A^op)^op :> Type := 1. +Succeed Definition t A `{x : IsGraph A} : x = @isgraph_op A^op (@isgraph_op A x) := 1. +Succeed Definition t A `{x : Is01Cat A} : x = @is01cat_op A^op _ (@is01cat_op A _ x) := 1. +Succeed Definition t A `{x : Is2Graph A} : x = @is2graph_op A^op _ (@is2graph_op A _ x) := 1. +Succeed Definition t A `{x : Is1Cat A} : x = @is1cat_op A^op _ _ _ (@is1cat_op A _ _ _ x) := 1. (** [core] only partially commutes with taking the opposite category. *) -Definition core1 A `{HasEquivs A} : (core A)^op = core A^op :> Type := 1. -Definition core2 A `{HasEquivs A} : isgraph_op (A:=core A) = isgraph_core (A:=A^op) := 1. -Definition core3 A `{HasEquivs A} : is01cat_op (A:=core A) = is01cat_core (A:=A^op) := 1. -Definition core4 A `{HasEquivs A} : is2graph_op (A:=core A) = is2graph_core (A:=A^op) := 1. +Succeed Definition t A `{HasEquivs A} : (core A)^op = core A^op :> Type := 1. +Succeed Definition t A `{HasEquivs A} : isgraph_op (A:=core A) = isgraph_core (A:=A^op) := 1. +Succeed Definition t A `{HasEquivs A} : is01cat_op (A:=core A) = is01cat_core (A:=A^op) := 1. +Succeed Definition t A `{HasEquivs A} : is2graph_op (A:=core A) = is2graph_core (A:=A^op) := 1. (** The Opaque line reduces the time from 0.3s to 0.07s. *) Opaque compose_catie_isretr. -Definition core5 A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op) := 1. +Succeed Definition t A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op) := 1. (** Opposite functors are definitionally involutive. *) -Definition test6 A B (F : A -> B) `{x : Is0Functor A B F} +Succeed Definition t A B (F : A -> B) `{x : Is0Functor A B F} : @is0functor_op _ _ F _ _ (@is0functor_op _ _ F _ _ x) = x := 1. -Definition test7 A B (F : A -> B) `{x : Is1Functor A B F} +Succeed Definition t A B (F : A -> B) `{x : Is1Functor A B F} : @is1functor_op _ _ F _ _ _ _ _ _ _ _ _ (@is1functor_op _ _ F _ _ _ _ _ _ _ _ _ x) = x := 1. (** Opposite bifunctors are definitionally involutive. *) -Definition test8 A B C (F : A -> B -> C) `{x : Is0Bifunctor A B C F} +Succeed Definition t A B C (F : A -> B -> C) `{x : Is0Bifunctor A B C F} : @is0bifunctor_op _ _ _ F _ _ _ (@is0bifunctor_op _ _ _ F _ _ _ x) = x := 1. -Definition test9 A B C (F : A -> B -> C) `{x : Is1Bifunctor A B C F} +Succeed Definition t A B C (F : A -> B -> C) `{x : Is1Bifunctor A B C F} : @is1bifunctor_op _ _ _ F _ _ _ _ _ _ _ _ _ _ _ _ _ (@is1bifunctor_op _ _ _ F _ _ _ _ _ _ _ _ _ _ _ _ _ x) = x := 1. (** Opposite natural transformations are definitionally involutive. *) -Definition test10 A `{Is01Cat A} B `{Is1Cat B} (F G : A -> B) +Succeed Definition t A `{Is01Cat A} B `{Is1Cat B} (F G : A -> B) `{!Is0Functor F, !Is0Functor G} (n : NatTrans F G) : nattrans_op (nattrans_op n) = n := 1. (** Opposite natural equivalences are definitionally involutive. *) -Definition test11 A `{Is01Cat A} B `{HasEquivs B} (F G : A -> B) +Succeed Definition t A `{Is01Cat A} B `{HasEquivs B} (F G : A -> B) `{!Is0Functor F, !Is0Functor G} (n : NatEquiv F G) : natequiv_op (natequiv_op n) = n := 1. + +(** Opposite left unitors are *not* definitionally involutive. *) +Fail Definition t A `{HasEquivs A} (unit : A) + (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : LeftUnitor F unit) + : @left_unitor_op _ _ _ _ _ _ F unit _ _ (@left_unitor_op _ _ _ _ _ _ F unit _ _ a) = a + := 1. + +(** Opposite right unitors are *not* definitionally involutive. *) +Fail Definition t A `{HasEquivs A} (unit : A) + (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : RightUnitor F unit) + : @right_unitor_op _ _ _ _ _ _ F unit _ _ (@right_unitor_op _ _ _ _ _ _ F unit _ _ a) = a + := 1. + +(** Opposite associators are *not* definitionally involutive. *) +Fail Definition t A `{HasEquivs A} + (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : Associator F) + : @associator_op _ _ _ _ _ _ F _ _ (@associator_op _ _ _ _ _ _ F _ _ a) = a + := 1. + +(** Opposite braidings are definitionally involutive. *) +Succeed Definition t A `{HasEquivs A} + (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : Braiding F) + : @braiding_op _ _ _ _ _ _ _ _ (@braiding_op _ _ _ _ _ _ _ _ a) = a + := 1. diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v index a6708400f36..865f8ceb6b6 100644 --- a/theories/WildCat/Bifunctor.v +++ b/theories/WildCat/Bifunctor.v @@ -406,12 +406,14 @@ Definition nattrans_flip {A B C : Type} : NatTrans (uncurry F) (uncurry G) -> NatTrans (uncurry (flip F)) (uncurry (flip G)). Proof. - intros [alpha nat]. + intros alpha. snrapply Build_NatTrans. - exact (alpha o equiv_prod_symm _ _). - - snrapply Build_Is1Natural. - intros [b a] [b' a'] [g f]. - exact (nat (a, b) (a', b') (f, g)). + - snrapply Build_Is1Natural'. + + intros [b a] [b' a'] [g f]. + exact (isnat (a:=(a, b)) (a':=(a', b')) alpha (f, g)). + + intros [b a] [b' a'] [g f]. + exact (isnat_tr (a:=(a, b)) (a':=(a', b')) alpha (f, g)). Defined. (** ** Opposite Bifunctors *) From 168072dc50a37ae821228429bddccdc10f059de0 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 27 May 2024 19:25:29 +0200 Subject: [PATCH 3/5] Update theories/WildCat/NatTrans.v Co-authored-by: Dan Christensen --- theories/WildCat/NatTrans.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v index e97a96885dd..eb35ed7d5df 100644 --- a/theories/WildCat/NatTrans.v +++ b/theories/WildCat/NatTrans.v @@ -151,10 +151,10 @@ Global Instance is1natural_op A B `{Is01Cat A} `{Is1Cat B} Proof. unfold op. snrapply Build_Is1Natural'. - - intros a b f. - by snrapply isnat_tr. - - intros a b f. - by snrapply isnat. + - intros a b. + exact (isnat_tr alpha). + - intros a b. + exact (isnat alpha). Defined. (** ** Natural transformations *) From 16bf5a0eb2da5cb95f2b21f0e618935f0c026b1a Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 27 May 2024 19:37:43 +0200 Subject: [PATCH 4/5] invert less when building naturality Signed-off-by: Ali Caglayan --- theories/WildCat/NatTrans.v | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v index eb35ed7d5df..ce2871fa1e6 100644 --- a/theories/WildCat/NatTrans.v +++ b/theories/WildCat/NatTrans.v @@ -258,10 +258,13 @@ Proof. snrapply Build_NatEquiv. - intro a. refine (Build_CatEquiv (alpha a)). - - snrapply Build_Is1Natural. - intros a a' f. - refine (cate_buildequiv_fun _ $@R _ $@ _ $@ (_ $@L cate_buildequiv_fun _)^$). - apply (isnat alpha). + - snrapply Build_Is1Natural'. + + intros a a' f. + refine ((cate_buildequiv_fun _ $@R _) $@ _ $@ (_ $@L cate_buildequiv_fun _)^$). + apply (isnat alpha). + + intros a a' f. + refine ((_ $@L cate_buildequiv_fun _) $@ _ $@ (cate_buildequiv_fun _ $@R _)^$). + apply (isnat_tr alpha). Defined. Definition natequiv_id {A B : Type} `{IsGraph A} `{HasEquivs B} @@ -308,10 +311,12 @@ Definition natequiv_inverse {A B : Type} `{IsGraph A} `{HasEquivs B} Proof. intros [alpha I]. snrapply Build_NatEquiv. - 1: intro a; symmetry; apply alpha. - snrapply Build_Is1Natural. - intros X Y f. - apply vinverse, I. + 1: exact (fun a => (alpha a)^-1$). + snrapply Build_Is1Natural'. + + intros X Y f. + apply vinverse, I. + + intros X Y f. + apply hinverse, I. Defined. (** This lemma might seem unnecessery since as functions ((F o G) o K) and (F o (G o K)) are definitionally equal. But the functor instances of both sides are different. This can be a nasty trap since you cannot see this difference clearly. *) From 2ca394fd1887de945053f2a30ca06fdbf36047e6 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 27 May 2024 21:30:07 +0200 Subject: [PATCH 5/5] make test names longer so it is clear they aren't args Signed-off-by: Ali Caglayan --- test/WildCat/Opposite.v | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/test/WildCat/Opposite.v b/test/WildCat/Opposite.v index 56f59deccf5..65a5558b3fb 100644 --- a/test/WildCat/Opposite.v +++ b/test/WildCat/Opposite.v @@ -2,71 +2,71 @@ From HoTT Require Import Basics WildCat.Core WildCat.Opposite WildCat.Equiv WildCat.NatTrans WildCat.Bifunctor WildCat.Monoidal. (** Opposites are definitionally involutive. *) -Succeed Definition t A : A = (A^op)^op :> Type := 1. -Succeed Definition t A `{x : IsGraph A} : x = @isgraph_op A^op (@isgraph_op A x) := 1. -Succeed Definition t A `{x : Is01Cat A} : x = @is01cat_op A^op _ (@is01cat_op A _ x) := 1. -Succeed Definition t A `{x : Is2Graph A} : x = @is2graph_op A^op _ (@is2graph_op A _ x) := 1. -Succeed Definition t A `{x : Is1Cat A} : x = @is1cat_op A^op _ _ _ (@is1cat_op A _ _ _ x) := 1. +Succeed Definition test A : A = (A^op)^op :> Type := 1. +Succeed Definition test A `{x : IsGraph A} : x = @isgraph_op A^op (@isgraph_op A x) := 1. +Succeed Definition test A `{x : Is01Cat A} : x = @is01cat_op A^op _ (@is01cat_op A _ x) := 1. +Succeed Definition test A `{x : Is2Graph A} : x = @is2graph_op A^op _ (@is2graph_op A _ x) := 1. +Succeed Definition test A `{x : Is1Cat A} : x = @is1cat_op A^op _ _ _ (@is1cat_op A _ _ _ x) := 1. (** [core] only partially commutes with taking the opposite category. *) -Succeed Definition t A `{HasEquivs A} : (core A)^op = core A^op :> Type := 1. -Succeed Definition t A `{HasEquivs A} : isgraph_op (A:=core A) = isgraph_core (A:=A^op) := 1. -Succeed Definition t A `{HasEquivs A} : is01cat_op (A:=core A) = is01cat_core (A:=A^op) := 1. -Succeed Definition t A `{HasEquivs A} : is2graph_op (A:=core A) = is2graph_core (A:=A^op) := 1. +Succeed Definition test A `{HasEquivs A} : (core A)^op = core A^op :> Type := 1. +Succeed Definition test A `{HasEquivs A} : isgraph_op (A:=core A) = isgraph_core (A:=A^op) := 1. +Succeed Definition test A `{HasEquivs A} : is01cat_op (A:=core A) = is01cat_core (A:=A^op) := 1. +Succeed Definition test A `{HasEquivs A} : is2graph_op (A:=core A) = is2graph_core (A:=A^op) := 1. (** The Opaque line reduces the time from 0.3s to 0.07s. *) Opaque compose_catie_isretr. -Succeed Definition t A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op) := 1. +Succeed Definition test A `{HasEquivs A} : is1cat_op (A:=core A) = is1cat_core (A:=A^op) := 1. (** Opposite functors are definitionally involutive. *) -Succeed Definition t A B (F : A -> B) `{x : Is0Functor A B F} +Succeed Definition test A B (F : A -> B) `{x : Is0Functor A B F} : @is0functor_op _ _ F _ _ (@is0functor_op _ _ F _ _ x) = x := 1. -Succeed Definition t A B (F : A -> B) `{x : Is1Functor A B F} +Succeed Definition test A B (F : A -> B) `{x : Is1Functor A B F} : @is1functor_op _ _ F _ _ _ _ _ _ _ _ _ (@is1functor_op _ _ F _ _ _ _ _ _ _ _ _ x) = x := 1. (** Opposite bifunctors are definitionally involutive. *) -Succeed Definition t A B C (F : A -> B -> C) `{x : Is0Bifunctor A B C F} +Succeed Definition test A B C (F : A -> B -> C) `{x : Is0Bifunctor A B C F} : @is0bifunctor_op _ _ _ F _ _ _ (@is0bifunctor_op _ _ _ F _ _ _ x) = x := 1. -Succeed Definition t A B C (F : A -> B -> C) `{x : Is1Bifunctor A B C F} +Succeed Definition test A B C (F : A -> B -> C) `{x : Is1Bifunctor A B C F} : @is1bifunctor_op _ _ _ F _ _ _ _ _ _ _ _ _ _ _ _ _ (@is1bifunctor_op _ _ _ F _ _ _ _ _ _ _ _ _ _ _ _ _ x) = x := 1. (** Opposite natural transformations are definitionally involutive. *) -Succeed Definition t A `{Is01Cat A} B `{Is1Cat B} (F G : A -> B) +Succeed Definition test A `{Is01Cat A} B `{Is1Cat B} (F G : A -> B) `{!Is0Functor F, !Is0Functor G} (n : NatTrans F G) : nattrans_op (nattrans_op n) = n := 1. (** Opposite natural equivalences are definitionally involutive. *) -Succeed Definition t A `{Is01Cat A} B `{HasEquivs B} (F G : A -> B) +Succeed Definition test A `{Is01Cat A} B `{HasEquivs B} (F G : A -> B) `{!Is0Functor F, !Is0Functor G} (n : NatEquiv F G) : natequiv_op (natequiv_op n) = n := 1. (** Opposite left unitors are *not* definitionally involutive. *) -Fail Definition t A `{HasEquivs A} (unit : A) +Fail Definition test A `{HasEquivs A} (unit : A) (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : LeftUnitor F unit) : @left_unitor_op _ _ _ _ _ _ F unit _ _ (@left_unitor_op _ _ _ _ _ _ F unit _ _ a) = a := 1. (** Opposite right unitors are *not* definitionally involutive. *) -Fail Definition t A `{HasEquivs A} (unit : A) +Fail Definition test A `{HasEquivs A} (unit : A) (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : RightUnitor F unit) : @right_unitor_op _ _ _ _ _ _ F unit _ _ (@right_unitor_op _ _ _ _ _ _ F unit _ _ a) = a := 1. (** Opposite associators are *not* definitionally involutive. *) -Fail Definition t A `{HasEquivs A} +Fail Definition test A `{HasEquivs A} (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : Associator F) : @associator_op _ _ _ _ _ _ F _ _ (@associator_op _ _ _ _ _ _ F _ _ a) = a := 1. (** Opposite braidings are definitionally involutive. *) -Succeed Definition t A `{HasEquivs A} +Succeed Definition test A `{HasEquivs A} (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : Braiding F) : @braiding_op _ _ _ _ _ _ _ _ (@braiding_op _ _ _ _ _ _ _ _ a) = a := 1.