fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Make postulate

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-01 14:58:49 +01:00
parent ae46a48861
commit ff2952e9ad
1 changed files with 8 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Cat/Category/Monad.agda
View file

@ -76,14 +76,13 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
isDistributive {X} {Y} {Z} g f = sym done isDistributive {X} {Y} {Z} g f = sym done
where where
module R² = Functor F[ R ∘ R ] module R² = Functor F[ R ∘ R ]
distrib : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B} postulate
→ R.func→ (a ∘ b ∘ c) distrib : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
≡ R.func→ a ∘ R.func→ b ∘ R.func→ c → R.func→ (a ∘ b ∘ c)
distrib = {!!} ≡ R.func→ a ∘ R.func→ b ∘ R.func→ c
comm : ∀ {A B C D E} comm : ∀ {A B C D E}
→ {a : Arrow D E} {b : Arrow C D} {c : Arrow B C} {d : Arrow A B} → {a : Arrow D E} {b : Arrow C D} {c : Arrow B C} {d : Arrow A B}
→ a ∘ (b ∘ c ∘ d) ≡ a ∘ b ∘ c ∘ d → a ∘ (b ∘ c ∘ d) ≡ a ∘ b ∘ c ∘ d
comm = {!!}
lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z) lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z)
lemmm = isAssociative lemmm = isAssociative
lem4 : μ (R.func* Z) ∘ R².func→ g ≡ R.func→ g ∘ μ Y lem4 : μ (R.func* Z) ∘ R².func→ g ≡ R.func→ g ∘ μ Y
@ -110,8 +109,7 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
Monad.isMonad (Monad≡ {m} {n} eq i) = res i Monad.isMonad (Monad≡ {m} {n} eq i) = res i
where where
-- TODO: PathJ nightmare + `propIsMonad`. -- TODO: PathJ nightmare + `propIsMonad`.
res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ] postulate res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
res = {!!}
-- "A monad in the Kleisli form" [voe] -- "A monad in the Kleisli form" [voe]
module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where