# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1488428705 -32400
# Node ID 2f07f4dd9a6dcf53014190801b2c5f128f0d2c49
# Parent  3c2ce4474d92336e04d812ba1f592ae4a5ba9c40
fix

diff -r 3c2ce4474d92 -r 2f07f4dd9a6d discrete.agda
--- a/discrete.agda	Thu Mar 02 11:36:31 2017 +0900
+++ b/discrete.agda	Thu Mar 02 13:25:05 2017 +0900
@@ -141,12 +141,17 @@
           fmap  h | t0 | t1 | arrow-f = f
           fmap  h | t0 | t1 | arrow-g = g
           ≈-cong :  {a : Obj A} {b : Obj A} {f g : Hom A a b}  → A [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
-          ≈-cong  = {!!}
-          identity :  (x : Obj A) → A [ fmap ( id1 A x ) ≈  id1 A (fobj x) ]
-          identity x  =  {!!}
-          -- identity x  with obj→ x
-          -- identity _  | t0 = ?
-          -- identity _  | t1 = ?
+          ≈-cong  {a} {b} {f} {g}  f≈g = {!!}
+          identity : (x : Obj A ) ->  A [ {!!} ≈ {!!} ] -- {!!} -- A [ fmap (id1 A x) ≈  id1 A (fobj x) ]
+          identity x with obj→ x 
+          identity x  | t0 =  let open ≈-Reasoning (A) in begin
+                 fmap (id1 A x)
+              ≈⟨ {!!} ⟩
+                 id1 A {!!}
+              ≈⟨⟩
+                 id1 A (fobj x )
+              ∎
+          identity _  | t1  =  let open ≈-Reasoning (A) in {!!}
           distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} →
                A [ fmap (A [ g o f ])  ≈  A [ fmap g o fmap f ] ]
           distr1  {a} {b} {c} {f} {g}  = {!!}
diff -r 3c2ce4474d92 -r 2f07f4dd9a6d negnat.agda
--- a/negnat.agda	Thu Mar 02 11:36:31 2017 +0900
+++ b/negnat.agda	Thu Mar 02 13:25:05 2017 +0900
@@ -61,7 +61,6 @@
 
 
 --  http://stackoverflow.com/questions/18347542/agda-how-does-one-obtain-a-value-of-a-dependent-type
-
 even : ℕ -> Set
 even zero = ⊤
 even (suc zero) =  ⊥