More stuff about kleisli \equiv monoidal

2018-03-05 10:28:16 +01:00 · 2018-03-05 10:28:16 +01:00 · 8f8800cb67
parent b079f5e426
commit 8f8800cb67
7 changed files with 166 additions and 73 deletions
--- 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
--- 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ℂ
--- 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
--- 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
--- 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
--- 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 = 𝟙 𝔻
--- 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 {ℂ = ℂ}