Simplify/annotate a few things

HoTT · Nov 7, 2024 · ead1620 · ead1620
1 parent ce97ca8
commit ead1620
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 6 deletions.
diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
@@ -91,7 +91,7 @@ Section TruncationModality.
   (** ** Functoriality *)
 
   (** Since a modality lives on a single universe, by default if we simply define [Trunc_functor] to be [O_functor] then it would force [X] and [Y] to live in the same universe.  But since we defined [Trunc] as a cumulative inductive, if we add universe annotations we can make [Trunc_functor] more universe-polymorphic than [O_functor] is.  This is sometimes useful.  *)
-  Definition Trunc_functor@{i j k} {X : Type@{i}} {Y : Type@{j}} (f : X -> Y)
+  Definition Trunc_functor@{i j k | i <= k, j <= k} {X : Type@{i}} {Y : Type@{j}} (f : X -> Y)
     : Tr@{i} n X -> Tr@{j} n Y
     := O_functor@{k k k} (Tr n) f.
 

diff --git a/theories/Types/Bool.v b/theories/Types/Bool.v
@@ -67,10 +67,7 @@ Section BoolDecidable.
                     | false, true => inr false_ne_true
                   end.
 
-  Corollary hset_bool : IsHSet Bool.
-  Proof.
-    exact _.
-  Defined.
+  Definition hset_bool : IsHSet Bool := _.
 End BoolDecidable.
 
 (** In particular, [negb] has no fixed points *)

diff --git a/theories/Types/Empty.v b/theories/Types/Empty.v
@@ -39,7 +39,7 @@ Definition equiv_empty_rec@{u} `{Funext} (A : Type@{u})
 
 Global Instance istrunc_Empty@{} (n : trunc_index) : IsTrunc n.+1 Empty.
 Proof.
-  refine (@istrunc_leq (-1)%trunc n.+1 tt _ _).
+  refine (@istrunc_leq (-1) n.+1 tt _ _).
   apply istrunc_S.
   intros [].
 Defined.