From d01514cbdbdd3204bd3a61e7367e647e0a49f08f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 8 Mar 2018 11:29:16 +0100 Subject: [PATCH] Do not use ugly ':'-syntax to disambiguate fields --- src/Cat/Categories/Cat.agda | 91 +++++++++++++++++-------------------- 1 file changed, 41 insertions(+), 50 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index e1c6d75..71901ca 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -5,7 +5,6 @@ module Cat.Categories.Cat where open import Agda.Primitive open import Cubical -open import Function open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) open import Cat.Category @@ -62,44 +61,44 @@ module _ (ℓ ℓ' : Level) where -- category. In some places it may not actually be needed, however. module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where private - :Object: = Object ℂ × Object 𝔻 - :Arrow: : :Object: → :Object: → Set ℓ' - :Arrow: (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] - :𝟙: : {o : :Object:} → :Arrow: o o - :𝟙: = 𝟙 ℂ , 𝟙 𝔻 - _:⊕:_ : - {a b c : :Object:} → - :Arrow: b c → - :Arrow: a b → - :Arrow: a c - _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} + Obj = Object ℂ × Object 𝔻 + Arr : Obj → Obj → Set ℓ' + Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] + 𝟙' : {o : Obj} → Arr o o + 𝟙' = 𝟙 ℂ , 𝟙 𝔻 + _∘_ : + {a b c : Obj} → + Arr b c → + Arr a b → + Arr a c + _∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} - :rawProduct: : RawCategory ℓ ℓ' - RawCategory.Object :rawProduct: = :Object: - RawCategory.Arrow :rawProduct: = :Arrow: - RawCategory.𝟙 :rawProduct: = :𝟙: - RawCategory._∘_ :rawProduct: = _:⊕:_ - open RawCategory :rawProduct: + rawProduct : RawCategory ℓ ℓ' + RawCategory.Object rawProduct = Obj + RawCategory.Arrow rawProduct = Arr + RawCategory.𝟙 rawProduct = 𝟙' + RawCategory._∘_ rawProduct = _∘_ + open RawCategory rawProduct module ℂ = Category ℂ module 𝔻 = Category 𝔻 open import Cubical.Sigma - arrowsAreSets : ArrowsAreSets -- {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B) + arrowsAreSets : ArrowsAreSets arrowsAreSets = setSig {sA = ℂ.arrowsAreSets} {sB = λ x → 𝔻.arrowsAreSets} - isIdentity : IsIdentity :𝟙: + isIdentity : IsIdentity 𝟙' isIdentity = Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity) , Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity) - postulate univalent : Univalence.Univalent :rawProduct: isIdentity + postulate univalent : Univalence.Univalent rawProduct isIdentity instance - :isCategory: : IsCategory :rawProduct: - IsCategory.isAssociative :isCategory: = Σ≡ ℂ.isAssociative 𝔻.isAssociative - IsCategory.isIdentity :isCategory: = isIdentity - IsCategory.arrowsAreSets :isCategory: = arrowsAreSets - IsCategory.univalent :isCategory: = univalent + isCategory : IsCategory rawProduct + IsCategory.isAssociative isCategory = Σ≡ ℂ.isAssociative 𝔻.isAssociative + IsCategory.isIdentity isCategory = isIdentity + IsCategory.arrowsAreSets isCategory = arrowsAreSets + IsCategory.univalent isCategory = univalent obj : Category ℓ ℓ' - Category.raw obj = :rawProduct: + Category.raw obj = rawProduct proj₁ : Functor obj ℂ proj₁ = record @@ -177,8 +176,8 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where Categoryℓ = Category ℓ ℓ open Fun ℂ 𝔻 renaming (identity to idN) private - :omap: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻 - :omap: (F , A) = F.omap A + omap : Functor ℂ 𝔻 × Object ℂ → Object 𝔻 + omap (F , A) = F.omap A where module F = Functor F @@ -200,9 +199,9 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where module F = Functor F module G = Functor G - :fmap: : (pobj : NaturalTransformation F G × ℂ [ A , B ]) + fmap : (pobj : NaturalTransformation F G × ℂ [ A , B ]) → 𝔻 [ F.omap A , G.omap B ] - :fmap: ((θ , θNat) , f) = result + fmap ((θ , θNat) , f) = result where θA : 𝔻 [ F.omap A , G.omap A ] θA = θ A @@ -233,23 +232,16 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where C : Object ℂ C = proj₂ c - -- NaturalTransformation F G × ℂ .Arrow A B - -- :ident: : :fmap: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙 - -- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity) - -- where - -- open module 𝔻 = IsCategory (𝔻 .isCategory) - -- Unfortunately the equational version has some ambigous arguments. - - :ident: : :fmap: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 - :ident: = begin - :fmap: {c} {c} (𝟙 (prodObj ×p ℂ) {c}) ≡⟨⟩ - :fmap: {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩ + ident : fmap {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 + ident = begin + fmap {c} {c} (𝟙 (prodObj ×p ℂ) {c}) ≡⟨⟩ + fmap {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩ 𝔻 [ identityTrans F C ∘ F.fmap (𝟙 ℂ)] ≡⟨⟩ 𝔻 [ 𝟙 𝔻 ∘ F.fmap (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩ F.fmap (𝟙 ℂ) ≡⟨ F.isIdentity ⟩ 𝟙 𝔻 ∎ where - open module F = Functor F + module F = Functor F module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where private @@ -289,10 +281,10 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where ηθ = proj₁ ηθNT ηθNat = proj₂ ηθNT - :isDistributive: : + isDistributive : 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F.fmap ( ℂ [ g ∘ f ] ) ] ≡ 𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ 𝔻 [ θ B ∘ F.fmap f ] ] - :isDistributive: = begin + isDistributive = begin 𝔻 [ (ηθ C) ∘ F.fmap (ℂ [ g ∘ f ]) ] ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ 𝔻 [ H.fmap (ℂ [ g ∘ f ]) ∘ (ηθ A) ] @@ -314,15 +306,14 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where 𝔻 [ 𝔻 [ η C ∘ G.fmap g ] ∘ 𝔻 [ θ B ∘ F.fmap f ] ] ∎ eval : Functor (CatProduct.obj prodObj ℂ) 𝔻 - -- :eval: : Functor (prodObj ×p ℂ) 𝔻 eval = record { raw = record - { omap = :omap: - ; fmap = λ {dom} {cod} → :fmap: {dom} {cod} + { omap = omap + ; fmap = λ {dom} {cod} → fmap {dom} {cod} } ; isFunctor = record - { isIdentity = λ {o} → :ident: {o} - ; isDistributive = λ {f u n k y} → :isDistributive: {f} {u} {n} {k} {y} + { isIdentity = λ {o} → ident {o} + ; isDistributive = λ {f u n k y} → isDistributive {f} {u} {n} {k} {y} } }