Minor fixes to Truncations/Core, Ideal, Bool, Empty

theories/Algebra/Rings/Ideal.v

@@ -396,7 +396,7 @@ Arguments ligt_add_neg {R X r s}.
 Arguments ligt_mul {R X r s}.
 
 (** Left ideal generated by a subset. *)
-Definition leftideal_generated {R : Ring} (X : R -> Type) : LeftIdeal R.
+Definition leftideal_generated@{u v} {R : Ring@{u}} (X : R -> Type@{v}) : LeftIdeal@{u v} R.
 Proof.
   snrapply Build_LeftIdeal.
   - snrapply Build_Subgroup'.
@@ -410,7 +410,7 @@ Proof.
 Defined.
 
 (** Right ideal generated by a subset. *)
-Definition rightideal_generated {R : Ring} (X : R -> Type) : RightIdeal R
+Definition rightideal_generated@{u v} {R : Ring@{u}} (X : R -> Type@{v}) : RightIdeal@{u v} R
   := Build_RightIdeal R (leftideal_generated (R:=rng_op R) X) _.
 
 (** Underlying type family of a two-sided ideal generated by subset. *)
@@ -456,7 +456,7 @@ Proof.
     nrapply igt_mul_r.
 Defined. 
 
-(** *** Finitely gnerated ideal. *)
+(** *** Finitely generated ideal *)
 
 (** Finitely generated ideals *)
 Definition ideal_generated_finite {R : Ring} {n : nat} (X : Fin n -> R) : Ideal R.

theories/Truncations/Core.v

@@ -1,9 +1,9 @@
 Require Import Basics Types WildCat.Core WildCat.Universe HFiber.
 Require Import Modalities.Modality.
-(* Users of this file almost always want to be able to write [Tr n] for both a [Modality] and a [ReflectiveSubuniverse], so they want the coercion [modality_to_reflective_subuniverse]: *)
+(** Users of this file almost always want to be able to write [Tr n] for both a [Modality] and a [ReflectiveSubuniverse], so they want the coercion [modality_to_reflective_subuniverse]: *)
 Require Export (coercions) Modalities.Modality.
 
-(** * Truncations of types, in all dimensions *)
+(** * Truncations of types *)
 
 Local Open Scope path_scope.
 Generalizable Variables A X n.
@@ -12,7 +12,7 @@ Generalizable Variables A X n.
 
 (** The definition of [Trunc n], the n-truncation of a type.
 
-If Coq supported higher inductive types natively, we would construct this as somthing like:
+If Coq supported higher inductive types natively, we would construct this as something like:
 
    Inductive Trunc n (A : Type) : Type :=
    | tr : A -> Trunc n A
@@ -23,30 +23,28 @@ However, while we are faking our higher-inductives anyway, we can take some shor
 *)
 
 Module Export Trunc.
-Delimit Scope trunc_scope with trunc.
 
-Cumulative Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
-  tr : A -> Trunc n A.
-Bind Scope trunc_scope with Trunc.
-Arguments tr {n A} a.
+  Cumulative Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+    tr : A -> Trunc n A.
+  Arguments tr {n A} a.
 
-(** Without explicit universe parameters, this instance is insufficiently polymorphic. *)
-Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
-: IsTrunc@{j} n (Trunc@{i} n A).
-Admitted.
+  (** Without explicit universe parameters, this instance is insufficiently polymorphic. *)
+  Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
+    : IsTrunc@{j} n (Trunc@{i} n A).
+  Admitted.
 
