From b6f28add2c788526effdf4de86268235e07987a8 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 27 Jan 2024 10:53:17 -0500 Subject: [PATCH 01/10] Use snrefine instead of simple notypeclasses refine --- theories/Basics/Equivalences.v | 14 +++++++------- theories/Categories/Category/Sigma/Univalent.v | 2 +- theories/Modalities/Descent.v | 6 +++--- theories/Modalities/Localization.v | 2 +- theories/Modalities/Nullification.v | 2 +- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v index 1034a488773..433c65c9d7a 100644 --- a/theories/Basics/Equivalences.v +++ b/theories/Basics/Equivalences.v @@ -599,7 +599,7 @@ Ltac build_record := (* Construct an equivalence between two possibly-nested record/sigma types that differ only by associativity and permutation of their components. We could use [Build_Equiv] and directly construct [eisadj] by decomposing to reflexivity as well, but often with large nested types it seems to be faster to adjointify. *) Ltac make_equiv := - simple notypeclasses refine (equiv_adjointify _ _ _ _); + snrefine (equiv_adjointify _ _ _ _); [ decomposing_intros; build_record | decomposing_intros; build_record | decomposing_intros; exact idpath @@ -607,9 +607,9 @@ Ltac make_equiv := (** In case anyone ever needs it, here's the version that doesn't adjointify. It's not the default, because it can be slow. *) Ltac make_equiv_without_adjointification := - simple notypeclasses refine (Build_Equiv _ _ _ _); + snrefine (Build_Equiv _ _ _ _); [ decomposing_intros; build_record | - simple notypeclasses refine (Build_IsEquiv _ _ _ _ _ _ _); + snrefine (Build_IsEquiv _ _ _ _ _ _ _); [ decomposing_intros; build_record | decomposing_intros; exact idpath | decomposing_intros; exact idpath @@ -626,7 +626,7 @@ Goal forall (A : Type) (B : A -> Type) (C : forall a:A, B a -> Type) (D : forall make_equiv. Undo. (** Here's the eventually successful proof script produced by [make_equiv], extracted from [Info 0 make_equiv] and prettified, so you can step through it and see how the tactic works. *) - simple notypeclasses refine (equiv_adjointify _ _ _ _). + snrefine (equiv_adjointify _ _ _ _). - (** Here begins [decomposing_intros] *) intros x; cbn in x. elim x; clear x. @@ -697,7 +697,7 @@ Goal forall (A:Type) (R:A->A->Type), intros A R. make_equiv. Undo. - simple notypeclasses refine (equiv_adjointify _ _ _ _). + snrefine (equiv_adjointify _ _ _ _). - intros x; cbn in x. elim x; clear x. intros a1; cbn in a1. @@ -785,7 +785,7 @@ Ltac build_record_with_evars := (** Now here's the improved version of [make_equiv]. *) Ltac make_equiv_contr_basedpaths := - simple notypeclasses refine (equiv_adjointify _ _ _ _); + snrefine (equiv_adjointify _ _ _ _); (** [solve [ unshelve TAC ]] ensures that [TAC] succeeds without leaving any leftover evars. *) [ decomposing_intros_with_paths; solve [ unshelve build_record_with_evars ] | decomposing_intros_with_paths; solve [ unshelve build_record_with_evars ] @@ -802,7 +802,7 @@ Section Examples. Proof. make_equiv_contr_basedpaths. Undo. - simple notypeclasses refine (equiv_adjointify _ _ _ _). + snrefine (equiv_adjointify _ _ _ _). - (** Here begins [decomposing_intros_with_paths] *) intros x; cbn in x. elim x; clear x. diff --git a/theories/Categories/Category/Sigma/Univalent.v b/theories/Categories/Category/Sigma/Univalent.v index 966312d1a34..bed82289eb2 100644 --- a/theories/Categories/Category/Sigma/Univalent.v +++ b/theories/Categories/Category/Sigma/Univalent.v @@ -336,7 +336,7 @@ Section on_both. : IsCategory A'. Proof. intros s d. - simple notypeclasses refine (isequiv_homotopic + snrefine (isequiv_homotopic ((equiv_iso_A'^-1) o (functor_sigma _ _) o (path_sigma_uncurried _ _ _)^-1) diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v index 72749d4bd3a..a6c6bdba951 100644 --- a/theories/Modalities/Descent.v +++ b/theories/Modalities/Descent.v @@ -226,7 +226,7 @@ Global Instance OO_inverts_functor_hfiber : O_inverts O (functor_hfiber p b). Proof. unfold functor_hfiber. - simple notypeclasses refine (OO_inverts_functor_sigma _ _). + snrefine (OO_inverts_functor_sigma _ _). 1:exact _. intros a; cbn. refine (isequiv_homotopic (O_functor O (concat (p a)^) o O_functor O (@ap _ _ k (f a) b)) _). @@ -313,10 +313,10 @@ Global Instance OO_inverts_functor_pullback : O_inverts O (functor_pullback f1 g1 f2 g2 h k l p q). Proof. unfold functor_pullback. - simple notypeclasses refine (OO_inverts_functor_sigma _ _). + snrefine (OO_inverts_functor_sigma _ _). 1:exact _. intros b1; cbn. - simple notypeclasses refine (OO_inverts_functor_sigma _ _). + snrefine (OO_inverts_functor_sigma _ _). 1:exact _. intros c1; cbn. pose @isequiv_compose. (* Speed up typeclass search. *) diff --git a/theories/Modalities/Localization.v b/theories/Modalities/Localization.v index ce004a1ca6f..ee7edc0f1a8 100644 --- a/theories/Modalities/Localization.v +++ b/theories/Modalities/Localization.v @@ -339,7 +339,7 @@ End Localization. Definition Loc@{a i} (f : LocalGenerators@{a}) : ReflectiveSubuniverse@{i}. Proof. - simple notypeclasses refine (Build_ReflectiveSubuniverse + snrefine (Build_ReflectiveSubuniverse (Build_Subuniverse (IsLocal f) _ _) (fun A => Build_PreReflects _ A (Localize f A) _ (@loc f A)) (fun A => Build_Reflects _ _ _ _)). diff --git a/theories/Modalities/Nullification.v b/theories/Modalities/Nullification.v index 219edcb5f4e..cc037219ceb 100644 --- a/theories/Modalities/Nullification.v +++ b/theories/Modalities/Nullification.v @@ -50,7 +50,7 @@ Proof. - exact _. - intros A. (** We take care with universes. *) - simple notypeclasses refine (reflectsD_from_OO_ind@{i} _ _ _). + snrefine (reflectsD_from_OO_ind@{i} _ _ _). + intros B B_inO g. refine (Localize_ind@{a i i i} (null_to_local_generators S) A B g _); intros i. apply ooextendable_over_unit; intros c. From 3975076eb1d48fcadc6eb1e513bb4d96a11be375 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 28 Jan 2024 12:48:29 -0500 Subject: [PATCH 02/10] Add "n" (notypeclasses) to some (s)rapply and (s)refine tactics --- theories/Classes/interfaces/abstract_algebra.v | 2 +- theories/Colimits/Colimit_Sigma.v | 2 +- theories/Cubical/PathSquare.v | 2 +- theories/Diagrams/Cocone.v | 2 +- theories/HIT/FreeIntQuotient.v | 4 ++-- theories/Homotopy/ExactSequence.v | 2 +- theories/Homotopy/HomotopyGroup.v | 2 +- theories/Homotopy/PinSn.v | 2 +- theories/Modalities/Lex.v | 2 +- theories/WildCat/Induced.v | 2 +- theories/WildCat/Opposite.v | 2 +- theories/WildCat/Sum.v | 2 +- 12 files changed, 13 insertions(+), 13 deletions(-) diff --git a/theories/Classes/interfaces/abstract_algebra.v b/theories/Classes/interfaces/abstract_algebra.v index e4c3083752e..329bc80826b 100644 --- a/theories/Classes/interfaces/abstract_algebra.v +++ b/theories/Classes/interfaces/abstract_algebra.v @@ -461,7 +461,7 @@ Proof. srapply (contr_equiv _ (ap (equiv_sigma_prod0 _ _)^-1)). srapply (contr_equiv _ (equiv_path_prod _ _)). destruct a'' as [a a''], b'' as [b b'']; cbn. - srapply contr_prod. + snrapply contr_prod. all: srapply contr_paths_contr. all: srapply contr_inhabited_hprop. all: srapply istrunc_forall. diff --git a/theories/Colimits/Colimit_Sigma.v b/theories/Colimits/Colimit_Sigma.v index 0803380f670..69003e431ec 100644 --- a/theories/Colimits/Colimit_Sigma.v +++ b/theories/Colimits/Colimit_Sigma.v @@ -107,7 +107,7 @@ Section ColimitSigma. apply path_forall; intros [y x]; simpl. rewrite <- cocone_precompose_postcompose. srapply (apD10 (g := fun x => f (y; x)) _ x). - srapply equiv_moveR_equiv_V. + snrapply equiv_moveR_equiv_V. srapply path_cocone. 1: reflexivity. intros i j g x'; simpl. diff --git a/theories/Cubical/PathSquare.v b/theories/Cubical/PathSquare.v index 988aa6557c2..a693fdfa84d 100644 --- a/theories/Cubical/PathSquare.v +++ b/theories/Cubical/PathSquare.v @@ -71,7 +71,7 @@ Definition equiv_sq_path {A} {a00 a10 a01 a11 : A} {p0x : a00 = a01} {p1x : a10 = a11} : px0 @ p1x = p0x @ px1 <~> PathSquare px0 px1 p0x p1x. Proof. - srapply Build_Equiv. + snrapply Build_Equiv. { destruct p0x, p1x. intro e. generalize (e @ concat_1p _). diff --git a/theories/Diagrams/Cocone.v b/theories/Diagrams/Cocone.v index cbc82f09037..174e0e844f9 100644 --- a/theories/Diagrams/Cocone.v +++ b/theories/Diagrams/Cocone.v @@ -252,7 +252,7 @@ Section FunctorialityCocone. (C : Cocone D X) (_ : UniversalCocone C) : UniversalCocone (cocone_postcompose C f). Proof. - srapply Build_UniversalCocone; intro. + snrapply Build_UniversalCocone; intro. rewrite <- (path_forall _ _ (fun g => cocone_postcompose_comp f g C)). srapply isequiv_compose. Defined. diff --git a/theories/HIT/FreeIntQuotient.v b/theories/HIT/FreeIntQuotient.v index 073cebf9f1c..9b3a0c59dc8 100644 --- a/theories/HIT/FreeIntQuotient.v +++ b/theories/HIT/FreeIntQuotient.v @@ -25,7 +25,7 @@ Section FreeIntAction. (** Together, [R] and [f] define a fibration over [Circle]. By the flattening lemma, its total space is equivalent to the quotient. *) Global Instance isset_RmodZ : IsHSet RmodZ. Proof. - refine (istrunc_equiv_istrunc + nrefine (istrunc_equiv_istrunc { z : Circle & Circle_rec Type R (path_universe f) z} (_ oE (@equiv_flattening _ Unit Unit idmap idmap (fun _ => R) (fun _ => f))^-1 @@ -74,7 +74,7 @@ Section FreeIntAction. exact (Coeq_rec_beta_cglue _ _ _ _). - apply istrunc_S. intros xu yv. - refine (istrunc_equiv_istrunc (n := -1) _ (equiv_path_sigma _ xu yv)). + nrefine (istrunc_equiv_istrunc (n := -1) _ (equiv_path_sigma _ xu yv)). destruct xu as [x u], yv as [y v]; cbn. apply hprop_allpath. intros [p r] [q s]. diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v index 14018928b96..407df6933a4 100644 --- a/theories/Homotopy/ExactSequence.v +++ b/theories/Homotopy/ExactSequence.v @@ -250,7 +250,7 @@ Definition isexact_equiv_fiber n {F F' X Y : pType} `{E : IsExact n _ _ _ i f} : IsExact n (i o* phi) f. Proof. - srapply Build_IsExact. + snrapply Build_IsExact. 1: apply iscomplex_equiv_fiber, cx_isexact. apply (conn_map_homotopic _ (cxfib cx_isexact o* phi)). { intro x; cbn. diff --git a/theories/Homotopy/HomotopyGroup.v b/theories/Homotopy/HomotopyGroup.v index 654745d8c66..0939248c0da 100644 --- a/theories/Homotopy/HomotopyGroup.v +++ b/theories/Homotopy/HomotopyGroup.v @@ -262,7 +262,7 @@ Defined. Lemma grp_iso_pi_prod {n : nat} (X Y : pType) : GroupIsomorphism (Pi n.+1 (X * Y)) (grp_prod (Pi n.+1 X) (Pi n.+1 Y)). Proof. - srapply Build_GroupIsomorphism. + snrapply Build_GroupIsomorphism. (* The underlying map is the natural one, so it is automatically a group homomorphism. *) - apply grp_prod_corec. + exact (fmap (Pi n.+1) (@pfst X Y)). diff --git a/theories/Homotopy/PinSn.v b/theories/Homotopy/PinSn.v index a8115d2925a..8c6774a6e29 100644 --- a/theories/Homotopy/PinSn.v +++ b/theories/Homotopy/PinSn.v @@ -78,7 +78,7 @@ Section PinSn. refine (_ $oE groupiso_pi_loops n.+1 (psphere n.+3)). refine (IHn $oE _). symmetry. - srapply (grp_iso_pi_connmap _ (loop_susp_unit (psphere n.+2))). + snrapply (grp_iso_pi_connmap _ (loop_susp_unit (psphere n.+2))). (* The (n+2)-sphere is (n+1)-connected, so [loop_susp_unit] is [n +2+ n]-connected. Since [n.+2 <= n +2+ n], we're done, after some [trunc_index] juggling. *) apply (isconnmap_pred_add n.-2). rewrite 2 trunc_index_add_succ. diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v index 3d7807a2e1e..7ffc61cabe4 100644 --- a/theories/Modalities/Lex.v +++ b/theories/Modalities/Lex.v @@ -181,7 +181,7 @@ Section LexModality. pose proof (O_inverts_isconnected O (fun _:A => tt)). exists (OO_descend_O_inverts O O (fun _:A => tt) P tt); split. - apply OO_descend_O_inverts_inO. - - intros; rapply OO_descend_O_inverts_beta. + - intros; nrapply OO_descend_O_inverts_beta. Defined. (** RSS Theorem 3.11 (iii): in the accessible case, the universe is modal. *) diff --git a/theories/WildCat/Induced.v b/theories/WildCat/Induced.v index 3a368f2b983..04eb1a60b7c 100644 --- a/theories/WildCat/Induced.v +++ b/theories/WildCat/Induced.v @@ -52,7 +52,7 @@ Section Induced_category. Local Instance is1cat_induced `{Is1Cat B} : Is1Cat A. Proof. - srapply Build_Is1Cat; + snrapply Build_Is1Cat; unfold isgraph_induced, is2graph_induced, is01cat_induced, is0functor_induced in *; cbn in *. diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v index 64659d9b919..844debec491 100644 --- a/theories/WildCat/Opposite.v +++ b/theories/WildCat/Opposite.v @@ -36,7 +36,7 @@ Defined. Global Instance is1cat_op {A : Type} `{Is1Cat A} : Is1Cat A^op. Proof. - srapply Build_Is1Cat; unfold op in *; cbv in *. + snrapply Build_Is1Cat; unfold op in *; cbv in *. - intros a b. apply is01cat_hom. - intros a b. diff --git a/theories/WildCat/Sum.v b/theories/WildCat/Sum.v index 6d897d88514..32331dcf618 100644 --- a/theories/WildCat/Sum.v +++ b/theories/WildCat/Sum.v @@ -37,7 +37,7 @@ Defined. Global Instance is1cat_sum A B `{ Is1Cat A } `{ Is1Cat B} : Is1Cat (A + B). Proof. - srapply Build_Is1Cat. + snrapply Build_Is1Cat. - intros x y. srapply Build_Is01Cat; destruct x as [a1 | b1], y as [a2 | b2]; From 38ed29c675ef44889f1f85f1a7bd40d072a5c990 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 28 Jan 2024 13:26:03 -0500 Subject: [PATCH 03/10] Remove `{Univalence} when it isn't needed --- theories/Algebra/AbGroups/AbPushout.v | 2 +- theories/Algebra/AbSES/Core.v | 2 +- theories/Algebra/AbSES/Pullback.v | 4 ++-- theories/Algebra/AbSES/Pushout.v | 6 +++--- theories/Classes/theory/integers.v | 2 +- theories/Homotopy/EMSpace.v | 2 +- theories/Sets/Ordinals.v | 2 +- theories/Spaces/Int/LoopExp.v | 2 +- 8 files changed, 11 insertions(+), 11 deletions(-) diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v index 2db3ff2f0ee..5ca08bee130 100644 --- a/theories/Algebra/AbGroups/AbPushout.v +++ b/theories/Algebra/AbGroups/AbPushout.v @@ -169,7 +169,7 @@ Defined. (** ** Properties of pushouts of maps *) (** The pushout of an epimorphism is an epimorphism. *) -Global Instance ab_pushout_surjection_inr `{Univalence} {A B C : AbGroup} +Global Instance ab_pushout_surjection_inr {A B C : AbGroup} (f : A $-> B) (g : A $-> C) `{S : IsSurjection f} : IsSurjection (ab_pushout_inr (f:=f) (g:=g)). Proof. diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v index 625e0d1327a..0d1c3c5e9b6 100644 --- a/theories/Algebra/AbSES/Core.v +++ b/theories/Algebra/AbSES/Core.v @@ -486,7 +486,7 @@ Definition loops_abses `{Univalence} {A B : AbGroup} := equiv_path_abses oE abses_endomorphism_trivial^-1. (** We can transfer a loop of the trivial short exact sequence to any other. *) -Definition hom_loops_data_abses `{Univalence} {A B : AbGroup} (E : AbSES B A) +Definition hom_loops_data_abses {A B : AbGroup} (E : AbSES B A) : (B $-> A) -> abses_path_data E E. Proof. intro phi. diff --git a/theories/Algebra/AbSES/Pullback.v b/theories/Algebra/AbSES/Pullback.v index 2f67a820c16..a429de529eb 100644 --- a/theories/Algebra/AbSES/Pullback.v +++ b/theories/Algebra/AbSES/Pullback.v @@ -114,7 +114,7 @@ Definition abses_directsum_distributive_pullbacks `{Univalence} := (abses_pullback_component1_id (abses_directsum_pullback_morphism f g) (fun _ => idpath))^. -Definition abses_path_pullback_projection_commsq `{Univalence} +Definition abses_path_pullback_projection_commsq {A B B' : AbGroup@{u}} (bt : B' $-> B) (E : AbSES B A) (F : AbSES B' A) (p : abses_pullback bt E = F) : exists phi : middle F $-> E, projection E o phi == bt o projection F. @@ -329,7 +329,7 @@ Defined. (** *** Pulling [E] back along [projection E] is trivial *) -Definition abses_pullback_projection_morphism `{Univalence} {B A : AbGroup} (E : AbSES B A) +Definition abses_pullback_projection_morphism {B A : AbGroup} (E : AbSES B A) : AbSESMorphism (pt : AbSES E A) E. Proof. srapply (Build_AbSESMorphism grp_homo_id _ (projection E)). diff --git a/theories/Algebra/AbSES/Pushout.v b/theories/Algebra/AbSES/Pushout.v index fabda362812..93529d4b632 100644 --- a/theories/Algebra/AbSES/Pushout.v +++ b/theories/Algebra/AbSES/Pushout.v @@ -266,7 +266,7 @@ Definition abses_pushout_pmap `{Univalence} {A A' B : AbGroup} (f : A $-> A') := to_pointed (abses_pushout' f). (** The following general lemma lets us show that [abses_pushout f E] is trivial in cases of interest. It says that if you have a map [phi : E -> A'], then if you push out along the restriction [phi $o inclusion E], the result is trivial. Specifically, we get a morphism witnessing this fact. *) -Definition abses_pushout_trivial_morphism `{Univalence} {B A A' : AbGroup} +Definition abses_pushout_trivial_morphism {B A A' : AbGroup} (E : AbSES B A) (f : A $-> A') (phi : middle E $-> A') (k : f == phi $o inclusion E) : AbSESMorphism E (pt : AbSES B A'). @@ -280,7 +280,7 @@ Proof. Defined. (** The pushout of a short exact sequence along its inclusion map is trivial. *) -Definition abses_pushout_inclusion_morphism `{Univalence} {B A : AbGroup} (E : AbSES B A) +Definition abses_pushout_inclusion_morphism {B A : AbGroup} (E : AbSES B A) : AbSESMorphism E (pt : AbSES B E) := abses_pushout_trivial_morphism E (inclusion E) grp_homo_id (fun _ => idpath). @@ -290,7 +290,7 @@ Definition abses_pushout_inclusion `{Univalence} {B A : AbGroup} (E : AbSES B A) (abses_pushout_inclusion_morphism E) (fun _ => idpath). (** Pushing out along [grp_homo_const] is trivial. *) -Definition abses_pushout_const_morphism `{Univalence} {B A A' : AbGroup} (E : AbSES B A) +Definition abses_pushout_const_morphism {B A A' : AbGroup} (E : AbSES B A) : AbSESMorphism E (pt : AbSES B A') := abses_pushout_trivial_morphism E grp_homo_const grp_homo_const (fun _ => idpath). diff --git a/theories/Classes/theory/integers.v b/theories/Classes/theory/integers.v index f9f705dbdc1..4d173c4fe4e 100644 --- a/theories/Classes/theory/integers.v +++ b/theories/Classes/theory/integers.v @@ -79,7 +79,7 @@ apply ap,E. Qed. Section retract_is_int. - Context `{Funext} `{Univalence}. + Context `{Funext}. Context `{Integers Z} `{IsRing Z2} {Z2ap : Apart Z2} {Z2le Z2lt} `{!FullPseudoSemiRingOrder (A:=Z2) Z2le Z2lt}. Context (f : Z -> Z2) `{!IsEquiv f} `{!IsSemiRingPreserving f} diff --git a/theories/Homotopy/EMSpace.v b/theories/Homotopy/EMSpace.v index 660d3008051..a2f366558e2 100644 --- a/theories/Homotopy/EMSpace.v +++ b/theories/Homotopy/EMSpace.v @@ -96,7 +96,7 @@ Section EilenbergMacLane. symmetry; apply (groupiso_pi_loops _ _). Defined. - Definition iscohhspace_em `{Univalence} {G : AbGroup} (n : nat) + Definition iscohhspace_em {G : AbGroup} (n : nat) : IsCohHSpace K(G, n). Proof. nrapply iscohhspace_equiv_cohhspace. diff --git a/theories/Sets/Ordinals.v b/theories/Sets/Ordinals.v index 53551658106..106f8c575de 100644 --- a/theories/Sets/Ordinals.v +++ b/theories/Sets/Ordinals.v @@ -512,7 +512,7 @@ Proof. rewrite transport_arrow_toconst. rewrite inv_V. apply initial_segment_property. Qed. -Lemma equiv_initial_segment_simulation `{Univalence} +Lemma equiv_initial_segment_simulation `{PropResizing} {A : Type@{A}} {R : Lt@{_ R} A} `{IsOrdinal A R} {B : Type@{B}} {Q : Lt@{_ Q} B} `{IsOrdinal B Q} diff --git a/theories/Spaces/Int/LoopExp.v b/theories/Spaces/Int/LoopExp.v index d32efdf650d..34f23f8da38 100644 --- a/theories/Spaces/Int/LoopExp.v +++ b/theories/Spaces/Int/LoopExp.v @@ -174,7 +174,7 @@ Qed. (** Under univalence, exponentiation of loops corresponds to iteration of autoequivalences. *) -Definition equiv_path_loopexp `{Univalence} +Definition equiv_path_loopexp {A : Type} (p : A = A) (z : Int) (a : A) : equiv_path A A (loopexp p z) a = int_iter (equiv_path A A p) z a. Proof. From b5fcdb8a4439793e612f0f04e0a8e157f06db7f0 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 28 Jan 2024 13:31:21 -0500 Subject: [PATCH 04/10] Change `{Univalence} to `{Funext} when possible --- theories/Algebra/AbSES/DirectSum.v | 2 +- theories/Algebra/AbSES/Pullback.v | 2 +- theories/Algebra/AbSES/SixTerm.v | 2 +- theories/Algebra/Groups/Group.v | 2 +- theories/Categories/Grothendieck/ToSet/Univalent.v | 2 +- theories/Colimits/Quotient/Choice.v | 6 +++--- theories/Homotopy/ExactSequence.v | 2 +- theories/Homotopy/Join/Core.v | 2 +- theories/Pointed/Loops.v | 4 ++-- theories/Sets/Ordinals.v | 2 +- theories/Truncations/Connectedness.v | 2 +- 11 files changed, 14 insertions(+), 14 deletions(-) diff --git a/theories/Algebra/AbSES/DirectSum.v b/theories/Algebra/AbSES/DirectSum.v index f4ba9e8c899..51fb2b27c9e 100644 --- a/theories/Algebra/AbSES/DirectSum.v +++ b/theories/Algebra/AbSES/DirectSum.v @@ -93,7 +93,7 @@ Proof. Defined. (** For [E, F, G : AbSES B A], there is a morphism [(E + F) + G -> (G + F) + E] induced by the above map, where [+] denotes [abses_direct_sum]. *) -Lemma abses_twist_directsum `{Univalence} {A B : AbGroup} (E F G : AbSES B A) +Lemma abses_twist_directsum `{Funext} {A B : AbGroup} (E F G : AbSES B A) : AbSESMorphism (abses_direct_sum (abses_direct_sum E F) G) (abses_direct_sum (abses_direct_sum G F) E). Proof. diff --git a/theories/Algebra/AbSES/Pullback.v b/theories/Algebra/AbSES/Pullback.v index a429de529eb..c23ee784951 100644 --- a/theories/Algebra/AbSES/Pullback.v +++ b/theories/Algebra/AbSES/Pullback.v @@ -392,7 +392,7 @@ Definition abses_pullback_phomotopic `{Univalence} {A B B' : AbGroup} (** *** Pulling back along a complex *) -Definition iscomplex_abses_pullback' `{Univalence} {A B0 B1 B2 : AbGroup} +Definition iscomplex_abses_pullback' `{Funext} {A B0 B1 B2 : AbGroup} (f : B0 $-> B1) (g : B1 $-> B2) (h : g $o f == grp_homo_const) : abses_pullback' f $o* abses_pullback' g $=>* @pmap_abses_const _ _ _ A. Proof. diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v index 818f00e6750..34a8ccb7e9d 100644 --- a/theories/Algebra/AbSES/SixTerm.v +++ b/theories/Algebra/AbSES/SixTerm.v @@ -24,7 +24,7 @@ Proof. Defined. (** Exactness of [ab_hom B G -> ab_hom E G -> ab_hom A G]. One can also deduce this from [isexact_abses_pullback]. *) -Definition isexact_ext_contra_sixterm_ii `{Univalence} +Definition isexact_ext_contra_sixterm_ii `{Funext} {B A G : AbGroup} (E : AbSES B A) : IsExact (Tr (-1)) (fmap10 (A:=Group^op) ab_hom (projection E) G) diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index d417140ba25..e4789ffc04b 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -772,7 +772,7 @@ Proof. apply path_contr. Defined. -Global Instance ishprop_grp_iso_trivial `{Univalence} (G : Group) +Global Instance ishprop_grp_iso_trivial `{Funext} (G : Group) : IsHProp (G ≅ grp_trivial). Proof. apply equiv_hprop_allpath. diff --git a/theories/Categories/Grothendieck/ToSet/Univalent.v b/theories/Categories/Grothendieck/ToSet/Univalent.v index 902a0f103a8..cf50d700483 100644 --- a/theories/Categories/Grothendieck/ToSet/Univalent.v +++ b/theories/Categories/Grothendieck/ToSet/Univalent.v @@ -15,7 +15,7 @@ Set Asymmetric Patterns. Local Open Scope morphism_scope. Section Grothendieck. - Context `{Univalence}. + Context `{Funext}. Variable C : PreCategory. Context `{IsCategory C}. diff --git a/theories/Colimits/Quotient/Choice.v b/theories/Colimits/Quotient/Choice.v index 9f77be44d58..b18b5a6d0d8 100644 --- a/theories/Colimits/Quotient/Choice.v +++ b/theories/Colimits/Quotient/Choice.v @@ -83,7 +83,7 @@ End choose_has_quotient_choice. (** The following section derives [HasTrChoice 0 A] from [HasQuotientChoice A]. *) Section has_tr0_choice_quotientchoice. - Context `{Univalence} (A : Type) (qch : HasQuotientChoice A). + Context `{Funext} (A : Type) (qch : HasQuotientChoice A). Local Definition RelUnit (B : A -> Type) (a : A) (b1 b2 : B a) : HProp := Build_HProp Unit. @@ -154,7 +154,7 @@ Proof. Qed. Global Instance isequiv_has_tr0_choice_to_has_quotient_choice - `{Univalence} (A : Type) + `{Funext} (A : Type) : IsEquiv (has_quotient_choice_tr0choice A). Proof. srapply isequiv_iff_hprop. @@ -163,7 +163,7 @@ Proof. Qed. Definition equiv_has_tr0_choice_has_quotient_choice - `{Univalence} (A : Type) + `{Funext} (A : Type) : HasTrChoice 0 A <~> HasQuotientChoice A := Build_Equiv _ _ (has_quotient_choice_tr0choice A) _. diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v index 407df6933a4..c42fcae4485 100644 --- a/theories/Homotopy/ExactSequence.v +++ b/theories/Homotopy/ExactSequence.v @@ -128,7 +128,7 @@ Proof. Defined. (** If Y is a set, then IsComplex is an HProp. *) -Global Instance ishprop_iscomplex_hset `{Univalence} {F X Y : pType} `{IsHSet Y} +Global Instance ishprop_iscomplex_hset `{Funext} {F X Y : pType} `{IsHSet Y} (i : F ->* X) (f : X ->* Y) : IsHProp (IsComplex i f) := _. diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v index 561f6195da7..1d76ad8990f 100644 --- a/theories/Homotopy/Join/Core.v +++ b/theories/Homotopy/Join/Core.v @@ -794,7 +794,7 @@ Section JoinTrunc. Defined. (** Joins add connectivity *) - Global Instance isconnected_join `{Univalence} {m n : trunc_index} + Global Instance isconnected_join `{Funext} {m n : trunc_index} (A B : Type) `{IsConnected m A} `{IsConnected n B} : IsConnected (m +2+ n) (Join A B). Proof. diff --git a/theories/Pointed/Loops.v b/theories/Pointed/Loops.v index 00c016388c3..3870802d073 100644 --- a/theories/Pointed/Loops.v +++ b/theories/Pointed/Loops.v @@ -392,7 +392,7 @@ Proof. Defined. (* 7.2.7 *) -Theorem equiv_istrunc_istrunc_loops `{Univalence} n X +Theorem equiv_istrunc_istrunc_loops `{Funext} n X : IsTrunc n.+2 X <~> forall (x : X), IsTrunc n.+1 (loops [X, x]). Proof. srapply equiv_iff_hprop. @@ -404,7 +404,7 @@ Proof. Defined. (* 7.2.9, with [n] here meaning the same as [n-1] there. Note that [n.-1] in the statement is short for [trunc_index_pred (nat_to_trunc_index n)] which is definitionally equal to [(trunc_index_inc minus_two n).+1]. *) -Theorem equiv_istrunc_contr_iterated_loops `{Univalence} (n : nat) +Theorem equiv_istrunc_contr_iterated_loops `{Funext} (n : nat) : forall A, IsTrunc n.-1 A <~> forall a : A, Contr (iterated_loops n [A, a]). Proof. induction n; intro A. diff --git a/theories/Sets/Ordinals.v b/theories/Sets/Ordinals.v index 106f8c575de..7a36f03beb1 100644 --- a/theories/Sets/Ordinals.v +++ b/theories/Sets/Ordinals.v @@ -348,7 +348,7 @@ Proof. Qed. -Global Instance ishprop_Isomorphism `{Univalence} (A B : Ordinal) +Global Instance ishprop_Isomorphism `{Funext} (A B : Ordinal) : IsHProp (Isomorphism A B). Proof. apply hprop_allpath; intros f g. apply path_sigma_hprop; cbn. diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v index 935a14d5a79..6d5792c3e96 100644 --- a/theories/Truncations/Connectedness.v +++ b/theories/Truncations/Connectedness.v @@ -36,7 +36,7 @@ One reason for our choice is that this way, the n-truncated and n-connected maps (Mnemonic for the indexing: think of the base case, where k=n; then we know we can eliminate, so the space of extensions is contractible.) This lemma is most useful via corollaries like the wedge-inclusion, the wiggly wedge, and their n-ary generalizations. *) -Lemma istrunc_extension_along_conn `{Univalence} {m n : trunc_index} +Lemma istrunc_extension_along_conn `{Funext} {m n : trunc_index} {A B : Type} (f : A -> B) `{IsConnMap n _ _ f} (P : B -> Type) {HP : forall b:B, IsTrunc (m +2+ n) (P b)} (d : forall a:A, P (f a)) From 9825e71e34eec7fbc67266698733f6a75a37adaf Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 28 Jan 2024 14:18:46 -0500 Subject: [PATCH 05/10] Remove `{Funext} when not needed --- theories/Algebra/AbSES/Core.v | 2 +- theories/Algebra/AbSES/Pullback.v | 8 ++++---- theories/Algebra/AbSES/PullbackFiberSequence.v | 8 ++++---- theories/Algebra/Groups/ShortExactSequence.v | 2 +- theories/Categories/FunctorCategory/Morphisms.v | 2 +- theories/Limits/Limit.v | 2 +- theories/Modalities/ReflectiveSubuniverse.v | 4 ++-- theories/Modalities/Separated.v | 2 +- theories/Truncations/Core.v | 2 +- theories/Types/Equiv.v | 2 +- theories/WildCat/Adjoint.v | 2 +- theories/WildCat/NatTrans.v | 2 +- 12 files changed, 19 insertions(+), 19 deletions(-) diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v index 0d1c3c5e9b6..8b0f9dda33a 100644 --- a/theories/Algebra/AbSES/Core.v +++ b/theories/Algebra/AbSES/Core.v @@ -189,7 +189,7 @@ Definition abses_path_data {B A : AbGroup@{u}} (E F : AbSES B A) & (phi $o inclusion _ == inclusion _) * (projection _ == projection _ $o phi)}. -Definition abses_path_data_to_iso `{Funext} {B A : AbGroup@{u}} (E F: AbSES B A) +Definition abses_path_data_to_iso {B A : AbGroup@{u}} (E F: AbSES B A) : abses_path_data E F -> abses_path_data_iso E F. Proof. - intros [phi [p q]]. diff --git a/theories/Algebra/AbSES/Pullback.v b/theories/Algebra/AbSES/Pullback.v index c23ee784951..8d08fdc8950 100644 --- a/theories/Algebra/AbSES/Pullback.v +++ b/theories/Algebra/AbSES/Pullback.v @@ -76,7 +76,7 @@ Proof. all: by apply equiv_path_grouphomomorphism. Defined. -Definition abses_pullback_component1_id' `{Funext} +Definition abses_pullback_component1_id' {A B B' : AbGroup@{u}} {E : AbSES B A} {F : AbSES B' A} (f : AbSESMorphism E F) (h : component1 f == grp_homo_id) : E $== abses_pullback (component3 f) F. @@ -289,7 +289,7 @@ Defined. (** *** Pulling back along constant maps *) -Lemma abses_pullback_const' `{Funext} {A B B' : AbGroup} +Lemma abses_pullback_const' {A B B' : AbGroup} : const pt $=> (@abses_pullback A B B' grp_homo_const). Proof. intro E. @@ -310,7 +310,7 @@ Definition abses_pullback_const `{Univalence} {A B B' : AbGroup} : const pt == @abses_pullback A B B' grp_homo_const := fun x => (equiv_path_abses_iso (abses_pullback_const' x)). -Lemma abses_pullback_pconst' `{Funext} {A B B' : AbGroup} +Lemma abses_pullback_pconst' {A B B' : AbGroup} : @pmap_abses_const B' A B A $=>* abses_pullback' grp_homo_const. Proof. srefine (_; _). @@ -392,7 +392,7 @@ Definition abses_pullback_phomotopic `{Univalence} {A B B' : AbGroup} (** *** Pulling back along a complex *) -Definition iscomplex_abses_pullback' `{Funext} {A B0 B1 B2 : AbGroup} +Definition iscomplex_abses_pullback' {A B0 B1 B2 : AbGroup} (f : B0 $-> B1) (g : B1 $-> B2) (h : g $o f == grp_homo_const) : abses_pullback' f $o* abses_pullback' g $=>* @pmap_abses_const _ _ _ A. Proof. diff --git a/theories/Algebra/AbSES/PullbackFiberSequence.v b/theories/Algebra/AbSES/PullbackFiberSequence.v index 4e05e625e55..005f51b8846 100644 --- a/theories/Algebra/AbSES/PullbackFiberSequence.v +++ b/theories/Algebra/AbSES/PullbackFiberSequence.v @@ -149,7 +149,7 @@ Defined. (** For exactness we need not only a preimage of [F] but a preimage of [(F,p)] along [cxfib]. We now define and prove this in terms of path data. *) (** The analog of [cxfib] induced by pullback in terms of path data. *) -Definition cxfib' `{Funext} {A B C : AbGroup} (E : AbSES C B) +Definition cxfib' {A B C : AbGroup} (E : AbSES C B) : AbSES C A -> graph_hfiber (abses_pullback (A:=A) (inclusion E)) pt. Proof. intro Y. @@ -160,7 +160,7 @@ Proof. symmetry; apply abses_pullback_const'. Defined. -Definition hfiber_cxfib' `{Funext} {A B C : AbGroup} (E : AbSES C B) +Definition hfiber_cxfib' {A B C : AbGroup} (E : AbSES C B) (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) := {Y : AbSES C A & hfiber_abses_path (cxfib' E Y) (F; p)}. @@ -210,7 +210,7 @@ Proof. Defined. (** The type of paths in [hfiber_cxfib'] in terms of path data. *) -Definition path_hfiber_cxfib' `{Funext} {A B C : AbGroup} {E : AbSES C B} +Definition path_hfiber_cxfib' {A B C : AbGroup} {E : AbSES C B} {F : AbSES (middle E) A} {p : abses_pullback (inclusion E) F $== pt} (X Y : hfiber_cxfib' (B:=B) E F p) : Type. @@ -284,7 +284,7 @@ Defined. (** To conclude exactness in terms of path data, we show that the fibre is a proposition, hence contractible. *) (** Given a point [(Y;Q)] in the fiber of [cxfib'] over [(F;p)] there is an induced map as follows. *) -Local Definition hfiber_cxfib'_induced_map `{Funext} {A B C : AbGroup} (E : AbSES C B) +Local Definition hfiber_cxfib'_induced_map {A B C : AbGroup} (E : AbSES C B) (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) (Y : hfiber_cxfib' E F p) : ab_biprod A B $-> abses_pullback (projection E) Y.1. diff --git a/theories/Algebra/Groups/ShortExactSequence.v b/theories/Algebra/Groups/ShortExactSequence.v index 0a77c3088ca..411305c96a6 100644 --- a/theories/Algebra/Groups/ShortExactSequence.v +++ b/theories/Algebra/Groups/ShortExactSequence.v @@ -39,7 +39,7 @@ Proof. Defined. (** A complex 0 -> A -> B of groups is purely exact if and only if the map A -> B is an embedding. *) -Lemma iff_grp_isexact_isembedding `{Funext} {A B : Group} (f : A $-> B) +Lemma iff_grp_isexact_isembedding {A B : Group} (f : A $-> B) : IsExact purely (@grp_homo_const grp_trivial A) f <-> IsEmbedding f. Proof. split. diff --git a/theories/Categories/FunctorCategory/Morphisms.v b/theories/Categories/FunctorCategory/Morphisms.v index be2cba55ba1..2e6d2cb37d4 100644 --- a/theories/Categories/FunctorCategory/Morphisms.v +++ b/theories/Categories/FunctorCategory/Morphisms.v @@ -46,7 +46,7 @@ Hint Extern 10 (@IsIsomorphism _ _ _ (@components_of ?C ?D ?F ?G ?T ?x)) => apply (fun H' => @isisomorphism_components_of _ C D F G T H' x) : typeclass_instances. -Definition inverse `{Funext} +Definition inverse C D (F G : Functor C D) (T : NaturalTransformation F G) `{forall x, IsIsomorphism (T x)} : NaturalTransformation G F. diff --git a/theories/Limits/Limit.v b/theories/Limits/Limit.v index 1d3cff849bc..81598042516 100644 --- a/theories/Limits/Limit.v +++ b/theories/Limits/Limit.v @@ -171,7 +171,7 @@ Defined. (** * Limits are right adjoint to constant diagram *) -Theorem limit_adjoint `{Funext} {G : Graph} {D : Diagram G} {C : Type} +Theorem limit_adjoint {G : Graph} {D : Diagram G} {C : Type} : (C -> Limit D) <~> DiagramMap (diagram_const C) D. Proof. srapply equiv_adjointify. diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v index 585aa177b28..aa3fe46d7dc 100644 --- a/theories/Modalities/ReflectiveSubuniverse.v +++ b/theories/Modalities/ReflectiveSubuniverse.v @@ -51,7 +51,7 @@ Definition inO_equiv_inO' {O : Subuniverse} : In O U := inO_equiv_inO T f. -Definition iff_inO_equiv `{Funext} (O : Subuniverse) +Definition iff_inO_equiv (O : Subuniverse) {T : Type} {U : Type} (f : T <~> U) : In O T <-> In O U := (fun H => inO_equiv_inO' _ f, fun H => inO_equiv_inO' _ f^-1). @@ -1636,7 +1636,7 @@ Section ConnectedMaps. Defined. (** Being connected is an hprop *) - Global Instance ishprop_isconnmap `{Funext} {A B : Type} (f : A -> B) + Global Instance ishprop_isconnmap {A B : Type} (f : A -> B) : IsHProp (IsConnMap O f). Proof. apply istrunc_forall. diff --git a/theories/Modalities/Separated.v b/theories/Modalities/Separated.v index d02da34f7bb..c27a421bd78 100644 --- a/theories/Modalities/Separated.v +++ b/theories/Modalities/Separated.v @@ -120,7 +120,7 @@ Proof. Defined. (* As a special case, if X embeds into an n-type for n >= -1 then X is an n-type. Note that this doesn't hold for n = -2. *) -Corollary istrunc_embedding_trunc `{Funext} {X Y : Type} {n : trunc_index} `{istr : IsTrunc n.+1 Y} +Corollary istrunc_embedding_trunc {X Y : Type} {n : trunc_index} `{istr : IsTrunc n.+1 Y} (i : X -> Y) `{isem : IsEmbedding i} : IsTrunc n.+1 X. Proof. apply istrunc_S. diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v index 063d7b7f59c..95e1296da22 100644 --- a/theories/Truncations/Core.v +++ b/theories/Truncations/Core.v @@ -123,7 +123,7 @@ Section TruncationModality. : IsEquiv (Trunc_functor f) := isequiv_O_functor (Tr n) f. - Definition equiv_Trunc_prod_cmp `{Funext} {X Y} + Definition equiv_Trunc_prod_cmp {X Y} : Tr n (X * Y) <~> Tr n X * Tr n Y := equiv_O_prod_cmp (Tr n) X Y. diff --git a/theories/Types/Equiv.v b/theories/Types/Equiv.v index 49ef24dda37..39487864daf 100644 --- a/theories/Types/Equiv.v +++ b/theories/Types/Equiv.v @@ -108,7 +108,7 @@ Section AssumeFunext. := equiv_isequiv (equiv_path_equiv e1 e2). (** The inverse equivalence is homotopic to [ap equiv_fun], so that is also an equivalence. *) - Global Instance isequiv_ap_equiv_fun `{Funext} {A B : Type} (e1 e2 : A <~> B) + Global Instance isequiv_ap_equiv_fun {A B : Type} (e1 e2 : A <~> B) : IsEquiv (ap (x:=e1) (y:=e2) (@equiv_fun A B)). Proof. snrapply isequiv_homotopic. diff --git a/theories/WildCat/Adjoint.v b/theories/WildCat/Adjoint.v index 333f3d3362f..68d865e06e6 100644 --- a/theories/WildCat/Adjoint.v +++ b/theories/WildCat/Adjoint.v @@ -324,7 +324,7 @@ End UnitCounitAdjunction. 2. 2-cat theory: postcomp (-)* is a 2-functor so preserves adjunctions. *) -Lemma adjunction_postcomp `{Funext} (C D J : Type) +Lemma adjunction_postcomp (C D J : Type) `{HasEquivs C, HasEquivs D, Is01Cat J} (F : Fun11 C D) (G : Fun11 D C) `{!HasMorExt C, !HasMorExt D, !HasMorExt (Fun01 J C), !HasMorExt (Fun01 J D)} : F ⊣ G -> fun11_fun01_postcomp (A:=J) F ⊣ fun11_fun01_postcomp (A:=J) G. diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v index 273d5554ed4..2e155b6aabf 100644 --- a/theories/WildCat/NatTrans.v +++ b/theories/WildCat/NatTrans.v @@ -272,7 +272,7 @@ Definition PointedTransformation {B C : Type} `{Is1Cat B, Is1Gpd C} Notation "F $=>* G" := (PointedTransformation F G) (at level 70). -Definition ptransformation_inverse `{Funext} {B C : Type} `{Is1Cat B, Is1Gpd C} +Definition ptransformation_inverse {B C : Type} `{Is1Cat B, Is1Gpd C} `{IsPointed B, IsPointed C} (F G : B -->* C) : (F $=>* G) -> (G $=>* F). Proof. From 7aad88d3e3a304c018a84431fca94826e958063e Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 28 Jan 2024 14:43:48 -0500 Subject: [PATCH 06/10] ReflectiveSubuniverse: remove Univalence and Funext from a Context line --- theories/Modalities/ReflectiveSubuniverse.v | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v index aa3fe46d7dc..501449ece62 100644 --- a/theories/Modalities/ReflectiveSubuniverse.v +++ b/theories/Modalities/ReflectiveSubuniverse.v @@ -1589,7 +1589,6 @@ Class IsConnMap (O : ReflectiveSubuniverse@{i}) Global Existing Instance isconnected_hfiber_conn_map. Section ConnectedMaps. - Context `{Univalence} `{Funext}. Universe i. Context (O : ReflectiveSubuniverse@{i}). @@ -1636,7 +1635,7 @@ Section ConnectedMaps. Defined. (** Being connected is an hprop *) - Global Instance ishprop_isconnmap {A B : Type} (f : A -> B) + Global Instance ishprop_isconnmap `{Funext} {A B : Type} (f : A -> B) : IsHProp (IsConnMap O f). Proof. apply istrunc_forall. @@ -1706,7 +1705,7 @@ Section ConnectedMaps. : ooExtendableAlong f P := fun n => extendable_conn_map_inO n f P. - Lemma allpath_extension_conn_map + Lemma allpath_extension_conn_map `{Funext} {A B : Type} (f : A -> B) `{IsConnMap O _ _ f} (P : B -> Type) `{forall b:B, In O (P b)} (d : forall a:A, P (f a)) @@ -1718,7 +1717,7 @@ Section ConnectedMaps. Defined. (** It follows that [conn_map_elim] is actually an equivalence. *) - Theorem isequiv_o_conn_map + Theorem isequiv_o_conn_map `{Funext} {A B : Type} (f : A -> B) `{IsConnMap O _ _ f} (P : B -> Type) `{forall b:B, In O (P b)} : IsEquiv (fun (g : forall b:B, P b) => g oD f). @@ -1734,14 +1733,14 @@ Section ConnectedMaps. apply path_forall; intros x; apply conn_map_comp. Defined. - Definition equiv_o_conn_map + Definition equiv_o_conn_map `{Funext} {A B : Type} (f : A -> B) `{IsConnMap O _ _ f} (P : B -> Type) `{forall b:B, In O (P b)} : (forall b, P b) <~> (forall a, P (f a)) := Build_Equiv _ _ _ (isequiv_o_conn_map f P). (** When considering lexness properties, we often want to consider the property of the universe of modal types being modal. We can't say this directly (except in the accessible, hence liftable, case) because it lives in a higher universe, but we can make a direct extendability statement. Here we prove a lemma that oo-extendability into the universe follows from plain extendability, essentially because the type of equivalences between two [O]-modal types is [O]-modal. *) - Definition ooextendable_TypeO_from_extension + Definition ooextendable_TypeO_from_extension `{Univalence} {A B : Type} (f : A -> B) `{IsConnMap O _ _ f} (extP : forall P : A -> Type_ O, ExtensionAlong f (fun _ : B => Type_ O) P) : ooExtendableAlong f (fun _ => Type_ O). From 6d32032716a23d297336b1d4933dbb833c776bbf Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 28 Jan 2024 15:24:10 -0500 Subject: [PATCH 07/10] Add .Core to many Require Import lines --- theories/Algebra/AbGroups/AbProjective.v | 2 +- theories/Algebra/AbGroups/AbPullback.v | 2 +- theories/Algebra/AbGroups/AbPushout.v | 2 +- theories/Algebra/AbGroups/Cyclic.v | 2 +- theories/Algebra/AbGroups/Z.v | 2 +- theories/Algebra/AbSES/BaerSum.v | 4 ++-- theories/Algebra/AbSES/DirectSum.v | 4 ++-- theories/Algebra/AbSES/Pullback.v | 2 +- theories/Algebra/AbSES/PullbackFiberSequence.v | 2 +- theories/Algebra/AbSES/Pushout.v | 2 +- theories/Algebra/Groups/FreeGroup.v | 2 +- theories/Algebra/Groups/GroupCoeq.v | 2 +- theories/Algebra/Groups/GrpPullback.v | 2 +- theories/Algebra/Groups/Image.v | 2 +- theories/Algebra/Groups/Kernel.v | 2 +- theories/Algebra/Groups/Lagrange.v | 2 +- theories/Algebra/Groups/ShortExactSequence.v | 2 +- theories/Algebra/Groups/Subgroup.v | 2 +- theories/Algebra/Rings/Z.v | 2 +- theories/Algebra/Universal/Operation.v | 2 +- theories/BoundedSearch.v | 2 +- theories/Categories/ChainCategory.v | 2 +- theories/Categories/Functor/Attributes.v | 2 +- .../Categories/Functor/Composition/Functorial/Attributes.v | 2 +- theories/Categories/FundamentalPreGroupoidCategory.v | 2 +- theories/Categories/HomotopyPreCategory.v | 2 +- theories/Categories/SimplicialSets.v | 2 +- theories/Classes/interfaces/abstract_algebra.v | 2 +- theories/Colimits/Quotient/Choice.v | 2 +- theories/Colimits/Sequential.v | 2 +- theories/HIT/V.v | 2 +- theories/Homotopy/EncodeDecode.v | 2 +- theories/Homotopy/EvaluationFibration.v | 2 +- theories/Homotopy/HSpace/Core.v | 2 +- theories/Homotopy/Hopf.v | 4 ++-- theories/Homotopy/SuccessorStructure.v | 4 ++-- theories/Homotopy/WhiteheadsPrinciple.v | 2 +- theories/Sets/GCH.v | 2 +- theories/Sets/GCHtoAC.v | 2 +- theories/Spaces/BAut/Cantor.v | 2 +- theories/Spaces/Finite/Fin.v | 2 +- theories/Spaces/Finite/FinInduction.v | 2 +- theories/Spaces/Finite/FinNat.v | 2 +- theories/Spaces/Finite/FinSeq.v | 2 +- theories/Spaces/Finite/Finite.v | 2 +- theories/Spaces/Int/Core.v | 2 +- theories/Spaces/Torus/TorusHomotopy.v | 2 +- 47 files changed, 51 insertions(+), 51 deletions(-) diff --git a/theories/Algebra/AbGroups/AbProjective.v b/theories/Algebra/AbGroups/AbProjective.v index 5ee2c848b45..fbcc0460c63 100644 --- a/theories/Algebra/AbGroups/AbProjective.v +++ b/theories/Algebra/AbGroups/AbProjective.v @@ -1,5 +1,5 @@ Require Import Basics Types AbelianGroup AbPullback - WildCat Limits.Pullback ReflectiveSubuniverse Truncations.Core. + WildCat.Core Limits.Pullback ReflectiveSubuniverse Truncations.Core. (** * Projective abelian groups *) diff --git a/theories/Algebra/AbGroups/AbPullback.v b/theories/Algebra/AbGroups/AbPullback.v index cf82766fa06..473e332485d 100644 --- a/theories/Algebra/AbGroups/AbPullback.v +++ b/theories/Algebra/AbGroups/AbPullback.v @@ -2,7 +2,7 @@ Require Import Basics. Require Import Limits.Pullback Cubical.PathSquare. Require Export Algebra.Groups.GrpPullback. Require Import Algebra.AbGroups.AbelianGroup. -Require Import WildCat. +Require Import WildCat.Core. (** * Pullbacks of abelian groups *) diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v index 5ca08bee130..5af7dd66b52 100644 --- a/theories/Algebra/AbGroups/AbPushout.v +++ b/theories/Algebra/AbGroups/AbPushout.v @@ -1,5 +1,5 @@ Require Import Basics Types Truncations.Core Modalities.ReflectiveSubuniverse. -Require Import WildCat HSet. +Require Import WildCat.Core HSet. Require Export Algebra.Groups.Image Algebra.Groups.QuotientGroup. Require Import AbGroups.AbelianGroup AbGroups.Biproduct. diff --git a/theories/Algebra/AbGroups/Cyclic.v b/theories/Algebra/AbGroups/Cyclic.v index f5b811143bb..c982b8c0378 100644 --- a/theories/Algebra/AbGroups/Cyclic.v +++ b/theories/Algebra/AbGroups/Cyclic.v @@ -1,4 +1,4 @@ -Require Import Basics Types WildCat Truncations.Core +Require Import Basics Types WildCat.Core Truncations.Core AbelianGroup AbHom Centralizer AbProjective Groups.FreeGroup. diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v index 520b2388621..2ac9c525870 100644 --- a/theories/Algebra/AbGroups/Z.v +++ b/theories/Algebra/AbGroups/Z.v @@ -1,5 +1,5 @@ Require Import Basics. -Require Import Spaces.Pos Spaces.Int. +Require Import Spaces.Pos.Core Spaces.Int. Require Import Algebra.AbGroups.AbelianGroup. (** * The group of integers *) diff --git a/theories/Algebra/AbSES/BaerSum.v b/theories/Algebra/AbSES/BaerSum.v index 4e7cfe2e5c7..6e77c489d91 100644 --- a/theories/Algebra/AbSES/BaerSum.v +++ b/theories/Algebra/AbSES/BaerSum.v @@ -1,8 +1,8 @@ Require Import Basics Types. -Require Import WildCat Pointed. +Require Import WildCat Pointed.Core. Require Import AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom. Require Import AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum. -Require Import Homotopy.HSpace. +Require Import Homotopy.HSpace.Core. Local Open Scope mc_scope. Local Open Scope mc_add_scope. diff --git a/theories/Algebra/AbSES/DirectSum.v b/theories/Algebra/AbSES/DirectSum.v index 51fb2b27c9e..efa5b56bbb2 100644 --- a/theories/Algebra/AbSES/DirectSum.v +++ b/theories/Algebra/AbSES/DirectSum.v @@ -1,6 +1,6 @@ Require Import Basics Types Truncations.Core. -Require Import Pointed. -Require Import WildCat Homotopy.ExactSequence. +Require Import Pointed.Core. +Require Import WildCat.Core Homotopy.ExactSequence. Require Import AbGroups.AbelianGroup AbSES.Core AbGroups.Biproduct. Local Open Scope pointed_scope. diff --git a/theories/Algebra/AbSES/Pullback.v b/theories/Algebra/AbSES/Pullback.v index 8d08fdc8950..56533ffd165 100644 --- a/theories/Algebra/AbSES/Pullback.v +++ b/theories/Algebra/AbSES/Pullback.v @@ -1,6 +1,6 @@ Require Import Basics Types. Require Import HSet Limits.Pullback. -Require Import WildCat Pointed Homotopy.ExactSequence. +Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Modalities.ReflectiveSubuniverse. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum. diff --git a/theories/Algebra/AbSES/PullbackFiberSequence.v b/theories/Algebra/AbSES/PullbackFiberSequence.v index 005f51b8846..b7cd4c2e97b 100644 --- a/theories/Algebra/AbSES/PullbackFiberSequence.v +++ b/theories/Algebra/AbSES/PullbackFiberSequence.v @@ -1,5 +1,5 @@ Require Import Basics Types HSet HFiber Limits.Pullback. -Require Import WildCat Pointed Homotopy.ExactSequence. +Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Groups.QuotientGroup. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.Pullback. diff --git a/theories/Algebra/AbSES/Pushout.v b/theories/Algebra/AbSES/Pushout.v index 93529d4b632..022f02b7979 100644 --- a/theories/Algebra/AbSES/Pushout.v +++ b/theories/Algebra/AbSES/Pushout.v @@ -1,5 +1,5 @@ Require Import Basics Types Truncations.Core. -Require Import WildCat Pointed Homotopy.ExactSequence HIT.epi. +Require Import WildCat Pointed.Core Homotopy.ExactSequence HIT.epi. Require Import Modalities.ReflectiveSubuniverse. Require Import AbelianGroup AbPushout AbHom AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum. diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index c7bf18fb94a..f17f518e525 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -1,5 +1,5 @@ Require Import Basics Types Group Subgroup - WildCat Colimits.Coeq + WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list. diff --git a/theories/Algebra/Groups/GroupCoeq.v b/theories/Algebra/Groups/GroupCoeq.v index f491597fa5c..92d1d1a8b80 100644 --- a/theories/Algebra/Groups/GroupCoeq.v +++ b/theories/Algebra/Groups/GroupCoeq.v @@ -1,5 +1,5 @@ Require Import Basics Types. -Require Import WildCat. +Require Import WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Colimits.Coeq. diff --git a/theories/Algebra/Groups/GrpPullback.v b/theories/Algebra/Groups/GrpPullback.v index 39a5d322144..c3c3dca73c3 100644 --- a/theories/Algebra/Groups/GrpPullback.v +++ b/theories/Algebra/Groups/GrpPullback.v @@ -1,6 +1,6 @@ Require Import Basics Types Limits.Pullback Cubical.PathSquare. Require Import Algebra.Groups.Group. -Require Import WildCat. +Require Import WildCat.Core. (** Pullbacks of groups are formalized by equipping the set-pullback with the desired group structure. The universal property in the category of groups is proved by saying that the corecursion principle (grp_pullback_corec) is an equivalence. *) diff --git a/theories/Algebra/Groups/Image.v b/theories/Algebra/Groups/Image.v index 20d5f0d2b8d..2b3f9e11187 100644 --- a/theories/Algebra/Groups/Image.v +++ b/theories/Algebra/Groups/Image.v @@ -2,7 +2,7 @@ Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. -Require Import WildCat. +Require Import WildCat.Core. Require Import HSet. (** Image of group homomorphisms *) diff --git a/theories/Algebra/Groups/Kernel.v b/theories/Algebra/Groups/Kernel.v index eeb628d4f27..e4e2d0b25b8 100644 --- a/theories/Algebra/Groups/Kernel.v +++ b/theories/Algebra/Groups/Kernel.v @@ -1,7 +1,7 @@ Require Import Basics Types. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. -Require Import WildCat. +Require Import WildCat.Core. (** * Kernels of group homomorphisms *) diff --git a/theories/Algebra/Groups/Lagrange.v b/theories/Algebra/Groups/Lagrange.v index ce0d0f9ef02..fe64f3b655d 100644 --- a/theories/Algebra/Groups/Lagrange.v +++ b/theories/Algebra/Groups/Lagrange.v @@ -3,7 +3,7 @@ Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import Algebra.Groups.QuotientGroup. Require Import Spaces.Finite.Finite. -Require Import Spaces.Nat. +Require Import Spaces.Nat.Core. (** ** Lagrange's theorem *) diff --git a/theories/Algebra/Groups/ShortExactSequence.v b/theories/Algebra/Groups/ShortExactSequence.v index 411305c96a6..a73d33c5511 100644 --- a/theories/Algebra/Groups/ShortExactSequence.v +++ b/theories/Algebra/Groups/ShortExactSequence.v @@ -1,6 +1,6 @@ Require Import Basics Types. Require Import Truncations.Core. -Require Import WildCat Pointed. +Require Import WildCat.Core Pointed. Require Import Groups.Group Groups.Subgroup Groups.Kernel. Require Import Homotopy.ExactSequence Modalities.Identity. diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 8ca7f7a2cad..a1efd7f3b1f 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -1,4 +1,4 @@ -Require Import Basics Types HFiber WildCat. +Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType. diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v index 3f03806d4a6..b2a63ec2130 100644 --- a/theories/Algebra/Rings/Z.v +++ b/theories/Algebra/Rings/Z.v @@ -2,7 +2,7 @@ Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Require Import Algebra.Rings.CRing. Require Import Spaces.Int Spaces.Pos. -Require Import WildCat. +Require Import WildCat.Core. (** In this file we define the ring Z of integers. The underlying abelian group is already defined in Algebra.AbGroups.Z. Many of the ring axioms are proven and made opaque. Typically, everything inside IsRing can be opaque since we will only ever rewrite along them and they are hprops. This also means we don't have to be too careful with how our proofs are structured. This allows us to freely use tactics such as rewrite. It would perhaps be possible to shorten many of the proofs here, but it would probably be unneeded due to the opacicty. *) diff --git a/theories/Algebra/Universal/Operation.v b/theories/Algebra/Universal/Operation.v index b28ffa3ad44..e3c27f4ad2f 100644 --- a/theories/Algebra/Universal/Operation.v +++ b/theories/Algebra/Universal/Operation.v @@ -8,7 +8,7 @@ Require Export HoTT.Algebra.Universal.Algebra. Require Import HoTT.Types HoTT.Spaces.Finite - HoTT.Spaces.Nat. + HoTT.Spaces.Nat.Core. Local Open Scope Algebra_scope. Local Open Scope nat_scope. diff --git a/theories/BoundedSearch.v b/theories/BoundedSearch.v index ce5f2e8aad7..234b13955c6 100644 --- a/theories/BoundedSearch.v +++ b/theories/BoundedSearch.v @@ -1,6 +1,6 @@ Require Import HoTT.Basics HoTT.Types. Require Import HoTT.Truncations.Core. -Require Import HoTT.Spaces.Nat. +Require Import HoTT.Spaces.Nat.Core. Section bounded_search. diff --git a/theories/Categories/ChainCategory.v b/theories/Categories/ChainCategory.v index 5e82a61957f..d62cb3cae5e 100644 --- a/theories/Categories/ChainCategory.v +++ b/theories/Categories/ChainCategory.v @@ -2,7 +2,7 @@ Require Import Category.Subcategory.Full. Require Import Category.Sigma.Univalent. Require Import Category.Morphisms Category.Univalent Category.Strict. -Require Import HoTT.Basics HoTT.Types HoTT.Spaces.Nat. +Require Import HoTT.Basics HoTT.Types HoTT.Spaces.Nat.Core. Set Universe Polymorphism. Set Implicit Arguments. diff --git a/theories/Categories/Functor/Attributes.v b/theories/Categories/Functor/Attributes.v index 8f3aea5df58..963d301e7d5 100644 --- a/theories/Categories/Functor/Attributes.v +++ b/theories/Categories/Functor/Attributes.v @@ -1,6 +1,6 @@ (** * Attributes of functors (full, faithful, split essentially surjective) *) Require Import Category.Core Functor.Core HomFunctor Category.Morphisms Category.Dual Functor.Dual Category.Prod Functor.Prod NaturalTransformation.Core SetCategory.Core Functor.Composition.Core. -Require Import Basics.Trunc Types.Universe HIT.iso HoTT.Truncations. +Require Import Basics.Trunc Types.Universe HIT.iso HoTT.Truncations.Core. Set Universe Polymorphism. Set Implicit Arguments. diff --git a/theories/Categories/Functor/Composition/Functorial/Attributes.v b/theories/Categories/Functor/Composition/Functorial/Attributes.v index 55a80922032..b1945a59e62 100644 --- a/theories/Categories/Functor/Composition/Functorial/Attributes.v +++ b/theories/Categories/Functor/Composition/Functorial/Attributes.v @@ -7,7 +7,7 @@ Require Import Functor.Attributes. Require Import FunctorCategory.Core. Require Import Category.Morphisms. Require Import NaturalTransformation.Paths. -Require Import HoTT.Truncations. +Require Import HoTT.Truncations.Core. Set Universe Polymorphism. Set Implicit Arguments. diff --git a/theories/Categories/FundamentalPreGroupoidCategory.v b/theories/Categories/FundamentalPreGroupoidCategory.v index 378dc8b3f3e..7ff479bc09f 100644 --- a/theories/Categories/FundamentalPreGroupoidCategory.v +++ b/theories/Categories/FundamentalPreGroupoidCategory.v @@ -1,6 +1,6 @@ (** * Fundamental Pregroupoids *) Require Import Category.Core. -Require Import HoTT.Truncations. +Require Import HoTT.Truncations.Core. Require Import HoTT.Basics. Set Universe Polymorphism. diff --git a/theories/Categories/HomotopyPreCategory.v b/theories/Categories/HomotopyPreCategory.v index b0438b6c416..b08ecc5a33d 100644 --- a/theories/Categories/HomotopyPreCategory.v +++ b/theories/Categories/HomotopyPreCategory.v @@ -1,6 +1,6 @@ (** * Homotopy PreCategory of Types *) Require Import Category.Core. -Require Import HoTT.Basics HoTT.Truncations. +Require Import HoTT.Basics HoTT.Truncations.Core. Set Universe Polymorphism. Set Implicit Arguments. diff --git a/theories/Categories/SimplicialSets.v b/theories/Categories/SimplicialSets.v index 85d78b6cd44..2ddf17959b1 100644 --- a/theories/Categories/SimplicialSets.v +++ b/theories/Categories/SimplicialSets.v @@ -1,5 +1,5 @@ (** * The simplex category Δ, and the precategory of simplicial sets, [Δᵒᵖ → set] *) -Require Import Basics Types Spaces.Nat. +Require Import Basics Types Spaces.Nat.Core. Require Import Category.Core Functor.Core Functor.Paths. Require Import SetCategory.Core. Require Import ChainCategory FunctorCategory.Core. diff --git a/theories/Classes/interfaces/abstract_algebra.v b/theories/Classes/interfaces/abstract_algebra.v index 329bc80826b..99a9b4d564d 100644 --- a/theories/Classes/interfaces/abstract_algebra.v +++ b/theories/Classes/interfaces/abstract_algebra.v @@ -1,4 +1,4 @@ -Require Import Spaces.Nat. +Require Import Spaces.Nat.Core. Require Export HoTT.Classes.interfaces.canonical_names. Require Import Modalities.ReflectiveSubuniverse. diff --git a/theories/Colimits/Quotient/Choice.v b/theories/Colimits/Quotient/Choice.v index b18b5a6d0d8..11ea1fc9085 100644 --- a/theories/Colimits/Quotient/Choice.v +++ b/theories/Colimits/Quotient/Choice.v @@ -2,7 +2,7 @@ Require Import HoTT.Basics HoTT.Types HoTT.HSet - HoTT.Truncations + HoTT.Truncations.Core HoTT.Colimits.Quotient HoTT.Projective. diff --git a/theories/Colimits/Sequential.v b/theories/Colimits/Sequential.v index f652fafd696..a42de66a1ab 100644 --- a/theories/Colimits/Sequential.v +++ b/theories/Colimits/Sequential.v @@ -6,7 +6,7 @@ Require Import Diagrams.Diagram. Require Import Diagrams.Sequence. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. -Require Import Spaces.Nat. +Require Import Spaces.Nat.Core. Require Import PathAny. Local Open Scope nat_scope. diff --git a/theories/HIT/V.v b/theories/HIT/V.v index 7825706e6a6..52a30dbc0cd 100644 --- a/theories/HIT/V.v +++ b/theories/HIT/V.v @@ -5,7 +5,7 @@ Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. -Require Import HoTT.Truncations Colimits.Quotient. +Require Import HoTT.Truncations.Core Colimits.Quotient. Local Open Scope nat_scope. Local Open Scope path_scope. diff --git a/theories/Homotopy/EncodeDecode.v b/theories/Homotopy/EncodeDecode.v index 199497b40ec..bdf6611dc01 100644 --- a/theories/Homotopy/EncodeDecode.v +++ b/theories/Homotopy/EncodeDecode.v @@ -1,5 +1,5 @@ Require Import Basics Pointed. -Require Import Truncations. +Require Import Truncations.Core. (** ** Encode-decode method of characterizing identity types *) diff --git a/theories/Homotopy/EvaluationFibration.v b/theories/Homotopy/EvaluationFibration.v index 20a6d865ace..738f35c0bea 100644 --- a/theories/Homotopy/EvaluationFibration.v +++ b/theories/Homotopy/EvaluationFibration.v @@ -1,4 +1,4 @@ -From HoTT Require Import Basics Types Truncations.Core Pointed Homotopy.Cover. +From HoTT Require Import Basics Types Truncations.Core Pointed.Core Homotopy.Cover. Local Open Scope pointed_scope. Local Open Scope trunc_scope. diff --git a/theories/Homotopy/HSpace/Core.v b/theories/Homotopy/HSpace/Core.v index 7925473a2f2..1932ac8da00 100644 --- a/theories/Homotopy/HSpace/Core.v +++ b/theories/Homotopy/HSpace/Core.v @@ -3,7 +3,7 @@ Require Export Classes.interfaces.canonical_names (SgOp, sg_op, Negate, negate, Associative, simple_associativity, associativity, LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity). Export canonical_names.BinOpNotations. -Require Import Basics Types Pointed WildCat. +Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness. Local Open Scope pointed_scope. diff --git a/theories/Homotopy/Hopf.v b/theories/Homotopy/Hopf.v index d1ec95cae38..cfdd09a38c0 100644 --- a/theories/Homotopy/Hopf.v +++ b/theories/Homotopy/Hopf.v @@ -1,7 +1,7 @@ Require Import Types Basics Pointed Truncations. Require Import HSpace Suspension ExactSequence HomotopyGroup. -Require Import WildCat Modalities.ReflectiveSubuniverse Modalities.Descent. -Require Import HSet Spaces.Nat. +Require Import WildCat.Core Modalities.ReflectiveSubuniverse Modalities.Descent. +Require Import HSet Spaces.Nat.Core. Local Open Scope pointed_scope. Local Open Scope trunc_scope. diff --git a/theories/Homotopy/SuccessorStructure.v b/theories/Homotopy/SuccessorStructure.v index f2b381f85f6..49b8752b866 100644 --- a/theories/Homotopy/SuccessorStructure.v +++ b/theories/Homotopy/SuccessorStructure.v @@ -1,8 +1,8 @@ Require Import Basics. Require Import Nat.Core. -Require Import Spaces.Int. +Require Import Spaces.Int.Core. Require Import Spaces.Finite.Fin. -Require Import WildCat. +Require Import WildCat.Core. Local Set Universe Minimization ToSet. diff --git a/theories/Homotopy/WhiteheadsPrinciple.v b/theories/Homotopy/WhiteheadsPrinciple.v index 69efe0c8e84..4adc43b41e1 100644 --- a/theories/Homotopy/WhiteheadsPrinciple.v +++ b/theories/Homotopy/WhiteheadsPrinciple.v @@ -1,6 +1,6 @@ Require Import Basics Types. Require Import Pointed. -Require Import WildCat HFiber. +Require Import WildCat.Core HFiber. Require Import Truncations. Require Import Algebra.Groups. Require Import Homotopy.HomotopyGroup. diff --git a/theories/Sets/GCH.v b/theories/Sets/GCH.v index 4dc68b29a61..1af20b57937 100644 --- a/theories/Sets/GCH.v +++ b/theories/Sets/GCH.v @@ -1,6 +1,6 @@ From HoTT Require Import TruncType abstract_algebra. From HoTT Require Import PropResizing.PropResizing. -From HoTT Require Import Spaces.Nat Spaces.Card. +From HoTT Require Import Spaces.Nat.Core Spaces.Card. Open Scope type. diff --git a/theories/Sets/GCHtoAC.v b/theories/Sets/GCHtoAC.v index 06fddf89259..14ffd208cdd 100644 --- a/theories/Sets/GCHtoAC.v +++ b/theories/Sets/GCHtoAC.v @@ -1,6 +1,6 @@ From HoTT Require Import TruncType ExcludedMiddle abstract_algebra. From HoTT Require Import PropResizing.PropResizing. -From HoTT Require Import Spaces.Nat Spaces.Card. +From HoTT Require Import Spaces.Nat.Core Spaces.Card. From HoTT Require Import Equiv.BiInv. From HoTT Require Import HIT.unique_choice. diff --git a/theories/Spaces/BAut/Cantor.v b/theories/Spaces/BAut/Cantor.v index 40f0ea5031a..47e26b80e93 100644 --- a/theories/Spaces/BAut/Cantor.v +++ b/theories/Spaces/BAut/Cantor.v @@ -1,7 +1,7 @@ (* -*- mode: coq; mode: visual-line -*- *) Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. -Require Import HoTT.Truncations Spaces.BAut Spaces.Cantor. +Require Import HoTT.Truncations.Core Spaces.BAut Spaces.Cantor. Local Open Scope equiv_scope. Local Open Scope path_scope. diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v index b81e7e0236a..8db2f914a3c 100644 --- a/theories/Spaces/Finite/Fin.v +++ b/theories/Spaces/Finite/Fin.v @@ -2,7 +2,7 @@ Require Import Basics. Require Import Types. Require Import HSet. -Require Import Spaces.Nat. +Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit. (** By setting this, using [simple_induction] instead of [induction], and specifying universe variables in a couple of places, we can avoid all universe variables in this file. Several results are confirmed to use no universe variables with an @{} annotation. *) diff --git a/theories/Spaces/Finite/FinInduction.v b/theories/Spaces/Finite/FinInduction.v index f7844606a19..ab3fefe470a 100644 --- a/theories/Spaces/Finite/FinInduction.v +++ b/theories/Spaces/Finite/FinInduction.v @@ -2,7 +2,7 @@ Require Import HoTT.Basics HoTT.Types HoTT.HSet - HoTT.Spaces.Nat + HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.FinNat HoTT.Spaces.Finite.Fin. diff --git a/theories/Spaces/Finite/FinNat.v b/theories/Spaces/Finite/FinNat.v index a36abb06fe5..6314ae40233 100644 --- a/theories/Spaces/Finite/FinNat.v +++ b/theories/Spaces/Finite/FinNat.v @@ -2,7 +2,7 @@ Require Import HoTT.Basics HoTT.Types HoTT.HSet - HoTT.Spaces.Nat + HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin. Local Open Scope nat_scope. diff --git a/theories/Spaces/Finite/FinSeq.v b/theories/Spaces/Finite/FinSeq.v index 5001a0ccaad..330061197d3 100644 --- a/theories/Spaces/Finite/FinSeq.v +++ b/theories/Spaces/Finite/FinSeq.v @@ -4,7 +4,7 @@ Require Import HoTT.HSet HoTT.Spaces.Finite.Fin HoTT.Spaces.Finite.FinInduction - HoTT.Spaces.Nat. + HoTT.Spaces.Nat.Core. Local Open Scope nat_scope. diff --git a/theories/Spaces/Finite/Finite.v b/theories/Spaces/Finite/Finite.v index 3f11f4bb174..387e9e7432c 100644 --- a/theories/Spaces/Finite/Finite.v +++ b/theories/Spaces/Finite/Finite.v @@ -2,7 +2,7 @@ Require Import Basics. Require Import Types. Require Import HSet. -Require Import Spaces.Nat. +Require Import Spaces.Nat.Core. Require Import HFiber. Require Import Factorization. Require Import Truncations. diff --git a/theories/Spaces/Int/Core.v b/theories/Spaces/Int/Core.v index 4b90aba6d6a..17805667520 100644 --- a/theories/Spaces/Int/Core.v +++ b/theories/Spaces/Int/Core.v @@ -1,5 +1,5 @@ Require Import Basics. -Require Import Spaces.Pos. +Require Import Spaces.Pos.Core. Local Set Universe Minimization ToSet. diff --git a/theories/Spaces/Torus/TorusHomotopy.v b/theories/Spaces/Torus/TorusHomotopy.v index ef20a811351..839212d9981 100644 --- a/theories/Spaces/Torus/TorusHomotopy.v +++ b/theories/Spaces/Torus/TorusHomotopy.v @@ -4,7 +4,7 @@ Require Import Modalities.ReflectiveSubuniverse Truncations.Core. Require Import Algebra.AbGroups. Require Import Homotopy.HomotopyGroup. Require Import Homotopy.PinSn. -Require Import Spaces.Int Spaces.Circle. +Require Import Spaces.Int.Core Spaces.Circle. Require Import Spaces.Torus.Torus. Require Import Spaces.Torus.TorusEquivCircles. From c30a8ac3413e73038ac5b9bb2ddcc883986e3695 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 28 Jan 2024 15:25:22 -0500 Subject: [PATCH 08/10] WhiteheadsPrinciple: import Groups.Group instead of Groups --- theories/Homotopy/WhiteheadsPrinciple.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Homotopy/WhiteheadsPrinciple.v b/theories/Homotopy/WhiteheadsPrinciple.v index 4adc43b41e1..986098bb052 100644 --- a/theories/Homotopy/WhiteheadsPrinciple.v +++ b/theories/Homotopy/WhiteheadsPrinciple.v @@ -2,7 +2,7 @@ Require Import Basics Types. Require Import Pointed. Require Import WildCat.Core HFiber. Require Import Truncations. -Require Import Algebra.Groups. +Require Import Algebra.Groups.Group. Require Import Homotopy.HomotopyGroup. Local Open Scope pointed_scope. From a92ccd2b9cb0c59fa301c3b220efcc17b0f49735 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 28 Jan 2024 16:04:38 -0500 Subject: [PATCH 09/10] etc/coqcreplace.py: a script for trying search & replace on files --- etc/coqcreplace.py | 228 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 228 insertions(+) create mode 100755 etc/coqcreplace.py diff --git a/etc/coqcreplace.py b/etc/coqcreplace.py new file mode 100755 index 00000000000..e2a81d20ac3 --- /dev/null +++ b/etc/coqcreplace.py @@ -0,0 +1,228 @@ +#!/usr/bin/python3 + +# A wrapper for coqc that will try to replace a regular expression +# with a replacement string. The results need to be inspected by +# hand, as it will often be too eager. See the "Limitations" section +# below. + +# The patterns are specified using environment variables, using python's +# regular expression syntax, e.g.: +# export COQC_SEARCH='(^|[^n])(refine|rapply)' +# export COQC_REPLACE='\1n\2' +# This will replace an occurence of 'refine' or 'rapply' that is either +# at the start of the line or preceeded by a character other than 'n' +# with the same thing with an 'n' inserted. '\1' and '\2' refer to +# the parts of the input line that matched the expressions in parentheses. +# - COQC_SEARCH is matched against each *line* of the file separately, +# not including newlines. +# - Matches are replaced one at a time, from left to right, and each one +# is tested and kept only if the file builds successfully and meets the +# timing constraint. +# - After a replacement, the line is scanned for the next match that +# starts *after* that replacement string. +# - After a failed replacement, the string is scanned for the next match +# that starts one character to the right of the last match, allowing +# for overlapping matches. +# - Lines containing 'noreplace' are left as is. This can be put in as +# a temporary marker inside a comment. +# Other examples: +# export COQC_SEARCH='\W*`{Univalence}' +# export COQC_REPLACE='' +# +# export COQC_SEARCH='(Truncations|Spaces\.Nat|Spaces\.Pos|Spaces\.Int|Spaces\.No|Pointed|Homotopy.Join|Homotopy.HSpace|WildCat|Algebra.AbSES)' +# export COQC_REPLACE='\1.Core' +# Search for "min(20" below for how to restrict this to the start of each file. + +# Can be used as +# path/to/coqcreplace.py path/tofile.v +# but in order to get the right arguments passed to coqc, it is better to do +# make COQC=path/to/coqcreplace.py path/tofile.vo +# or +# export COQC=path/to/coqcreplace.py +# make file.vo +# To run on the whole library, avoiding test/ and contrib/, can do: +# export COQC=path/to/coqcreplace.py +# make clean; make -j theories/HoTT.vo theories/Categories.vo +# Use "unset COQC" when done. + +# You'll need to also adjust the timing policy. See below. + +# Can be run with -j<#cores> or -j1. Timing is more accurate with -j1. + +# Note that the make process sometimes calls coqc to, e.g., find out the +# Coq version, so we transparently call coqc for such commands. + +# Also, stdout is usually redirected to a timing file, so we send all of +# our additional output to stderr. + +# Below, file_excludes is set to a list of files to not process. Not sure +# if this is needed. + +# Limitations: +# - Doesn't know about comments. +# - Shouldn't be run on test/ folder, as many definitions there are preceded +# with "Fail". +# - It's possible that a change (e.g. to a tactic) doesn't cause a file to fail, +# but causes a *later* file to fail. Currently the only work-around is to +# add the first file to the file_excludes list below, or to mark the +# problematic line with "noreplace". + +import subprocess +import sys +import os +import time +import re + +# You can choose a fixed timeout or a dynamic timeout. +# For this script, you probably always want a dynamic timeout. +# A change is only accepted if the new time is <= the time given +# by the formula, where duration is the best time seen so far. + +# Set your timeout policy, in seconds: + +# This policy only accepts changes that make at least a small +# improvement to the timing. This is appropriate for changes that are +# intended to improve build speed. But note that there are random +# fluctuations, so this will also accept changes that are neutral. +# The second part, duration*0.9, is there just to ensure that the +# return value is always positive. + +#def calc_timeout(duration): return max(duration-0.03, duration*0.9) + +# If changes have other benefits, e.g. reducing dependencies, and are +# very unlikely to increase the build time, then you might want to +# accept them even if the time increases slightly, to account for +# timing noise. + +def calc_timeout(duration): return max(duration+0.1, duration*1.05) + +# time.perf_counter is better than time.time, since the latter is +# affected by changes to the system clock. Both return a floating point +# value in seconds. +timer = time.perf_counter + +# The default timeout value here will be used for the first run. +# Returns (exit code of coqc, elapsed time). If the elapsed time +# is greater than the timeout, returns (1111, elapsed time). +def coqc(quiet=False, timeout=60): + start = timer() + try: + if quiet: + cp = subprocess.run(['coqc'] + sys.argv[1:], timeout=timeout, + stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL) + else: + cp = subprocess.run(['coqc'] + sys.argv[1:], timeout=timeout) + except subprocess.TimeoutExpired: + return 1111, timer() - start + # subprocess.run uses a busy loop to check the timeout, so it may allow + # the command to run longer than the limit. So we also check here. + elapsed = timer() - start + if elapsed > timeout: + return 1111, elapsed + else: + return cp.returncode, elapsed + +# Files to not process, e.g. summary files, files defining tactics used elsewhere, etc. +file_excludes=[ + ] + +# Given a match object match, a replacement string (which can include \1, etc), +# and the string s that was searched, return string with the replacement done. +def replace_match(match, replace, s): + return s[:match.start()] + match.expand(replace) + s[match.end():] + +def replace(vfile): + changes = 0 + attempts = 0 + timeouts = 0 + + # Ensure that the file builds with no changes: + ret, duration1 = coqc(False) + # Exit immediately if it fails, or if the file is excluded from further treatment. + if ret != 0 or vfile in file_excludes: + return ret, changes, attempts, timeouts + + # Do a second run to get a more stable duration value: + ret2, duration2 = coqc(False) + duration = (duration1 + duration2)/2.0 + + with open(vfile, 'r', encoding="utf-8") as f: + lines = f.readlines() + os.rename(vfile, vfile+'.bak') + + # Replace len(lines) with min(20, len(lines)) to only look for matches in first 20 lines: + for i in range(len(lines)): + # Save last successful line; we'll modify lines[i]: + line = lines[i] + + # Don't make changes to lines with this tag: + if 'noreplace' in line: continue + + end = len(line) + # Exclude carriage return and newline from search: + while end > 0 and line[end-1] in '\n\r': end -= 1 + start = 0 + + while True: + # Note: When start > 0, '^' will never match; but '$' does match endpos + match = coqc_search.search(lines[i], pos=start, endpos=end) + if not match: + break + lines[i] = replace_match(match, coqc_replace, lines[i]) + + attempts += 1 + with open(vfile, 'w', encoding="utf-8") as f: + f.write(''.join(lines)) + ret, newduration = coqc(True, timeout=calc_timeout(duration)) + + if ret == 0: + start = match.end() + changes += 1 + duration = newduration + else: + lines[i] = line + start = match.start() + 1 + if ret == 1111: + timeouts += 1 + + if changes == 0: + # Get rid of the backup file if we made no changes: + os.rename(vfile+'.bak', vfile) + if attempts > 0: + # Ensure we are in a consistent state: + ret, _ = coqc(True) + else: + # We only need to do an extra run if the last one failed: + if ret != 0: + with open(vfile, 'w', encoding="utf-8") as f: + f.write(''.join(lines)) + ret, _ = coqc() + + return ret, changes, attempts, timeouts + +if __name__ == '__main__': + vfiles = [arg for arg in sys.argv if arg.endswith('.v')] + + if len(vfiles) == 0: + # We are called for some other reason. Just call coqc and exit. + sys.exit(coqc()[0]) + elif len(vfiles) > 1: + print('!!! Called with more than one vfile???', file=sys.stderr) + sys.exit(coqc()[0]) + + # These will give errors if the environment variables are not set: + coqc_search = re.compile(os.environ['COQC_SEARCH']) + coqc_replace = os.environ['COQC_REPLACE'] + + vfile = vfiles[0] + + ret, changes, attempts, timeouts = replace(vfile) + + if changes > 0: + print('>>> %2d changes made to %s' % (changes, vfile), file=sys.stderr) + if attempts > 0: + print('--- %2d attempts made to %s' % (attempts, vfile), file=sys.stderr) + if timeouts > 0: + print('ttt %2d timeouts for %s' % (timeouts, vfile), file=sys.stderr) + + sys.exit(ret) From 22f5981b30fd1eed413e6872713a0dedd6f85426 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 28 Jan 2024 16:05:13 -0500 Subject: [PATCH 10/10] etc/coqcstriprequires.py: minor updates --- etc/coqcstriprequires.py | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/etc/coqcstriprequires.py b/etc/coqcstriprequires.py index da9ed9d1784..7fe2a04a79d 100755 --- a/etc/coqcstriprequires.py +++ b/etc/coqcstriprequires.py @@ -13,7 +13,8 @@ # make file.vo # To run on the whole library, avoiding test/ and contrib/, can do: # export COQC=path/to/coqcstriprequires.py -# make clean; make -j theories/HoTT.vo +# make clean; make -j theories/HoTT.vo theories/Categories.vo +# Use "unset COQC" when done. # Can be run with -j8 or -j1. You should adjust the timeout policy # depending on which case you use. See below. @@ -84,6 +85,8 @@ def calc_timeout(duration): return max(duration+0.005, duration*1.03) timer = time.perf_counter # The default timeout value here will be used for the first run. +# Returns (exit code of coqc, elapsed time). If the elapsed time +# is greater than the timeout, returns (1111, elapsed time). def coqc(quiet=False, timeout=60): start = timer() try: @@ -94,7 +97,13 @@ def coqc(quiet=False, timeout=60): cp = subprocess.run(['coqc'] + sys.argv[1:], timeout=timeout) except subprocess.TimeoutExpired: return 1111, timer() - start - return cp.returncode, timer() - start + # subprocess.run uses a busy loop to check the timeout, so it may allow + # the command to run longer than the limit. So we also check here. + elapsed = timer() - start + if elapsed > timeout: + return 1111, elapsed + else: + return cp.returncode, elapsed # Join words with spaces, ignoring None. def myjoin(words):