From 57d7eab4cb9fc2cc366f398e96de44deb65f2a31 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Feb 2018 13:37:07 +0100
Subject: [PATCH] Make sets a category according to HoTT

---
 src/Cat/Categories/Sets.agda | 168 +++++++++++++++++++++--------------
 src/Cat/Category.agda        |  13 +--
 2 files changed, 106 insertions(+), 75 deletions(-)

diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 5263aa1..4d23936 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -9,80 +9,116 @@ import Function
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
-open Category
+
+module _ (ℓ : Level) where
+  private
+    open RawCategory
+    open IsCategory
+    open import Cubical.Univalence
+    open import Cubical.NType.Properties
+    open import Cubical.Universe
+
+    SetsRaw : RawCategory (lsuc ℓ) ℓ
+    Object SetsRaw = Cubical.Universe.0-Set
+    Arrow SetsRaw (T , _) (U , _) = T → U
+    𝟙 SetsRaw = Function.id
+    _∘_ SetsRaw = Function._∘′_
+
+    setIsSet : (A : Set ℓ) → isSet A
+    setIsSet A x y p q = {!ua!}
+
+    SetsIsCategory : IsCategory SetsRaw
+    assoc SetsIsCategory = refl
+    proj₁ (ident SetsIsCategory) = funExt λ _ → refl
+    proj₂ (ident SetsIsCategory) = funExt λ _ → refl
+    arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s
+    univalent SetsIsCategory = {!!}
+
+  𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
+  Category.raw 𝓢𝓮𝓽 = SetsRaw
+  Category.isCategory 𝓢𝓮𝓽 = SetsIsCategory
+  Sets = 𝓢𝓮𝓽
 
 module _ {ℓ : Level} where
-  SetsRaw : RawCategory (lsuc ℓ) ℓ
-  RawCategory.Object SetsRaw = Set ℓ
-  RawCategory.Arrow SetsRaw = λ T U → T → U
-  RawCategory.𝟙 SetsRaw = Function.id
-  RawCategory._∘_ SetsRaw = Function._∘′_
-
-  open IsCategory
-  SetsIsCategory : IsCategory SetsRaw
-  assoc SetsIsCategory = refl
-  proj₁ (ident SetsIsCategory) = funExt λ _ → refl
-  proj₂ (ident SetsIsCategory) = funExt λ _ → refl
-  arrowIsSet SetsIsCategory = {!!}
-  univalent SetsIsCategory = {!!}
-
-  Sets : Category (lsuc ℓ) ℓ
-  raw Sets = SetsRaw
-  isCategory Sets = SetsIsCategory
-
   private
-    module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
-      _&&&_ : (X → A × B)
-      _&&&_ x = f x , g x
-    module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
-      lem : Sets [ proj₁ ∘ (f &&& g)] ≡ f × Sets [ proj₂ ∘ (f &&& g)] ≡ g
-      proj₁ lem = refl
-      proj₂ lem = refl
-    instance
-      isProduct : {A B : Object Sets} → IsProduct Sets {A} {B} proj₁ proj₂
-      isProduct f g = f &&& g , lem f g
+    𝓢 = 𝓢𝓮𝓽 ℓ
+    open Category 𝓢
+    open import Cubical.Sigma
 
-    product : (A B : Object Sets) → Product {ℂ = Sets} A B
-    product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }
+    module _ (0A 0B : Object) where
+      private
+        A : Set ℓ
+        A = proj₁ 0A
+        sA : isSet A
+        sA = proj₂ 0A
+        B : Set ℓ
+        B = proj₁ 0B
+        sB : isSet B
+        sB = proj₂ 0B
+        0A×0B : Object
+        0A×0B = (A × B) , sigPresSet sA λ _ → sB
+
+        module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
+          _&&&_ : (X → A × B)
+          _&&&_ x = f x , g x
+        module _ {0X : Object} where
+          X = proj₁ 0X
+          module _ (f : X → A ) (g : X → B) where
+            lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
+            proj₁ lem = refl
+            proj₂ lem = refl
+        instance
+          isProduct : IsProduct 𝓢 {0A} {0B} {0A×0B} proj₁ proj₂
+          isProduct {X = X} f g = (f &&& g) , lem {0X = X} f g
+
+      product : Product {ℂ = 𝓢} 0A 0B
+      product = record
+        { obj = 0A×0B
+        ; proj₁ = Data.Product.proj₁
+        ; proj₂ = Data.Product.proj₂
+        ; isProduct = λ { {X} → isProduct {X = X}}
+        }
 
   instance
