Ditch the modules; closes #1209

_CoqProject

@@ -137,6 +137,8 @@ theories/Spaces/Torus/TorusHomotopy.v
 theories/Modalities/ReflectiveSubuniverse.v
 theories/Modalities/Modality.v
 theories/Modalities/Accessible.v
+theories/Modalities/Descent.v
+theories/Modalities/Separated.v
 theories/Modalities/Lex.v
 theories/Modalities/Topological.v
 theories/Modalities/Notnot.v

contrib/HoTTBook.v

@@ -454,7 +454,7 @@ Definition Book_3_6_2 `{Funext} (A : Type) (B : A -> Type)
 (* ================================================== thm:prop-equiv-trunc *)
 (** Lemma 3.9.1 *)
 
-Definition Book_3_9_1 := @HoTT.Truncations.Core.TrM.RSU.isequiv_to_O_inO (-1)%trunc.
+Definition Book_3_9_1 := @HoTT.Modalities.ReflectiveSubuniverse.isequiv_to_O_inO (Tr (-1)).
 
 (* ================================================== cor:UC *)
 (** Corollary 3.9.2 *)
@@ -490,7 +490,7 @@ Definition Book_3_11_6 := @HoTT.Types.Forall.trunc_forall.
 (** Lemma 3.11.7 *)
 
 Definition Book_3_11_7a := @HoTT.Idempotents.contr_retracttype.
-Definition Book_3_11_7 := @HoTT.Truncations.Core.TrM.RSU.inO_to_O_retract (-2)%trunc.
+Definition Book_3_11_7 := @HoTT.Modalities.ReflectiveSubuniverse.inO_to_O_retract (Tr (-2)).
 
 (* ================================================== thm:contr-paths *)
 (** Lemma 3.11.8 *)
@@ -639,7 +639,7 @@ Definition Book_4_6_1 := @HoTT.Basics.Trunc.IsTruncMap (-1).
 (* ================================================== thm:mono-surj-equiv *)
 (** Theorem 4.6.3 *)
 
-Definition Book_4_6_3 := @HoTT.Truncations.Core.TrM.RSU.isequiv_conn_ino_map.
+Definition Book_4_6_3 := @HoTT.Modalities.ReflectiveSubuniverse.isequiv_conn_ino_map.
 
 (* ================================================== thm:two-out-of-three *)
 (** Theorem 4.7.1 *)
@@ -862,7 +862,7 @@ Definition Book_6_9_1 := @HoTT.Truncations.Core.Trunc.Trunc_ind 0.
 (* ================================================== thm:trunc0-lump *)
 (** Lemma 6.9.2 *)
 
-Definition Book_6_9_2 := @HoTT.Truncations.Core.TrM.isequiv_o_to_O.
+Definition Book_6_9_2 := @HoTT.Modalities.ReflectiveSubuniverse.isequiv_o_to_O.
 
 (* ================================================== thm:set-pushout *)
 (** Lemma 6.9.3 *)
@@ -1107,7 +1107,7 @@ Definition Book_7_3_12 := @HoTT.Truncations.Core.equiv_path_Tr.
 (* ================================================== cor:totrunc-is-connected *)
 (** Corollary 7.5.8 *)
 
-Definition Book_7_5_8 := @HoTT.Truncations.Core.TrM.conn_map_to_O.
+Definition Book_7_5_8 := @HoTT.Modalities.Modality.conn_map_to_O.
 
 (* ================================================== thm:nconn-to-ntype-const *)
 (** Corollary 7.5.9 *)

contrib/HoTTBookExercises.v

@@ -1563,7 +1563,7 @@ End Book_7_1.
 (* ================================================== ex:double-negation-modality *)
 (** Exercise 7.12 *)
 
-Definition Book_7_12 := HoTT.Modalities.Notnot.Notnot.
+Definition Book_7_12 := @HoTT.Modalities.Notnot.NotNot.
 
 (* ================================================== ex:prop-modalities *)
 (** Exercise 7.13 *)

theories/Algebra/AbelianGroup.v

@@ -4,7 +4,6 @@ Require Import HIT.Coeq.
 Require Import Algebra.Group.
 Require Import Algebra.Subgroup.
 Require Import Cubical.
-Import TrM.
 
 Local Open Scope mc_mult_scope.
 

theories/Algebra/Aut.v

@@ -4,7 +4,6 @@ Require Import Types.
 Require Import Truncations.
 Require Import Factorization.
 Require Import Algebra.ooGroup.
-Import TrM.
 
 Local Open Scope path_scope.
 
@@ -23,13 +22,13 @@ Definition equiv_baut_image_unit X
 Proof.
   unfold BAut, image; simpl.
   apply equiv_functor_sigma_id; intros Z; simpl.
-  apply equiv_O_functor; unfold hfiber.
+  apply Trunc_functor_equiv; unfold hfiber.
   refine ((equiv_contr_sigma _)^-1 oE _).
   apply equiv_path_inverse.
 Defined.
 
 (** Now we can define [Aut X], by proving that [BAut X] is connected. *)
-Definition Aut (X : Type@{i}) : ooGroup@{j u a}.
+Definition Aut (X : Type) : ooGroup.
 Proof.
   refine (Build_ooGroup
             (Build_pType { Z : Type & merely (Z = X) } (X ; tr 1)) _).

theories/Algebra/ooGroup.v

@@ -5,8 +5,6 @@ Require Import Pointed.
 Require Import Truncations.
 Require Import Colimits.Quotient.
 
-Import TrM.
-
 Local Open Scope path_scope.
 
 (** Keyed unification makes [rewrite !loops_functor_group] take a really long time.  See https://coq.inria.fr/bugs/show_bug.cgi?id=4544 for more discussion. *)
@@ -19,8 +17,8 @@ Local Unset Keyed Unification.
 (** ** Definition *)
 
 Record ooGroup :=
-  { classifying_space : pType@{i} ;
-    isconn_classifying_space : IsConnected@{u a i} 0 classifying_space
+  { classifying_space : pType ;
+    isconn_classifying_space : IsConnected 0 classifying_space
   }.
 
 Global Existing Instance isconn_classifying_space.

theories/Classes/interfaces/canonical_names.v

@@ -398,7 +398,7 @@ Class Bind (M : Type -> Type) := bind : forall {A B}, M A -> (A -> M B) -> M B.
 Class Enumerable@{i} (A : Type@{i}) :=
   { enumerator : nat -> A
   ; enumerator_issurj :>
-    TrM.RSU.IsConnMap@{Uhuge Ularge i i Ularge} (trunc_S minus_two) enumerator }.
+    IsConnMap@{i} (trunc_S minus_two) enumerator }.
 Arguments enumerator A {_} _.
 Arguments enumerator_issurj A {_} _.
 

theories/Classes/theory/rationals.v

@@ -556,7 +556,7 @@ destruct (le_or_lt (enumerator Q n) 0) as [E|E].
 Defined.
 
 Lemma Qpos_is_enumerator :
-  TrM.RSU.IsConnMap@{Uhuge Ularge UQ UQ Ularge} (trunc_S minus_two) Qpos_enumerator.
+  IsConnMap@{UQ} (trunc_S minus_two) Qpos_enumerator.
 Proof.
 apply BuildIsSurjection.
 unfold hfiber.

theories/Comodalities/CoreflectiveSubuniverse.v

@@ -2,7 +2,6 @@
 Require Import HoTT.Basics HoTT.Types.
 Require Import UnivalenceImpliesFunext.
 Require Import Modalities.Modality Modalities.Open.
-Import OpM.
 
 Local Open Scope path_scope.
 

theories/Constant.v

@@ -3,7 +3,6 @@ Require Import HoTT.Basics HoTT.Types.
 Require Import HProp FunextVarieties.
 Require Import Extensions Factorization Modalities.Modality.
 Require Import HoTT.Truncations.
-Import TrM.
 
 Local Open Scope path_scope.
 Local Open Scope trunc_scope.

theories/DProp.v

@@ -5,7 +5,6 @@
 Require Import HoTT.Basics HoTT.Types.
 Require Import TruncType HProp UnivalenceImpliesFunext.
 Require Import HoTT.Truncations.
-Import TrM.
 
 Local Open Scope path_scope.
 

theories/Extensions.v

@@ -18,33 +18,29 @@ Section Extensions.
   (* TODO: consider naming for [ExtensionAlong] and subsequent lemmas.  As a name for the type itself, [Extension] or [ExtensionAlong] seems great; but resultant lemma names such as [path_extension] (following existing naming conventions) are rather misleading. *)
 
   (** This elimination rule (and others) can be seen as saying that, given a fibration over the codomain and a section of it over the domain, there is some *extension* of this to a section over the whole codomain.  It can also be considered as an equivalent form of an [hfiber] of precomposition-with-[f] that replaces paths by pointwise paths, thereby avoiding [Funext]. *)
-
-  Definition ExtensionAlong {A B : Type} (f : A -> B)
-             (P : B -> Type) (d : forall x:A, P (f x))
-    := { s : forall y:B, P y & forall x:A, s (f x) = d x }.
-  (** [ExtensionAlong] takes 5 universe parameters:
+  Definition ExtensionAlong@{a b p m} {A : Type@{a}} {B : Type@{b}} (f : A -> B)
+             (P : B -> Type@{p}) (d : forall x:A, P (f x))
+    := (* { s : forall y:B, P y & forall x:A, s (f x) = d x }. *)
+       sig@{m m} (fun (s : forall y:B, P y) => forall x:A, s (f x) = d x).
+   (** [ExtensionAlong] takes 4 universe parameters:
       - the size of A
       - the size of B
       - the size of P
-      - >= max(B,P)
-      - >= max(A,P).
-    The following [Check] verifies that this is in fact the case. *)
-  (** We would like to say [Check], but because of bug #4517, https://coq.inria.fr/bugs/show_bug.cgi?id=4517, we can't. *)
-  Definition check_ExtensionAlong@{a b p m n} : True@{Set}.
-  Proof.
-    Check ExtensionAlong@{a b p m n}.
-  Abort.
-  (** If necessary, we could coalesce the latter two with a universe annotation, but that would make the definition harder to read. *)
+      - >= max(A,B,P)
+   *)
 
-  (** It's occasionally useful to be able to modify those max universes. *)
-  Definition lift_extensionalong@{a b p m1 n1 m2 n2} {A : Type@{a}} {B : Type@{b}} (f : A -> B)
-             (P : B -> Type@{p}) (d : forall x:A, P (f x))
-  : ExtensionAlong@{a b p m1 n1} f P d -> ExtensionAlong@{a b p m2 n2} f P d
-    := fun ext => (ext.1 ; ext.2).
+  (** It's occasionally useful to be able to modify those universes.  For each of the universes [a], [b], [p], we give an initial one, a final one, and a "minimum" one smaller than both and where the type actually lives. *)
+  Definition lift_extensionalong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} {A : Type@{amin}} {B : Type@{bmin}} (f : A -> B)
+             (P : B -> Type@{pmin}) (d : forall x:A, P (f x))
+    : ExtensionAlong@{a1 b1 p1 m1} f P d -> ExtensionAlong@{a2 b2 p2 m2} f P d.
+  Proof.
+    intros ext.
+    (** If we just give [ext], it will collapse the universes.  (Anyone stepping through this proof should do [Set Printing Universes] and look at the universes to see that they're different in [ext] and in the goal.)  So we decompose [ext] into two components and give them separately. *)
+    assert (e2 := ext.2); set (e1 := ext.1) in e2.
+    cbn in e2. (** Curiously, without this line we get a spurious universe inequality [p1 <= m2]. *)
+    exact (e1;e2).
+  Defined.
   (** We called it [lift_extensionalong], but in fact it doesn't require the new universes to be bigger than the old ones, only that they both satisfy the max condition. *)
-  Definition lower_extensionalong@{a b p e0 e1} {A : Type@{a}} {B : Type@{b}} (f : A -> B)
-             (P : B -> Type@{p}) (d : forall x:A, P (f x))
-    := lift_extensionalong@{a b p e0 e1 e0 e1} f P d.
 
   Definition equiv_path_extension `{Funext} {A B : Type} {f : A -> B}
              {P : B -> Type} {d : forall x:A, P (f x)}
