Mercurial > hg > Members > kono > Proof > category

changeset 453:3c2ce4474d92

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
try incomplete pattern for discrete
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 11:36:31 +0900
parents 7ed0045e4adf
children 2f07f4dd9a6d
files discrete.agda negnat.agda
diffstat 2 files changed, 83 insertions(+), 255 deletions(-) [+]
line wrap: on
line diff
--- a/discrete.agda	Tue Feb 28 22:33:03 2017 +0900
+++ b/discrete.agda	Thu Mar 02 11:36:31 2017 +0900
@@ -3,12 +3,13 @@
 
 module discrete where
 
-open import cat-utility
-open import HomReasoning
 open import Relation.Binary.Core
 open import Relation.Nullary
 open import Data.Empty
+open import Data.Unit
 open import Data.Maybe
+open import cat-utility
+open import HomReasoning
 
 open Functor
 
@@ -33,83 +34,21 @@
 
 record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁}  ) : Set ( c₂)  where
    field
-       hom   :  Maybe ( Arrow {c₁} {c₂} a b )
-   constraint1 :  {c₁ c₂ : Level } → TwoObject {c₁}  → TwoObject {c₁} → Maybe (  ⊥   )
-   constraint1 t0 t0  = nothing
-   constraint1 {c₁} {c₂} t1 t0  = just ( {!!}  )
-   constraint1 t0 t1  = nothing
-   constraint1 t1 t1  = nothing
+       hom   :  Arrow {c₁} {c₂} a b 
 
