diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v index 827ca182ab..725bea0625 100644 --- a/theories/Algebra/Rings/Ideal.v +++ b/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. diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v index de019b590a..1527dbfb92 100644 --- a/theories/Truncations/Core.v +++ b/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,22 +23,20 @@ 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. @@ -46,7 +44,7 @@ End Trunc. 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 *) diff --git a/theories/Types/Bool.v b/theories/Types/Bool.v index b27e833f21..f24cd297a8 100644 --- 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 index dcbd8d37fc..ef66e13922 100644 --- 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. @@ -47,9 +47,9 @@ 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. *)