Mercurial > hg > Members > kono > Proof > category

changeset 400:89785764bccb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 17 Mar 2016 08:34:10 +0900
parents 8304007dc2f8
children e4c10d6375f6
files limit-to.agda
diffstat 1 files changed, 20 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Thu Mar 17 08:07:38 2016 +0900
+++ b/limit-to.agda	Thu Mar 17 08:34:10 2016 +0900
@@ -37,25 +37,26 @@
 
 open RawHom
 
-arrow2hom :  {c₁ ℓ : Level}  -> {a : TwoObject {c₁}  } {b : TwoObject {c₁}  } -> Arrow  {ℓ } -> RawHom  { c₁}  {ℓ } a b
-arrow2hom f =  record { RawMap = f } 
-
 record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
    field
-      hom : RawHom { c₁}  {ℓ } a b
-      arrow-iso : arrow2hom ( RawMap hom )  ≡ hom
-   Map : Arrow
-   Map = RawMap hom
+      hom : Maybe ( RawHom { c₁}  {ℓ } a b )
+
+open  Two-Hom 
+
+Map :  {c₁ ℓ : Level } -> (a b : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a b -> Maybe ( Arrow  {ℓ } )
+Map f with hom f
+Map f | nothing = nothing
+Map _ | just f = RawMap f
 
 Two-id :  {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a a 
 Two-id _  = record { hom = record { RawMap = id-t0 } ;   arrow-iso = refl }
 
 -- arrow composition
 
-twocomp :  {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Arrow {ℓ } 
-twocomp id-t0  f  = f
-twocomp f id-t0 = f
-twocomp _ _ = nil
+twocomp :  {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Maybe (Arrow {ℓ } )
+twocomp id-t0  f  = just f
+twocomp f id-t0 = just f
+twocomp _ _ = nothing
 
 twocmp-associative :  {ℓ : Level } -> ( f : Arrow {ℓ } ) -> ( g : Arrow {ℓ } ) -> ( h : Arrow {ℓ } ) →  twocomp f  (twocomp g  h)  ≡  twocomp (twocomp f  g)  h 
 twocmp-associative id-t0 _ _ = refl
@@ -101,18 +102,15 @@
 
 
 _×_ :  { 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 =  arrow ;
-                    arrow-iso =  arrow-iso   (RawMap arrow  ) }
+_×_   { c₁} {ℓ} {a} {b} {c} f g  with hom f | hom g
+_×_   { c₁} {ℓ} {a} {b} {c} f g  | nothing | _ = record { hom = nothing }
+_×_   { c₁} {ℓ} {a} {b} {c} f g  | _ | nothig = record { hom = nothing }
+_×_   { c₁} {ℓ} {a} {b} {c} _ _ | just f | just g  = comp f g
    where
-      arrow  =   arrow2hom {c₁ } {ℓ } {a} {c} ( twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g)  ) 
-      arrow-iso : (f : Arrow { ℓ} ) -> 
-             arrow2hom {c₁} {ℓ } {a} {c} f ≡ record { RawMap = f }
-      arrow-iso   id-t0 = refl
-      arrow-iso  arrow-f = refl
-      arrow-iso  arrow-g = refl
-      arrow-iso  nil = refl
-
-open Two-Hom
+      comp  :  {a c : TwoObject {c₁}} (f : Arrow {ℓ}) -> (g : Arrow {ℓ}) ->  Two-Hom { c₁}  {ℓ}  a c
+      comp  f g with ( twocomp  {ℓ} ( RawMap f) ( RawMap g)  ) 
+      comp  f g | nothing = record { hom = nothing }
+      comp  f g | just h = record { hom = record { RawMap = h } }
 
 
 TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  (ℓ ⊔ c₁)  ℓ