--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/maybe-monad.agda	Wed Jul 19 20:38:02 2017 +0900
@@ -0,0 +1,47 @@
+open import Level
+open import Category
+open import Category.Sets
+module maybe-monad  {c : Level} where
+
+open import HomReasoning
+open import cat-utility
+open import Relation.Binary.Core
+
+import Relation.Binary.PropositionalEquality
+-- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
+postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+
+data maybe  (A : Set c) :  Set c where
+    just :  A → maybe A
+    nothing : maybe A
+
+-- Maybe : A → ⊥ + A
+
+A = Sets {c}
+
+Maybe : Functor A A
+Maybe = record {
+      FObj = λ a → maybe a
+    ; FMap = λ {a} {b} f → fmap f
+    ; isFunctor = record {
+             identity = λ {x} → extensionality A ( λ y → identity1 x y )
+             ; distr = λ {a} {b} {c} {f} {g}   → extensionality A ( λ w → distr2 a b c f g w )
+             ; ≈-cong = λ {a} {b} {c} {f} f≡g  → extensionality A ( λ z → ≈-cong1  a b c f z f≡g )
+      }
+  } where
+     fmap : {a b : Obj A} → (f : Hom A a b ) → Hom A (maybe a) (maybe b)
+     fmap f nothing = nothing
+     fmap f (just x) = just (f x)
+     identity1 : (x : Obj A) → (y : maybe x ) → fmap (id1 A x) y ≡ id1 A (maybe x) y
+     identity1 x nothing = refl
+     identity1 x (just y) = refl
+     distr2 : (x y z : Obj A) (f : Hom A x y ) ( g : Hom A y z ) → (w : maybe x) →  fmap (λ w → g (f w)) w  ≡  fmap g ( fmap f w)
+     distr2 x y z f g nothing = refl
+     distr2 x y z f g (just w) = refl
+     ≈-cong1 : (x y : Obj A) ( f g : Hom A x y ) → ( z : maybe x ) → f ≡ g  → fmap f z ≡ fmap g z
+     ≈-cong1 x y f g nothing refl = refl
+     ≈-cong1 x y f g (just z) refl = refl
+
+-- Maybe-η : 1 → A
+
+-- Maybe-μ : AA → A

--- a/yoneda.agda	Sun Jul 16 14:05:18 2017 +0900
+++ b/yoneda.agda	Wed Jul 19 20:38:02 2017 +0900
@@ -311,3 +311,16 @@
 YonedaLemma21 :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a x : Obj A} ( f : ( FObj (FObj (YonedaFunctor A ) a) x) ) →  inv A f  ≡ a
 YonedaLemma21 A {a} {x} f = refl
 
+-- open import  Relation.Binary.HeterogeneousEquality
+-- 
+-- a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
+-- a1 refl = refl
+-- 
+-- YonedaInjective :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A}
+--     → FObj (YonedaFunctor A ) a ≡ FObj (YonedaFunctor A ) b 
+--     → a ≡ b
+-- YonedaInjective A {a} {b} eq = y1 ( ≡-cong ( λ k → FObj k a) eq ) 
+--   where
+--     y1 : Hom A a a ≡ Hom A a b  → a ≡ b
+--     y1 eq = {!!}
+