-comp :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  Maybe ( Arrow {c₁} {c₂} b c ) →  Maybe ( Arrow {c₁} {c₂} a b )  →  Maybe ( Arrow {c₁} {c₂} a c )
-comp {_}  {_}  {_} {_} {_}  nothing     _                =   nothing 
-comp {_}  {_}  {_} {_} {_}  (just _     ) nothing          =   nothing 
-comp {_}  {_}  {t0} {t1} {t1}  (just id-t1 ) ( just arrow-f )  =   just arrow-f 
-comp {_}  {_}  {t0} {t1} {t1}  (just id-t1 ) ( just arrow-g ) =   just arrow-g 
-comp {_}  {_}  {t1} {t1} {t1}  (just id-t1 ) ( just id-t1   ) =   just id-t1 
-comp {_}  {_}  {t0} {t0} {t1}  (just arrow-f ) ( just id-t0 )   =   just arrow-f 
-comp {_}  {_}  {t0} {t0} {t1}  (just arrow-g ) ( just id-t0 )   =   just arrow-g 
-comp {_}  {_}  {t0} {t0} {t0}  (just id-t0 ) ( just id-t0  )  =   just id-t0 
-comp {_}  {_}  {_} {_} {_}  (just _ ) ( just _ )  =   nothing 
+comp :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  Arrow {c₁} {c₂} b c  →  Arrow {c₁} {c₂} a b   →  Arrow {c₁} {c₂} a c 
+comp {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-f   =   arrow-f 
+comp {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-g  =   arrow-g 
+comp {_}  {_}  {t1} {t1} {t1}  id-t1   id-t1    =   id-t1 
+comp {_}  {_}  {t0} {t0} {t1}  arrow-f   id-t0    =   arrow-f 
+comp {_}  {_}  {t0} {t0} {t1}  arrow-g   id-t0    =   arrow-g 
+comp {_}  {_}  {t0} {t0} {t0}  id-t0   id-t0    =   id-t0 
 
 open TwoHom
 
 _×_ :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  ( TwoHom {c₁}  {c₂} b c ) →  ( TwoHom {c₁} {c₂} a b )  →  ( TwoHom {c₁}  {c₂} a c )
 _×_  {c₁}  {c₂}  {a} {b} {c} f g  = record { hom = comp  {c₁}  {c₂}  {a} {b} {c} (hom f) (hom g ) }
 
-_==_ :  ∀{ c₁ c₂ a b }   →  Rel (Maybe (Arrow {c₁} {c₂} a b )) (c₂)
-_==_   =  Eq   _≡_
-
-==refl :  ∀{  c₁ c₂ a b }  →  ∀ {x : Maybe (Arrow  {c₁} {c₂} a b )} → x == x
-==refl {_} {_} {_} {_} {just x}  = just refl
-==refl {_} {_} {_} {_} {nothing} = nothing
-
-==sym :  ∀{  c₁ c₂ a b }   → ∀ {x y :  Maybe (Arrow  {c₁}  {c₂}  a b )} →  x == y →  y == x
-==sym (just x≈y) = just (≡-sym x≈y)
-==sym nothing    = nothing
-
-==trans :  ∀{  c₁ c₂ a b }   → ∀ {x y z :   Maybe (Arrow  {c₁}  {c₂}  a b )  } →
-         x == y → y == z  → x == z
-==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z)
-==trans nothing    nothing    = nothing
-
-==cong :  ∀{  c₁ c₂ a b c d }   → ∀ {x y :  Maybe (Arrow  {c₁}  {c₂}  a b )} →  
-        (f : Maybe (Arrow  {c₁}  {c₂}  a b ) → Maybe (Arrow  {c₁}  {c₂}  c d ) ) → x  ==  y →  f x == f y
-==cong   {  c₁} {c₂} {a} {b } {c} {d} {nothing} {nothing} f nothing = ==refl
-==cong   {  c₁} {c₂} {a} {b } {c} {d} {just x} {just .x} f (just refl)  = ==refl
-
-
-module ==-Reasoning {c₁ c₂ : Level} where
-
-        infixr  2 _∎
-        infixr 2 _==⟨_⟩_ _==⟨⟩_
-        infix  1 begin_
-
-
-        data _IsRelatedTo_   {c₁ c₂ : Level}  {a b : TwoObject {c₁}  }  (x y : (Maybe (Arrow  {c₁}  {c₂}  a b ))) :
-                             Set  c₂ where
-            relTo : (x≈y : x  == y  ) → x IsRelatedTo y
-
-        begin_ :  { a b : TwoObject  {c₁} } {x : Maybe (Arrow  {c₁}  {c₂}  a b ) } {y : Maybe (Arrow  {c₁}  {c₂}  a b )} →
-                   x IsRelatedTo y →  x ==  y
-        begin relTo x≈y = x≈y
-
-        _==⟨_⟩_ :  { a b : TwoObject  {c₁} } (x :  Maybe (Arrow  {c₁}  {c₂}  a b )) {y z :  Maybe (Arrow  {c₁}  {c₂}  a b ) } →
-                    x == y  → y IsRelatedTo z → x IsRelatedTo z
-        _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z)
-
-        
-        _==⟨⟩_ :   { a b : TwoObject  {c₁} }(x : Maybe (Arrow  {c₁}  {c₂}  a b )) {y : Maybe (Arrow  {c₁}  {c₂}  a b  )}
-                    → x IsRelatedTo y → x IsRelatedTo y
-        _ ==⟨⟩ x≈y = x≈y
-
-        _∎ :   { a b : TwoObject  {c₁} }(x :  Maybe (Arrow  {c₁}  {c₂}  a b )) → x IsRelatedTo x
-        _∎ _ = relTo ==refl
-
-
--- TwoHom1Eq :  {c₁  c₂ : Level } {a b : TwoObject  {c₁} } {f g :  ( TwoHom1 {c₁}  {c₂ } a b)}  →
---             hom (Map f) == hom (Map g) → f == g
--- TwoHom1Eq  = ?
-
 
 --          f    g    h
 --       d <- c <- b <- a
@@ -120,126 +59,73 @@
        {f : (TwoHom {c₁}  {c₂ } c d )} →
        {g : (TwoHom {c₁}  {c₂ } b c )} →
        {h : (TwoHom {c₁}  {c₂ } a b )} →
-       hom ( f × (g × h)) == hom ((f × g) × h )
+       hom ( f × (g × h)) ≡ hom ((f × g) × h )
 assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with  hom f | hom g | hom h
