Merge pull request #1918 from jdchristensen/requires

Reduce Required files

contrib/HoTTBook.v

@@ -58,7 +58,7 @@
 *)
 
 From HoTT Require Import Basics Truncations.
-From HoTT Require Idempotents Spaces.Spheres Spaces.No Spaces.Nat.
+From HoTT Require Idempotents Spaces.No Spaces.Nat.
 From HoTT Require HIT.V HIT.Flattening Homotopy.WhiteheadsPrinciple Homotopy.Hopf.
 From HoTT Require Categories.
 From HoTT Require Metatheory.IntervalImpliesFunext Metatheory.UnivalenceImpliesFunext.

contrib/SetoidRewrite.v

@@ -11,11 +11,11 @@ All files that import WildCat/SetoidRewrite.v will also recursively import the e
 (** Because of this, this file needs to be the *first* file Require'd in any file that uses it.  Otherwise, the typeclasses hintdb is cleared, breaking typeclass inference.  Moreover, if Foo Requires this file, then Foo must also be the first file Require'd in any file that Requires Foo, and so on. In the long term it would be good if this could be avoided.*)
 
 From Coq Require Init.Tactics.
-From HoTT Require Import Basics.Overture Basics.Tactics.
+From HoTT Require Import Basics.Overture.
 From HoTT Require Import Types.Forall.
 From Coq Require Setoids.Setoid.
 Import CMorphisms.ProperNotations.
-From HoTT Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod
+From HoTT Require Import WildCat.Core
   WildCat.NatTrans WildCat.Equiv.
 
 #[export] Instance reflexive_proper_proxy {A : Type}

theories/Algebra/AbGroups/AbPushout.v

@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core Modalities.ReflectiveSubuniverse.
+Require Import Basics Types Truncations.Core.
 Require Import WildCat.Core HSet.
 Require Export Algebra.Groups.Image Algebra.Groups.QuotientGroup.
 Require Import AbGroups.AbelianGroup AbGroups.Biproduct.

theories/Algebra/AbGroups/Abelianization.v

@@ -1,7 +1,6 @@
 Require Import Basics Types Truncations.Core.
 Require Import Cubical WildCat.
 Require Import Colimits.Coeq.
-Require Import Algebra.Groups.Group.
 Require Import Algebra.AbGroups.AbelianGroup.
 Require Import Modalities.ReflectiveSubuniverse.
 

theories/Algebra/Congruence.v

