Merge pull request #2038 from Alizter/fix-scope-binding-for-type

Fix binding of type_scope to Sortclass

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

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.

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))
               _

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)

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)

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

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.

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.

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.

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).

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] ]

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