Use co-patterns

src/Cat/Categories/Cube.agda

@@ -65,15 +65,16 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
 
     Hom = Σ Hom' rules
 
+  module Raw = RawCategory
   -- The category of names and substitutions
   Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
-  Rawℂ = record
-    { Object = FiniteDecidableSubset
-    -- { Object = Ns → Bool
-    ; Arrow = Hom
-    ; 𝟙 = λ { {o} → inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } }
-    ; _∘_ = {!!}
-    }
-  postulate RawIsCategoryℂ : IsCategory Rawℂ
+  Raw.Object Rawℂ = FiniteDecidableSubset
+  Raw.Arrow Rawℂ = Hom
+  Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
+  Raw._∘_ Rawℂ = {!!}
+
+  postulate IsCategoryℂ : IsCategory Rawℂ
+
   ℂ : Category ℓ ℓ
-  ℂ = Rawℂ , RawIsCategoryℂ
+  raw ℂ = Rawℂ
+  isCategory ℂ = IsCategoryℂ

src/Cat/Categories/Fam.agda

@@ -46,9 +46,9 @@ module _ (ℓa ℓb : Level) where
       isCategory = record
         { assoc = λ {A} {B} {C} {D} {f} {g} {h} → assoc {D = D} {f} {g} {h}
         ; ident = λ {A} {B} {f} → ident {A} {B} {f = f}
-        ; arrow-is-set = ?
-        ; univalent = ?
+        ; arrow-is-set = {!!}
+        ; univalent = {!!}
         }
 
   Fam : Category (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
-  Fam = RawFam , isCategory
+  Category.raw Fam = RawFam

src/Cat/Categories/Fun.agda

@@ -110,12 +110,12 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     :isCategory: = record
       { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
       ; ident = λ {A B} → :ident: {A} {B}
-      ; arrow-is-set = ?
-      ; univalent = ?
+      ; arrow-is-set = {!!}
+      ; univalent = {!!}
       }
 
   Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-  Fun = RawFun , :isCategory:
+  raw Fun = RawFun
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   open import Cat.Categories.Sets

src/Cat/Categories/Sets.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --allow-unsolved-metas --cubical #-}
 module Cat.Categories.Sets where
 
 open import Cubical
@@ -13,23 +13,22 @@ open Category
 
 module _ {ℓ : Level} where
   SetsRaw : RawCategory (lsuc ℓ) ℓ
-  SetsRaw = record
-       { Object = Set ℓ
-       ; Arrow = λ T U → T → U
-       ; 𝟙 = Function.id
-       ; _∘_ = Function._∘′_
-       }
+  RawCategory.Object SetsRaw = Set ℓ
+  RawCategory.Arrow SetsRaw = λ T U → T → U
+  RawCategory.𝟙 SetsRaw = Function.id
+  RawCategory._∘_ SetsRaw = Function._∘′_
 
+  open IsCategory
   SetsIsCategory : IsCategory SetsRaw
-  SetsIsCategory = record
-    { assoc = refl
-    ; ident = funExt (λ _ → refl) , funExt (λ _ → refl)
-    ; arrow-is-set = {!!}
-    ; univalent = {!!}
-    }
+  assoc SetsIsCategory = refl
+  proj₁ (ident SetsIsCategory) = funExt λ _ → refl
+  proj₂ (ident SetsIsCategory) = funExt λ _ → refl
+  arrow-is-set SetsIsCategory = {!!}
+  univalent SetsIsCategory = {!!}
 
   Sets : Category (lsuc ℓ) ℓ
-  Sets = SetsRaw , SetsIsCategory
+  raw Sets = SetsRaw
+  isCategory Sets = SetsIsCategory
 
   private
     module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where

src/Cat/Category.agda

@@ -109,12 +109,10 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where
       module x = IsCategory x
       module y = IsCategory y
 
-Category : (ℓa ℓb : Level) → Set (lsuc (ℓa ⊔ ℓb))
-Category ℓa ℓb = Σ (RawCategory ℓa ℓb) IsCategory
-
-module Category {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-  raw = fst ℂ
-  isCategory = snd ℂ
+record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
+  field
+    raw : RawCategory ℓa ℓb
+    {{isCategory}} : IsCategory raw
 
   private
     module ℂ = RawCategory raw
@@ -134,42 +132,57 @@ module Category {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   _[_∘_] : {A B C : Object} → (g : ℂ.Arrow B C) → (f : ℂ.Arrow A B) → ℂ.Arrow A C
   _[_∘_] = ℂ._∘_
 
-open Category using ( Object ; _[_,_] ; _[_∘_])
 
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private
     open Category ℂ
-    module ℂ = RawCategory (ℂ .fst)
-    OpRaw : RawCategory ℓa ℓb
-    OpRaw = record
-      { Object = ℂ.Object
-      ; Arrow = Function.flip ℂ.Arrow
-      ; 𝟙 = ℂ.𝟙
-      ; _∘_ = Function.flip (ℂ._∘_)
-      }
-    open IsCategory isCategory
-    OpIsCategory : IsCategory OpRaw
-    OpIsCategory = record
-      { assoc = sym assoc
-      ; ident = swap ident
-      ; arrow-is-set = {!!}
-      ; univalent = {!!}
-      }
-  Opposite : Category ℓa ℓb
-  Opposite = OpRaw , OpIsCategory
 
--- A consequence of no-eta-equality; `Opposite-is-involution` is no longer
--- definitional - i.e.; you must match on the fields:
---
--- Opposite-is-involution : ∀ {ℓ ℓ'} → {C : Category {ℓ} {ℓ'}} → Opposite (Opposite C) ≡ C
--- Object (Opposite-is-involution {C = C} i) = Object C
--- Arrow (Opposite-is-involution i) = {!!}
--- 𝟙 (Opposite-is-involution i) = {!!}
--- _⊕_ (Opposite-is-involution i) = {!!}
--- assoc (Opposite-is-involution i) = {!!}
--- ident (Opposite-is-involution i) = {!!}
+    OpRaw : RawCategory ℓa ℓb
+    RawCategory.Object OpRaw = Object
+    RawCategory.Arrow OpRaw = Function.flip Arrow
+    RawCategory.𝟙 OpRaw = 𝟙
+    RawCategory._∘_ OpRaw = Function.flip _∘_
+
+    open IsCategory isCategory
+
+    OpIsCategory : IsCategory OpRaw
+    IsCategory.assoc OpIsCategory = sym assoc
+    IsCategory.ident OpIsCategory = swap ident
+    IsCategory.arrow-is-set OpIsCategory = {!!}
+    IsCategory.univalent OpIsCategory = {!!}
+
+  Opposite : Category ℓa ℓb
+  raw Opposite = OpRaw
+  Category.isCategory Opposite = OpIsCategory
+
+-- As demonstrated here a side-effect of having no-eta-equality on constructors
+-- means that we need to pick things apart to show that things are indeed
+-- definitionally equal. I.e; a thing that would normally be provable in one
+-- line now takes more than 20!!
+module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
+  private
+    open RawCategory
+    module C = Category ℂ
+    rawOp : Category.raw (Opposite (Opposite ℂ)) ≡ Category.raw ℂ
+    Object (rawOp _) = C.Object
+    Arrow (rawOp _) = C.Arrow
+    𝟙 (rawOp _) = C.𝟙
+    _∘_ (rawOp _) = C._∘_
+    open Category
+    open IsCategory
+    module IsCat = IsCategory (ℂ .isCategory)
+    rawIsCat : (i : I) → IsCategory (rawOp i)
+    assoc (rawIsCat i) = IsCat.assoc
+    ident (rawIsCat i) = IsCat.ident
+    arrow-is-set (rawIsCat i) = IsCat.arrow-is-set
+    univalent (rawIsCat i) = IsCat.univalent
+
+  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)