From 9349b3755011e984e23019fa75948e449d27615d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 6 Feb 2018 14:24:34 +0100 Subject: [PATCH] Refactor Functor - only in module Functor --- src/Cat/Categories/Fun.agda | 36 +++++---- src/Cat/Categories/Sets.agda | 12 ++- src/Cat/Category.agda | 8 +- src/Cat/Category/Functor.agda | 143 +++++++++++++++++++++++----------- src/Cat/CwF.agda | 6 +- 5 files changed, 133 insertions(+), 72 deletions(-) diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 26e71b1..e60a118 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -14,15 +14,18 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat open Functor module _ (F G : Functor ℂ 𝔻) where + private + module F = Functor F + module G = Functor G -- 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 ℂ} → (f : ℂ [ A , B ]) - → 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ] + → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ] NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd') NaturalTransformation = Σ Transformation Natural @@ -30,13 +33,12 @@ 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} + NaturalTransformation≡ : {α β : NaturalTransformation} → (eq₁ : α .proj₁ ≡ β .proj₁) → (eq₂ : PathP (λ i → {A B : Object ℂ} (f : ℂ [ A , B ]) - → 𝔻 [ eq₁ i B ∘ F .func→ f ] - ≡ 𝔻 [ G .func→ f ∘ eq₁ i A ]) + → 𝔻 [ eq₁ i B ∘ F.func→ f ] + ≡ 𝔻 [ G.func→ f ∘ eq₁ i A ]) (α .proj₂) (β .proj₂)) → α ≡ β NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i @@ -52,7 +54,8 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat 𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩ 𝔻 [ F→ f ∘ identityTrans F A ] ∎ where - F→ = F .func→ + module F = Functor F + F→ = F.func→ module 𝔻 = IsCategory (isCategory 𝔻) identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F @@ -60,20 +63,23 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat module _ {F G H : Functor ℂ 𝔻} where private + module F = Functor F + module G = Functor G + module H = Functor H _∘nt_ : Transformation G H → Transformation F G → Transformation F H (θ ∘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 𝔻) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index aade6d0..5263aa1 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -56,8 +56,10 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'}) -- The "co-yoneda" embedding. representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ representable {ℂ = ℂ} A = record - { func* = λ B → ℂ [ A , B ] - ; func→ = ℂ [_∘_] + { raw = record + { func* = λ B → ℂ [ A , B ] + ; func→ = ℂ [_∘_] + } ; isFunctor = record { ident = funExt λ _ → proj₂ ident ; distrib = funExt λ x → sym assoc @@ -73,8 +75,10 @@ Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'}) -- Alternate name: `yoneda` presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ presheaf {ℂ = ℂ} B = record - { func* = λ A → ℂ [ A , B ] - ; func→ = λ f g → ℂ [ g ∘ f ] + { raw = record + { 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 5cd7c5b..168b2fc 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -53,10 +53,6 @@ record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where -- (univalent). record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where open RawCategory ℂ - -- (Object : Set ℓ) - -- (Arrow : Object → Object → Set ℓ') - -- (𝟙 : {o : Object} → Arrow o o) - -- (_∘_ : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c) field assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D } → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f @@ -100,9 +96,9 @@ module _ {ℓa} {ℓb} {ℂ : RawCategory ℓa ℓb} where ( x.arrowIsSet (fst x.ident) (fst y.ident) i , x.arrowIsSet (snd x.ident) (snd y.ident) i ) - ; arrowIsSet = λ p q → + ; arrowIsSet = λ p q → let - golden : x.arrowIsSet p q ≡ y.arrowIsSet p q + golden : x.arrowIsSet p q ≡ y.arrowIsSet p q golden = {!!} in golden i diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 912557e..8097071 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -6,61 +6,110 @@ open import Function open import Cat.Category -open Category hiding (_∘_) +open Category hiding (_∘_ ; raw) -module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where - record IsFunctor - (func* : Object ℂ → Object 𝔻) - (func→ : {A B : Object ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]) - : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where +module _ {ℓc ℓc' ℓd ℓd'} + (ℂ : Category ℓc ℓc') + (𝔻 : Category ℓd ℓd') + where + + private + ℓ = ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd' + 𝓤 = Set ℓ + + record RawFunctor : 𝓤 where + field + func* : Object ℂ → Object 𝔻 + func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ] + + record IsFunctor (F : RawFunctor) : 𝓤 where + open RawFunctor F field 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 ]} → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ] record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where field - func* : Object ℂ → Object 𝔻 - func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ] - {{isFunctor}} : IsFunctor func* func→ + raw : RawFunctor + {{isFunctor}} : IsFunctor raw + + private + module R = RawFunctor raw + + func* : Object ℂ → Object 𝔻 + func* = R.func* + + func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ] + func→ = R.func→ open IsFunctor open Functor +-- TODO: Is `IsFunctor` a proposition? +module _ + {ℓa ℓb : Level} + {ℂ 𝔻 : Category ℓa ℓb} + {F : RawFunctor ℂ 𝔻} + where + private + module 𝔻 = IsCategory (isCategory 𝔻) + + -- isProp : Set ℓ + -- isProp = (x y : A) → x ≡ y + + IsFunctorIsProp : isProp (IsFunctor _ _ F) + IsFunctorIsProp isF0 isF1 i = record + { ident = 𝔻.arrowIsSet isF0.ident isF1.ident i + ; distrib = 𝔻.arrowIsSet isF0.distrib isF1.distrib i + } + where + module isF0 = IsFunctor isF0 + module isF1 = IsFunctor isF1 + +-- Alternate version of above where `F` is a path in +module _ + {ℓa ℓb : Level} + {ℂ 𝔻 : Category ℓa ℓb} + {F : I → RawFunctor ℂ 𝔻} + where + private + module 𝔻 = IsCategory (isCategory 𝔻) + IsProp' : {ℓ : Level} (A : I → Set ℓ) → Set ℓ + IsProp' A = (a0 : A i0) (a1 : A i1) → A [ a0 ≡ a1 ] + + postulate IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i) + -- IsFunctorIsProp' isF0 isF1 i = record + -- { ident = {!𝔻.arrowIsSet {!isF0.ident!} {!isF1.ident!} i!} + -- ; distrib = {!𝔻.arrowIsSet {!isF0.distrib!} {!isF1.distrib!} i!} + -- } + -- where + -- module isF0 = IsFunctor isF0 + -- module isF1 = IsFunctor isF1 + module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where - - IsFunctor≡ - : {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}) - [ F .ident ≡ G .ident ]) - → (eqD : - (λ i → ∀ {A B C} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} - → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]) - [ F .distrib ≡ G .distrib ]) - → (λ _ → IsFunctor ℂ 𝔻 (λ i → func* i) func→) [ F ≡ G ] - IsFunctor≡ eqI eqD i = record { ident = eqI i ; distrib = eqD i } - Functor≡ : {F G : Functor ℂ 𝔻} - → (eq* : F .func* ≡ G .func*) + → (eq* : func* F ≡ func* G) → (eq→ : (λ i → ∀ {x y} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ]) - [ F .func→ ≡ G .func→ ]) - -- → (eqIsF : PathP (λ i → IsFunctor ℂ 𝔻 (eq* i) (eq→ i)) (F .isFunctor) (G .isFunctor)) - → (eqIsFunctor : (λ i → IsFunctor ℂ 𝔻 (eq* i) (eq→ i)) [ F .isFunctor ≡ G .isFunctor ]) + [ func→ F ≡ func→ G ]) → F ≡ G - Functor≡ eq* eq→ eqIsFunctor i = record { func* = eq* i ; func→ = eq→ i ; isFunctor = eqIsFunctor i } + Functor≡ {F} {G} eq* eq→ i = record + { raw = eqR i + ; isFunctor = f i + } + where + eqR : raw F ≡ raw G + eqR i = record { func* = eq* i ; func→ = eq→ i } + postulate T : isSet (IsFunctor _ _ (raw F)) + f : (λ i → IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ] + f = IsFunctorIsProp' (isFunctor F) (isFunctor G) module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where private - F* = F .func* - F→ = F .func→ - G* = G .func* - G→ = G .func→ + F* = func* F + F→ = func→ F + G* = func* G + G→ = func→ G 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 ] @@ -70,12 +119,12 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ F .isFunctor .distrib ⟩ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎ - _∘f_ : Functor A C - _∘f_ = - record - { func* = F* ∘ G* - ; func→ = F→ ∘ G→ - ; isFunctor = record + _∘fr_ : RawFunctor A C + RawFunctor.func* _∘fr_ = F* ∘ G* + RawFunctor.func→ _∘fr_ = F→ ∘ G→ + instance + isFunctor' : IsFunctor A C _∘fr_ + isFunctor' = record { ident = begin (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩ F→ (G→ (𝟙 A)) ≡⟨ cong F→ (G .isFunctor .ident)⟩ @@ -83,13 +132,17 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F 𝟙 C ∎ ; distrib = dist } - } + + _∘f_ : Functor A C + raw _∘f_ = _∘fr_ -- The identity functor identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C identity = record - { func* = λ x → x - ; func→ = λ x → x + { raw = record + { func* = λ x → x + ; func→ = λ x → x + } ; isFunctor = record { ident = refl ; distrib = refl diff --git a/src/Cat/CwF.agda b/src/Cat/CwF.agda index 44e725e..5735ac3 100644 --- a/src/Cat/CwF.agda +++ b/src/Cat/CwF.agda @@ -25,8 +25,10 @@ module _ {ℓa ℓb : Level} where T : Functor (Opposite ℂ) (Fam ℓa ℓb) -- Empty context [] : Terminal ℂ + private + module T = Functor T Type : (Γ : Object ℂ) → Set ℓa - Type Γ = proj₁ (T .func* Γ) + Type Γ = proj₁ (T.func* Γ) module _ {Γ : Object ℂ} {A : Type Γ} where @@ -35,7 +37,7 @@ module _ {ℓa ℓb : Level} where (λ f → {x : proj₁ (func* T B)} → proj₂ (func* T B) x → proj₂ (func* T A) (f x)) - k = T .func→ γ + k = T.func→ γ k₁ : proj₁ (func* T B) → proj₁ (func* T A) k₁ = proj₁ k k₂ : ({x : proj₁ (func* T B)} →