From 8022ed349d8c4259cb52700d68091216d41b340f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 5 Feb 2018 12:21:39 +0100 Subject: [PATCH] "re-delegate" projections in new module `Category` --- src/Cat/Categories/Fun.agda | 12 +++--- src/Cat/Categories/Sets.agda | 12 +++--- src/Cat/Category.agda | 69 ++++++++++++++++++-------------- src/Cat/Category/Free.agda | 12 +++--- src/Cat/Category/Properties.agda | 2 +- src/Cat/CwF.agda | 14 +++---- src/Cat/Functor.agda | 26 ++++++------ 7 files changed, 77 insertions(+), 70 deletions(-) diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 3778cdb..6719ac6 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -16,11 +16,11 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat module _ (F G : Functor ℂ 𝔻) where -- What do you call a non-natural tranformation? Transformation : Set (ℓc ⊔ ℓd') - Transformation = (C : ℂ .Object) → 𝔻 [ F .func* C , G .func* C ] + Transformation = (C : Object ℂ) → 𝔻 [ F .func* C , G .func* C ] Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd')) Natural θ - = {A B : ℂ .Object} + = {A B : Object ℂ} → (f : ℂ [ A , B ]) → 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ] @@ -34,7 +34,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat NaturalTransformation≡ : {α β : NaturalTransformation F G} → (eq₁ : α .proj₁ ≡ β .proj₁) → (eq₂ : PathP - (λ i → {A B : ℂ .Object} (f : ℂ [ A , B ]) + (λ i → {A B : Object ℂ} (f : ℂ [ A , B ]) → 𝔻 [ eq₁ i B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ eq₁ i A ]) (α .proj₂) (β .proj₂)) @@ -42,14 +42,14 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i identityTrans : (F : Functor ℂ 𝔻) → Transformation F F - identityTrans F C = 𝔻 .𝟙 + identityTrans F C = 𝟙 𝔻 identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F) identityNatural F {A = A} {B = B} f = begin 𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩ - 𝔻 [ 𝔻 .𝟙 ∘ F→ f ] ≡⟨ proj₂ 𝔻.ident ⟩ + 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.ident ⟩ F→ f ≡⟨ sym (proj₁ 𝔻.ident) ⟩ - 𝔻 [ F→ f ∘ 𝔻 .𝟙 ] ≡⟨⟩ + 𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩ 𝔻 [ F→ f ∘ identityTrans F A ] ∎ where F→ = F .func→ diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index e9c93bd..259ec44 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -39,10 +39,10 @@ module _ {ℓ : Level} where proj₁ lem = refl proj₂ lem = refl instance - isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} proj₁ proj₂ + isProduct : {A B : Object Sets} → IsProduct Sets {A} {B} proj₁ proj₂ isProduct f g = f &&& g , lem f g - product : (A B : Sets .Object) → Product {ℂ = Sets} A B + product : (A B : Object Sets) → Product {ℂ = Sets} A B product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct } instance @@ -56,8 +56,8 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'}) -- The "co-yoneda" embedding. representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ representable {ℂ = ℂ} A = record - { func* = λ B → ℂ .Arrow A B - ; func→ = ℂ ._∘_ + { func* = λ B → ℂ [ A , B ] + ; func→ = ℂ [_∘_] ; isFunctor = record { ident = funExt λ _ → proj₂ ident ; distrib = funExt λ x → sym assoc @@ -73,8 +73,8 @@ Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'}) -- Alternate name: `yoneda` presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ presheaf {ℂ = ℂ} B = record - { func* = λ A → ℂ .Arrow A B - ; func→ = λ f g → ℂ ._∘_ g f + { func* = λ A → ℂ [ A , B ] + ; func→ = λ f g → ℂ [ g ∘ f ] ; isFunctor = record { ident = funExt λ x → proj₁ ident ; distrib = funExt λ x → assoc diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 4154dce..bdb632c 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -114,27 +114,34 @@ Category ℓa ℓb = Σ (RawCategory ℓa ℓb) IsCategory module Category {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where raw = fst ℂ - open RawCategory raw public isCategory = snd ℂ -open RawCategory + private + module ℂ = RawCategory raw --- _∈_ : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → (ℂ .fst .Object → Set ℓb) → Set (ℓa ⊔ ℓb) --- A ∈ ℂ = + Object : Set ℓa + Object = ℂ.Object -Obj : ∀ {ℓa ℓb} → Category ℓa ℓb → Set ℓa -Obj ℂ = ℂ .fst .Object + Arrow = ℂ.Arrow -_[_,_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → (A : Obj ℂ) → (B : Obj ℂ) → Set ℓ' -ℂ [ A , B ] = ℂ .fst .Arrow A B + 𝟙 = ℂ.𝟙 -_[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : Obj ℂ} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ] -ℂ [ g ∘ f ] = ℂ .fst ._∘_ g f + _∘_ = ℂ._∘_ -module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Obj ℂ} where + _[_,_] : (A : Object) → (B : Object) → Set ℓb + _[_,_] = ℂ.Arrow + + _[_∘_] : {A B C : Object} → (g : ℂ.Arrow B C) → (f : ℂ.Arrow A B) → ℂ.Arrow A C + _[_∘_] = ℂ._∘_ + +open Category using ( Object ; _[_,_] ; _[_∘_]) + +-- open RawCategory + +module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where IsProduct : (π₁ : ℂ [ obj , A ]) (π₂ : ℂ [ obj , B ]) → Set (ℓ ⊔ ℓ') IsProduct π₁ π₂ - = ∀ {X : Obj ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ]) + = ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ]) → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ × ℂ [ π₂ ∘ x ] ≡ x₂) -- Tip from Andrea; Consider this style for efficiency: @@ -144,10 +151,10 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Obj ℂ} where -- isProduct : ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B) -- → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ. _⊕_ π₂ x ≡ x₂) -record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Obj ℂ) : Set (ℓ ⊔ ℓ') where +record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) : Set (ℓ ⊔ ℓ') where no-eta-equality field - obj : Obj ℂ + obj : Object ℂ proj₁ : ℂ [ obj , A ] proj₂ : ℂ [ obj , B ] {{isProduct}} : IsProduct ℂ proj₁ proj₂ @@ -158,15 +165,15 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Obj ℂ) : Se record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where field - product : ∀ (A B : Obj ℂ) → Product {ℂ = ℂ} A B + product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B open Product - objectProduct : (A B : Obj ℂ) → Obj ℂ + objectProduct : (A B : Object ℂ) → Object ℂ objectProduct A B = Product.obj (product A B) -- The product mentioned in awodey in Def 6.1 is not the regular product of arrows. -- It's a "parallel" product - parallelProduct : {A A' B B' : Obj ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ] + parallelProduct : {A A' B B' : Object ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ objectProduct A B , objectProduct A' B' ] parallelProduct {A = A} {A' = A'} {B = B} {B' = B'} a b = arrowProduct (product A' B') (ℂ [ a ∘ (product A B) .proj₁ ]) @@ -209,30 +216,30 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} open HasProducts hasProducts open Product hiding (obj) private - _×p_ : (A B : Obj ℂ) → Obj ℂ + _×p_ : (A B : Object ℂ) → Object ℂ _×p_ A B = Product.obj (product A B) - module _ (B C : Obj ℂ) where - IsExponential : (Cᴮ : Obj ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ') - IsExponential Cᴮ eval = ∀ (A : Obj ℂ) (f : ℂ [ A ×p B , C ]) - → ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (Category.raw ℂ .𝟙)] ≡ f) + module _ (B C : Object ℂ) where + IsExponential : (Cᴮ : Object ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ') + IsExponential Cᴮ eval = ∀ (A : Object ℂ) (f : ℂ [ A ×p B , C ]) + → ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (Category.𝟙 ℂ)] ≡ f) record Exponential : Set (ℓ ⊔ ℓ') where field -- obj ≡ Cᴮ - obj : Obj ℂ + obj : Object ℂ eval : ℂ [ obj ×p B , C ] {{isExponential}} : IsExponential obj eval -- If I make this an instance-argument then the instance resolution -- algorithm goes into an infinite loop. Why? exponentialsHaveProducts : HasProducts ℂ exponentialsHaveProducts = hasProducts - transpose : (A : Obj ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ] + transpose : (A : Object ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ] transpose A f = fst (isExponential A f) record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where field - exponent : (A B : Obj ℂ) → Exponential ℂ A B + exponent : (A B : Object ℂ) → Exponential ℂ A B record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where field @@ -242,15 +249,15 @@ record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where unique = isContr - IsInitial : Obj ℂ → Set (ℓa ⊔ ℓb) - IsInitial I = {X : Obj ℂ} → unique (ℂ [ I , X ]) + IsInitial : Object ℂ → Set (ℓa ⊔ ℓb) + IsInitial I = {X : Object ℂ} → unique (ℂ [ I , X ]) - IsTerminal : Obj ℂ → Set (ℓa ⊔ ℓb) + IsTerminal : Object ℂ → Set (ℓa ⊔ ℓb) -- ∃![ ? ] ? - IsTerminal T = {X : Obj ℂ} → unique (ℂ [ X , T ]) + IsTerminal T = {X : Object ℂ} → unique (ℂ [ X , T ]) Initial : Set (ℓa ⊔ ℓb) - Initial = Σ (Obj ℂ) IsInitial + Initial = Σ (Object ℂ) IsInitial Terminal : Set (ℓa ⊔ ℓb) - Terminal = Σ (Obj ℂ) IsTerminal + Terminal = Σ (Object ℂ) IsTerminal diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda index 1225aa3..c8732d1 100644 --- a/src/Cat/Category/Free.agda +++ b/src/Cat/Category/Free.agda @@ -12,23 +12,23 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where open module ℂ = Category ℂ postulate - Path : ( a b : Obj ℂ ) → Set ℓ' - emptyPath : (o : Obj ℂ) → Path o o - concatenate : {a b c : Obj ℂ} → Path b c → Path a b → Path a c + Path : (a b : ℂ.Object) → Set ℓ' + emptyPath : (o : ℂ.Object) → Path o o + concatenate : {a b c : ℂ.Object} → Path b c → Path a b → Path a c private - module _ {A B C D : Obj ℂ} {r : Path A B} {q : Path B C} {p : Path C D} where + module _ {A B C D : ℂ.Object} {r : Path A B} {q : Path B C} {p : Path C D} where postulate p-assoc : concatenate {A} {C} {D} p (concatenate {A} {B} {C} q r) ≡ concatenate {A} {B} {D} (concatenate {B} {C} {D} p q) r - module _ {A B : Obj ℂ} {p : Path A B} where + module _ {A B : ℂ.Object} {p : Path A B} where postulate ident-r : concatenate {A} {A} {B} p (emptyPath A) ≡ p ident-l : concatenate {A} {B} {B} (emptyPath B) p ≡ p RawFree : RawCategory ℓ ℓ' RawFree = record - { Object = Obj ℂ + { Object = ℂ.Object ; Arrow = Path ; 𝟙 = λ {o} → emptyPath o ; _∘_ = λ {a b c} → concatenate {a} {b} {c} diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 20631e4..2477447 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -12,7 +12,7 @@ open import Cat.Categories.Sets open import Cat.Equality open Equality.Data.Product -module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Object } {X : ℂ .Category.Object} (f : ℂ .Category.Arrow A B) where +module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where open Category ℂ open IsCategory (isCategory) diff --git a/src/Cat/CwF.agda b/src/Cat/CwF.agda index 9313885..c3099ca 100644 --- a/src/Cat/CwF.agda +++ b/src/Cat/CwF.agda @@ -17,20 +17,20 @@ module _ {ℓa ℓb : Level} where -- "A base category" ℂ : Category ℓa ℓb -- It's objects are called contexts - Contexts = ℂ .Object + Contexts = Object ℂ -- It's arrows are called substitutions - Substitutions = ℂ .Arrow + Substitutions = Arrow ℂ field -- A functor T T : Functor (Opposite ℂ) (Fam ℓa ℓb) -- Empty context [] : Terminal ℂ - Type : (Γ : ℂ .Object) → Set ℓa + Type : (Γ : Object ℂ) → Set ℓa Type Γ = proj₁ (T .func* Γ) - module _ {Γ : ℂ .Object} {A : Type Γ} where + module _ {Γ : Object ℂ} {A : Type Γ} where - module _ {A B : ℂ .Object} {γ : ℂ [ A , B ]} where + module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where k : Σ (proj₁ (func* T B) → proj₁ (func* T A)) (λ f → {x : proj₁ (func* T B)} → @@ -44,8 +44,8 @@ module _ {ℓa ℓb : Level} where record ContextComprehension : Set (ℓa ⊔ ℓb) where field - Γ&A : ℂ .Object - proj1 : ℂ .Arrow Γ&A Γ + Γ&A : Object ℂ + proj1 : ℂ [ Γ&A , Γ ] -- proj2 : ???? -- if γ : ℂ [ A , B ] diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda index e88238d..890801b 100644 --- a/src/Cat/Functor.agda +++ b/src/Cat/Functor.agda @@ -10,20 +10,20 @@ open Category hiding (_∘_) module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where record IsFunctor - (func* : Obj ℂ → Obj 𝔻) - (func→ : {A B : Obj ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]) + (func* : Object ℂ → Object 𝔻) + (func→ : {A B : Object ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]) : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where field - ident : {c : Obj ℂ} → func→ (ℂ .𝟙 {c}) ≡ 𝔻 .𝟙 {func* c} + ident : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c} -- TODO: Avoid use of ugly explicit arguments somehow. -- This guy managed to do it: -- https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda - distrib : {A B C : ℂ .Object} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} + distrib : {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ] record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where field - func* : ℂ .Object → 𝔻 .Object + func* : Object ℂ → Object 𝔻 func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ] {{isFunctor}} : IsFunctor func* func→ @@ -33,11 +33,11 @@ open Functor module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where IsFunctor≡ - : {func* : ℂ .Object → 𝔻 .Object} - {func→ : {A B : ℂ .Object} → ℂ .Arrow A B → 𝔻 .Arrow (func* A) (func* B)} + : {func* : Object ℂ → Object 𝔻} + {func→ : {A B : Object ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]} {F G : IsFunctor ℂ 𝔻 func* func→} → (eqI - : (λ i → ∀ {A} → func→ (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {func* A}) + : (λ i → ∀ {A} → func→ (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {func* A}) [ F .ident ≡ G .ident ]) → (eqD : (λ i → ∀ {A B C} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} @@ -61,7 +61,7 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F F→ = F .func→ G* = G .func* G→ = G .func→ - module _ {a0 a1 a2 : A .Object} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where + module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] dist = begin @@ -77,10 +77,10 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F ; func→ = F→ ∘ G→ ; isFunctor = record { ident = begin - (F→ ∘ G→) (A .𝟙) ≡⟨ refl ⟩ - F→ (G→ (A .𝟙)) ≡⟨ cong F→ (G .isFunctor .ident)⟩ - F→ (B .𝟙) ≡⟨ F .isFunctor .ident ⟩ - C .𝟙 ∎ + (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩ + F→ (G→ (𝟙 A)) ≡⟨ cong F→ (G .isFunctor .ident)⟩ + F→ (𝟙 B) ≡⟨ F .isFunctor .ident ⟩ + 𝟙 C ∎ ; distrib = dist } }