From bd824143bcb0a621e640f6a58eb0180993143e7f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 25 Jan 2018 12:54:00 +0100 Subject: [PATCH 1/4] Update reference to Agda-version --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 9b3a8a7..4a56ea0 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ consisting of the proposal for the thesis). Installation ============ You probably need a very recent version of the Agda compiler. At the time -of writing the solution has been tested with Agda version 2.6.0-9af3e07. +of writing the solution has been tested with Agda version 2.6.0-5d84754. Dependencies ------------ From 6e25083a471cd73584fd0653ac254873de18d9ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 25 Jan 2018 13:58:56 +0100 Subject: [PATCH 2/4] Comments in yoneda --- src/Cat/Category/Properties.agda | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 90bc1b8..35a4a39 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -56,8 +56,6 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where open Exponential private Catℓ = Cat ℓ ℓ - CatHasExponentials : HasExponentials Catℓ - CatHasExponentials = Cat.hasExponentials ℓ -- Exp : Set (lsuc (lsuc ℓ)) -- Exp = Exponential (Cat (lsuc ℓ) ℓ) @@ -66,7 +64,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where _⇑_ : (A B : Catℓ .Object) → Catℓ .Object A ⇑ B = (exponent A B) .obj where - open HasExponentials CatHasExponentials + open HasExponentials (Cat.hasExponentials ℓ) private -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't. @@ -75,10 +73,17 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object :func*: A = {!!} + -- prsh = presheaf {ℂ = ℂ} + -- :func*:' : ℂ .Object → Presheaf ℂ + -- :func*:' = prsh + -- module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where + -- open import Cat.Categories.Fun + -- :func→:' : NaturalTransformation (prsh A) (prsh B) + yoneda : Functor ℂ (Setz ⇑ (Opposite ℂ)) yoneda = record { func* = :func*: - ; func→ = {!!} + ; func→ = {!:func→:'!} ; ident = {!!} ; distrib = {!!} } From ee2e84edfefeff9c1c99178e3ae0563e2d40cf9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 25 Jan 2018 14:11:28 +0100 Subject: [PATCH 3/4] Remove unused bindings --- src/Cat/Categories/Cat.agda | 2 -- src/Cat/Category/Properties.agda | 3 ++- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 4bac632..1bd1c51 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -34,8 +34,6 @@ module _ (ℓ ℓ' : Level) where (λ i → {x y : A .Object} → A .Arrow x y → D .Arrow (eq* i x) (eq* i y)) (func→ (h ∘f (g ∘f f))) (func→ ((h ∘f g) ∘f f)) eq→ = refl - id-l = (h ∘f (g ∘f f)) .ident -- = func→ (h ∘f (g ∘f f)) (𝟙 A) ≡ 𝟙 D - id-r = ((h ∘f g) ∘f f) .ident -- = func→ ((h ∘f g) ∘f f) (𝟙 A) ≡ 𝟙 D postulate eqI : PathP (λ i → ∀ {c : A .Object} → eq→ i (A .𝟙 {c}) ≡ D .𝟙 {eq* i c}) (ident ((h ∘f (g ∘f f)))) diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 35a4a39..a641f28 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -74,6 +74,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where :func*: A = {!!} -- prsh = presheaf {ℂ = ℂ} + -- k = prsh {!!} -- :func*:' : ℂ .Object → Presheaf ℂ -- :func*:' = prsh -- module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where @@ -83,7 +84,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where yoneda : Functor ℂ (Setz ⇑ (Opposite ℂ)) yoneda = record { func* = :func*: - ; func→ = {!:func→:'!} + ; func→ = {!!} ; ident = {!!} ; distrib = {!!} } From 229502261923b9cb80063f005ef10ca999e25b7a Mon Sep 17 00:00:00 2001 From: Andrea Vezzosi Date: Thu, 25 Jan 2018 17:04:00 +0000 Subject: [PATCH 4/4] used presheaf as first component of yoneda --- src/Cat/Category/Properties.agda | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index a641f28..6edaca1 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -52,6 +52,8 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where open import Cat.Category open Category open import Cat.Categories.Cat using (Cat) + open import Cat.Categories.Fun + open import Cat.Categories.Sets module Cat = Cat.Categories.Cat open Exponential private @@ -66,12 +68,12 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where where open HasExponentials (Cat.hasExponentials ℓ) - private - -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't. - Setz : Category ℓ ℓ - Setz = {!Sets!} - :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object - :func*: A = {!!} + -- private + -- -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't. + -- Setz : Category ℓ ℓ + -- Setz = {!Sets!} + -- :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object + -- :func*: A = {!!} -- prsh = presheaf {ℂ = ℂ} -- k = prsh {!!} @@ -81,9 +83,9 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where -- open import Cat.Categories.Fun -- :func→:' : NaturalTransformation (prsh A) (prsh B) - yoneda : Functor ℂ (Setz ⇑ (Opposite ℂ)) + yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}}) yoneda = record - { func* = :func*: + { func* = presheaf {ℂ = ℂ} ; func→ = {!!} ; ident = {!!} ; distrib = {!!}