From 86d3d7368e03a7d56e465b7a3195f0ffbb113e78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 30 Jan 2018 22:41:18 +0100 Subject: [PATCH] Use equality construction principle Also update submodules --- libs/agda-stdlib | 2 +- libs/cubical | 2 +- src/Cat/Categories/Cat.agda | 18 +++++++++-------- src/Cat/Categories/Fun.agda | 2 +- src/Cat/Category/Properties.agda | 33 ++++++++++++++++++-------------- src/Cat/Equality.agda | 21 ++++++++++++++++++++ src/Cat/Functor.agda | 29 ++++++++++++++-------------- 7 files changed, 68 insertions(+), 39 deletions(-) create mode 100644 src/Cat/Equality.agda diff --git a/libs/agda-stdlib b/libs/agda-stdlib index de23244..b5bfbc3 160000 --- a/libs/agda-stdlib +++ b/libs/agda-stdlib @@ -1 +1 @@ -Subproject commit de23244a73d6dab55715fd5a107a5de805c55764 +Subproject commit b5bfbc3c170b0bd0c9aaac1b4d4b3f9b06832bf6 diff --git a/libs/cubical b/libs/cubical index a83f5f4..1d6730c 160000 --- a/libs/cubical +++ b/libs/cubical @@ -1 +1 @@ -Subproject commit a83f5f4c63e5dfd8143ac03163868c63a56802de +Subproject commit 1d6730c4999daa2b04e9dd39faa0791d0b5c3b48 diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index d78e4ca..0de7a6a 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -44,7 +44,7 @@ module _ (ℓ ℓ' : Level) where ((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 - assc = Functor≡ eq* eq→ eqI eqD + assc = Functor≡ eq* eq→ (IsFunctor≡ eqI eqD) module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where module _ where @@ -58,16 +58,17 @@ module _ (ℓ ℓ' : Level) where (func→ (F ∘f identity)) (func→ F) eq→ = refl postulate - eqI-r : PathP (λ i → {c : ℂ .Object} - → PathP (λ _ → Arrow 𝔻 (func* F c) (func* F c)) (func→ F (ℂ .𝟙)) (𝔻 .𝟙)) - ((F ∘f identity) .isFunctor .ident) (F .isFunctor .ident) + eqI-r + : (λ i → {c : ℂ .Object} → (λ _ → 𝔻 [ func* F c , func* F c ]) + [ func→ F (ℂ .𝟙) ≡ 𝔻 .𝟙 ]) + [(F ∘f identity) .isFunctor .ident ≡ F .isFunctor .ident ] 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 ]) ((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib) ident-r : F ∘f identity ≡ F - ident-r = Functor≡ eq* eq→ eqI-r eqD-r + ident-r = Functor≡ eq* eq→ (IsFunctor≡ eqI-r eqD-r) module _ where private postulate @@ -75,13 +76,14 @@ module _ (ℓ ℓ' : Level) where eq→ : PathP (λ i → {x y : Object ℂ} → ℂ .Arrow x y → 𝔻 .Arrow (eq* i x) (eq* i y)) ((identity ∘f F) .func→) (F .func→) - eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A}) - ((identity ∘f F) .isFunctor .ident) (F .isFunctor .ident) + eqI : (λ 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 ]) ((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib) + -- (λ z → eq* i z) (eq→ i) ident-l : identity ∘f F ≡ F - ident-l = Functor≡ eq* eq→ eqI eqD + ident-l = Functor≡ eq* eq→ λ i → record { ident = eqI i ; distrib = eqD i } Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') Cat = diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index e3d0c83..cd0457d 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -53,7 +53,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat 𝔻 [ F→ f ∘ identityTrans F A ] ∎ where F→ = F .func→ - open module 𝔻 = IsCategory (𝔻 .isCategory) + module 𝔻 = IsCategory (𝔻 .isCategory) identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F identityNat F = identityTrans F , identityNatural F diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index c672a53..7a0f705 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -9,6 +9,8 @@ open import Cubical open import Cat.Category open import Cat.Functor 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 open Category ℂ @@ -58,6 +60,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where private Catℓ = Cat ℓ ℓ prshf = presheaf {ℂ = ℂ} + module ℂ = IsCategory (ℂ .isCategory) -- Exp : Set (lsuc (lsuc ℓ)) -- Exp = Exponential (Cat (lsuc ℓ) ℓ) @@ -70,22 +73,24 @@ 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 - where - lem = (ℂ .isCategory) .IsCategory.assoc + :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc + module _ {c : ℂ .Object} where - eqTrans : (:func→: (ℂ .𝟙 {c})) .proj₁ ≡ (Fun .𝟙 {o = prshf c}) .proj₁ - eqTrans = funExt λ x → funExt λ x → ℂ .isCategory .IsCategory.ident .proj₂ - 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) + eqTrans : (λ _ → Transformation (prshf c) (prshf c)) + [ (λ _ x → ℂ [ ℂ .𝟙 ∘ x ]) ≡ identityTrans (prshf c) ] + eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂ + + eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i)) + [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)] + eqNat = {!!} + -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] → + -- let + -- k : ℂ [ {!!} , {!!} ] + -- k = ℂ[A,c] + -- in {!ℂ [ ? ∘ ? ]!} + :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c}) - :ident: = NaturalTransformation≡ eqTrans eqNat + :ident: = Σ≡ eqTrans eqNat yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}}) yoneda = record diff --git a/src/Cat/Equality.agda b/src/Cat/Equality.agda new file mode 100644 index 0000000..251adb8 --- /dev/null +++ b/src/Cat/Equality.agda @@ -0,0 +1,21 @@ +-- Defines equality-principles for data-types from the standard library. + +module Cat.Equality where + +open import Level +open import Cubical + +-- _[_≡_] = PathP + +module Equality where + module Data where + module Product where + open import Data.Product public + + module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B} + (proj₁≡ : (λ _ → A) [ proj₁ a ≡ proj₁ b ]) + (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where + + Σ≡ : a ≡ b + proj₁ (Σ≡ i) = proj₁≡ i + proj₂ (Σ≡ i) = proj₂≡ i diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda index 056e142..ffd8209 100644 --- a/src/Cat/Functor.agda +++ b/src/Cat/Functor.agda @@ -32,27 +32,28 @@ open Functor module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where - -- IsFunctor≡ : ∀ {A B : ℂ .Object} {func* : ℂ .Object → 𝔻 .Object} {func→ : {A B : ℂ .Object} → ℂ .Arrow A B → 𝔻 .Arrow (func* A) (func* B)} {F G : IsFunctor ℂ 𝔻 func* func→} - -- → (eqI : PathP (λ i → ∀ {A : ℂ .Object} → func→ (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {func* A}) - -- (F .ident) (G .ident)) - -- → (eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} - -- → func→ (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (func→ g) (func→ f)) - -- (F .distrib) (G .distrib)) - -- → F ≡ G - -- IsFunctor≡ eqI eqD i = record { ident = eqI i ; distrib = eqD i } + IsFunctor≡ + : {func* : ℂ .Object → 𝔻 .Object} + {func→ : {A B : ℂ .Object} → ℂ .Arrow A B → 𝔻 .Arrow (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→ : PathP (λ 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)) - → (eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A}) - (F .isFunctor .ident) (G .isFunctor .ident)) - → (eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} - → eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ]) - (F .isFunctor .distrib) (G .isFunctor .distrib)) + → (eqIsFunctor : (λ i → IsFunctor ℂ 𝔻 (eq* i) (eq→ i)) [ F .isFunctor ≡ G .isFunctor ]) → F ≡ G - Functor≡ eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; isFunctor = record { ident = eqI i ; distrib = eqD i } } + Functor≡ eq* eq→ eqIsFunctor i = record { func* = eq* i ; func→ = eq→ i ; isFunctor = eqIsFunctor i } module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where private