From 255b0236f98ff85e3fd319c4a3036501d091c4db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 30 Jan 2018 19:19:16 +0100 Subject: [PATCH] Use alternative syntax for arrow composition --- src/Cat/Categories/Cat.agda | 79 +++++++++++++++++--------------- src/Cat/Categories/Fun.agda | 53 ++++++++++++--------- src/Cat/Categories/Rel.agda | 2 +- src/Cat/Categories/Sets.agda | 18 ++++---- src/Cat/Category.agda | 30 ++++++------ src/Cat/Category/Free.agda | 2 +- src/Cat/Category/Properties.agda | 42 +++++++++-------- src/Cat/Cubical.agda | 6 +-- src/Cat/Functor.agda | 2 +- 9 files changed, 124 insertions(+), 110 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index b8f91ab..d78e4ca 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -22,7 +22,7 @@ eqpair eqa eqb i = eqa i , eqb i open Functor open IsFunctor -open Category +open Category hiding (_∘_) -- The category of categories module _ (ℓ ℓ' : Level) where @@ -40,7 +40,7 @@ module _ (ℓ ℓ' : Level) where ((h ∘f (g ∘f f)) .isFunctor .ident) (((h ∘f g) ∘f f) .isFunctor .ident) postulate eqD : PathP (λ i → { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''} - → eq→ i (A ._⊕_ a' a) ≡ D ._⊕_ (eq→ i a') (eq→ i a)) + → eq→ i (A [ a' ∘ a ]) ≡ D [ eq→ i a' ∘ eq→ i a ]) ((h ∘f (g ∘f f)) .isFunctor .distrib) (((h ∘f g) ∘f f) .isFunctor .distrib) assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f @@ -64,7 +64,7 @@ module _ (ℓ ℓ' : Level) where eqD-r : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} → - eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f)) + eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ]) ((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib) ident-r : F ∘f identity ≡ F ident-r = Functor≡ eq* eq→ eqI-r eqD-r @@ -78,7 +78,7 @@ module _ (ℓ ℓ' : Level) where eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A}) ((identity ∘f F) .isFunctor .ident) (F .isFunctor .ident) eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} - → eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f)) + → eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ]) ((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib) ident-l : identity ∘f F ≡ F ident-l = Functor≡ eq* eq→ eqI eqD @@ -89,7 +89,7 @@ module _ (ℓ ℓ' : Level) where { Object = Category ℓ ℓ' ; Arrow = Functor ; 𝟙 = identity - ; _⊕_ = _∘f_ + ; _∘_ = _∘f_ -- What gives here? Why can I not name the variables directly? ; isCategory = record { assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h} @@ -112,7 +112,7 @@ module _ {ℓ ℓ' : Level} where :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} + _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} instance :isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_ @@ -131,7 +131,7 @@ module _ {ℓ ℓ' : Level} where { Object = :Object: ; Arrow = :Arrow: ; 𝟙 = :𝟙: - ; _⊕_ = _:⊕:_ + ; _∘_ = _:⊕:_ } proj₁ : Arrow Catt :product: ℂ @@ -161,16 +161,16 @@ module _ {ℓ ℓ' : Level} where -- Need to "lift equality of functors" -- If I want to do this like I do it for pairs it's gonna be a pain. - postulate isUniqL : (Catt ⊕ proj₁) x ≡ x₁ + postulate isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁ -- isUniqL = Functor≡ refl refl {!!} {!!} - postulate isUniqR : (Catt ⊕ proj₂) x ≡ x₂ + postulate isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂ -- isUniqR = Functor≡ refl refl {!!} {!!} - isUniq : (Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂ + isUniq : Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂ isUniq = isUniqL , isUniqR - uniq : ∃![ x ] ((Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂) + uniq : ∃![ x ] (Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂) uniq = x , isUniq instance @@ -199,9 +199,6 @@ module _ (ℓ : Level) where Catℓ = Cat ℓ ℓ module _ (ℂ 𝔻 : Category ℓ ℓ) where private - _𝔻⊕_ = 𝔻 ._⊕_ - _ℂ⊕_ = ℂ ._⊕_ - :obj: : Cat ℓ ℓ .Object :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻} @@ -233,13 +230,13 @@ module _ (ℓ : Level) where G→f : 𝔻 .Arrow (G .func* A) (G .func* B) G→f = G .func→ f l : 𝔻 .Arrow (F .func* A) (G .func* B) - l = θB 𝔻⊕ F→f + l = 𝔻 [ θB ∘ F→f ] r : 𝔻 .Arrow (F .func* A) (G .func* B) - r = G→f 𝔻⊕ θA + r = 𝔻 [ G→f ∘ θA ] -- There are two choices at this point, -- but I suppose the whole point is that -- by `θNat f` we have `l ≡ r` - -- lem : θ B 𝔻⊕ F .func→ f ≡ G .func→ f 𝔻⊕ θ A + -- lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ] -- lem = θNat f result : 𝔻 .Arrow (F .func* A) (G .func* B) result = l @@ -257,17 +254,16 @@ module _ (ℓ : Level) where -- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙 -- :ident: = trans (proj₂ 𝔻.ident) (F .ident) -- where - -- _𝔻⊕_ = 𝔻 ._⊕_ -- open module 𝔻 = IsCategory (𝔻 .isCategory) -- Unfortunately the equational version has some ambigous arguments. :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙 {o = proj₂ c}) ≡ 𝔻 .𝟙 :ident: = begin :func→: {c} {c} ((:obj: ×p ℂ) .Product.obj .𝟙 {c}) ≡⟨⟩ :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡⟨⟩ - (identityTrans F C 𝔻⊕ F .func→ (ℂ .𝟙)) ≡⟨⟩ - 𝔻 .𝟙 𝔻⊕ F .func→ (ℂ .𝟙) ≡⟨ proj₂ 𝔻.ident ⟩ + 𝔻 [ identityTrans F C ∘ F .func→ (ℂ .𝟙)] ≡⟨⟩ + 𝔻 [ 𝔻 .𝟙 ∘ F .func→ (ℂ .𝟙)] ≡⟨ proj₂ 𝔻.ident ⟩ F .func→ (ℂ .𝟙) ≡⟨ F.ident ⟩ - 𝔻 .𝟙 ∎ + 𝔻 .𝟙 ∎ where open module 𝔻 = IsCategory (𝔻 .isCategory) open module F = IsFunctor (F .isFunctor) @@ -280,7 +276,7 @@ module _ (ℓ : Level) where H = H×C .proj₁ C = H×C .proj₂ -- Not entirely clear what this is at this point: - _P⊕_ = (:obj: ×p ℂ) .Product.obj ._⊕_ {F×A} {G×B} {H×C} + _P⊕_ = (:obj: ×p ℂ) .Product.obj .Category._∘_ {F×A} {G×B} {H×C} module _ -- NaturalTransformation F G × ℂ .Arrow A B {θ×f : NaturalTransformation F G × ℂ .Arrow A B} @@ -300,26 +296,33 @@ module _ (ℓ : Level) where g = proj₂ η×g ηθNT : NaturalTransformation F H - ηθNT = Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat) + ηθNT = Fun .Category._∘_ {F} {G} {H} (η , ηNat) (θ , θNat) ηθ = proj₁ ηθNT ηθNat = proj₂ ηθNT :distrib: : - (η C 𝔻⊕ θ C) 𝔻⊕ F .func→ (g ℂ⊕ f) - ≡ (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f) + 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F .func→ ( ℂ [ g ∘ f ] ) ] + ≡ 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ] :distrib: = begin - (ηθ C) 𝔻⊕ F .func→ (g ℂ⊕ f) ≡⟨ ηθNat (g ℂ⊕ f) ⟩ - H .func→ (g ℂ⊕ f) 𝔻⊕ (ηθ A) ≡⟨ cong (λ φ → φ 𝔻⊕ ηθ A) (H.distrib) ⟩ - (H .func→ g 𝔻⊕ H .func→ f) 𝔻⊕ (ηθ A) ≡⟨ sym assoc ⟩ - H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A)) ≡⟨⟩ - H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A)) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) assoc ⟩ - H .func→ g 𝔻⊕ ((H .func→ f 𝔻⊕ η A) 𝔻⊕ θ A) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (cong (λ φ → φ 𝔻⊕ θ A) (sym (ηNat f))) ⟩ - H .func→ g 𝔻⊕ ((η B 𝔻⊕ G .func→ f) 𝔻⊕ θ A) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (sym assoc) ⟩ - H .func→ g 𝔻⊕ (η B 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) ≡⟨ assoc ⟩ - (H .func→ g 𝔻⊕ η B) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ → φ 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) (sym (ηNat g)) ⟩ - (η C 𝔻⊕ G .func→ g) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ → (η C 𝔻⊕ G .func→ g) 𝔻⊕ φ) (sym (θNat f)) ⟩ - (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f) ∎ + 𝔻 [ (ηθ C) ∘ F .func→ (ℂ [ g ∘ f ]) ] + ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ + 𝔻 [ H .func→ (ℂ [ g ∘ f ]) ∘ (ηθ A) ] + ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩ + 𝔻 [ 𝔻 [ H .func→ g ∘ H .func→ f ] ∘ (ηθ A) ] + ≡⟨ sym assoc ⟩ + 𝔻 [ H .func→ g ∘ 𝔻 [ H .func→ f ∘ ηθ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) assoc ⟩ + 𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ H .func→ f ∘ η A ] ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩ + 𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ η B ∘ G .func→ f ] ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (sym assoc) ⟩ + 𝔻 [ H .func→ g ∘ 𝔻 [ η B ∘ 𝔻 [ G .func→ f ∘ θ A ] ] ] ≡⟨ assoc ⟩ + 𝔻 [ 𝔻 [ H .func→ g ∘ η B ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ G .func→ f ∘ θ A ] ]) (sym (ηNat g)) ⟩ + 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ φ ]) (sym (θNat f)) ⟩ + 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ] ∎ where open IsCategory (𝔻 .isCategory) open module H = IsFunctor (H .isFunctor) @@ -339,9 +342,9 @@ module _ (ℓ : Level) where postulate transpose : Functor 𝔸 :obj: - eq : Catℓ ._⊕_ :eval: (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ≡ F + eq : Catℓ [ :eval: ∘ (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ] ≡ F - catTranspose : ∃![ F~ ] (Catℓ ._⊕_ :eval: (parallelProduct F~ (Catℓ .𝟙 {o = ℂ})) ≡ F) + catTranspose : ∃![ F~ ] (Catℓ [ :eval: ∘ (parallelProduct F~ (Catℓ .𝟙 {o = ℂ}))] ≡ F ) catTranspose = transpose , eq :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index c818e76..e3d0c83 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -10,19 +10,19 @@ open import Cat.Category open import Cat.Functor module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where - open Category + open Category hiding ( _∘_ ; Arrow ) open Functor module _ (F G : Functor ℂ 𝔻) where -- What do you call a non-natural tranformation? Transformation : Set (ℓc ⊔ ℓd') - Transformation = (C : ℂ .Object) → 𝔻 .Arrow (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} - → (f : ℂ .Arrow A B) - → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A) + → (f : ℂ [ A , B ]) + → 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ] NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd') NaturalTransformation = Σ Transformation Natural @@ -30,18 +30,28 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat -- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd')) -- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A) + module _ {F G : Functor ℂ 𝔻} where + NaturalTransformation≡ : {α β : NaturalTransformation F G} + → (eq₁ : α .proj₁ ≡ β .proj₁) + → (eq₂ : PathP + (λ i → {A B : ℂ .Object} (f : ℂ [ A , B ]) + → 𝔻 [ eq₁ i B ∘ F .func→ f ] + ≡ 𝔻 [ G .func→ f ∘ eq₁ i A ]) + (α .proj₂) (β .proj₂)) + → α ≡ β + NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i + identityTrans : (F : Functor ℂ 𝔻) → Transformation F F 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 ≡⟨ sym (proj₁ 𝔻.ident) ⟩ - F→ f 𝔻⊕ 𝔻 .𝟙 ≡⟨⟩ - F→ f 𝔻⊕ identityTrans F A ∎ + 𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩ + 𝔻 [ 𝔻 .𝟙 ∘ F→ f ] ≡⟨ proj₂ 𝔻.ident ⟩ + F→ f ≡⟨ sym (proj₁ 𝔻.ident) ⟩ + 𝔻 [ F→ f ∘ 𝔻 .𝟙 ] ≡⟨⟩ + 𝔻 [ F→ f ∘ identityTrans F A ] ∎ where - _𝔻⊕_ = 𝔻 ._⊕_ F→ = F .func→ open module 𝔻 = IsCategory (𝔻 .isCategory) @@ -50,21 +60,20 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat module _ {F G H : Functor ℂ 𝔻} where private - _𝔻⊕_ = 𝔻 ._⊕_ _∘nt_ : Transformation G H → Transformation F G → Transformation F H - (θ ∘nt η) C = θ C 𝔻⊕ η C + (θ ∘nt η) C = 𝔻 [ θ C ∘ η C ] NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin - ((θ ∘nt η) B) 𝔻⊕ (F .func→ f) ≡⟨⟩ - (θ B 𝔻⊕ η B) 𝔻⊕ (F .func→ f) ≡⟨ sym assoc ⟩ - θ B 𝔻⊕ (η B 𝔻⊕ (F .func→ f)) ≡⟨ cong (λ φ → θ B 𝔻⊕ φ) (ηNat f) ⟩ - θ B 𝔻⊕ ((G .func→ f) 𝔻⊕ η A) ≡⟨ assoc ⟩ - (θ B 𝔻⊕ (G .func→ f)) 𝔻⊕ η A ≡⟨ cong (λ φ → φ 𝔻⊕ η A) (θNat f) ⟩ - (((H .func→ f) 𝔻⊕ θ A) 𝔻⊕ η A) ≡⟨ sym assoc ⟩ - ((H .func→ f) 𝔻⊕ (θ A 𝔻⊕ η A)) ≡⟨⟩ - ((H .func→ f) 𝔻⊕ ((θ ∘nt η) A)) ∎ + 𝔻 [ (θ ∘nt η) B ∘ F .func→ f ] ≡⟨⟩ + 𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F .func→ f ] ≡⟨ sym assoc ⟩ + 𝔻 [ θ B ∘ 𝔻 [ η B ∘ F .func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩ + 𝔻 [ θ B ∘ 𝔻 [ G .func→ f ∘ η A ] ] ≡⟨ assoc ⟩ + 𝔻 [ 𝔻 [ θ B ∘ G .func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩ + 𝔻 [ 𝔻 [ H .func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym assoc ⟩ + 𝔻 [ H .func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩ + 𝔻 [ H .func→ f ∘ (θ ∘nt η) A ] ∎ where open IsCategory (𝔻 .isCategory) NatComp = _:⊕:_ @@ -100,7 +109,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat { Object = Functor ℂ 𝔻 ; Arrow = NaturalTransformation ; 𝟙 = λ {F} → identityNat F - ; _⊕_ = λ {F G H} → _:⊕:_ {F} {G} {H} + ; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H} } module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where @@ -112,5 +121,5 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where { Object = Presheaf ℂ ; Arrow = NaturalTransformation ; 𝟙 = λ {F} → identityNat F - ; _⊕_ = λ {F G H} → NatComp {F = F} {G = G} {H = H} + ; _∘_ = λ {F G H} → NatComp {F = F} {G = G} {H = H} } diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 42d63ab..43f3409 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -159,6 +159,6 @@ Rel = record { Object = Set ; Arrow = λ S R → Subset (S × R) ; 𝟙 = λ {S} → Diag S - ; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )} + ; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )} ; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r } } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 634a3a7..31a0b63 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -3,7 +3,6 @@ module Cat.Categories.Sets where open import Cubical open import Agda.Primitive open import Data.Product -open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) open import Cat.Category open import Cat.Functor @@ -15,7 +14,7 @@ module _ {ℓ : Level} where { Object = Set ℓ ; Arrow = λ T U → T → U ; 𝟙 = id - ; _⊕_ = _∘′_ + ; _∘_ = _∘′_ ; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) } } where @@ -26,16 +25,15 @@ module _ {ℓ : Level} where _&&&_ : (X → A × B) _&&&_ x = f x , g x module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where - _S⊕_ = Sets ._⊕_ - lem : proj₁ S⊕ (f &&& g) ≡ f × snd S⊕ (f &&& g) ≡ g + lem : Sets [ proj₁ ∘ (f &&& g)] ≡ f × Sets [ proj₂ ∘ (f &&& g)] ≡ g proj₁ lem = refl proj₂ lem = refl instance - isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} fst snd + isProduct : {A B : Sets .Object} → 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 = record { obj = A × B ; proj₁ = fst ; proj₂ = snd ; isProduct = isProduct } + product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct } instance SetsHasProducts : HasProducts Sets @@ -49,9 +47,9 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'}) representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ representable {ℂ = ℂ} A = record { func* = λ B → ℂ .Arrow A B - ; func→ = ℂ ._⊕_ + ; func→ = ℂ ._∘_ ; isFunctor = record - { ident = funExt λ _ → snd ident + { ident = funExt λ _ → proj₂ ident ; distrib = funExt λ x → sym assoc } } @@ -66,9 +64,9 @@ Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'}) presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ presheaf {ℂ = ℂ} B = record { func* = λ A → ℂ .Arrow A B - ; func→ = λ f g → ℂ ._⊕_ g f + ; func→ = λ f g → ℂ ._∘_ g f ; isFunctor = record - { ident = funExt λ x → fst ident + { ident = funExt λ x → proj₁ ident ; distrib = funExt λ x → assoc } } diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 99e4cd1..586e00f 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -10,7 +10,7 @@ open import Data.Product renaming ; ∃! to ∃!≈ ) open import Data.Empty -open import Function +import Function open import Cubical ∃! : ∀ {a b} {A : Set a} @@ -43,9 +43,9 @@ record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where Object : Set ℓ Arrow : Object → Object → Set ℓ' 𝟙 : {o : Object} → Arrow o o - _⊕_ : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c - {{isCategory}} : IsCategory Object Arrow 𝟙 _⊕_ - infixl 45 _⊕_ + _∘_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C + {{isCategory}} : IsCategory Object Arrow 𝟙 _∘_ + infixl 10 _∘_ domain : { a b : Object } → Arrow a b → Object domain {a = a} _ = a codomain : { a b : Object } → Arrow a b → Object @@ -57,18 +57,18 @@ _[_,_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → (A : ℂ .Object) → _[_,_] = Arrow _[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : ℂ .Object} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ] -_[_∘_] = _⊕_ +_[_∘_] = _∘_ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where module _ { A B : ℂ .Object } where Isomorphism : (f : ℂ .Arrow A B) → Set ℓ' - Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ ._⊕_ g f ≡ ℂ .𝟙 × ℂ ._⊕_ f g ≡ ℂ .𝟙 + Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ [ g ∘ f ] ≡ ℂ .𝟙 × ℂ [ f ∘ g ] ≡ ℂ .𝟙 Epimorphism : {X : ℂ .Object } → (f : ℂ .Arrow A B) → Set ℓ' - Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ ._⊕_ g₀ f ≡ ℂ ._⊕_ g₁ f → g₀ ≡ g₁ + Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ [ g₀ ∘ f ] ≡ ℂ [ g₁ ∘ f ] → g₀ ≡ g₁ Monomorphism : {X : ℂ .Object} → (f : ℂ .Arrow A B) → Set ℓ' - Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ ._⊕_ f g₀ ≡ ℂ ._⊕_ f g₁ → g₀ ≡ g₁ + Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ [ f ∘ g₀ ] ≡ ℂ [ f ∘ g₁ ] → g₀ ≡ g₁ -- Isomorphism of objects _≅_ : (A B : Object ℂ) → Set ℓ' @@ -78,7 +78,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} whe IsProduct : (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ') IsProduct π₁ π₂ = ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B) - → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ ._⊕_ π₂ x ≡ x₂) + → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ × ℂ [ π₂ ∘ x ] ≡ x₂) -- Tip from Andrea; Consider this style for efficiency: -- record IsProduct {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'}) @@ -112,17 +112,17 @@ record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ parallelProduct : {A A' B B' : ℂ .Object} → ℂ .Arrow A A' → ℂ .Arrow B B' → ℂ .Arrow (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₁)) - (ℂ ._⊕_ b ((product A B) .proj₂)) + (ℂ [ a ∘ (product A B) .proj₁ ]) + (ℂ [ b ∘ (product A B) .proj₂ ]) module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where Opposite : Category ℓ ℓ' Opposite = record { Object = ℂ .Object - ; Arrow = flip (ℂ .Arrow) + ; Arrow = Function.flip (ℂ .Arrow) ; 𝟙 = ℂ .𝟙 - ; _⊕_ = flip (ℂ ._⊕_) + ; _∘_ = Function.flip (ℂ ._∘_) ; isCategory = record { assoc = sym assoc ; ident = swap ident } } where @@ -145,7 +145,7 @@ Hom ℂ A B = Arrow ℂ A B module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where HomFromArrow : (A : ℂ .Object) → {B B' : ℂ .Object} → (g : ℂ .Arrow B B') → Hom ℂ A B → Hom ℂ A B' - HomFromArrow _A = _⊕_ ℂ + HomFromArrow _A = ℂ ._∘_ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where open HasProducts hasProducts @@ -157,7 +157,7 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} module _ (B C : ℂ .Category.Object) where IsExponential : (Cᴮ : ℂ .Object) → ℂ .Arrow (Cᴮ ×p B) C → Set (ℓ ⊔ ℓ') IsExponential Cᴮ eval = ∀ (A : ℂ .Object) (f : ℂ .Arrow (A ×p B) C) - → ∃![ f~ ] (ℂ ._⊕_ eval (parallelProduct f~ (ℂ .𝟙)) ≡ f) + → ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (ℂ .𝟙)] ≡ f) record Exponential : Set (ℓ ⊔ ℓ') where field diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda index 5686356..1facb03 100644 --- a/src/Cat/Category/Free.agda +++ b/src/Cat/Category/Free.agda @@ -31,6 +31,6 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where { Object = Obj ; Arrow = Path ; 𝟙 = λ {o} → emptyPath o - ; _⊕_ = λ {a b c} → concatenate {a} {b} {c} + ; _∘_ = λ {a b c} → concatenate {a} {b} {c} ; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l } } diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 2a540ba..c672a53 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -15,27 +15,26 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Obje open IsCategory (isCategory) iso-is-epi : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f - iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = - begin + iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin g₀ ≡⟨ sym (proj₁ ident) ⟩ - g₀ ⊕ 𝟙 ≡⟨ cong (_⊕_ g₀) (sym right-inv) ⟩ - g₀ ⊕ (f ⊕ f-) ≡⟨ assoc ⟩ - (g₀ ⊕ f) ⊕ f- ≡⟨ cong (λ φ → φ ⊕ f-) eq ⟩ - (g₁ ⊕ f) ⊕ f- ≡⟨ sym assoc ⟩ - g₁ ⊕ (f ⊕ f-) ≡⟨ cong (_⊕_ g₁) right-inv ⟩ - g₁ ⊕ 𝟙 ≡⟨ proj₁ ident ⟩ + g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩ + g₀ ∘ (f ∘ f-) ≡⟨ assoc ⟩ + (g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩ + (g₁ ∘ f) ∘ f- ≡⟨ sym assoc ⟩ + g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩ + g₁ ∘ 𝟙 ≡⟨ proj₁ ident ⟩ g₁ ∎ iso-is-mono : Isomorphism {ℂ = ℂ} f → Monomorphism {ℂ = ℂ} {X = X} f iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq = begin g₀ ≡⟨ sym (proj₂ ident) ⟩ - 𝟙 ⊕ g₀ ≡⟨ cong (λ φ → φ ⊕ g₀) (sym left-inv) ⟩ - (f- ⊕ f) ⊕ g₀ ≡⟨ sym assoc ⟩ - f- ⊕ (f ⊕ g₀) ≡⟨ cong (_⊕_ f-) eq ⟩ - f- ⊕ (f ⊕ g₁) ≡⟨ assoc ⟩ - (f- ⊕ f) ⊕ g₁ ≡⟨ cong (λ φ → φ ⊕ g₁) left-inv ⟩ - 𝟙 ⊕ g₁ ≡⟨ proj₂ ident ⟩ + 𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ + (f- ∘ f) ∘ g₀ ≡⟨ sym assoc ⟩ + f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩ + f- ∘ (f ∘ g₁) ≡⟨ assoc ⟩ + (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩ + 𝟙 ∘ g₁ ≡⟨ proj₂ ident ⟩ g₁ ∎ iso-is-epi-mono : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f × Monomorphism {ℂ = ℂ} {X = X} f @@ -71,17 +70,22 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where :func→: : NaturalTransformation (prshf A) (prshf B) - :func→: = (λ C x → (ℂ ._⊕_ f x)) , λ f₁ → funExt λ x → lem + :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ x → lem where lem = (ℂ .isCategory) .IsCategory.assoc module _ {c : ℂ .Object} where eqTrans : (:func→: (ℂ .𝟙 {c})) .proj₁ ≡ (Fun .𝟙 {o = prshf c}) .proj₁ eqTrans = funExt λ x → funExt λ x → ℂ .isCategory .IsCategory.ident .proj₂ - eqNat : (i : I) → Natural (prshf c) (prshf c) (eqTrans i) - eqNat i f = {!!} - + eqNat + : PathP (λ i → {A B : ℂ .Object} (f : Opposite ℂ .Arrow A B) + → Sets [ eqTrans i B ∘ prshf c .Functor.func→ f ] + ≡ Sets [ prshf c .Functor.func→ f ∘ eqTrans i A ]) + ((:func→: (ℂ .𝟙 {c})) .proj₂) ((Fun .𝟙 {o = prshf c}) .proj₂) + eqNat = λ i f i' x₁ → {!ℂ ._⊕_ ? ?!} + -- eqNat i f = {!!} + -- Sets ._⊕_ (eq₁ i B) (prshf A .func→ f) ≡ Sets ._⊕_ (prshf B .func→ f) (eq₁ i A) :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c}) - :ident: i = eqTrans i , eqNat i + :ident: = NaturalTransformation≡ eqTrans eqNat yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}}) yoneda = record diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda index bc3baae..c92defe 100644 --- a/src/Cat/Cubical.agda +++ b/src/Cat/Cubical.agda @@ -18,7 +18,7 @@ open import Cat.Functor -- categorical version of CTT module CwF {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where - open Category + open Category hiding (_∘_) open Functor open import Function open import Cubical @@ -53,7 +53,7 @@ module CwF {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where { Object = Obj ; Arrow = Arr ; 𝟙 = one - ; _⊕_ = λ {a b c} → _:⊕:_ {a} {b} {c} + ; _∘_ = λ {a b c} → _:⊕:_ {a} {b} {c} } Contexts = ℂ .Object @@ -96,6 +96,6 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where { Object = Ns → Bool ; Arrow = Mor ; 𝟙 = {!!} - ; _⊕_ = {!!} + ; _∘_ = {!!} ; isCategory = {!!} } diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda index 8d97a08..056e142 100644 --- a/src/Cat/Functor.agda +++ b/src/Cat/Functor.agda @@ -6,7 +6,7 @@ open import Function open import Cat.Category -open Category +open Category hiding (_∘_) module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where record IsFunctor