From 183906dc8c59d8bae268b385bac9c04939fe99da 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:39:56 +0100
Subject: [PATCH] Define and use custom prelude

---
 src/Cat/Categories/Cat.agda       |  8 +++----
 src/Cat/Categories/Sets.agda      | 40 ++++++++++++++++++++++++++-----
 src/Cat/Category.agda             | 35 +++++++--------------------
 src/Cat/Category/Exponential.agda |  4 +---
 src/Cat/Category/Product.agda     |  7 ++----
 src/Cat/Prelude.agda              | 40 +++++++++++++++++++++++++++++++
 6 files changed, 89 insertions(+), 45 deletions(-)
 create mode 100644 src/Cat/Prelude.agda

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 1be64e0..2e28452 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -3,8 +3,7 @@
 
 module Cat.Categories.Cat where
 
-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 Cubical
 open import Cubical.Sigma
@@ -14,6 +13,7 @@ open import Cat.Category.Functor
 open import Cat.Category.Product
 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
@@ -182,8 +182,6 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
 -- it is therefory also cartesian closed.
 module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
   private
-    open Data.Product
-    open import Cat.Categories.Fun
     module ℂ = Category ℂ
     module 𝔻 = Category 𝔻
     Categoryℓ = Category ℓ ℓ
@@ -217,7 +215,7 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
   module _ {c : Functor ℂ 𝔻 × ℂ.Object} where
     open Σ c renaming (proj₁ to F ; proj₂ to C)
 
-    ident : fmap {c} {c} (NT.identity F , ℂ.𝟙 {A = proj₂ c}) ≡ 𝔻.𝟙
+    ident : fmap {c} {c} (NT.identity F , ℂ.𝟙 {A = snd c}) ≡ 𝔻.𝟙
     ident = begin
       fmap {c} {c} (Category.𝟙 (object ⊗ ℂ) {c})        ≡⟨⟩
       fmap {c} {c} (idN F , ℂ.𝟙)               ≡⟨⟩
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 98da7b1..52db3a5 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -2,15 +2,13 @@
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 module Cat.Categories.Sets where
 
-open import Agda.Primitive
-open import Data.Product
+open import Cat.Prelude hiding (_≃_)
+import Data.Product
+
 open import Function using (_∘_)
 
--- open import Cubical using (funExt ; refl ; isSet ; isProp ; _≡_ ; isEquiv ; sym ; trans ; _[_≡_] ; I ; Path ; PathP)
 open import Cubical hiding (_≃_)
 open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua)
-open import Cubical.GradLemma
-open import Cubical.NType.Properties
 
 open import Cat.Category
 open import Cat.Category.Functor
@@ -260,9 +258,39 @@ module _ (ℓ : Level) where
       -- `(id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)` ?
       res : isEquiv (hA ≡ hB) (hA ≅ hB) (_≃_.eqv t)
       res = _≃_.isEqv t
+      thr : (hA ≡ hB) ≃ (hA ≅ hB)
+      thr = con _ res
+      -- p : _ → (hX : Object) → Path (hA ≅ hB) (hA ≡ hB)
+      -- p = ?
+      -- p hA X i0 = hA ~ X
+      -- p hA X i1 = Path Obj hA X
+
+      -- From Thierry:
+      --
+      -- -Any- equality proof of
+      --
+      -- Id (Obj C) c0 c1
+      --
+      -- and
+      --
+      -- iso c0 c1
+      --
+      -- is enough to ensure univalence.
+      -- This is because this implies that
+      --
+      -- Sigma (x : Obj C) is c0 x
+      --
+      -- is contractible, which implies univalence.
+
+    univalent' : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB)
+    univalent' hA = {!!} , {!!}
+
     module _ {hA hB : hSet {ℓ}} where
+
+      -- Thierry: `thr0` implies univalence.
       univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (Univalence.id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)
