# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1373095706 -32400
# Node ID b1fd8d8689a96fe0df0725454a087e8dbe008200
# Parent  16572013c362c10be3dc513eca88c912b9edc217
add accessor

diff -r 16572013c362 -r b1fd8d8689a9 nat.agda
--- 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 = {!!}