Mercurial > hg > Members > kono > Proof > category

changeset 6:b1fd8d8689a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add accessor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Jul 2013 16:28:26 +0900
parents 16572013c362
children 79d9c30e995a
files nat.agda
diffstat 1 files changed, 7 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sat Jul 06 14:56:23 2013 +0900
+++ b/nat.agda	Sat Jul 06 16:28:26 2013 +0900
@@ -69,6 +69,10 @@
 
 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NNAT A A identityFunctor T) (μ : NNAT A A (T ○ T) T)
        : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+  eta : NNAT A A identityFunctor T
+  eta = η
+  mu : NNAT A A (T ○ T) T
+  mu = μ
   field
     isMonad : IsMonad A T η μ
 
@@ -136,7 +140,7 @@
                  { M : Monad A T η μ } 
                  ( K : Kleisli A T η μ M) 
                       -> A  [ join K b (NAT η b) f  ≈ f ]
-Lemma7 m = {!!}
+Lemma7 k = {!!}
 
 Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
@@ -147,7 +151,7 @@
                  { M : Monad A T η μ } 
                  ( K : Kleisli A T η μ M) 
                       -> A  [ join K b f (NAT η a)  ≈ f ]
-Lemma8 m = {!!}
+Lemma8 k = ?
 
 Lemma9 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
@@ -160,7 +164,7 @@
                  { M : Monad A T η μ } 
                  ( K : Kleisli A T η μ M) 
                       -> A  [ join K d h (join K c g f)  ≈ join K d ( join K d h g) f ]
-Lemma9 m = {!!}
+Lemma9 k = {!!}