-Definition Trunc_ind {n A}
-  (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
-  : (forall a, P (tr a)) -> (forall aa, P aa)
-:= (fun f aa => match aa with tr a => fun _ => f a end Pt).
+  Definition Trunc_ind {n A}
+    (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
+    : (forall a, P (tr a)) -> (forall aa, P aa)
+    := fun f aa => match aa with tr a => fun _ => f a end Pt.
 
 End Trunc.
 
 (** The non-dependent version of the eliminator. *)
 
 Definition Trunc_rec {n A X} `{IsTrunc n X}
   : (A -> X) -> (Trunc n A -> X)
-:= Trunc_ind (fun _ => X).
+  := Trunc_ind (fun _ => X).
 
 Definition Trunc_rec_tr n {A : Type}
   : Trunc_rec (A:=A) (tr (n:=n)) == idmap
@@ -93,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.
 
@@ -117,10 +115,6 @@ Section TruncationModality.
     : @Trunc_functor X X idmap == idmap
     := O_functor_idmap (Tr n) X.
 
-  Definition isequiv_Trunc_functor {X Y} (f : X -> Y) `{IsEquiv _ _ f}
-    : IsEquiv (Trunc_functor f)
-    := isequiv_O_functor (Tr n) f.
-
   Definition equiv_Trunc_prod_cmp {X Y}
     : Tr n (X * Y) <~> Tr n X * Tr n Y
     := equiv_O_prod_cmp (Tr n) X Y.
@@ -329,9 +323,8 @@ Proof.
     reflexivity.
 Defined.
 
-(** ** Tactic to remove truncations in hypotheses if possible
+(** ** Tactic to remove truncations in hypotheses if possible *)
 
-  See [strip_reflections] and [strip_modalities] for generalizations to other reflective subuniverses and modalities. *)
 Ltac strip_truncations :=
   (** search for truncated hypotheses *)
   progress repeat
@@ -343,8 +336,8 @@ Ltac strip_truncations :=
         [];
         intro T
   end.
-(** We would like to define this in terms of the [strip_modalities] tactic, however [O_ind] uses more universes than [Trunc_ind] which causes some problems down the line. *)
-(* Ltac strip_truncations := strip_modalities. *)
+
+(** See [strip_reflections] and [strip_modalities] for generalizations to other reflective subuniverses and modalities.  We provide this version because it sometimes needs fewer universes (due to the cumulativity of [Trunc]).  However, that same cumulativity sometimes causes free universe variables.  For a hypothesis of type [Trunc@{i} X], we can use [Trunc_ind@{i j}], but sometimes Coq uses [Trunc_ind@{k j}] with [i <= k] and [k] otherwise free.  In these cases, [strip_reflections] and/or [strip_modalities] may generate fewer universe variables. *)
 
 (** ** Iterated truncations *)
 

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

theories/Types/Empty.v

@@ -39,17 +39,17 @@ 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.
 
 Global Instance isequiv_all_to_empty (T : Type) (f : T -> Empty) : IsEquiv f.
 Proof.
   refine (Build_IsEquiv _ _ _ 
-    (Empty_ind (fun _ => T))                (* := equiv_inf *)
-    (fun fals:Empty => match fals with end) (* : f o equiv_inf == idmap *)
-    (fun t:T => match (f t) with end)       (* : equiv_inf o f == idmap *)
+    (Empty_ind (fun _ => T))                (* := equiv_inv *)
+    (fun fals:Empty => match fals with end) (* : f o equiv_inv == idmap *)
+    (fun t:T => match (f t) with end)       (* : equiv_inv o f == idmap *)
     (_)                                     (* adjointify part *)  ).
   intro t. 
   exact (Empty_rec (f t)).
@@ -60,7 +60,4 @@ Definition equiv_to_empty {T : Type} (f : T -> Empty) : T <~> Empty
 
 (** ** Paths *)
 
-(** We could probably prove some theorems about non-existing paths in
-   [Empty], but this is really quite useless. As soon as an element
-   of [Empty] is hypothesized, we can prove whatever we like with
-   a simple elimination. *)
+(** We could probably prove some theorems about non-existing paths in [Empty], but this is really quite useless. As soon as an element of [Empty] is hypothesized, we can prove whatever we like with a simple elimination. *)