@@ -97,7 +93,7 @@ Section Extensions.
     := match n with
          | 0 => Unit
          | S n => (forall (g : forall a, C (f a)),
-                     ExtensionAlong@{i j k l l} f C g) *
+                     ExtensionAlong@{i j k l} f C g) *
                   forall (h k : forall b, C b),
                     ExtendableAlong n f (fun b => h b = k b)
        end.
@@ -106,36 +102,24 @@ Section Extensions.
       - size of B
       - size of C
       - size of result (>= A,B,C) *)
-  (** We would like to say [Check], but because of bug #4517, https://coq.inria.fr/bugs/show_bug.cgi?id=4517, we can't. *)
-  Definition check_ExtendableAlong@{a b c r} : True@{Set}.
-  Proof.
-    Check ExtendableAlong@{a b c r}.
-  Abort.
 
   Global Arguments ExtendableAlong n%nat_scope {A B}%type_scope (f C)%function_scope.
 
   (** We can modify the universes, as with [ExtensionAlong]. *)
-  Definition lift_extendablealong@{i j k l1 l2}
-             (n : nat) {A : Type@{i}} {B : Type@{j}}
-             (f : A -> B) (C : B -> Type@{k})
-  : ExtendableAlong@{i j k l1} n f C -> ExtendableAlong@{i j k l2} n f C.
+  Definition lift_extendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2}
+             (n : nat) {A : Type@{amin}} {B : Type@{bmin}}
+             (f : A -> B) (P : B -> Type@{pmin})
+  : ExtendableAlong@{a1 b1 p1 m1} n f P -> ExtendableAlong@{a2 b2 p2 m2} n f P.
   Proof.
