Mercurial > hg > Members > kono > Proof > category

changeset 390:1301270b8942

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
null does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 15 Mar 2016 11:45:43 +0900
parents 79c7ab66152b
children 2ee1496b31d7
files limit-to.agda
diffstat 1 files changed, 21 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Tue Mar 15 10:52:39 2016 +0900
+++ b/limit-to.agda	Tue Mar 15 11:45:43 2016 +0900
@@ -35,15 +35,16 @@
 record RawHom {c₁ ℓ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set  (c₁  ⊔ ℓ) where
    field
        RawMap    : Arrow  {ℓ }
+       isNull    : TwoObject  {c₁}
 
 open RawHom
 
 arrow2hom :  {c₁ ℓ : Level}  -> (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) -> Arrow  {ℓ } -> RawHom  { c₁}  {ℓ } a b
-arrow2hom t0 t0 id-t0 =  record { RawMap = id-t0  } 
-arrow2hom t1 t1 id-t1 =  record { RawMap = id-t1  } 
-arrow2hom t0 t1 arrow-f =  record { RawMap = arrow-f } 
-arrow2hom t0 t1 arrow-g =  record { RawMap = arrow-g  } 
-arrow2hom _ _ _  =  record { RawMap = nil  } 
+arrow2hom t0 t0 id-t0 =  record { RawMap = id-t0 ; isNull = t0  } 
+arrow2hom t1 t1 id-t1 =  record { RawMap = id-t1 ; isNull = t0  } 
+arrow2hom t0 t1 arrow-f =  record { RawMap = arrow-f ; isNull = t0 } 
+arrow2hom t0 t1 arrow-g =  record { RawMap = arrow-g ; isNull = t0  } 
+arrow2hom _ _ f  =  record { RawMap = f ; isNull = t1  } 
 
 record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
    field
@@ -53,13 +54,13 @@
    Map = RawMap hom
 
 Two-id :  {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a a 
-Two-id t0  = record { hom = record { RawMap = id-t0  } ;  arrow-iso = refl }
-Two-id t1  = record { hom = record { RawMap = id-t1  } ;  arrow-iso = refl }
+Two-id t0  = record { hom = record { isNull = t0 ;RawMap = id-t0  } ;   arrow-iso = refl }
+Two-id t1  = record { hom = record { isNull = t0 ;RawMap = id-t1  } ;   arrow-iso = refl }
 
 Two-nothing : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> Two-Hom  {c₁} { ℓ} a b
 Two-nothing a b  = record { hom = record { RawMap = nil } ; arrow-iso = arrow-iso  a b }
    where
-      arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> arrow2hom {c₁} {ℓ } a b nil ≡ record { RawMap = nil }
+      arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> arrow2hom {c₁} {ℓ } a b nil ≡ record { RawMap = nil ; isNull = t1 }
       arrow-iso  t0 t0 =  refl
       arrow-iso  t0 t1 =  refl
       arrow-iso  t1 t0 =  refl
@@ -74,19 +75,19 @@
 
 _×_ :  { c₁  ℓ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {ℓ}  B C →  Two-Hom { c₁}  {ℓ}  A B  →  Two-Hom { c₁}  {ℓ}  A C 
 _×_   { c₁} {ℓ} {a} {b} {c} f g  = record { hom = 
-           record { RawMap =     twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g) } ;  
-                    arrow-iso =  arrow-iso a c ( twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g) ) }
+           record { RawMap =     arrow ; isNull = nul } ;  
+                    arrow-iso =  arrow-iso a c ( arrow ) nul }
    where
-      arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> (f : Arrow { ℓ} ) -> arrow2hom {c₁} {ℓ } a b f ≡ record { RawMap = f }
-      arrow-iso t0 t0 id-t0  = refl
-      arrow-iso t1 t1 id-t1  = refl
-      arrow-iso t0 t1 arrow-f  = refl
-      arrow-iso t0 t1 arrow-g  = refl
-      arrow-iso t0 t0 nil  = refl
-      arrow-iso t0 t1 nil  = refl
-      arrow-iso t1 t0 nil  = refl
-      arrow-iso t1 t1 nil  = refl
-      arrow-iso _ _ _  = {!!}
+      arrow  =   twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g) 
+      nul  =   isNull ( arrow2hom a b arrow  )
+      arrow-iso : {c₁ ℓ : Level } -> ( a b : TwoObject  {c₁} ) -> (f : Arrow { ℓ} ) -> ( n : TwoObject {c₁} ) -> 
+             arrow2hom {c₁} {ℓ } a b f  ≡ record { RawMap = f ; isNull = n }
+      arrow-iso t0 t0 id-t0  t0 = refl
+      arrow-iso t1 t1 id-t1  t0 = refl
+      arrow-iso t0 t1 arrow-f  t0 = refl
+      arrow-iso t0 t1 arrow-g  t0 = refl
+      arrow-iso _ _ _  t0 = {!!}
+      arrow-iso _ _ _  t1 = ?
 
 open Two-Hom