Merge branch 'dev'

BACKLOG.md

@@ -0,0 +1,6 @@
+Backlog
+=======
+
+Prove univalence for various categories
+
+Prove postulates in `Cat.Wishlist`

CHANGELOG.md

@@ -0,0 +1,17 @@
+Changelog
+=========
+
+Version 1.1.0
+-------------
+In this version categories have been refactored - there's now a notion of a raw
+category, and a proper category which has the data (raw category) as well as
+the laws.
+
+Furthermore the type of arrows must be homotopy sets and they must satisfy univalence.
+
+I've made a module `Cat.Wishlist` where I just postulate things that I hope to
+implement upstream in `cubical`.
+
+I have proven that `IsCategory` is a mere proposition.
+
+I've also updated the category of sets to adhere to this new definition.

README.md

@@ -1,17 +1,29 @@
 Description
 ===========
-This project includes code as well as my masters thesis (currently just
+This project aims to formalize some parts of category theory using cubical agda
-consisting of the proposal for the thesis).
+— an extension to agda permitting univalence. To learn more about this
+[readthedocs](https://agda.readthedocs.io/en/latest/language/cubical.html).
+
+This project draws a lot of inspiration from [the
+HoTT-book](https://homotopytypetheory.org/book/).
 
 Installation
 ============
-You probably need a very recent version of the Agda compiler. At the time
-of writing the solution has been tested with Agda version 2.6.0-5d84754.
 
 Dependencies
 ------------
+To succesfully compile the following is needed:
+
+* Agda version >= `707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`.
+* [Agda Standard Library](https://github.com/agda/agda-stdlib)
+* [Cubical](https://github.com/Saizan/cubical-demo/)
+
+It's important to have the right version of these - but which one is the right
+is in constant flux. It's most likely the newest one.
+
 I've used git submodules to manage dependencies. Unfortunately Agda does not
-allow specifying libraries to be used only as local dependencies.
+allow specifying libraries to be used only as local dependencies. So the
+submodules are mostly used for documentation.
 
 You can let Agda know about these libraries by appending them to your global
 libraries file like so: (NB!: There is a good reason this is not in a

libs/agda-stdlib

@@ -1 +1 @@
-Subproject commit 157497a5335ad0069c7aaffbc65932c40a28ee68
+Subproject commit 87d28d7d753f73abd20665d7bbb88f9d72ed88aa

libs/cubical

@@ -1 +1 @@
-Subproject commit 12c2c628e9e202f1698a4c32e0356d5ca8cb6151
+Subproject commit 9bfbacbb30d4673332566f6e4a58fd04e3904106

src/Cat/Categories/Free.agda

@@ -8,55 +8,65 @@ open import Data.Product
 open import Cat.Category
 
 open IsCategory
-open Category
 
 -- data Path {ℓ : Level} {A : Set ℓ} : (a b : A) → Set ℓ where
 --   emptyPath : {a : A} → Path a a
 --   concatenate : {a b c : A} → Path a b → Path b c → Path a b
 
+-- import Data.List
+-- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
+-- P = {!Data.List.List ?!}
+-- Generalized paths:
+data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where
+  empty : {a : A} → Path R a a
+  cons : {a b c : A} → R b c → Path R a b → Path R a c
+
+concatenate _++_ : ∀ {ℓ ℓ'} {A : Set ℓ} {a b c : A} {R : A → A → Set ℓ'} → Path R b c → Path R a b → Path R a c
+concatenate empty p = p
+concatenate (cons x q) p = cons x (concatenate q p)
+_++_ = concatenate
+
+singleton : ∀ {ℓ} {𝓤 : Set ℓ} {ℓr} {R : 𝓤 → 𝓤 → Set ℓr} {A B : 𝓤} → R A B → Path R A B
+singleton f = cons f empty
+
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   module ℂ = Category ℂ
-
+  open Category ℂ
-  -- import Data.List
-  -- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
-  -- P = {!Data.List.List ?!}
-  -- Generalized paths:
-  -- data P {ℓ : Level} {A : Set ℓ} (R : A → A → Set ℓ) : (a b : A) → Set ℓ where
-  --   e : {a : A} → P R a a
-  --   c : {a b c : A} → R a b → P R b c → P R a c
-
-  -- Path's are like lists with directions.
-  -- This implementation is specialized to categories.
-  data Path : (a b : Object ℂ) → Set (ℓ ⊔ ℓ') where
-    empty : {A : Object ℂ} → Path A A
-    cons : ∀ {A B C} → ℂ [ B , C ] → Path A B → Path A C
-
-  concatenate : ∀ {A B C : Object ℂ}  → Path B C → Path A B → Path A C
-  concatenate empty p = p
-  concatenate (cons x q) p = cons x (concatenate q p)
 
   private
-    module _ {A B C D : Object ℂ} where
+    p-assoc : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D}
-      p-assoc : {r : Path A B} {q : Path B C} {p : Path C D} → concatenate p (concatenate q r) ≡ concatenate (concatenate p q) r
+      → p ++ (q ++ r) ≡ (p ++ q) ++ r
-      p-assoc {r} {q} {p} = {!!}
+    p-assoc {r = r} {q} {empty} = refl
-    module _ {A B : Object ℂ} {p : Path A B} where
+    p-assoc {A} {B} {C} {D} {r = r} {q} {cons x p} = begin
-      -- postulate
+      cons x p ++ (q ++ r)   ≡⟨ cong (cons x) lem ⟩
-      --   ident-r : concatenate {A} {A} {B} p (lift 𝟙) ≡ p
+      cons x ((p ++ q) ++ r) ≡⟨⟩
-      --   ident-l : concatenate {A} {B} {B} (lift 𝟙) p ≡ p
+      (cons x p ++ q) ++ r ∎
-    module _ {A B : Object ℂ} where
+      where
-      isSet : Cubical.isSet (Path A B)
+        lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r)
-      isSet = {!!}
+        lem = p-assoc {r = r} {q} {p}
+
+    ident-r : ∀ {A} {B} {p : Path Arrow A B} → concatenate p empty ≡ p
+    ident-r {p = empty} = refl
+    ident-r {p = cons x p} = cong (cons x) ident-r
+
+    ident-l : ∀ {A} {B} {p : Path Arrow A B} → concatenate empty p ≡ p
+    ident-l = refl
+
+    module _ {A B : Object} where
+      isSet : Cubical.isSet (Path Arrow A B)
+      isSet a b p q = {!!}
+
   RawFree : RawCategory ℓ (ℓ ⊔ ℓ')
   RawFree = record
-    { Object = Object ℂ
+    { Object = Object
-    ; Arrow = Path
+    ; Arrow = Path Arrow
-    ; 𝟙 = λ {o} → {!lift 𝟙!}
+    ; 𝟙 = empty
-    ; _∘_ = λ {a b c} → {!concatenate {a} {b} {c}!}
+    ; _∘_ = concatenate
     }
   RawIsCategoryFree : IsCategory RawFree
   RawIsCategoryFree = record
-    { assoc = {!p-assoc!}
+    { assoc = λ { {f = f} {g} {h} → p-assoc {r = f} {g} {h}}
-    ; ident = {!ident-r , ident-l!}
+    ; ident = ident-r , ident-l
     ; arrowIsSet = {!!}
     ; univalent = {!!}
     }

src/Cat/Categories/Fun.agda

@@ -9,6 +9,7 @@ import Cubical.GradLemma
 module UIP = Cubical.GradLemma
 open import Cubical.Sigma
 open import Cubical.NType
+open import Cubical.NType.Properties
 open import Data.Nat using (_≤_ ; z≤n ; s≤s)
 module Nat = Data.Nat
 
@@ -20,7 +21,7 @@ open import Cat.Equality
 open Equality.Data.Product
 
 module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
-  open Category hiding ( _∘_ ; Arrow )
+  open Category using (Object ; 𝟙)
   open Functor
 
   module _ (F G : Functor ℂ 𝔻) where
@@ -69,7 +70,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     where
       module F = Functor F
       F→ = F.func→
-      module 𝔻 = IsCategory (isCategory 𝔻)
+      module 𝔻 = Category 𝔻
 
   identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
   identityNat F = identityTrans F , identityNatural F
@@ -94,13 +95,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
       𝔻 [ H.func→ f ∘ (θ ∘nt η) A ]     ∎
       where
-        open IsCategory (isCategory 𝔻)
+        open Category 𝔻
 
     NatComp = _:⊕:_
 
   private
     module _ {F G : Functor ℂ 𝔻} where
-      module 𝔻 = IsCategory (isCategory 𝔻)
+      module 𝔻 = Category 𝔻
 
       transformationIsSet : isSet (Transformation F G)
       transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C)   (λ l → q l C) i j
@@ -125,18 +126,37 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
         θ = proj₁ θ'
         η = proj₁ η'
         ζ = proj₁ ζ'
+        θNat = proj₂ θ'
+        ηNat = proj₂ η'
+        ζNat = proj₂ ζ'
+        L : NaturalTransformation A D
+        L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
+        R : NaturalTransformation A D
+        R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
       _g⊕f_ = _:⊕:_ {A} {B} {C}
       _h⊕g_ = _:⊕:_ {B} {C} {D}
-      :assoc: : (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ')) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
+      :assoc: : L ≡ R
-      :assoc: = Σ≡ (funExt (λ _ → assoc)) {!!}
+      :assoc: = lemSig (naturalIsProp {F = A} {D})
+        L R (funExt (λ x → assoc))
         where
-          open IsCategory (isCategory 𝔻)
+          open Category 𝔻
 
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
+      private
+        allNatural = naturalIsProp {F = A} {B}
+        f' = proj₁ f
+        module 𝔻Data = Category 𝔻
+        eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
+        eq-r C = begin
+          𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
+          𝔻 [ f' C ∘ 𝔻Data.𝟙 ]  ≡⟨ proj₁ (𝔻.ident {A} {B}) ⟩
+          f' C ∎
+        eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
+        eq-l C = proj₂ (𝔻.ident {A} {B})
       ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
-      ident-r = {!!}
+      ident-r = lemSig allNatural _ _ (funExt eq-r)
       ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
-      ident-l = {!!}
+      ident-l = lemSig allNatural _ _ (funExt eq-l)
       :ident:
         : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
         × (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
@@ -161,7 +181,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       }
 
   Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-  raw Fun = RawFun
+  Category.raw Fun = RawFun
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   open import Cat.Categories.Sets

src/Cat/Categories/Sets.agda

@@ -9,80 +9,113 @@ 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._∘′_
+
+    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)
+    open Category 𝓢
-      _&&&_ x = f x , g x
+    open import Cubical.Sigma
-    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
 
-    product : (A B : Object Sets) → Product {ℂ = Sets} A B
+    module _ (0A 0B : Object) where
-    product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }
+      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
+module _ {ℓa ℓb : Level} where
-Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
+  module _ (ℂ : Category ℓa ℓb) where
-Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
+    -- Covariant Presheaf
+    Representable : Set (ℓa ⊔ lsuc ℓb)
+    Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
 
--- The "co-yoneda" embedding.
+    -- Contravariant Presheaf
-representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
+    Presheaf : Set (ℓa ⊔ lsuc ℓb)
-representable {ℂ = ℂ} A = record
+    Presheaf = Functor (Opposite ℂ) (𝓢𝓮𝓽 ℓb)
-  { raw = record
-    { func* = λ B → ℂ [ A , B ]
-    ; func→ = ℂ [_∘_]
-    }
-  ; isFunctor = record
-    { ident = funExt λ _ → proj₂ ident
-    ; distrib = funExt λ x → sym assoc
-    }
-  }
-  where
-    open IsCategory (isCategory ℂ)
 
--- Contravariant Presheaf
+  -- The "co-yoneda" embedding.
-Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
+  representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
-Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
+  representable {ℂ = ℂ} A = record
-
+    { raw = record
--- Alternate name: `yoneda`
+      { func* = λ B → ℂ [ A , B ] , arrowIsSet
-presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
+      ; func→ = ℂ [_∘_]
-presheaf {ℂ = ℂ} B = record
+      }
-  { raw = record
+    ; isFunctor = record
-    { func* = λ A → ℂ [ A , B ]
+      { ident = funExt λ _ → proj₂ ident
-    ; func→ = λ f g → ℂ [ g ∘ f ]
+      ; distrib = funExt λ x → sym assoc
-  }
+      }
-  ; isFunctor = record
-    { ident = funExt λ x → proj₁ ident
-    ; distrib = funExt λ x → assoc
     }
-  }
+    where
-  where
+      open Category ℂ
-    open IsCategory (isCategory ℂ)
+
+  -- 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 ℂ

src/Cat/Category.agda

@@ -14,6 +14,8 @@ import Function
 open import Cubical
 open import Cubical.NType.Properties using ( propIsEquiv )
 
+open import Cat.Wishlist
+
 ∃! : ∀ {a b} {A : Set a}
   → (A → Set b) → Set (a ⊔ b)
 ∃! = ∃!≈ _≡_
@@ -23,64 +25,39 @@ open import Cubical.NType.Properties using ( propIsEquiv )
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
--- This follows from [HoTT-book: §7.1.10]
+record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
--- Andrea says the proof is in `cubical` but I can't find it.
-postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A)
-
-record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
-  -- adding no-eta-equality can speed up type-checking.
-  -- ONLY IF you define your categories with copatterns though.
   no-eta-equality
   field
-    -- Need something like:
+    Object : Set ℓa
-    -- Object : Σ (Set ℓ) isGroupoid
+    Arrow  : Object → Object → Set ℓb
-    Object : Set ℓ
+    𝟙      : {A : Object} → Arrow A A
-    -- And:
-    -- Arrow  : Object → Object → Σ (Set ℓ') isSet
-    Arrow  : Object → Object → Set ℓ'
-    𝟙      : {o : Object} → Arrow o o
     _∘_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
+
   infixl 10 _∘_
+
   domain : { a b : Object } → Arrow a b → Object
   domain {a = a} _ = a
+
   codomain : { a b : Object } → Arrow a b → Object
   codomain {b = b} _ = b
 
--- Thierry: All projections must be `isProp`'s
+  IsAssociative : Set (ℓa ⊔ ℓb)
+  IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D}
+    → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
 
--- According to definitions 9.1.1 and 9.1.6 in the HoTT book the
+  IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb)
--- arrows of a category form a set (arrow-is-set), and there is an
+  IsIdentity id = {A B : Object} {f : Arrow A B}
--- equivalence between the equality of objects and isomorphisms
+    → f ∘ id ≡ f × id ∘ f ≡ f
--- (univalent).
+
-record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
+  IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
-  open RawCategory ℂ
+  IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
-  module Raw = RawCategory ℂ
-  field
-    assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
-      → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
-    ident : {A B : Object} {f : Arrow A B}
-      → f ∘ 𝟙 ≡ f × 𝟙 ∘ f ≡ f
-    arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
 
   Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
-  Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
+  Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
 
   _≅_ : (A B : Object) → Set ℓb
   _≅_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
 
-  idIso : (A : Object) → A ≅ A
-  idIso A = 𝟙 , (𝟙 , ident)
-
-  id-to-iso : (A B : Object) → A ≡ B → A ≅ B
-  id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A)
-
-  -- TODO: might want to implement isEquiv differently, there are 3
-  -- equivalent formulations in the book.
-  Univalent : Set (ℓa ⊔ ℓb)
-  Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
-  field
-    univalent : Univalent
-
   module _ {A B : Object} where
     Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb
     Epimorphism {X} f = ( g₀ g₁ : Arrow B X ) → g₀ ∘ f ≡ g₁ ∘ f → g₀ ≡ g₁
@@ -88,69 +65,137 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb
     Monomorphism {X} f = ( g₀ g₁ : Arrow X A ) → f ∘ g₀ ≡ f ∘ g₁ → g₀ ≡ g₁
 
-module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
+  IsInitial  : Object → Set (ℓa ⊔ ℓb)
-  -- TODO, provable by using  arrow-is-set and that isProp (isEquiv _ _ _)
+  IsInitial  I = {X : Object} → isContr (Arrow I X)
-  -- This lemma will be useful to prove the equality of two categories.
-  IsCategory-is-prop : isProp (IsCategory ℂ)
-  IsCategory-is-prop x y i = record
-    -- Why choose `x`'s `arrowIsSet`?
-    { assoc = x.arrowIsSet _ _ x.assoc y.assoc i
-    ; ident =
-      ( x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
-      , x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
-      )
-    ; arrowIsSet = isSetIsProp x.arrowIsSet y.arrowIsSet i
-    ; univalent = {!!}
-    }
-    where
-      module x = IsCategory x
-      module y = IsCategory y
-      xuni : x.Univalent
-      xuni = x.univalent
-      yuni : y.Univalent
-      yuni = y.univalent
-      open RawCategory ℂ
-      T :  I → Set (ℓa ⊔ ℓb)
-      T i = {A B : Object} →
-        isEquiv (A ≡ B) (A x.≅ B)
-          (λ A≡B →
-            transp
-            (λ j →
-            Σ-syntax (Arrow A (A≡B j))
-            (λ f → Σ-syntax (Arrow (A≡B j) A) (λ g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙)))
-            ( 𝟙
-            , 𝟙
-            , x.arrowIsSet _ _ (fst x.ident) (fst y.ident) i
-            , x.arrowIsSet _ _ (snd x.ident) (snd y.ident) i
-            )
-          )
-      eqUni : T [ xuni ≡ yuni ]
-      eqUni = {!!}
 
+  IsTerminal : Object → Set (ℓa ⊔ ℓb)
+  IsTerminal T = {X : Object} → isContr (Arrow X T)
+
+  Initial  : Set (ℓa ⊔ ℓb)
+  Initial  = Σ Object IsInitial
+
+  Terminal : Set (ℓa ⊔ ℓb)
+  Terminal = Σ Object IsTerminal
+
+-- Univalence is indexed by a raw category as well as an identity proof.
+module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
+  open RawCategory ℂ
+  module _ (ident : IsIdentity 𝟙) 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)
+
+    -- TODO: might want to implement isEquiv
+    -- differently, there are 3
+    -- equivalent formulations in the book.
+    Univalent : Set (ℓa ⊔ ℓb)
+    Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
+
+record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
+  open RawCategory ℂ
+  open Univalence ℂ public
+  field
+    assoc : IsAssociative
+    ident : IsIdentity 𝟙
+    arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
+    univalent : Univalent ident
+
+-- `IsCategory` is a mere proposition.
+module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
+  open RawCategory C
+  module _ (ℂ : IsCategory C) where
+    open IsCategory ℂ
+    open import Cubical.NType
+    open import Cubical.NType.Properties
+
+    propIsAssociative : isProp IsAssociative
+    propIsAssociative x y i = arrowIsSet _ _ x y i
+
+    propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
+    propIsIdentity a b i
+      = arrowIsSet _ _ (fst a) (fst b) i
+      , arrowIsSet _ _ (snd a) (snd b) i
+
+    propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
+    propArrowIsSet a b i = isSetIsProp a b i
+
+    propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
+    propIsInverseOf x y = λ i →
+      let
+        h : fst x ≡ fst y
+        h = arrowIsSet _ _ (fst x) (fst y)
+        hh : snd x ≡ snd y
+        hh = arrowIsSet _ _ (snd x) (snd y)
+      in h i , hh i
+
+    module _ {A B : Object} {f : Arrow A B} where
+      isoIsProp : isProp (Isomorphism f)
+      isoIsProp a@(g , η , ε) a'@(g' , η' , ε') =
+        lemSig (λ g → propIsInverseOf) a a' geq
+          where
+            open Cubical.NType.Properties
+            geq : g ≡ g'
+            geq = begin
+              g            ≡⟨ sym (fst ident) ⟩
+              g ∘ 𝟙        ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
+              g ∘ (f ∘ g') ≡⟨ assoc ⟩
+              (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
+              𝟙 ∘ g'       ≡⟨ snd ident ⟩
+              g'           ∎
+
+    propUnivalent : isProp (Univalent ident)
+    propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
+
+  private
+    module _ (x y : IsCategory C) where
+      module IC = IsCategory
+      module X = IsCategory x
+      module Y = IsCategory y
+      open Univalence C
+      -- In a few places I use the result of propositionality of the various
+      -- projections of `IsCategory` - I've arbitrarily chosed to use this
+      -- result from `x : IsCategory C`. I don't know which (if any) possibly
+      -- adverse effects this may have.
+      ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
+      ident = propIsIdentity x X.ident Y.ident
+      done : x ≡ y
+      U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univalent a) → Set _
+      U eqwal bbb = (λ i → Univalent (eqwal i)) [ X.univalent ≡ bbb ]
+      P : (y : IsIdentity 𝟙)
+        → (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _
+      P y eq = ∀ (b' : Univalent y) → U eq b'
+      helper : ∀ (b' : Univalent X.ident)
+        → (λ _ → Univalent X.ident) [ X.univalent ≡ b' ]
+      helper univ = propUnivalent x X.univalent univ
+      foo = pathJ P helper Y.ident ident
+      eqUni : U ident Y.univalent
+      eqUni = foo Y.univalent
+      IC.assoc      (done i) = propIsAssociative x X.assoc Y.assoc i
+      IC.ident      (done i) = ident i
+      IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i
+      IC.univalent  (done i) = eqUni i
+
+  propIsCategory : isProp (IsCategory C)
+  propIsCategory = done
 
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   field
     raw : RawCategory ℓa ℓb
     {{isCategory}} : IsCategory raw
 
-  private
+  open RawCategory raw public
-    module ℂ = RawCategory raw
+  open IsCategory isCategory public
-
-  Object : Set ℓa
-  Object = ℂ.Object
-
-  Arrow = ℂ.Arrow
-
-  𝟙 = ℂ.𝟙
-
-  _∘_ = ℂ._∘_
 
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  open Category ℂ
   _[_,_] : (A : Object) → (B : Object) → Set ℓb
-  _[_,_] = ℂ.Arrow
+  _[_,_] = Arrow
-
-  _[_∘_] : {A B C : Object} → (g : ℂ.Arrow B C) → (f : ℂ.Arrow A B) → ℂ.Arrow A C
-  _[_∘_] = ℂ._∘_
 
+  _[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
+  _[_∘_] = _∘_
 
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private
@@ -162,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
@@ -199,20 +242,3 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
   Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ
   raw (Opposite-is-involution i) = rawOp i
   isCategory (Opposite-is-involution i) = rawIsCat i
-
-module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-  open Category
-  unique = isContr
-
-  IsInitial : Object ℂ → Set (ℓa ⊔ ℓb)
-  IsInitial I = {X : Object ℂ} → unique (ℂ [ I , X ])
-
-  IsTerminal : Object ℂ → Set (ℓa ⊔ ℓb)
-  -- ∃![ ? ] ?
-  IsTerminal T = {X : Object ℂ} → unique (ℂ [ X , T ])
-
-  Initial : Set (ℓa ⊔ ℓb)
-  Initial = Σ (Object ℂ) IsInitial
-
-  Terminal : Set (ℓa ⊔ ℓb)
-  Terminal = Σ (Object ℂ) IsTerminal

src/Cat/Category/Functor.agda

@@ -47,7 +47,6 @@ module _ {ℓc ℓc' ℓd ℓd'}
 open IsFunctor
 open Functor
 
--- TODO: Is `IsFunctor` a proposition?
 module _
     {ℓa ℓb : Level}
     {ℂ 𝔻 : Category ℓa ℓb}
@@ -56,11 +55,8 @@ module _
   private
     module 𝔻 = IsCategory (isCategory 𝔻)
 
-  -- isProp  : Set ℓ
+  propIsFunctor : isProp (IsFunctor _ _ F)
-  -- isProp  = (x y : A) → x ≡ y
+  propIsFunctor isF0 isF1 i = record
-
-  IsFunctorIsProp : isProp (IsFunctor _ _ F)
-  IsFunctorIsProp isF0 isF1 i = record
     { ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i
     ; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
     }
@@ -81,7 +77,7 @@ module _
 
   IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
   IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
-    (\ F → IsFunctorIsProp {F = F}) (\ i → F i)
+    (\ F → propIsFunctor {F = F}) (\ i → F i)
     where
       open import Cubical.NType.Properties using (lemPropF)
 

src/Cat/Category/Properties.agda

@@ -14,7 +14,6 @@ open Equality.Data.Product
 
 module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
   open Category ℂ
-  open IsCategory (isCategory)
 
   iso-is-epi : Isomorphism f → Epimorphism {X = X} f
   iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin

src/Cat/Wishlist.agda

@@ -1,6 +1,15 @@
 module Cat.Wishlist where
 
+open import Level
 open import Cubical.NType
 open import Data.Nat using (_≤_ ; z≤n ; s≤s)
 
 postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
+
+module _ {ℓ : Level} {A : Set ℓ} where
+  -- This is §7.1.10 in [HoTT]. Andrea says the proof is in `cubical` but I
+  -- can't find it.
+  postulate propHasLevel : ∀ n → isProp (HasLevel n A)
+
+  isSetIsProp : isProp (isSet A)
+  isSetIsProp = propHasLevel (S (S ⟨-2⟩))