-      univalent = let k = _≃_.isEqv (sym≃ conclusion) in {!k!}
+      univalent = univalent'→univalent univalent'
+      -- let k = _≃_.isEqv (sym≃ conclusion) in {! k!}
 
     SetsIsCategory : IsCategory SetsRaw
     IsCategory.isAssociative SetsIsCategory = refl
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 0db82c2..74e4262 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -28,36 +28,14 @@
 
 module Cat.Category where
 
-open import Agda.Primitive
-open import Data.Unit.Base
-open import Data.Product renaming
+open import Cat.Prelude
+  renaming
   ( proj₁ to fst
   ; proj₂ to snd
-  ; ∃! to ∃!≈
   )
-open import Data.Empty
+
 import      Function
 
-open import Cubical
-open import Cubical.NType
-open import Cubical.NType.Properties
-
-open import Cat.Wishlist
-
------------------
--- * Utilities --
------------------
-
--- | Unique existensials.
-∃! : ∀ {a b} {A : Set a}
-  → (A → Set b) → Set (a ⊔ b)
-∃! = ∃!≈ _≡_
-
-∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
-∃!-syntax = ∃
-
-syntax ∃!-syntax (λ x → B) = ∃![ x ] B
-
 -----------------
 -- * Categories --
 -----------------
@@ -148,6 +126,12 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     --     ∀ A → isContr (Σ[ X ∈ Object ] iso A X)
 
     -- future work ideas: compile to CAM
+    Univalent' : Set _
+    Univalent' = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
+
+    module _ (univalent' : Univalent') where
+      univalent'→univalent : Univalent
+      univalent'→univalent = {!!}
 
 -- | The mere proposition of being a category.
 --
@@ -229,7 +213,6 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
       isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
         lemSig (λ g → propIsInverseOf) a a' geq
           where
-            open Cubical.NType.Properties
             geq : g ≡ g'
             geq = begin
               g            ≡⟨ sym rightIdentity ⟩
diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda
index 87769f6..76652d2 100644
--- a/src/Cat/Category/Exponential.agda
+++ b/src/Cat/Category/Exponential.agda
@@ -1,8 +1,6 @@
 module Cat.Category.Exponential where
 
-open import Agda.Primitive
-open import Data.Product hiding (_×_)
-open import Cubical
+open import Cat.Prelude hiding (_×_)
 
 open import Cat.Category
 open import Cat.Category.Product
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index c459566..1ce45c5 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -1,11 +1,8 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 module Cat.Category.Product where
 
-open import Agda.Primitive
-open import Cubical
-open import Cubical.NType.Properties using (lemPropF)
-
-open import Data.Product as P hiding (_×_ ; proj₁ ; proj₂)
+open import Cat.Prelude hiding (_×_ ; proj₁ ; proj₂)
+import Data.Product as P
 
 open import Cat.Category
 
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
new file mode 100644
index 0000000..0a047d9
--- /dev/null
+++ b/src/Cat/Prelude.agda
@@ -0,0 +1,40 @@
+-- | Custom prelude for this module
+module Cat.Prelude where
+
+open import Agda.Primitive public
+-- FIXME Use:
+-- open import Agda.Builtin.Sigma public
+-- Rather than
+open import Data.Product public
+  renaming (∃! to ∃!≈)
+
+-- TODO Import Data.Function under appropriate names.
+
+open import Cubical public
+-- FIXME rename `gradLemma` to `fromIsomorphism` - perhaps just use wrapper
+-- module.
+open import Cubical.GradLemma
+  using (gradLemma)
+  public
+open import Cubical.NType
+  using (⟨-2⟩)
+  public
+open import Cubical.NType.Properties
+  using
+    ( lemPropF ; lemSig ;  lemSigP ; isSetIsProp
+    ; propPi ; propHasLevel ; setPi ; propSet)
+  public
+
+-----------------
+-- * Utilities --
+-----------------
+
+-- | Unique existensials.
+∃! : ∀ {a b} {A : Set a}
+  → (A → Set b) → Set (a ⊔ b)
+∃! = ∃!≈ _≡_
+
+∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∃!-syntax = ∃
+
+syntax ∃!-syntax (λ x → B) = ∃![ x ] B