-assoc-× {c₁} {c₂} {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ = nothing
-assoc-× {c₁} {c₂} {_} {_} {_} {_} {f} {g} {h} | just _ | nothing | _ = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0   | just id-t0   | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0   | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0   | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1   | just arrow-f | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1   | just arrow-g | just id-t0  = ==refl
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just arrow-f = ==refl
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just arrow-g = ==refl
-assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1   | just id-t1   | just id-t1  = ==refl
---  remaining all failure case 
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
-assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing
-assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing
-assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
-assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
-assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
-assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing
-assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-f) | (just id-t0) = nothing
-assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-g) | (just id-t0) = nothing
-assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
-assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
-assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-f) | (just _) = nothing
-assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-g) | (just _) = nothing
-assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
-assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing
-assoc-× {_} {_} {t1} {t0} {t0} {t0} {_} {_} {_} | (just id-t0) | (just id-t0) | (just _) = nothing
-assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just id-t0) | (just _) = nothing
-assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just id-t0) | (just _) = nothing
-assoc-× {_} {_} {t1} {t1} {t0} {_} {_} {_} {_} | (just _) | (just _) | (just _) = nothing
-assoc-× {_} {_} {t1} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) |  nothing = nothing
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0   | id-t0   | id-t0  = refl
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0   | id-t0  = refl
+assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0   | id-t0  = refl
+assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1   | arrow-f | id-t0  = refl
+assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1   | arrow-g | id-t0  = refl
+assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1   | id-t1   | arrow-f = refl
+assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1   | id-t1   | arrow-g = refl
+assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1   | id-t1   | id-t1  = refl
 
 TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) →  (TwoHom {c₁}  {c₂ } a a )
-TwoId {_} {_} t0 = record { hom =  just id-t0 }
-TwoId {_} {_} t1 = record { hom =  just id-t1 }
+TwoId {_} {_} t0 = record { hom =  id-t0 }
+TwoId {_} {_} t1 = record { hom =  id-t1 }
 
 open import Relation.Binary
