From c98c6d387c3359516411b216786400ff26d521b8 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 29 Jul 2024 14:53:38 +0200 Subject: [PATCH 1/2] Fix binding of type_scope to Sortclass We fix the order in which we bind type_scope to Sortclass allowing targets of function types to automatically be interpreted as types. This allows us to remove %type annotations throughout the library. Signed-off-by: Ali Caglayan --- contrib/HoTTBookExercises.v | 2 +- theories/Basics/Notations.v | 6 ++++-- theories/Spaces/BAut/Cantor.v | 2 +- theories/Spaces/Nat/Arithmetic.v | 4 ++-- theories/Spaces/No/Addition.v | 2 +- theories/Tactics.v | 4 ++-- 6 files changed, 11 insertions(+), 9 deletions(-) diff --git a/contrib/HoTTBookExercises.v b/contrib/HoTTBookExercises.v index a80996429c5..9595407da5c 100644 --- a/contrib/HoTTBookExercises.v +++ b/contrib/HoTTBookExercises.v @@ -1169,7 +1169,7 @@ End Book_4_5. Section Book_4_6_i. Definition is_qinv {A B : Type} (f : A -> B) - := { g : B -> A & ((f o g == idmap) * (g o f == idmap))%type }. + := { g : B -> A & (f o g == idmap) * (g o f == idmap) }. Definition qinv (A B : Type) := { f : A -> B & is_qinv f }. Definition qinv_id A : qinv A A diff --git a/theories/Basics/Notations.v b/theories/Basics/Notations.v index 3aa4ff17b2c..5acb4fcf3ec 100644 --- a/theories/Basics/Notations.v +++ b/theories/Basics/Notations.v @@ -1,3 +1,7 @@ +(** [type_scope] must be declared and bound early on so that later reserved notations register correctly. *) +Declare Scope type_scope. +Bind Scope type_scope with Sortclass. + (** To reserve this notation, we must first bootstrap, and preserve the underlying [forall] notation *) Notation "'forall' x .. y , P" := (forall x , .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity). Reserved Notation "'exists' x .. y , p" @@ -265,7 +269,6 @@ Reserved Infix ":::" (at level 60, right associativity). (** We define various scopes and open them in the order we expect to use them. *) Declare Scope core_scope. Declare Scope function_scope. -Declare Scope type_scope. Declare Scope equiv_scope. Declare Scope path_scope. Declare Scope fibration_scope. @@ -290,4 +293,3 @@ Global Open Scope type_scope. Global Open Scope core_scope. Bind Scope function_scope with Funclass. -Bind Scope type_scope with Sortclass. diff --git a/theories/Spaces/BAut/Cantor.v b/theories/Spaces/BAut/Cantor.v index 47e26b80e93..c624110fc27 100644 --- a/theories/Spaces/BAut/Cantor.v +++ b/theories/Spaces/BAut/Cantor.v @@ -20,7 +20,7 @@ Section Assumptions. Proof. intros Z. (** Here is the important part of this definition. *) - exists (Z + Cantor)%type. + exists (Z + Cantor). (** The rest is just a proof that [Z+Cantor] is again equivalent to [Cantor], using [cantor_fold] and the assumption that [Z] is equivalent to [Cantor]. *) pose (e := Z.2); simpl in e; clearbody e. strip_truncations. diff --git a/theories/Spaces/Nat/Arithmetic.v b/theories/Spaces/Nat/Arithmetic.v index 2bb6df21370..76a9f0bf4f5 100644 --- a/theories/Spaces/Nat/Arithmetic.v +++ b/theories/Spaces/Nat/Arithmetic.v @@ -93,7 +93,7 @@ Proof. Defined. Proposition diseq_implies_lt (n m : nat) - : n <> m -> sum (n < m) (n > m). + : n <> m -> (n < m) + (n > m). Proof. intros diseq. destruct (dec (n < m)) as [| a]; [ now left |]. @@ -271,7 +271,7 @@ Proof. Defined. Definition nleqSm_dichot {n m : nat} - : (n <= m.+1) -> sum (n <= m) (n = m.+1). + : (n <= m.+1) -> (n <= m) + (n = m.+1). Proof. revert m; simple_induction n n IHn. - intro. left. exact (leq_0_n m). diff --git a/theories/Spaces/No/Addition.v b/theories/Spaces/No/Addition.v index a20fe702477..94187db35a8 100644 --- a/theories/Spaces/No/Addition.v +++ b/theories/Spaces/No/Addition.v @@ -298,7 +298,7 @@ Section Addition. refine (path_No_easy _ _ _ _ eL eR _ _ _ _); intros; repeat match goal with - | [ H : (?A + ?B)%type |- _ ] => destruct H + | [ H : (?A + ?B) |- _ ] => destruct H end; repeat match goal with | [ |- context[@equiv_fun ?A ?B ?e ?v] ] diff --git a/theories/Tactics.v b/theories/Tactics.v index a0714555fe5..0518bd4438c 100644 --- a/theories/Tactics.v +++ b/theories/Tactics.v @@ -49,7 +49,7 @@ Lemma path_forall_recr_beta' `{Funext} A B x0 P f g e Px g (@path_forall _ _ _ _ _ e) Px - = @transport ((forall a, B a) * B x0)%type + = @transport ((forall a, B a) * B x0) (fun x => P (fst x) (snd x)) (f, f x0) (g, g x0) @@ -140,7 +140,7 @@ Ltac transport_path_forall_hammer := (** An example showing that it works *) Lemma path_forall_2_beta' `{Funext} A B x0 x1 P f g e Px : @transport (forall a : A, B a) (fun f => P (f x0) (f x1)) f g (@path_forall _ _ _ _ _ e) Px - = @transport (B x0 * B x1)%type (fun x => P (fst x) (snd x)) (f x0, f x1) (g x0, g x1) (path_prod' (e x0) (e x1)) Px. + = @transport (B x0 * B x1) (fun x => P (fst x) (snd x)) (f x0, f x1) (g x0, g x1) (path_prod' (e x0) (e x1)) Px. Proof. transport_path_forall_hammer. repeat match goal with From 42647dca5b1d0412d77b8c5c1c476090be7c0594 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Wed, 31 Jul 2024 17:49:06 -0400 Subject: [PATCH 2/2] Categories: remove some %type annotations --- theories/Categories/Category/Prod.v | 6 +++--- theories/Categories/Category/Sigma/Univalent.v | 8 ++++---- theories/Categories/Category/Sum.v | 2 +- theories/Categories/ExponentialLaws/Tactics.v | 4 ++-- theories/Categories/Functor/Sum.v | 2 +- theories/Categories/NatCategory.v | 2 +- 6 files changed, 12 insertions(+), 12 deletions(-) diff --git a/theories/Categories/Category/Prod.v b/theories/Categories/Category/Prod.v index cc26ff69f9f..b1a31b81051 100644 --- a/theories/Categories/Category/Prod.v +++ b/theories/Categories/Category/Prod.v @@ -17,9 +17,9 @@ Section prod. Definition prod : PreCategory. refine (@Build_PreCategory - (C * D)%type - (fun s d => (morphism C (fst s) (fst d) - * morphism D (snd s) (snd d))%type) + (C * D) + (fun s d => morphism C (fst s) (fst d) + * morphism D (snd s) (snd d)) (fun x => (identity (fst x), identity (snd x))) (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) _ diff --git a/theories/Categories/Category/Sigma/Univalent.v b/theories/Categories/Category/Sigma/Univalent.v index bed82289eb2..eb86e42e55c 100644 --- a/theories/Categories/Category/Sigma/Univalent.v +++ b/theories/Categories/Category/Sigma/Univalent.v @@ -50,7 +50,7 @@ Section onmorphisms. Variable A : PreCategory. Variable Pmor : forall s d, morphism A s d -> Type. - Local Notation mor s d := { m : _ | Pmor s d m }%type. + Local Notation mor s d := { m : _ | Pmor s d m }. Context `(HPmor : forall s d, IsHSet (mor s d)). Variable Pidentity : forall x, @Pmor x x (@identity A _). @@ -148,11 +148,11 @@ Section on_both. Variable A : PreCategory. Variable Pobj : A -> Type. - Local Notation obj := { x : _ | Pobj x }%type (only parsing). + Local Notation obj := { x : _ | Pobj x } (only parsing). Variable Pmor : forall s d : obj, morphism A s.1 d.1 -> Type. - Local Notation mor s d := { m : _ | Pmor s d m }%type (only parsing). + Local Notation mor s d := { m : _ | Pmor s d m } (only parsing). Context `(HPmor : forall s d, IsHSet (mor s d)). Variable Pidentity : forall x, @Pmor x x (@identity A _). @@ -283,7 +283,7 @@ Section on_both. Local Definition equiv_iso_A'_eisretr_helper {s d} (x : {e : @Isomorphic A s.1 d.1 - | Pmor_iso_T s d e e^-1 (@left_inverse _ _ _ e e) right_inverse }%type) + | Pmor_iso_T s d e e^-1 (@left_inverse _ _ _ e e) right_inverse }) : transport (fun e : @Isomorphic A s.1 d.1 => Pmor_iso_T s d e e^-1 left_inverse right_inverse) diff --git a/theories/Categories/Category/Sum.v b/theories/Categories/Category/Sum.v index 6608f7f4a63..89cab02edf5 100644 --- a/theories/Categories/Category/Sum.v +++ b/theories/Categories/Category/Sum.v @@ -43,7 +43,7 @@ End internals. Definition sum (C D : PreCategory) : PreCategory. Proof. refine (@Build_PreCategory - (C + D)%type + (C + D) (sum_morphism C D) (sum_identity C D) (sum_compose C D) diff --git a/theories/Categories/ExponentialLaws/Tactics.v b/theories/Categories/ExponentialLaws/Tactics.v index d280489b41c..e78835c799b 100644 --- a/theories/Categories/ExponentialLaws/Tactics.v +++ b/theories/Categories/ExponentialLaws/Tactics.v @@ -21,10 +21,10 @@ Ltac exp_laws_misc_t' := Ltac exp_laws_simplify_types' := idtac; match goal with - | [ H : (_ + _)%type |- _ ] => destruct H + | [ H : (_ + _) |- _ ] => destruct H | [ H : Unit |- _ ] => destruct H | [ H : Empty |- _ ] => destruct H - | [ H : (_ * _)%type |- _ ] => destruct H + | [ H : (_ * _) |- _ ] => destruct H | [ |- _ = _ :> Functor _ _ ] => progress path_functor | [ |- _ = _ :> NaturalTransformation _ _ ] => progress path_natural_transformation | [ |- _ = _ :> prod _ _ ] => apply path_prod diff --git a/theories/Categories/Functor/Sum.v b/theories/Categories/Functor/Sum.v index fc951597a8d..ab041edf94e 100644 --- a/theories/Categories/Functor/Sum.v +++ b/theories/Categories/Functor/Sum.v @@ -89,7 +89,7 @@ Section swap_functor. transport_path_forall_hammer. by repeat match goal with | [ H : Empty |- _ ] => destruct H - | [ H : (_ + _)%type |- _ ] => destruct H + | [ H : (_ + _) |- _ ] => destruct H | _ => progress hnf in * end. Qed. diff --git a/theories/Categories/NatCategory.v b/theories/Categories/NatCategory.v index 686f091a0f7..0a2e08aa550 100644 --- a/theories/Categories/NatCategory.v +++ b/theories/Categories/NatCategory.v @@ -18,7 +18,7 @@ Module Export Core. match n with | 0 => Empty | 1 => Unit - | S n' => (CardinalityRepresentative n' + Unit)%type + | S n' => CardinalityRepresentative n' + Unit end. Coercion CardinalityRepresentative : nat >-> Sortclass.