From 83ccde62e9ad91ca33f6e55af46dabf9fe614952 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 5 Feb 2018 14:47:15 +0100 Subject: [PATCH] Use co-patterns --- src/Cat/Categories/Cube.agda | 19 +++++---- src/Cat/Categories/Fam.agda | 6 +-- src/Cat/Categories/Fun.agda | 6 +-- src/Cat/Categories/Sets.agda | 27 ++++++------ src/Cat/Category.agda | 83 +++++++++++++++++++++--------------- 5 files changed, 77 insertions(+), 64 deletions(-) diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda index ec1a145..ee0eccc 100644 --- a/src/Cat/Categories/Cube.agda +++ b/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ℂ diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index 9fac2bf..600cabb 100644 --- a/src/Cat/Categories/Fam.agda +++ b/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 diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 6719ac6..c14823a 100644 --- a/src/Cat/Categories/Fun.agda +++ b/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 diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 1bc747d..e9a8b87 100644 --- a/src/Cat/Categories/Sets.agda +++ b/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 diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 036a3e4..5c7eb41 100644 --- a/src/Cat/Category.agda +++ b/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)