Merge pull request #226 from m-lindgren/remove-imports

Remove some unnecessary imports.
UniMath · Nov 5, 2022 · 71a4afe · 71a4afe
2 parents b507c6f + 53b8c51
commit 71a4afe
Show file tree

Hide file tree

Showing 27 changed files with 85 additions and 46 deletions.
diff --git a/TypeTheory/Articles/ALV_2017.v b/TypeTheory/Articles/ALV_2017.v
@@ -15,6 +15,7 @@ This file should contain _no substantial formalisation_, and should not be impor
 
 Require Import UniMath.Foundations.Sets.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
+Require Import UniMath.CategoryTheory.rezk_completion.
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
 

diff --git a/TypeTheory/Articles/ALV_2018.v b/TypeTheory/Articles/ALV_2018.v
@@ -12,6 +12,7 @@ This file is intended to accompany a sequel article to ALV-2017, currently in (d
 
 Require Import UniMath.Foundations.Sets.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
+Require Import UniMath.CategoryTheory.rezk_completion.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/Auxiliary/ArrowCategory.v b/TypeTheory/Auxiliary/ArrowCategory.v
@@ -2,7 +2,8 @@
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
 
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.ArrowCategory.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/Auxiliary/CategoryTheory.v b/TypeTheory/Auxiliary/CategoryTheory.v
@@ -1,18 +1,24 @@
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
 
-Require Import UniMath.CategoryTheory.All.
+Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
+Require Import UniMath.CategoryTheory.CategoryEquality.
+Require Import UniMath.CategoryTheory.DisplayedCats.ComprehensionC.
+
 (* a few libraries need to be reloaded after “All”,
    to claim precedence on overloaded names *)
+
 Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.limits.graphs.terminal.
+Require Import UniMath.CategoryTheory.limits.graphs.initial.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 
 
 (** * General notations and scopes *)
 
 (** We redeclare this notation, along with a new scope . *)
+Declare Scope mor_scope.
 Notation "ff ;; gg" := (compose ff gg)
   (at level 50, left associativity, format "ff  ;;  gg")
   : mor_scope.

diff --git a/TypeTheory/Auxiliary/CategoryTheoryImports.v b/TypeTheory/Auxiliary/CategoryTheoryImports.v
@@ -14,7 +14,7 @@ Require Export UniMath.CategoryTheory.whiskering.
 Require Export UniMath.CategoryTheory.Adjunctions.Core.
 Require Export UniMath.CategoryTheory.Equivalences.Core.
 Require Export UniMath.CategoryTheory.precomp_fully_faithful.
-Require Export UniMath.CategoryTheory.rezk_completion.
+(* Require Export UniMath.CategoryTheory.rezk_completion. *)
 Require Export UniMath.CategoryTheory.yoneda.
 Require Export UniMath.CategoryTheory.categories.HSET.Core.
 Require Export UniMath.CategoryTheory.categories.HSET.Univalence.

diff --git a/TypeTheory/Auxiliary/DisplayedCategories.v b/TypeTheory/Auxiliary/DisplayedCategories.v
@@ -2,7 +2,17 @@
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
 
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
+Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations.
+Require Import UniMath.CategoryTheory.DisplayedCats.Adjunctions.
+Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences.
+Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
+Require Import UniMath.CategoryTheory.DisplayedCats.Total.
+
+Require Import UniMath.CategoryTheory.Adjunctions.Core.
+Require Import UniMath.CategoryTheory.Equivalences.Core.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
@@ -268,7 +278,7 @@ Section Discrete_Fibrations.
              (f : c' --> c) (d : D c) (d' : D c')
     : (d' -->[f] d) = (lift_source is_discrete_fibration_D f d = d').
   Proof.
-    apply univalenceweq.
+    apply univalence.
     apply discrete_fibration_mor_weq.
   Defined.
 

diff --git a/TypeTheory/Auxiliary/Pullbacks.v b/TypeTheory/Auxiliary/Pullbacks.v
@@ -1,7 +1,7 @@
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
 
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
 (* a few libraries need to be reloaded after “All”,
    to claim precedence on overloaded names *)
 Require Import UniMath.CategoryTheory.limits.pullbacks.

diff --git a/TypeTheory/Auxiliary/SetsAndPresheaves.v b/TypeTheory/Auxiliary/SetsAndPresheaves.v
@@ -1,16 +1,19 @@
 
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
+Require Import UniMath.Combinatorics.StandardFiniteSets.
 
-Require Import UniMath.CategoryTheory.All.
 (* a few libraries need to be reloaded after “All”,
    to claim precedence on overloaded names *)
 Require Import UniMath.CategoryTheory.limits.graphs.limits.
 Require Import UniMath.CategoryTheory.limits.graphs.pullbacks.
 Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.categories.HSET.Limits.
+Require Import UniMath.CategoryTheory.categories.HSET.Univalence.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
+Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 
 (** * Presheaf generalities *)
 

diff --git a/TypeTheory/Auxiliary/TypeOfMorphisms.v b/TypeTheory/Auxiliary/TypeOfMorphisms.v
@@ -1,7 +1,11 @@
 
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.Equivalences.Core.
+Require Import UniMath.CategoryTheory.Adjunctions.Core.
+Require Import UniMath.CategoryTheory.FunctorCategory.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/Categories/category_FAM.v b/TypeTheory/Categories/category_FAM.v
@@ -9,10 +9,6 @@
 
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.Core.Categories.
-Require Import UniMath.CategoryTheory.Core.Functors.
-Require Import UniMath.CategoryTheory.yoneda.
-Require Import UniMath.CategoryTheory.rezk_completion.
 
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 Require Import TypeTheory.Auxiliary.Auxiliary.

diff --git a/TypeTheory/CompCats/FullyFaithfulDispFunctor.v b/TypeTheory/CompCats/FullyFaithfulDispFunctor.v
@@ -35,7 +35,10 @@ Accessors for [ff_disp_functor]:
 
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.CategoryEquality.
+Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
@@ -130,7 +133,7 @@ Section FullyFaithfulDispFunctor.
       apply impred_iscontr. intros A'.
       apply impred_iscontr. intros f.
       use (@iscontrweqf (∑ mord : UU, mord = pr2 D Γ A -->[f] pr2 D Γ' A')).
-      - use (weqtotal2 (idweq _)). intros mord. apply univalenceweq.
+      - use (weqtotal2 (idweq _)). intros mord. apply univalence.
       - apply iscontrcoconustot.
     Defined.
 

diff --git a/TypeTheory/CwF/CwF_def.v b/TypeTheory/CwF/CwF_def.v
@@ -17,6 +17,7 @@ Contents:
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
+Require Import UniMath.CategoryTheory.rezk_completion.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/CwF/RepMaps.v b/TypeTheory/CwF/RepMaps.v
@@ -17,6 +17,7 @@ Contents:
 
 Require Import UniMath.Foundations.Sets.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
+Require Import UniMath.CategoryTheory.rezk_completion.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Defs.v b/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Defs.v
@@ -24,7 +24,9 @@ NB: we follow UniMath’s convention that _category_ does not assume saturation/
 
 
 Require Import UniMath.Foundations.Sets.
-Require Import UniMath.CategoryTheory.All. (* TODO: work out what’s actually needed and move into [CategoryTheoryImports]. *)
+Require Import UniMath.MoreFoundations.PartA.
+Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Total.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.

diff --git a/TypeTheory/CwF_TypeCat/TypeCat_Reassoc.v b/TypeTheory/CwF_TypeCat/TypeCat_Reassoc.v
@@ -17,7 +17,10 @@ The equivalence is a bit more involved than one might hope; it proceeds in two m
 
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.opp_precat.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/Initiality/Environments.v b/TypeTheory/Initiality/Environments.v
@@ -1,6 +1,6 @@
 
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
@@ -66,7 +66,7 @@ Section Environments.
 
   Definition reind_idmap_environment {C : split_typecat}
       {Γ : C} {n} (E : environment Γ n)
-    : reind_environment (id _) E = E.
+    : reind_environment (identity _) E = E.
   Proof.
     apply funextfun; intros i; apply reind_idmap_type_with_term.
   Qed.

diff --git a/TypeTheory/Initiality/Initiality.v b/TypeTheory/Initiality/Initiality.v
@@ -1,8 +1,8 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.MoreFoundations.Propositions.
 (* [MoreFoundations.Propositions] seems to need individual importing to provide notation [∃!] as [iscontr_hProp] instead of just [iscontr]. TODO: figure out why; perhaps raise issue upstream? *)
-Require Import UniMath.CategoryTheory.All.
 
+Require Import UniMath.CategoryTheory.Core.Prelude.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/Initiality/Interpretation.v b/TypeTheory/Initiality/Interpretation.v
@@ -1,7 +1,7 @@
 (** This file defines the interpretation function, from the syntax of our toy type theory into any split type-cat with suitable structure. *)
 
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
 
 (* TODO: raise issue upstream: notation "_ ∘ _" is used for function-order composition of functions, but for diagrammatic-order composition of morphisms in categories! *)
 

diff --git a/TypeTheory/Initiality/SyntacticCategory.v b/TypeTheory/Initiality/SyntacticCategory.v
@@ -3,7 +3,9 @@
 As a matter of organisation: all concrete lemmas involving derivations should live upstream in [TypingLemmas]; this file should simply package them up into the appropriate categorical structure. *)
 
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.limits.graphs.terminal.
 Require UniMath.PAdics.lemmas. (* just for [setquotprpathsandR] *)
 
 Require Import TypeTheory.Auxiliary.Auxiliary.

diff --git a/TypeTheory/Initiality/SyntacticCategory_Structure.v b/TypeTheory/Initiality/SyntacticCategory_Structure.v
@@ -1,5 +1,5 @@
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Categories.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/Instances/Presheaves.v b/TypeTheory/Instances/Presheaves.v
@@ -103,20 +103,11 @@ Written by: Anders Mörtberg, 2017
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
 
-Require Import UniMath.CategoryTheory.All.
-(*
-Require Import UniMath.CategoryTheory.Core.Functors.
-Require Import UniMath.CategoryTheory.Adjunctions.Core.
-Require Import UniMath.CategoryTheory.opp_precat.
-Require Import UniMath.CategoryTheory.whiskering.
-Require Import UniMath.CategoryTheory.Equivalences.Core.
+Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 Require Import UniMath.CategoryTheory.RightKanExtension.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.graphs.eqdiag.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
-Require Import UniMath.CategoryTheory.Presheaf.
+Require Import UniMath.CategoryTheory.categories.HSET.Limits.
 Require Import UniMath.CategoryTheory.ElementsOp.
- *)
+
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
 Require Import TypeTheory.Auxiliary.Pullbacks.

diff --git a/TypeTheory/OtherDefs/CwF_Pitts_completion.v b/TypeTheory/OtherDefs/CwF_Pitts_completion.v
@@ -8,7 +8,11 @@
 
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.rezk_completion.
+Require Import UniMath.CategoryTheory.opp_precat.
+Require Import UniMath.CategoryTheory.categories.HSET.Core.
+Require Import UniMath.CategoryTheory.categories.HSET.Univalence.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/RelUniv/RelUnivTransfer.v b/TypeTheory/RelUniv/RelUnivTransfer.v
@@ -21,6 +21,7 @@ TODO:
 Require Import UniMath.Foundations.All.
 Require Import UniMath.MoreFoundations.All.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
+Require Import UniMath.CategoryTheory.rezk_completion.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
@@ -33,6 +34,7 @@ Require Import TypeTheory.RelUniv.Transport_along_Equivs.
 Require Import TypeTheory.RelUniv.RelUniv_Cat_Simple.
 Require Import TypeTheory.RelUniv.RelUniv_Cat.
 Require Import UniMath.CategoryTheory.catiso.
+Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
 Section RelUniv_Transfer.
 
@@ -345,8 +347,8 @@ Section RelUniv_Transfer.
             (S_ff : fully_faithful S).
 
     Let E := ((S,, (invS,, (pr1 eta, pr1 eps)))
-                ,, ((λ d,  (pr2 (Constructions.pointwise_z_iso_from_nat_z_iso eta d )))
-                    , (λ d', (pr2 (Constructions.pointwise_z_iso_from_nat_z_iso eps d')))))
+                ,, ((λ d,  (pr2 (pointwise_z_iso_from_nat_z_iso eta d )))
+                    , (λ d', (pr2 (pointwise_z_iso_from_nat_z_iso eps d')))))
             : equivalence_of_cats D D'.
 
     Let AE := adjointificiation E.