+open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
+
 TwoCat : {c₁ c₂ ℓ : Level  } →  Category   c₁  c₂  c₂
 TwoCat   {c₁}  {c₂} {ℓ} = record {
     Obj  = TwoObject  {c₁} ;
     Hom = λ a b →    ( TwoHom {c₁}  {c₂ } a b ) ;
     _o_ =  λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
-    _≈_ =  λ x y → hom x == hom y ;
+    _≈_ =  λ x y → hom x  ≡ hom y ;
     Id  =  λ{a} → TwoId {c₁ } { c₂} a ;
     isCategory  = record {
-            isEquivalence =  record {refl = ==refl ; trans = ==trans ; sym = ==sym } ;
+            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
             identityL  = λ{a b f} → identityL {c₁}  {c₂ } {a} {b} {f} ;
             identityR  = λ{a b f} → identityR {c₁}  {c₂ } {a} {b} {f} ;
             o-resp-≈  = λ{a b c f g h i} →  o-resp-≈  {c₁}  {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
             associative  = λ{a b c d f g h } → assoc-×   {c₁}  {c₂} {a} {b} {c} {d} {f} {g} {h}
        }
    }  where
-        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  hom ((TwoId B)  × f)  == hom f
-        identityL  {c₁}  {c₂}  {a} {b} {f}  with hom f | constraint1 f a b
-        identityL  {c₁}  {c₂}  {t1} {t0} {f} | _  | just C = ⊥-elim C
-        identityL  {c₁}  {c₂}  {t1} {t0} {_} | just _ | nothing = {!!}
-        identityL  {c₁}  {c₂}  {t0} {t0} {_} | nothing  | _ = nothing
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | nothing  | _ = nothing
-        identityL  {c₁}  {c₂}  {t1} {t0} {_} | nothing  | _ = nothing
-        identityL  {c₁}  {c₂}  {t1} {t1} {_} | nothing  | _ = nothing
-        identityL  {c₁}  {c₂}  {t1} {t1} {_} | just id-t1  | _ = ==refl
-        identityL  {c₁}  {c₂}  {t0} {t0} {_} | just id-t0 | _ = ==refl
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-f | _ = ==refl
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g | _ = ==refl
-        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   hom ( f × TwoId A )  == hom f
+        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  hom ((TwoId B)  × f)  ≡ hom f
+        identityL  {c₁}  {c₂}  {a} {b} {f} with hom f
+        identityL  {c₁}  {c₂}  {t1} {t1} | id-t1 = refl
+        identityL  {c₁}  {c₂}  {t0} {t0} | id-t0 = refl
+        identityL  {c₁}  {c₂}  {t0} {t1} | arrow-f = refl
+        identityL  {c₁}  {c₂}  {t0} {t1} | arrow-g = refl
+        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   hom ( f × TwoId A )  ≡ hom f
         identityR  {c₁}  {c₂}  {_} {_} {f}  with hom f
-        identityR  {c₁}  {c₂}  {t0} {t0} {_} | nothing  = nothing 
-        identityR  {c₁}  {c₂}  {t0} {t1} {_} | nothing  = nothing
-        identityR  {c₁}  {c₂}  {t1} {t0} {_} | nothing  = nothing
-        identityR  {c₁}  {c₂}  {t1} {t1} {_} | nothing  = nothing
-        identityR  {c₁}  {c₂}  {t1} {t1} {_} | just id-t1  = ==refl
-        identityR  {c₁}  {c₂}  {t0} {t0} {_} | just id-t0 = ==refl
-        identityR  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-f = ==refl
-        identityR  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g = ==refl
-        identityR  {c₁}  {c₂}  {t1} {t0} {_} | just _  = {!!}
+        identityR  {c₁}  {c₂}  {t1} {t1} | id-t1  = refl
+        identityR  {c₁}  {c₂}  {t0} {t0} | id-t0 = refl
+        identityR  {c₁}  {c₂}  {t0} {t1} | arrow-f = refl
+        identityR  {c₁}  {c₂}  {t0} {t1} | arrow-g = refl
         o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
-            hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g )
+            hom f  ≡ hom g → hom h  ≡ hom i → hom ( h × f )  ≡ hom ( i × g )
         o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {g} {h} {i}  f==g h==i  = 
-          let open  ==-Reasoning {c₁} {c₂ } in begin
+          let open  ≡-Reasoning in begin
                     hom ( h × f )
-                ==⟨⟩
+                ≡⟨ refl ⟩
                     comp (hom h) (hom f)
-                ==⟨ ==cong (λ x  → comp ( hom h ) x )  f==g ⟩
+                ≡⟨ cong (λ x  → comp ( hom h ) x )  f==g ⟩
                     comp (hom h) (hom g)
-                ==⟨ ==cong (λ x  → comp x ( hom g ) )  h==i ⟩
+                ≡⟨ cong (λ x  → comp x ( hom g ) )  h==i ⟩
                     comp (hom i) (hom g)
-                ==⟨⟩
+                ≡⟨ refl ⟩
                     hom ( i × g )
                 ∎
 
