Use prelude everywhere

src/Cat/Categories/CwF.agda

@@ -1,36 +1,33 @@
 module Cat.Categories.CwF where
 
-open import Agda.Primitive
-open import Data.Product
+open import Cat.Prelude
 
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Categories.Fam
 
-open Category
-open Functor
-
 module _ {ℓa ℓb : Level} where
   record CwF : Set (lsuc (ℓa ⊔ ℓb)) where
     -- "A category with families consists of"
     field
       -- "A base category"
       ℂ : Category ℓa ℓb
+    module ℂ = Category ℂ
     -- It's objects are called contexts
-    Contexts = Object ℂ
+    Contexts = ℂ.Object
     -- It's arrows are called substitutions
-    Substitutions = Arrow ℂ
+    Substitutions = ℂ.Arrow
     field
       -- A functor T
       T : Functor (opposite ℂ) (Fam ℓa ℓb)
       -- Empty context
-      [] : Terminal ℂ
+      [] : ℂ.Terminal
     private
       module T = Functor T
-    Type : (Γ : Object ℂ) → Set ℓa
+    Type : (Γ : ℂ.Object) → Set ℓa
     Type Γ = proj₁ (proj₁ (T.omap Γ))
 
-    module _ {Γ : Object ℂ} {A : Type Γ} where
+    module _ {Γ : ℂ.Object} {A : Type Γ} where
 
       -- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
       --   k : Σ (proj₁ (omap T B) → proj₁ (omap T A))
@@ -46,7 +43,7 @@ module _ {ℓa ℓb : Level} where
 
       record ContextComprehension : Set (ℓa ⊔ ℓb) where
         field
-          Γ&A : Object ℂ
+          Γ&A : ℂ.Object
           proj1 : ℂ [ Γ&A , Γ ]
           -- proj2 : ????
 

src/Cat/Categories/Free.agda

@@ -1,11 +1,9 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Categories.Free where
 
-open import Agda.Primitive
-open import Relation.Binary
+open import Cat.Prelude hiding (Path ; empty)
 
-open import Cubical hiding (Path ; empty)
-open import Data.Product
+open import Relation.Binary
 
 open import Cat.Category
 
@@ -60,7 +58,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     open Univalence isIdentity
 
     module _ {A B : ℂ.Object} where
-      arrowsAreSets : Cubical.isSet (Path ℂ.Arrow A B)
+      arrowsAreSets : isSet (Path ℂ.Arrow A B)
       arrowsAreSets a b p q = {!!}
 
       eqv : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso isIdentity A B)

src/Cat/Categories/Fun.agda

@@ -1,13 +1,7 @@
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 module Cat.Categories.Fun where
 
-open import Agda.Primitive
-open import Data.Product
-
-
-open import Cubical
-open import Cubical.GradLemma
-open import Cubical.NType.Properties
+open import Cat.Prelude
 
 open import Cat.Category
 open import Cat.Category.Functor hiding (identity)

src/Cat/Categories/Rel.agda

@@ -1,12 +1,8 @@
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Categories.Rel where
 
-open import Cubical
-open import Cubical.GradLemma
-open import Agda.Primitive
-open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
+open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd)
 open import Function
-import Cubical.FromStdLib
 
 open import Cat.Category
 
@@ -74,7 +70,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
 
       equi : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
         ≃ (a , b) ∈ S
-      equi = backwards Cubical.FromStdLib., isequiv
+      equi = backwards , isequiv
 
     ident-r : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
       ≡ (a , b) ∈ S
@@ -108,7 +104,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
 
       equi : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
         ≃ ab ∈ S
-      equi = backwards Cubical.FromStdLib., isequiv
+      equi = backwards , isequiv
 
     ident-l : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
       ≡ ab ∈ S
@@ -146,7 +142,7 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
 
     equi : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
       ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
-    equi = fwd Cubical.FromStdLib., isequiv
+    equi = fwd , isequiv
 
     -- isAssociativec : Q + (R + S) ≡ (Q + R) + S
   is-isAssociative : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)

src/Cat/Categories/Sets.agda

@@ -7,7 +7,6 @@ import Data.Product
 
 open import Function using (_∘_)
 
-open import Cubical hiding (_≃_)
 open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua)
 
 open import Cat.Category

src/Cat/Category/Monad.agda

@@ -20,14 +20,7 @@ The monoidal representation is exposed by default from this module.
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Category.Monad where
 
-open import Agda.Primitive
-
-open import Data.Product
-
-open import Cubical
-open import Cubical.NType.Properties using (lemPropF ; lemSig ;  lemSigP)
-open import Cubical.GradLemma        using (gradLemma)
-
+open import Cat.Prelude
 open import Cat.Category
 open import Cat.Category.Functor as F
 open import Cat.Category.NaturalTransformation

src/Cat/Category/Monad/Kleisli.agda

@@ -4,11 +4,7 @@ The Kleisli formulation of monads
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 open import Agda.Primitive
 
-open import Data.Product
-
-open import Cubical
-open import Cubical.NType.Properties using (lemPropF ; lemSig ;  lemSigP)
-open import Cubical.GradLemma        using (gradLemma)
+open import Cat.Prelude
 
 open import Cat.Category
 open import Cat.Category.Functor as F

src/Cat/Category/Monad/Monoidal.agda

@@ -4,11 +4,7 @@ Monoidal formulation of monads
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 open import Agda.Primitive
 
-open import Data.Product
-
-open import Cubical
-open import Cubical.NType.Properties using (lemPropF ; lemSig ;  lemSigP)
-open import Cubical.GradLemma        using (gradLemma)
+open import Cat.Prelude
 
 open import Cat.Category
 open import Cat.Category.Functor as F

src/Cat/Category/Monad/Voevodsky.agda

@@ -4,14 +4,8 @@ This module provides construction 2.3 in [voe]
 {-# OPTIONS --cubical --allow-unsolved-metas --caching #-}
 module Cat.Category.Monad.Voevodsky where
 
-open import Agda.Primitive
-
-open import Data.Product
-open import Function using (_∘_ ; _$_)
-
-open import Cubical
-open import Cubical.NType.Properties using (lemPropF ; lemSig ;  lemSigP)
-open import Cubical.GradLemma        using (gradLemma)
+open import Cat.Prelude
+open import Function
 
 open import Cat.Category
 open import Cat.Category.Functor as F

src/Cat/Category/NaturalTransformation.agda

@@ -19,15 +19,12 @@
 -- * A composition operator.
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 module Cat.Category.NaturalTransformation where
-open import Agda.Primitive
-open import Data.Product
+
+open import Cat.Prelude
+
 open import Data.Nat using (_≤_ ; z≤n ; s≤s)
 module Nat = Data.Nat
 
-open import Cubical
-open import Cubical.Sigma
-open import Cubical.NType.Properties
-
 open import Cat.Category
 open import Cat.Category.Functor hiding (identity)
 open import Cat.Wishlist

src/Cat/Prelude.agda

@@ -24,7 +24,7 @@ open import Cubical.NType.Properties
     ( lemPropF ; lemSig ;  lemSigP ; isSetIsProp
     ; propPi ; propHasLevel ; setPi ; propSet)
   public
-open import Cubical.Sigma using (setSig) public
+open import Cubical.Sigma using (setSig ; sigPresSet) public
 open import Cubical.Universe using (hSet) public
 
 -----------------