Mercurial > hg > Members > kono > Proof > category

changeset 454:2f07f4dd9a6d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 13:25:05 +0900
parents 3c2ce4474d92
children 55a9b6177ed4
files discrete.agda negnat.agda
diffstat 2 files changed, 11 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- 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}  = {!!}
--- 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) =  ⊥