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"
@@ -112,7 +116,7 @@
 Reserved Notation "x .2" (at level 1, format "x '.2'").
 
 (** Paths *)
 Reserved Notation "p ^" (at level 1, format "p '^'").
 Reserved Notation "p @ q" (at level 20).
 Reserved Notation "p # x" (right associativity, at level 65).
 Reserved Notation "p # x" (right associativity, at level 65).
@@ -225,8 +229,8 @@
 Reserved Notation "!! P" (at level 35, right associativity).
 Reserved Notation "u ~~ v" (at level 30).
 Reserved Notation "! x" (at level 3, format "'!' x").
 Reserved Notation "x \\ F" (at level 40, left associativity).
 Reserved Notation "x // F" (at level 40, left associativity).
 Reserved Notation "{ { xL | xR // xcut } }" (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Reserved Notation "x \ F" (at level 40, left associativity).
 Reserved Notation "x <> y" (at level 70, no associativity).
@@ -265,7 +269,6 @@
 (** 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 core_scope.
 
 Bind Scope function_scope with Funclass.
-Bind Scope type_scope with 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