@@ -359,8 +361,8 @@ Section RelUniv_Transfer.
                 _ (ε',,pr22 (adjointificiation E))
             : z_iso (C:=[D', D']) (invS ∙ S) (functor_identity D').
 
-    Let ηx := Constructions.pointwise_z_iso_from_nat_z_iso (z_iso_inv_from_z_iso η).
-    Let αx := Constructions.pointwise_z_iso_from_nat_z_iso (α,,α_is_iso).
+    Let ηx := pointwise_z_iso_from_nat_z_iso (z_iso_inv_from_z_iso η).
+    Let αx := pointwise_z_iso_from_nat_z_iso (α,,α_is_iso).
 
   Section Helpers.
 
@@ -565,8 +567,8 @@ Section RelUniv_Transfer.
       : z_iso u'
             (reluniv_functor_with_ess_surj (inv_reluniv_with_ess_surj u')).
     Proof.
-      set (εx := Constructions.pointwise_z_iso_from_nat_z_iso ε).
-      set (εx' := Constructions.pointwise_z_iso_from_nat_z_iso
+      set (εx := pointwise_z_iso_from_nat_z_iso ε).
+      set (εx' := pointwise_z_iso_from_nat_z_iso
                    (z_iso_inv_from_z_iso ε)).
       use make_z_iso.
       - use tpair.

diff --git a/TypeTheory/RelUniv/RelUnivYonedaCompletion.v b/TypeTheory/RelUniv/RelUnivYonedaCompletion.v
@@ -7,6 +7,7 @@
 (** This file provides the result: given a universe in [preShv C] relative to the Yoneda embedding [ Yo : C -> preShv C ], this transfers to a similar relative universe in [ preShv (RC C) ]. i.e. on the Rezk-completion of [C]. *)
 Require Import UniMath.Foundations.Sets.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
+Require Import UniMath.CategoryTheory.rezk_completion.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.

diff --git a/TypeTheory/RelUniv/Transport_along_Equivs.v b/TypeTheory/RelUniv/Transport_along_Equivs.v
@@ -27,8 +27,11 @@
 
 
 Require Import UniMath.Foundations.Sets.
-Require Import UniMath.CategoryTheory.All.
 
+Require Import UniMath.CategoryTheory.precomp_fully_faithful.
+Require Import UniMath.CategoryTheory.precomp_ess_surj.
+
+Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
 Require Import TypeTheory.Auxiliary.SetsAndPresheaves.

diff --git a/TypeTheory/TypeCat/Contextual.v b/TypeTheory/TypeCat/Contextual.v
@@ -2,12 +2,16 @@
 (** This file provides a definition (and basic development) of contextual categories as split type-cats/CwA’s in which every object is uniquely expressible as an iterated extension of a chosen terminal object. *)
 
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+
+Require Import UniMath.CategoryTheory.Core.Prelude.
+Require Import UniMath.CategoryTheory.limits.graphs.limits.
+Require Import UniMath.CategoryTheory.limits.graphs.terminal.
+
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
 Require Import TypeTheory.Auxiliary.Partial.
-Require Import TypeTheory.TypeCat.TypeCat.
 
+Require Import TypeTheory.TypeCat.TypeCat.
 Require Import TypeTheory.TypeCat.General.
 
 Section Extensions.

diff --git a/TypeTheory/TypeCat/ExtraStructure.v b/TypeTheory/TypeCat/ExtraStructure.v
@@ -2,7 +2,7 @@
 not yet integrated into the type theory of [Initiality.Syntax] and the statement/proof of initiality. *)
 
 Require Import UniMath.MoreFoundations.All.
-Require Import UniMath.CategoryTheory.All.
+Require Import UniMath.CategoryTheory.Core.Categories.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.