Categories: remove some %type annotations

HoTT · Jul 31, 2024 · 42647dc · 42647dc
1 parent 1c4250d
commit 42647dc
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 12 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.