-
-
-
-record  Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  :  Set   ( c₁ ⊔ c₂ ⊔ ℓ ) where 
-     field 
-         nil : {a b : Obj A } → Hom A a b
-         nil-id : {a  : Obj A } →  A [ nil {a} {a} ≈ id1 A a ]    -- too strong but we need this
-         nil-idL : {a b c : Obj A } → { f : Hom A a b } → A [ A [ nil {b} {c} o f ]   ≈ nil {a} {c} ]
-         nil-idR : {a b c : Obj A } → { f : Hom A b c } → A [ A [ f o nil {a} {b} ]   ≈ nil {a} {c} ]
-
-open Nil
-
-indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) →  
-    (obj : Obj A -> TwoObject {c₁}) (hom→ : {a b : Obj A} -> Hom A a b -> TwoObject {c₁})  → Functor A A
-indexFunctor  {c₁} {c₂} {ℓ} A none a b f g obj→ hom→ = record {
+indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  
+    (obj→ : Obj A -> TwoObject {c₁}) (hom→ : {a b : Obj A} -> Hom A a b -> TwoHom  {c₁} {c₂} (obj→ a) (obj→ b) )  → Functor A A
+indexFunctor  {c₁} {c₂} {ℓ} A a b f g obj→ hom→ = record {
          FObj = λ a → fobj a
        ; FMap = λ {a} {b} f → fmap {a} {b} f
        ; isFunctor = record {
-             identity = λ{x} → identity {x}
+             identity = λ{x} → identity x
              ; distr = λ {a} {b} {c} {f} {g}   → distr1 {a} {b} {c} {f} {g}
              ; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
        }
@@ -249,62 +135,23 @@
           fobj x | t0 = a
           fobj x | t1 = b
           fmap :  {x y : Obj A } →  (Hom A x y  ) → Hom A (fobj x) (fobj y)
-          fmap  {x} {y} h with obj→ x | obj→ y | hom→ h
-          fmap  h | t0 | t0 | _ = id1 A a
-          fmap  h | t1 | t1 | _ = id1 A b
-          fmap  h | t0 | t1 | t0 = f
-          fmap  h | t0 | t1 | t1 = g
-          fmap  h | _  | _  | _   = nil none
-          open  ≈-Reasoning A
-          ≈-cong :   {a : Obj A} {b : Obj A} {f g : Hom A a b}  → A [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
+          fmap  {x} {y} h with obj→ x | obj→ y | hom ( hom→ h )
+          fmap  h | t0 | t0 | id-t0 = id1 A a
+          fmap  h | t1 | t1 | id-t1 = id1 A b
+          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} with obj→ x
-          identity | t0  =  refl-hom
-          identity | t1  =  refl-hom
-          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 {a1} {b1} {c1} {f1} {g1} with obj→ a1 | obj→ b1 | obj→ c1 | hom→ f1 | hom→ g1 
-          distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t0 | t0 | _ | _ = begin
-                    id1 A a
-                ≈↑⟨ idL ⟩
-                    id1 A a o id1 A a
-                ∎
-          distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t1 | t1 | _ | _ = begin
-                    id1 A b
-                ≈↑⟨ idL ⟩
-                    id1 A b o id1 A b
-                ∎
-          distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t0 | t0 | _ | _ = begin
-                    nil none
-                ≈↑⟨ nil-idR none ⟩
-                    id1 A a o nil none
-                ∎
-          distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t1 | t0 | _ | _ = begin
-                    nil none
-                ≈↑⟨ nil-idL none ⟩
-                    nil none o id1 A b
-                ∎
-          distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t1 | t0 | _ | _ = begin
-                    id1 A a
-                ≈↑⟨ nil-id none ⟩
-                    nil none
-                ≈↑⟨ nil-idL none ⟩
-                    nil none o _
-                ∎
-          distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t0 | t1 | _ | _ = begin
-                    id1 A b
-                ≈↑⟨ nil-id none ⟩
-                    nil none
-                ≈↑⟨ nil-idR none ⟩
-                    _ o nil none
-                ∎
-          distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t0 | t1 | _ | _ =  begin
-                    {!!}
-                ≈⟨ {!!} ⟩
-                    {!!} o id1 A a
-                ∎
-          distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t1 | t1 | _ | _ = {!!}
+          identity :  (x : Obj A) → A [ fmap ( id1 A x ) ≈  id1 A (fobj x) ]
+          identity x  =  {!!}
+          -- identity x  with obj→ x
+          -- identity _  | t0 = ?
+          -- identity _  | t1 = ?
+          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}  = {!!}
+          -- distr1  {a} {b} {c} {f} {g}  with   (obj→ a) | (obj→ b ) | ( obj→ c ) | (  hom→  f ) | (  hom→  g ) 
+          -- distr1  {a} {b} {c} {f} {g}  | _ | _ | _ | _ | _ = ?
 
 
 
@@ -355,31 +202,13 @@
          eqlim = isLimit comp Γ
          c = {!!}
          e = {!!}
-         k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
-         k {d} h fh=gh  = {!!}
-         ek=h :  (d : Obj A ) (h : Hom A d a ) →  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  → A [ A [ e o k h fh=gh ] ≈ h ]
-         ek=h d h fh=gh =   begin
-                    e o k h fh=gh
-                ≈⟨ {!!}  ⟩
-                    h
-                ∎
-         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ]
-         uniq-nat  d h k' ek'=h =  begin
-                    {!!} o k'
-                ≈⟨⟩
-                    e o k'
-                ≈⟨ ek'=h ⟩
-                    h
-                ≈⟨⟩
-                    {!!}
-                ∎
-         uniquness :  (d : Obj A ) (h : Hom A d a ) →  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  →
+         k : {d : Obj A}  (h : Hom A d a) → {!!} -- A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
+         k = {!!} -- {d} h fh=gh  = {!!}
+         ek=h :  (d : Obj A ) (h : Hom A d a ) →  {!!} -- ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  → A [ A [ e o k h fh=gh ] ≈ h ]
+         ek=h = {!!} 
+         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c ) → {!!} -- A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ]
+         uniq-nat  = {!!}
+         uniquness :  (d : Obj A ) (h : Hom A d a ) →  ?　→ -- ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  →
                  ( k' : Hom A d c )
-                → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
-         uniquness d h fh=gh k' ek'=h =   begin
-                    k h fh=gh
-                ≈⟨  {!!}  ⟩
-                    k'
-                ∎
-
-
+                → {!!} -- A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
+         uniquness = {!!}
--- a/negnat.agda	Tue Feb 28 22:33:03 2017 +0900
+++ b/negnat.agda	Thu Mar 02 11:36:31 2017 +0900
@@ -49,13 +49,13 @@
 Fin-elim P s z fzero    = z
 Fin-elim P s z (fsuc x) = s (Fin-elim P s z x)
 
-Nope0 : ℕ → Set
-Nope0 = ℕ-elim (λ _ → Set) (λ _ → ⊤) ⊥
-
 Nope1  :  ℕ  -> Set 
 Nope1 zero    = ⊥
 Nope1 (suc _) = ⊤
 
+Nope0 : ℕ → Set
+Nope0 = ℕ-elim (λ _ → Set) (λ _ → ⊤) ⊥
+
 bad : Fin 0 → ⊥
 bad = Fin-elim (λ n _ → Nope0 n) (λ _ → _) _
 
@@ -88,7 +88,7 @@
 
 isEven : EvenDecidable
 isEven zero          = yes _
-isEven (suc zero)    = no λ ()
+isEven (suc zero)    = no (λ ())
 isEven (suc (suc n)) = isEven n
 
 data Bool : Set where
@@ -148,13 +148,6 @@
 mod (suc zero) = suc zero
 mod (suc (suc N)) = mod N
 
-lemma1 : { n :  ℕ } -> mod (suc (suc n ))  ≡  mod n
-lemma1 = refl
-
-lemma2 : { n :  ℕ } -> isEven (suc (suc n ))  ≡  isEven n
-lemma2 = refl
-
-
 proof1 : (n :  ℕ ) -> ( if ⌊ isEven n ⌋  then zero else (suc zero)  )  ≡ ( mod n )
 proof1 zero =  refl
 proof1 (suc zero) = refl
@@ -167,6 +160,12 @@
        mod n
    ≡⟨ sym (lemma1 {n}) ⟩
        mod (suc (suc n))
-   ∎
+   ∎ where
+        lemma1 : { n :  ℕ } -> mod (suc (suc n ))  ≡  mod n
+        lemma1 = refl
+        lemma2 : { n :  ℕ } -> isEven (suc (suc n ))  ≡  isEven n
+        lemma2 = refl
 
 
+
+