From 29f45d1426ed6b83357e1259d126c0f8831c72ab 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:47:01 +0100
Subject: [PATCH] Delete equality module

---
 src/Cat/Categories/Cat.agda  |  6 ------
 src/Cat/Categories/Cube.agda |  5 +----
 src/Cat/Categories/Fam.agda  |  9 +--------
 src/Cat/Category/Yoneda.agda |  6 +-----
 src/Cat/Equality.agda        | 22 ----------------------
 src/Cat/Prelude.agda         | 10 ++++++++++
 6 files changed, 13 insertions(+), 45 deletions(-)
 delete mode 100644 src/Cat/Equality.agda

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 2e28452..e8a6f73 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -5,9 +5,6 @@ module Cat.Categories.Cat where
 
 open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd)
 
-open import Cubical
-open import Cubical.Sigma
-
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
@@ -15,9 +12,6 @@ open import Cat.Category.Exponential hiding (_×_ ; product)
 open import Cat.Category.NaturalTransformation
 open import Cat.Categories.Fun
 
-open import Cat.Equality
-open Equality.Data.Product
-
 -- The category of categories
 module _ (ℓ ℓ' : Level) where
   private
diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda
index 00f10e3..f338343 100644
--- a/src/Cat/Categories/Cube.agda
+++ b/src/Cat/Categories/Cube.agda
@@ -1,21 +1,18 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Categories.Cube where
 
+open import Cat.Prelude
 open import Level
 open import Data.Bool hiding (T)
 open import Data.Sum hiding ([_,_])
 open import Data.Unit
 open import Data.Empty
-open import Data.Product
-open import Cubical
 open import Function
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
 
 open import Cat.Category
 open import Cat.Category.Functor
-open import Cat.Equality
-open Equality.Data.Product
 
 -- See chapter 1 for a discussion on how presheaf categories are CwF's.
 
diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index d100b77..6829a3b 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -1,17 +1,10 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Categories.Fam where
 
-open import Agda.Primitive
-open import Data.Product
+open import Cat.Prelude
 import Function
 
-open import Cubical
-open import Cubical.Universe
-
 open import Cat.Category
-open import Cat.Equality
-
-open Equality.Data.Product
 
 module _ (ℓa ℓb : Level) where
   private
diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda
index 7a1a0bc..47ac1ec 100644
--- a/src/Cat/Category/Yoneda.agda
+++ b/src/Cat/Category/Yoneda.agda
@@ -2,14 +2,10 @@
 
 module Cat.Category.Yoneda where
 
-open import Agda.Primitive
-open import Data.Product
-open import Cubical
-open import Cubical.NType.Properties
+open import Cat.Prelude
 
 open import Cat.Category
 open import Cat.Category.Functor
-open import Cat.Equality
 
 open import Cat.Categories.Fun
 open import Cat.Categories.Sets hiding (presheaf)
diff --git a/src/Cat/Equality.agda b/src/Cat/Equality.agda
deleted file mode 100644
index d6b3dc0..0000000
--- a/src/Cat/Equality.agda
+++ /dev/null
@@ -1,22 +0,0 @@
-{-# OPTIONS --cubical #-}
--- Defines equality-principles for data-types from the standard library.
-
-module Cat.Equality where
-
-open import Level
-open import Cubical
-
--- _[_≡_] = PathP
-
-module Equality where
-  module Data where
-    module Product where
-      open import Data.Product
-
-      module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
-        (proj₁≡ : (λ _ → A)            [ proj₁ a ≡ proj₁ b ])
-        (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where
-
-        Σ≡ : a ≡ b
-        proj₁ (Σ≡ i) = proj₁≡ i
-        proj₂ (Σ≡ i) = proj₂≡ i
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index 0a047d9..0c2f523 100644
--- a/src/Cat/Prelude.agda
+++ b/src/Cat/Prelude.agda
@@ -24,6 +24,8 @@ open import Cubical.NType.Properties
     ( lemPropF ; lemSig ;  lemSigP ; isSetIsProp
     ; propPi ; propHasLevel ; setPi ; propSet)
   public
+open import Cubical.Sigma using (setSig) public
+open import Cubical.Universe using (hSet) public
 
 -----------------
 -- * Utilities --
@@ -38,3 +40,11 @@ open import Cubical.NType.Properties
 ∃!-syntax = ∃
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
+
+module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
+  (proj₁≡ : (λ _ → A)            [ proj₁ a ≡ proj₁ b ])
+  (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where
+
+  Σ≡ : a ≡ b
+  proj₁ (Σ≡ i) = proj₁≡ i
+  proj₂ (Σ≡ i) = proj₂≡ i