diff --git a/src/Cat.agda b/src/Cat.agda index 20c5d69..478b725 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -1,19 +1,19 @@ module Cat where -import Cat.Category +open import Cat.Category -import Cat.Category.Functor -import Cat.Category.Product -import Cat.Category.Exponential -import Cat.Category.CartesianClosed -import Cat.Category.NaturalTransformation -import Cat.Category.Yoneda -import Cat.Category.Monad +open import Cat.Category.Functor +open import Cat.Category.Product +open import Cat.Category.Exponential +open import Cat.Category.CartesianClosed +open import Cat.Category.NaturalTransformation +open import Cat.Category.Yoneda +open import Cat.Category.Monad -import Cat.Categories.Sets -import Cat.Categories.Cat -import Cat.Categories.Rel -import Cat.Categories.Free -import Cat.Categories.Fun -import Cat.Categories.Cube -import Cat.Categories.CwF +open import Cat.Categories.Sets +open import Cat.Categories.Cat +open import Cat.Categories.Rel +open import Cat.Categories.Free +open import Cat.Categories.Fun +open import Cat.Categories.Cube +open import Cat.Categories.CwF diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda index fdee75e..00f10e3 100644 --- a/src/Cat/Categories/Cube.agda +++ b/src/Cat/Categories/Cube.agda @@ -26,24 +26,24 @@ open Category hiding (_∘_) open Functor module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where - -- Ns is the "namespace" - ℓo = (suc zero ⊔ ℓ) + private + -- Ns is the "namespace" + ℓo = (suc zero ⊔ ℓ) - FiniteDecidableSubset : Set ℓ - FiniteDecidableSubset = Ns → Dec ⊤ + FiniteDecidableSubset : Set ℓ + FiniteDecidableSubset = Ns → Dec ⊤ - isTrue : Bool → Set - isTrue false = ⊥ - isTrue true = ⊤ + isTrue : Bool → Set + isTrue false = ⊥ + isTrue true = ⊤ - elmsof : FiniteDecidableSubset → Set ℓ - elmsof P = Σ Ns (λ σ → True (P σ)) -- (σ : Ns) → isTrue (P σ) + elmsof : FiniteDecidableSubset → Set ℓ + elmsof P = Σ Ns (λ σ → True (P σ)) -- (σ : Ns) → isTrue (P σ) - 𝟚 : Set - 𝟚 = Bool + 𝟚 : Set + 𝟚 = Bool - module _ (I J : FiniteDecidableSubset) where - private + module _ (I J : FiniteDecidableSubset) where Hom' : Set ℓ Hom' = elmsof I → elmsof J ⊎ 𝟚 isInl : {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} → A ⊎ B → Set @@ -63,18 +63,18 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where ; (inj₂ _) → Lift ⊤ } - Hom = Σ Hom' rules + Hom = Σ Hom' rules - module Raw = RawCategory - -- The category of names and substitutions - Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo) - Raw.Object Rawℂ = FiniteDecidableSubset - Raw.Arrow Rawℂ = Hom - Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } - Raw._∘_ Rawℂ = {!!} + module Raw = RawCategory + -- The category of names and substitutions + Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo) + Raw.Object Rawℂ = FiniteDecidableSubset + Raw.Arrow Rawℂ = Hom + Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } + Raw._∘_ Rawℂ = {!!} - postulate IsCategoryℂ : IsCategory Rawℂ + postulate IsCategoryℂ : IsCategory Rawℂ - ℂ : Category ℓ ℓ - raw ℂ = Rawℂ - isCategory ℂ = IsCategoryℂ + ℂ : Category ℓ ℓ + raw ℂ = Rawℂ + isCategory ℂ = IsCategoryℂ diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 9a0c891..7e80478 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -20,10 +20,10 @@ singleton : ∀ {ℓ} {𝓤 : Set ℓ} {ℓr} {R : 𝓤 → 𝓤 → Set ℓr} { singleton f = cons f empty module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where - module ℂ = Category ℂ - open Category ℂ - private + module ℂ = Category ℂ + open Category ℂ + p-isAssociative : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D} → p ++ (q ++ r) ≡ (p ++ q) ++ r p-isAssociative {r = r} {q} {empty} = refl diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 898a331..08400ea 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -18,6 +18,10 @@ module _ {ℓc ℓc' ℓd ℓd'} ℓ = ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd' 𝓤 = Set ℓ + Omap = Object ℂ → Object 𝔻 + Fmap : Omap → Set _ + Fmap omap = ∀ {A B} + → ℂ [ A , B ] → 𝔻 [ omap A , omap B ] record RawFunctor : 𝓤 where field func* : Object ℂ → Object 𝔻 @@ -30,6 +34,30 @@ module _ {ℓc ℓc' ℓd ℓd'} IsDistributive = {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} → func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ] + -- | Equality principle for raw functors + -- + -- The type of `func→` depend on the value of `func*`. We can wrap this up + -- into an equality principle for this type like is done for e.g. `Σ` using + -- `pathJ`. + module _ {x y : RawFunctor} where + open RawFunctor + private + P : (omap : Omap) → (eq : func* x ≡ omap) → Set _ + P y eq = (fmap' : Fmap y) → (λ i → Fmap (eq i)) + [ func→ x ≡ fmap' ] + module _ + (eq : (λ i → Omap) [ func* x ≡ func* y ]) + (kk : P (func* x) refl) + where + private + p : P (func* y) eq + p = pathJ P kk (func* y) eq + eq→ : (λ i → Fmap (eq i)) [ func→ x ≡ func→ y ] + eq→ = p (func→ y) + RawFunctor≡ : x ≡ y + func* (RawFunctor≡ i) = eq i + func→ (RawFunctor≡ i) = eq→ i + record IsFunctor (F : RawFunctor) : 𝓤 where open RawFunctor F public field @@ -98,6 +126,16 @@ module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where eqIsF : (λ i → IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ] eqIsF = IsFunctorIsProp' (isFunctor F) (isFunctor G) + FunctorEq : {F G : Functor ℂ 𝔻} + → raw F ≡ raw G + → F ≡ G + raw (FunctorEq eq i) = eq i + isFunctor (FunctorEq {F} {G} eq i) + = res i + where + res : (λ i → IsFunctor ℂ 𝔻 (eq i)) [ isFunctor F ≡ isFunctor G ] + res = IsFunctorIsProp' (isFunctor F) (isFunctor G) + module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where private F* = func* F diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index e7305d3..8ba97df 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -279,18 +279,18 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where module R = Functor R module R⁰ = Functor R⁰ module R² = Functor R² - ηTrans : Transformation R⁰ R - ηTrans A = pure - ηNatural : Natural R⁰ R ηTrans + η : Transformation R⁰ R + η A = pure + ηNatural : Natural R⁰ R η ηNatural {A} {B} f = begin - ηTrans B ∘ R⁰.func→ f ≡⟨⟩ + η B ∘ R⁰.func→ f ≡⟨⟩ pure ∘ f ≡⟨ sym (isNatural _) ⟩ bind (pure ∘ f) ∘ pure ≡⟨⟩ fmap f ∘ pure ≡⟨⟩ - R.func→ f ∘ ηTrans A ∎ - μTrans : Transformation R² R - μTrans C = join - μNatural : Natural R² R μTrans + R.func→ f ∘ η A ∎ + μ : Transformation R² R + μ C = join + μNatural : Natural R² R μ μNatural f = begin join ∘ R².func→ f ≡⟨⟩ bind 𝟙 ∘ R².func→ f ≡⟨⟩ @@ -320,11 +320,11 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where where ηNatTrans : NaturalTransformation R⁰ R - proj₁ ηNatTrans = ηTrans + proj₁ ηNatTrans = η proj₂ ηNatTrans = ηNatural μNatTrans : NaturalTransformation R² R - proj₁ μNatTrans = μTrans + proj₁ μNatTrans = μ proj₂ μNatTrans = μNatural isNaturalForeign : IsNaturalForeign @@ -405,7 +405,8 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where -- This is problem 2.3 in [voe]. module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where private - open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_) + module ℂ = Category ℂ + open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_) open Functor using (func* ; func→) module M = Monoidal ℂ module K = Kleisli ℂ @@ -482,22 +483,79 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where -- I believe all the proofs here should be `refl`. module _ (m : K.Monad) where - open K.RawMonad (K.Monad.raw m) + open K.Monad m + -- open K.RawMonad (K.Monad.raw m) + bindEq : ∀ {X Y} + → K.RawMonad.bind (forthRaw (backRaw m)) {X} {Y} + ≡ K.RawMonad.bind (K.Monad.raw m) + bindEq {X} {Y} = begin + K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩ + (λ f → μ Y ∘ func→ R f) ≡⟨⟩ + (λ f → join ∘ fmap f) ≡⟨⟩ + (λ f → bind (f >>> pure) >>> bind 𝟙) ≡⟨ funExt lem ⟩ + (λ f → bind f) ≡⟨⟩ + bind ∎ + where + μ = proj₁ μNatTrans + lem : (f : Arrow X (RR Y)) → bind (f >>> pure) >>> bind 𝟙 ≡ bind f + lem f = begin + bind (f >>> pure) >>> bind 𝟙 + ≡⟨ isDistributive _ _ ⟩ + bind ((f >>> pure) >>> bind 𝟙) + ≡⟨ cong bind ℂ.isAssociative ⟩ + bind (f >>> (pure >>> bind 𝟙)) + ≡⟨ cong (λ φ → bind (f >>> φ)) (isNatural _) ⟩ + bind (f >>> 𝟙) + ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩ + bind f ∎ + + _&_ : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → A → (A → B) → B + x & f = f x + forthRawEq : forthRaw (backRaw m) ≡ K.Monad.raw m K.RawMonad.RR (forthRawEq _) = RR K.RawMonad.pure (forthRawEq _) = pure -- stuck - K.RawMonad.bind (forthRawEq i) = {!!} + K.RawMonad.bind (forthRawEq i) = bindEq i fortheq : (m : K.Monad) → forth (back m) ≡ m fortheq m = K.Monad≡ (forthRawEq m) module _ (m : M.Monad) where open M.RawMonad (M.Monad.raw m) + rawEq* : Functor.func* (K.Monad.R (forth m)) ≡ Functor.func* R + rawEq* = refl + left = Functor.raw (K.Monad.R (forth m)) + right = Functor.raw R + P : (omap : Omap ℂ ℂ) + → (eq : RawFunctor.func* left ≡ omap) + → (fmap' : Fmap ℂ ℂ omap) + → Set _ + P _ eq fmap' = (λ i → Fmap ℂ ℂ (eq i)) + [ RawFunctor.func→ left ≡ fmap' ] + -- rawEq→ : (λ i → Fmap ℂ ℂ (refl i)) [ Functor.func→ (K.Monad.R (forth m)) ≡ Functor.func→ R ] + rawEq→ : P (RawFunctor.func* right) refl (RawFunctor.func→ right) + -- rawEq→ : (fmap' : Fmap ℂ ℂ {!!}) → RawFunctor.func→ left ≡ fmap' + rawEq→ = begin + (λ {A} {B} → RawFunctor.func→ left) ≡⟨ {!!} ⟩ + (λ {A} {B} → RawFunctor.func→ right) ∎ + -- destfmap = + source = (Functor.raw (K.Monad.R (forth m))) + -- p : (fmap' : Fmap ℂ ℂ (RawFunctor.func* source)) → (λ i → Fmap ℂ ℂ (refl i)) [ func→ source ≡ fmap' ] + -- p = {!!} + rawEq : Functor.raw (K.Monad.R (forth m)) ≡ Functor.raw R + rawEq = RawFunctor≡ ℂ ℂ {x = left} {right} refl λ fmap' → {!rawEq→!} + Req : M.RawMonad.R (backRaw (forth m)) ≡ R + Req = FunctorEq rawEq + + ηeq : M.RawMonad.η (backRaw (forth m)) ≡ η + ηeq = {!!} + postulate ηNatTransEq : {!!} [ M.RawMonad.ηNatTrans (backRaw (forth m)) ≡ ηNatTrans ] + open NaturalTransformation ℂ ℂ backRawEq : backRaw (forth m) ≡ M.Monad.raw m -- stuck - M.RawMonad.R (backRawEq i) = {!!} - M.RawMonad.ηNatTrans (backRawEq i) = {!!} + M.RawMonad.R (backRawEq i) = Req i + M.RawMonad.ηNatTrans (backRawEq i) = let t = NaturalTransformation≡ F.identity R ηeq in {!t i!} M.RawMonad.μNatTrans (backRawEq i) = {!!} backeq : (m : M.Monad) → back (forth m) ≡ m diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index 8de0f34..f9ac434 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -23,6 +23,7 @@ open import Agda.Primitive open import Data.Product open import Cubical +open import Cubical.NType.Properties open import Cat.Category open import Cat.Category.Functor hiding (identity) @@ -48,17 +49,13 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level} NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd') NaturalTransformation = Σ Transformation Natural - -- TODO: Since naturality is a mere proposition this principle can be - -- simplified. + -- Think I need propPi and that arrows are sets + postulate propIsNatural : (θ : _) → isProp (Natural θ) + 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 ]) - (α .proj₂) (β .proj₂)) → α ≡ β - NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i + NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq identityTrans : (F : Functor ℂ 𝔻) → Transformation F F identityTrans F C = 𝟙 𝔻 diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index baf298b..abd76d0 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -16,14 +16,14 @@ open Equality.Data.Product open import Cat.Categories.Cat using (RawCat) module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat ℓ ℓ)) where - open import Cat.Categories.Fun - open import Cat.Categories.Sets - module Cat = Cat.Categories.Cat - open import Cat.Category.Exponential - open Functor - 𝓢 = Sets ℓ - open Fun (opposite ℂ) 𝓢 private + open import Cat.Categories.Fun + open import Cat.Categories.Sets + module Cat = Cat.Categories.Cat + open import Cat.Category.Exponential + open Functor + 𝓢 = Sets ℓ + open Fun (opposite ℂ) 𝓢 Catℓ : Category _ _ Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable} prshf = presheaf {ℂ = ℂ}