@@ -1,4 +1,4 @@
-Require Import Classes.interfaces.abstract_algebra.
+Require Import Classes.interfaces.canonical_names.
 
 (* We say that a relation is a congruence if it respects the operation.
   This is technically incorrect since we are not enforcing the relation to be an equivalence relation.

theories/Algebra/Groups/Group.v

@@ -1,6 +1,6 @@
 Require Import Basics Types HProp HFiber HSet.
 Require Import PathAny.
-Require Import (notations) Classes.interfaces.abstract_algebra.
+Require Import (notations) Classes.interfaces.canonical_names.
 Require Export (hints) Classes.interfaces.abstract_algebra.
 Require Export (hints) Classes.interfaces.canonical_names.
 (** We only export the parts of these that will be most useful to users of this file. *)

theories/Algebra/Rings/CRing.v

@@ -1,5 +1,4 @@
 Require Import WildCat.
-Require Import Spaces.Nat.Core.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.abstract_algebra.
 Require Import Algebra.AbGroups.

theories/Algebra/Rings/ChineseRemainder.v

@@ -1,4 +1,4 @@
-Require Import Classes.interfaces.abstract_algebra.
+Require Import Classes.interfaces.canonical_names.
 Require Import WildCat.
 Require Import Modalities.ReflectiveSubuniverse.
 Require Import Algebra.AbGroups.

theories/Algebra/Rings/Ideal.v

@@ -1,6 +1,6 @@
 Require Import Basics Types.
 Require Import Spaces.Finite.Fin.
-Require Import Classes.interfaces.abstract_algebra.
+Require Import Classes.interfaces.canonical_names.
 Require Import Algebra.Rings.Ring.
 Require Import Algebra.AbGroups.
 

theories/Algebra/Rings/Z.v

@@ -1,4 +1,4 @@
-Require Import Classes.interfaces.abstract_algebra.
+Require Import Classes.interfaces.canonical_names.
 Require Import Algebra.AbGroups.
 Require Import Algebra.Rings.CRing.
 Require Import Spaces.Int Spaces.Pos.

theories/Algebra/Universal/Algebra.v

@@ -7,8 +7,7 @@ Local Unset Elimination Schemes.
 Require Export HoTT.Basics.
 
 Require Import
-  HoTT.Types
-  HoTT.HSet.
+  HoTT.Types.
 
 Declare Scope Algebra_scope.
 Delimit Scope Algebra_scope with Algebra.

theories/Categories/Category/Pi.v

@@ -1,7 +1,6 @@
 (** * Dependent Product Category *)
 Require Import Category.Strict.
 Require Import Basics.Trunc.
-Require Import Types.Forall.
 
 Set Universe Polymorphism.
 Set Implicit Arguments.

theories/Categories/GroupoidCategory/Core.v

@@ -1,6 +1,6 @@
 (** * Groupoids *)
 Require Import Category.Morphisms Category.Strict.
-Require Import Trunc Types.Forall PathGroupoids Basics.Tactics.
+Require Import Trunc PathGroupoids Basics.Tactics.
 
 Set Universe Polymorphism.
 Set Implicit Arguments.

theories/Classes/implementations/field_of_fractions.v

@@ -1,4 +1,4 @@
-Require Import HoTT.HIT.quotient HoTT.Basics.Trunc.
+Require Import HoTT.HIT.quotient.
 Require Import 
   HoTT.Classes.interfaces.abstract_algebra
   HoTT.Classes.theory.dec_fields.

theories/Classes/implementations/list.v

@@ -1,5 +1,5 @@
 Require Import
-  HoTT.Classes.interfaces.abstract_algebra.
+  HoTT.Classes.interfaces.canonical_names.
 
 Generalizable Variables A B C.
 

theories/Classes/implementations/natpair_integers.v

@@ -1,5 +1,5 @@
 Require Import HoTT.HIT.quotient
-  HoTT.TruncType HoTT.Basics.Trunc.
+  HoTT.TruncType.
 Require Import
   HoTT.Classes.implementations.peano_naturals
   HoTT.Classes.interfaces.abstract_algebra

theories/Classes/interfaces/ua_algebra.v

@@ -8,7 +8,6 @@ Require Export
 
 Require Import
   HoTT.Types
-  HoTT.HSet
   HoTT.Classes.implementations.list.
 
 Import ne_list.notations.

theories/Classes/theory/additional_operations.v

@@ -1,4 +1,4 @@
-Require Import HoTT.Classes.interfaces.abstract_algebra.
+Require Import HoTT.Classes.interfaces.canonical_names.
 
 Generalizable Variables A R.
 

theories/Classes/theory/ua_first_isomorphism.v

@@ -6,7 +6,6 @@
 Require Import
   HSet
   Colimits.Quotient
-  Modalities.ReflectiveSubuniverse
   Classes.interfaces.canonical_names
   Classes.theory.ua_isomorphic
   Classes.theory.ua_subalgebra

theories/Classes/theory/ua_prod_algebra.v

@@ -1,6 +1,5 @@
 Require Import
   HoTT.Types.Bool
-  HoTT.Types.Forall
   HoTT.Classes.theory.ua_homomorphism.
 
 Import algebra_notations ne_list.notations.

theories/Colimits/Coeq.v

@@ -1,6 +1,5 @@
 Require Import Basics.
 Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod.
-Require Import Cubical.DPath.
 Require Import Colimits.GraphQuotient.
 
 Local Open Scope path_scope.

theories/Colimits/GraphQuotient.v

@@ -1,5 +1,5 @@
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences.
-Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Types.Forall Cubical.DPath.
+Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.
 
 (** * Quotient of a graph *)
 

theories/HIT/surjective_factor.v

@@ -1,5 +1,4 @@
 Require Import
-        HoTT.Types
         HoTT.Basics
         HoTT.Truncations.Core Modalities.Modality.
 

theories/HSet.v

@@ -1,6 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics.
-Require Import Types.Sigma Types.Forall Types.Paths Types.Unit Types.Arrow.
+Require Import Types.Sigma Types.Paths Types.Unit Types.Arrow.
 
 (** * H-Sets *)
 

theories/Homotopy/EMSpace.v

@@ -4,11 +4,9 @@ Require Import Cubical.DPath.
 Require Import Algebra.AbGroups.
 Require Import Homotopy.Suspension.
 Require Import Homotopy.ClassifyingSpace.
-Require Import Homotopy.HSpace.Core.
 Require Import Homotopy.HSpace.Coherent.
 Require Import Homotopy.HomotopyGroup.
 Require Import Homotopy.Hopf.
-Require Import TruncType.
 Require Import Truncations.Core Truncations.Connectedness.
 Require Import WildCat.
 

theories/NullHomotopy.v

@@ -1,6 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics.
-Require Import Types.Sigma Types.Forall.
+Require Import Types.Sigma.
 Local Open Scope path_scope.
 
 

theories/Pointed/pModality.v

@@ -1,4 +1,4 @@
-Require Import Basics Types ReflectiveSubuniverse Pointed.Core Pointed.pEquiv.
+Require Import Basics Types ReflectiveSubuniverse Pointed.Core.
 
 Local Open Scope pointed_scope.
 

theories/PropResizing/ImpredicativeTruncation.v

@@ -1,7 +1,7 @@
 (* -*- mode: coq; mode: visual-line -*-  *)
 (** * Impredicative truncations. *)
 
-Require Import HoTT.Basics HoTT.Types.
+Require Import HoTT.Basics.
 Require Import PropResizing.PropResizing.
 Local Open Scope path_scope.
 

theories/Sets/AC.v

@@ -1,4 +1,4 @@
-From HoTT Require Import ExcludedMiddle abstract_algebra.
+From HoTT Require Import ExcludedMiddle canonical_names.
 From HoTT Require Import HIT.unique_choice.
 From HoTT Require Import Spaces.Card.
 

theories/Spaces/Circle.v

@@ -5,7 +5,6 @@ Require Import HSet.
 Require Import Spaces.Pos Spaces.Int.
 Require Import Colimits.Coeq.
 Require Import Truncations.Core Truncations.Connectedness.
-Require Import Cubical.DPath.
 
 (** * Theorems about the [Circle]. *)
 

theories/Types/Forall.v

@@ -2,7 +2,7 @@
 (** * Theorems about dependent products *)
 
 Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids
-               Basics.Tactics Basics.Trunc Basics.Contractible.
+               Basics.Tactics Basics.Contractible.
 
 Require Export Basics.Trunc (istrunc_forall).
 

theories/Types/Sum.v

@@ -4,7 +4,7 @@
 Require Import HoTT.Basics.
 Require Import Types.Empty Types.Unit Types.Prod Types.Sigma.
 (** The following are only required for the equivalence between [sum] and a sigma type *)
-Require Import Types.Bool Types.Forall.
+Require Import Types.Bool.
 
 Local Open Scope trunc_scope.
 Local Open Scope path_scope.

theories/WildCat/Monoidal.v

@@ -1,4 +1,4 @@
-Require Import Basics.Overture Basics.Tactics.
+Require Import Basics.Overture.
 Require Import Types.Forall.
 Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv WildCat.NatTrans.
 

theories/WildCat/Products.v

@@ -1,7 +1,7 @@
 Require Import Basics.Equivalences Basics.Overture Basics.Tactics.
 Require Import Types.Bool Types.Prod.
 Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd
-               WildCat.Forall WildCat.NatTrans WildCat.Opposite WildCat.Prod
+               WildCat.Forall WildCat.NatTrans WildCat.Opposite
                WildCat.Universe WildCat.Yoneda WildCat.ZeroGroupoid.
 
 (** * Categories with products *)

theories/WildCat/ZeroGroupoid.v

@@ -1,6 +1,6 @@
-Require Import Basics.Overture Basics.Tactics Basics.Equivalences
+Require Import Basics.Overture Basics.Tactics
                Basics.PathGroupoids.
-Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd WildCat.Prod
+Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd
                WildCat.Forall.
 
 (** * The wild 1-category of 0-groupoids. *)