-    revert C; simple_induction n n IH; intros C.
+    revert P; simple_induction n n IH; intros P.
     - intros _; exact tt.
     - intros ext; split.
-      + intros g; exact (lift_extensionalong _ _ _ (fst ext g)).
-      + intros h k; exact (IH _ (snd ext h k)).
+      + intros g; exact (lift_extensionalong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} _ _ _ (fst ext g)).
+      + intros h k. 
+        (** Unles we give the universe explicitly here, [kmin] gets collapsed to [k1]. *)
+        pose (P' := (fun b => h b = k b) : B -> Type@{pmin}).
+        exact (IH P' (snd ext h k)).
   Defined.
-  (** We would like to say [Check], but because of bug #4517, https://coq.inria.fr/bugs/show_bug.cgi?id=4517, we can't. *)
-  Definition check_lift_extendablealong@{i j k l1 l2} : True@{Set}.
-  Proof.
-    Check lift_extendablealong@{i j k l1 l2}.
-  Abort.
-
-  Definition lower_extendablealong@{i j k e}
-             (n : nat) {A : Type@{i}} {B : Type@{j}}
-             (f : A -> B) (C : B -> Type@{k})
-    := lift_extendablealong@{i j k e e} n f C.
 
   Definition equiv_extendable_pathsplit `{Funext} (n : nat)
              {A B : Type} (C : B -> Type) (f : A -> B)
@@ -340,29 +324,15 @@ Section Extensions.
              (f : A -> B) (C : B -> Type@{k}) : Type@{l}
     := forall n : nat, ExtendableAlong@{i j k l} n f C.
   (** Universe parameters are the same as for [ExtendableAlong]. *)
-  (** We would like to say [Check], but because of bug #4517, https://coq.inria.fr/bugs/show_bug.cgi?id=4517, we can't. *)
-  Definition check_ooExtendableAlong@{a b c r} : True@{Set}.
-  Proof.
-    Check ooExtendableAlong@{a b c r}.
-  Abort.
 
   Global Arguments ooExtendableAlong {A B}%type_scope (f C)%function_scope.
 
   (** Universe modification. *)
-  Definition lift_ooextendablealong@{i j k l1 l2}
-             {A : Type@{i}} {B : Type@{j}}
-             (f : A -> B) (C : B -> Type@{k})
-  : ooExtendableAlong@{i j k l1} f C -> ooExtendableAlong@{i j k l2} f C
-    := fun ext n => lift_extendablealong n f C (ext n).
-  (** We would like to say [Check], but because of bug #4517, https://coq.inria.fr/bugs/show_bug.cgi?id=4517, we can't. *)
-  Definition check_ooextendablealong@{i j k l1 l2} : True@{Set}.
-  Proof.
-    Check lift_ooextendablealong@{i j k l1 l2}.
-  Abort.
-  Definition lower_ooextendablealong@{i j k e1 e2}
-             {A : Type@{i}} {B : Type@{j}}
-             (f : A -> B) (C : B -> Type@{k})
-    := lift_ooextendablealong@{i j k e1 e2} f C.
+  Definition lift_ooextendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2}
+             {A : Type@{amin}} {B : Type@{bmin}}
+             (f : A -> B) (P : B -> Type@{pmin})
+  : ooExtendableAlong@{a1 b1 p1 m1} f P -> ooExtendableAlong@{a2 b2 p2 m2} f P
+    := fun ext n => lift_extendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} n f P (ext n).
 
   (** We take part of the data from [ps 1] and part from [ps 2] so that the inverse chosen is the expected one. *)
   Definition isequiv_ooextendable `{Funext}

theories/Fibrations.v

@@ -307,6 +307,10 @@ Proof.
   intros x y. apply isequiv_fcontr,_.
 Defined.
 
+Definition equiv_ap_isembedding {A B} (f : A -> B) `{!IsEmbedding f} (x y : A)
+  : (x = y) <~> (f x = f y)
+  := Build_Equiv _ _ (ap f) _.
+
 Definition isembedding_isequiv_ap {A B} (f : A -> B) `{!forall x y, IsEquiv (@ap _ _ f x y)}
   : IsEmbedding f.
 Proof.

theories/HIT/Circle.v

@@ -10,7 +10,6 @@ Require Import HIT.Coeq.
 Require Import Modalities.Modality Truncations.
 Require Import Cubical.DPath.
 
-Import TrM.
 Local Open Scope path_scope.
 
 Generalizable Variables X A B f g n.
@@ -201,6 +200,7 @@ Proof.
   refine (trunc_equiv' (n := 0) Int equiv_loopS1_int^-1).
 Defined.
 
+
 (** ** Iteration of equivalences *)
 
 (** If [P : S1 -> Type] is defined by a type [X] and an autoequivalence [f], then the image of [n:Int] regarded as in [base = base] is [iter_int f n]. *)

theories/HIT/FreeIntQuotient.v

@@ -3,7 +3,6 @@ Require Import HoTT.Basics HoTT.Types UnivalenceImpliesFunext.
 Require Import TruncType HProp HSet.
 Require Import Spaces.Int.
 Require Import HIT.Coeq HIT.Circle HIT.Flattening Truncations.
-Import TrM.
 
 Local Open Scope path_scope.
 

theories/HIT/Spheres.v

@@ -8,7 +8,6 @@ Require Import HProp NullHomotopy.
 Require Import Homotopy.Suspension HIT.Circle HIT.TwoSphere.
 Require Import Pointed.pSusp Pointed.Core.
 Require Import Truncations.
-Import TrM.
 
 Local Open Scope pointed_scope.
 Local Open Scope trunc_scope.

theories/HIT/surjective_factor.v

@@ -21,7 +21,7 @@ Section surjective_factor.
   Qed.
 
   Definition surjective_factor_aux :=
-    @TrM.RSU.conn_map_elim
+    @conn_map_elim
       _ _ _ _ Esurj (fun b => exists c : C, forall a, g a = b -> f a = c)
       ishprop_surjective_factor_aux
       (fun a => exist (fun c => forall a, _ -> _ = c) (f a) (fun a' => Eg a' a)).

theories/HoTT.v

@@ -79,12 +79,14 @@ Require Export HoTT.Colimits.Colimit_Sigma.
 Require Export HoTT.Modalities.ReflectiveSubuniverse.
 Require Export HoTT.Modalities.Modality.
 Require Export HoTT.Modalities.Accessible.
-Require Export HoTT.Modalities.Lex.
-Require Export HoTT.Modalities.Topological.
 Require Export HoTT.Modalities.Notnot.
 Require Export HoTT.Modalities.Identity.
 Require Export HoTT.Modalities.Localization.
 Require Export HoTT.Modalities.Nullification.
+Require Export HoTT.Modalities.Descent.
+Require Export HoTT.Modalities.Separated.
+Require Export HoTT.Modalities.Lex.
+Require Export HoTT.Modalities.Topological.
 Require Export HoTT.Modalities.Open.
 Require Export HoTT.Modalities.Closed.
 Require Export HoTT.Modalities.Fracture.