-    SetsHasProducts : HasProducts Sets
+    SetsHasProducts : HasProducts 𝓢
     SetsHasProducts = record { product = product }
 
--- Covariant Presheaf
-Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
-Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
+module _ {ℓa ℓb : Level} where
+  module _ (ℂ : Category ℓa ℓb) where
+    -- Covariant Presheaf
+    Representable : Set (ℓa ⊔ lsuc ℓb)
+    Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
 
--- The "co-yoneda" embedding.
-representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
-representable {ℂ = ℂ} A = record
-  { raw = record
-    { func* = λ B → ℂ [ A , B ]
-    ; func→ = ℂ [_∘_]
-    }
-  ; isFunctor = record
-    { ident = funExt λ _ → proj₂ ident
-    ; distrib = funExt λ x → sym assoc
-    }
-  }
-  where
-    open IsCategory (isCategory ℂ)
+    -- Contravariant Presheaf
+    Presheaf : Set (ℓa ⊔ lsuc ℓb)
+    Presheaf = Functor (Opposite ℂ) (𝓢𝓮𝓽 ℓb)
 
--- Contravariant Presheaf
-Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
-Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
-
--- Alternate name: `yoneda`
-presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
-presheaf {ℂ = ℂ} B = record
-  { raw = record
-    { func* = λ A → ℂ [ A , B ]
-    ; func→ = λ f g → ℂ [ g ∘ f ]
-  }
-  ; isFunctor = record
-    { ident = funExt λ x → proj₁ ident
-    ; distrib = funExt λ x → assoc
+  -- The "co-yoneda" embedding.
+  representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
+  representable {ℂ = ℂ} A = record
+    { raw = record
+      { func* = λ B → ℂ [ A , B ] , arrowIsSet
+      ; func→ = ℂ [_∘_]
+      }
+    ; isFunctor = record
+      { ident = funExt λ _ → proj₂ ident
+      ; distrib = funExt λ x → sym assoc
+      }
     }
-  }
-  where
-    open IsCategory (isCategory ℂ)
+    where
+      open Category ℂ
+
+  -- Alternate name: `yoneda`
+  presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
+  presheaf {ℂ = ℂ} B = record
+    { raw = record
+      { func* = λ A → ℂ [ A , B ] , arrowIsSet
+      ; func→ = λ f g → ℂ [ g ∘ f ]
+    }
+    ; isFunctor = record
+      { ident = funExt λ x → proj₁ ident
+      ; distrib = funExt λ x → assoc
+      }
+    }
+    where
+      open Category ℂ
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 69c4aa8..686ae76 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -84,6 +84,7 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     idIso : (A : Object) → A ≅ A
     idIso A = 𝟙 , (𝟙 , ident)
 
+    -- Lemma 9.1.4 in [HoTT]
     id-to-iso : (A B : Object) → A ≡ B → A ≅ B
     id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A)
 
@@ -93,12 +94,6 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     Univalent : Set (ℓa ⊔ ℓb)
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
 
--- Thierry: All projections must be `isProp`'s
-
--- According to definitions 9.1.1 and 9.1.6 in the HoTT book the
--- arrows of a category form a set (arrow-is-set), and there is an
--- equivalence between the equality of objects and isomorphisms
--- (univalent).
 record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
   open RawCategory ℂ
   open Univalence ℂ public
@@ -192,14 +187,16 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     {{isCategory}} : IsCategory raw
 
   open RawCategory raw public
+  open IsCategory isCategory public
 
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  open Category ℂ
   _[_,_] : (A : Object) → (B : Object) → Set ℓb
   _[_,_] = Arrow
 
   _[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
   _[_∘_] = _∘_
 
-
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private
     open Category ℂ
@@ -210,8 +207,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     RawCategory.𝟙 OpRaw = 𝟙
     RawCategory._∘_ OpRaw = Function.flip _∘_
 
-    open IsCategory isCategory
-
     OpIsCategory : IsCategory OpRaw
     IsCategory.assoc OpIsCategory = sym assoc
     IsCategory.ident OpIsCategory = swap ident