From ae0ff092f844ae1927e5a6e43dcd4d80c1f63931 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Mar 2018 14:56:43 +0100
Subject: [PATCH] Use prelude everywhere

---
 src/Cat/Categories/CwF.agda                 | 19 ++++++++-----------
 src/Cat/Categories/Free.agda                |  8 +++-----
 src/Cat/Categories/Fun.agda                 |  8 +-------
 src/Cat/Categories/Rel.agda                 | 12 ++++--------
 src/Cat/Categories/Sets.agda                |  1 -
 src/Cat/Category/Monad.agda                 |  9 +--------
 src/Cat/Category/Monad/Kleisli.agda         |  6 +-----
 src/Cat/Category/Monad/Monoidal.agda        |  6 +-----
 src/Cat/Category/Monad/Voevodsky.agda       | 10 ++--------
 src/Cat/Category/NaturalTransformation.agda |  9 +++------
 src/Cat/Prelude.agda                        |  2 +-
 11 files changed, 25 insertions(+), 65 deletions(-)

diff --git a/src/Cat/Categories/CwF.agda b/src/Cat/Categories/CwF.agda
index ea369ef..45dbf2b 100644
--- a/src/Cat/Categories/CwF.agda
+++ b/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 : ????
 
diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index bda3820..1d262dd 100644
--- a/src/Cat/Categories/Free.agda
+++ b/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)
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 14bbdd2..18165d3 100644
--- a/src/Cat/Categories/Fun.agda
+++ 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)
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index ac645ef..5b44601 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/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)
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 52db3a5..a54cba1 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/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
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index f6cb1a9..3b65149 100644
--- a/src/Cat/Category/Monad.agda
+++ b/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
diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda
index eedbeb7..7377cdf 100644
--- a/src/Cat/Category/Monad/Kleisli.agda
+++ b/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
diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda
index 52cfc5e..360e5df 100644
--- a/src/Cat/Category/Monad/Monoidal.agda
+++ b/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
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index 5f27ed0..f30aa9a 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/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
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index 82ef983..13e3d89 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/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
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index 0c2f523..d936e60 100644
--- a/src/Cat/Prelude.agda
+++ b/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
 
 -----------------