Mercurial > hg > Members > kono > Proof > category

changeset 382:813cf2e2bd1a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
maybe map
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Mar 2016 12:29:42 +0900
parents 1ae9a3fcb0ee
children 2a27ab008299
files limit-to.agda
diffstat 1 files changed, 60 insertions(+), 46 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sun Mar 13 02:11:50 2016 +0900
+++ b/limit-to.agda	Sun Mar 13 12:29:42 2016 +0900
@@ -39,57 +39,56 @@
    id-t1 :  Arrow
    arrow-f :  Arrow
    arrow-g :  Arrow
-   arrow-f' :  Arrow
 
-arrowSel : (a : TwoObject   ) (b : TwoObject   ) (sel : TwoObject ) -> Arrow
-arrowSel t0 t0 _ =   id-t0 
-arrowSel t0 t1 t0 =  arrow-f 
-arrowSel t0 t1 t1 =  arrow-g 
-arrowSel t1 t0 _ =   arrow-f' 
-arrowSel t1 t1 _ =   id-t1 
+arrowSel : (a : TwoObject   ) (b : TwoObject   ) (sel : TwoObject ) -> Maybe Arrow
+arrowSel t0 t0 _ =   just id-t0 
+arrowSel t0 t1 t0 =  just arrow-f 
+arrowSel t0 t1 t1 =  just arrow-g 
+arrowSel t1 t0 _ =   nothing
+arrowSel t1 t1 _ =   just id-t1 
+
+arrow2Sel : Arrow -> TwoObject
+arrow2Sel id-t0  = t0
+arrow2Sel arrow-f  = t0
+arrow2Sel arrow-g  = t1
+arrow2Sel id-t1  = t0
 
 record Two-Hom   (a : TwoObject   ) (b : TwoObject   ) : Set  where
    field
-       Map    : Arrow 
+       Map    : Maybe Arrow 
        Sel    : TwoObject
        selection :  ( arrowSel a b Sel  ) ≡ Map
 
 open Two-Hom
 
-twomap : {a b : TwoObject} -> Maybe ( Two-Hom a b ) -> Maybe ( Arrow )
-twomap {_} {_} nothing = nothing
-twomap {t0} {t0} (just f)  =   just ( Map f )
-twomap {t0} {t1} (just f)  =   just ( Map f )
-twomap {t1} {t0} (just f)  =   nothing
-twomap {t1} {t1} (just f)  =   just ( Map f )
+two-hom-iso : {a b : TwoObject} -> (f : Maybe ( Two-Hom a b ) ) ->  twomap f ≡ twomap (  record { Map = Map f  ; Sel = Sel f  ; selection = selection f  } )
+two-hom-iso  = ?
+
 
-Two-id :  (a : TwoObject ) ->  Maybe ( Two-Hom a a )
-Two-id t0  = just ( record { Map = id-t0 ; Sel = t0 ; selection = refl } )
-Two-id t1  = just ( record { Map = id-t1 ; Sel = t0 ; selection = refl } )
+Two-id :  (a : TwoObject ) ->   Two-Hom a a 
+Two-id t0  = record { Map = just id-t0 ; Sel = t0 ; selection = refl } 
+Two-id t1  = record { Map = just id-t1 ; Sel = t0 ; selection = refl } 
 
-arrow2hom : {a b : TwoObject} -> Arrow  -> Maybe ( Two-Hom a b ) 
-arrow2hom {t0} {t0}  id-t0 = Two-id t0
-arrow2hom {t1} {t1}  id-t1 = Two-id t1
-arrow2hom {t0} {t1}  arrow-f = just ( record { Map = arrow-f ; Sel = t0 ; selection = refl } )
-arrow2hom {t0} {t1}  arrow-g = just ( record { Map = arrow-g ; Sel = t1 ; selection = refl } )
-arrow2hom {_} {_} _  = nothing
-
-lemma-iso  : {a b : TwoObject} -> { f :  Two-Hom a b  } -> just f ≡ arrow2hom ( arrowSel a b (Sel f) )  
-lemma-iso  = {!!}
+Two-nothing ( a b : TwoObject) : Two-Hom a b
+Two-nothing a b  = record { Map = nothing ; Sel = t0 ; selection = refl }
 
 -- arrow composition
 
-twocomp :  {A B C : TwoObject } → Maybe Arrow -> Maybe Arrow -> Maybe ( Two-Hom A C )
-twocomp    {a} {b} {c} nothing  ga  = nothing
+twocomp :  {A B C : TwoObject } → Maybe Arrow -> Maybe Arrow -> Two-Hom A C 
+twocomp    {a} {b} {c} nothing  ga  =  record { Map = nothing ; Sel = t0 ; selection = refl }
 twocomp    {a} {b} {c} fa  nothing  = nothing
-twocomp   {t0} {t0} {t0} ( just i ) ( just _ ) = arrow2hom i
-twocomp   {t0} {t0} {t1} ( just f ) ( just _ ) = arrow2hom f
+twocomp   {t0} {t0} {t0} ( just i ) ( just _ ) = Two-id t0
 twocomp   {t0} {t1} {t0} ( just _ ) ( just _ ) = nothing
-twocomp   {t0} {t1} {t1} ( just _ ) ( just g ) = arrow2hom g
 twocomp   {t1} {t0} {t0} ( just _ ) ( just _ ) = nothing
 twocomp   {t1} {t0} {t1} ( just _ ) ( just _ ) = nothing
 twocomp   {t1} {t1} {t0} ( just _ ) ( just _ ) = nothing
-twocomp   {t1} {t1} {t1} ( just _ ) ( just i ) = arrow2hom i
+twocomp   {t1} {t1} {t1} ( just _ ) ( just i ) = Two-id t1
+twocomp   {t0} {t0} {t1} ( just f ) ( just _ ) with arrow2Sel f
+... | t0 =    record { Map = just arrow-f ; Sel = t0 ; selection = refl } 
+... | t1 =    record { Map = just arrow-g ; Sel = t1 ; selection = refl } 
+twocomp   {t0} {t1} {t1} ( just _ ) ( just g )  with arrow2Sel g 
+... | t0 =   ( record { Map = just arrow-f ; Sel = t0 ; selection = refl } 
+... | t1 =    record { Map = just arrow-g ; Sel = t1 ; selection = refl } 
 
 _×_ :  {A B C : TwoObject } → Maybe ( Two-Hom B C ) → Maybe ( Two-Hom A B ) → Maybe ( Two-Hom A C )
 _×_   {a} {b} {c} f g  = twocomp {a} {b} {c} ( twomap {b} {c} f ) ( twomap {a} {b} g )
@@ -117,17 +116,32 @@
         identityL' {t1} {t0} {f = nothing}  = refl
         identityL' {t1} {t1} {f = nothing}  = refl
         identityL' {t0} {t0} {just f} = ≡-cong (\x -> just x) ( selection f ) 
-        identityL' {t1} {t1} {just f} = ?
+        identityL' {t1} {t1} {just f} = ≡-cong (\x -> just x) ( selection f ) 
         identityL' {t1} {t0} {just f} = refl
         identityL' {t0} {t1} {just f} with (Sel f)
-        identityL' {t0} {t1} {just f} | t0 =  {!!}
+        identityL' {t0} {t1} {just f} | t0 =   let open ≡-Reasoning in
+              begin
+                twomap {t0} {t1} (twocomp {t0} {t1} {t1} (just id-t1) (just (Map f)))
+              ≡⟨  sym ( ≡-cong (\x -> twomap {t0} {t1} (twocomp {t0} {t1} {t1} (just id-t1) (just x ))) refl ) ⟩
+                twomap {t0} {t1} (twocomp {t0} {t1} {t1} (just id-t1) (just ( arrowSel t0 t1 t0 )))
+              ≡⟨⟩
+                twomap {t0} {t1} (twocomp {t0} {t1} {t1} (just id-t1) (just arrow-f ))
+              ≡⟨⟩
+                just arrow-f
+              ≡⟨⟩
+                just (arrowSel t0 t1 t0 )
+              ≡⟨ {!!} ⟩
+                just (arrowSel t0 t1 (Sel f) )
+              ≡⟨ ≡-cong (\x -> just x) ( selection f ) ⟩
+                just (Map f)
+             ∎
         identityL' {t0} {t1} {just f} | t1 =  {!!}
         identityR' : {A B : TwoObject} {f : Maybe ( Two-Hom A B)} →  twomap ( f × Two-id A  ) ≡ twomap f
         identityR' {t0} {t0} {f = nothing}  = refl
         identityR' {t0} {t1} {f = nothing}  = refl
         identityR' {t1} {t0} {f = nothing}  = refl
         identityR' {t1} {t1} {f = nothing}  = refl
-        identityR' {t0} {t0} {just f} = {!!} 
+        identityR' {t0} {t0} {just f} = ≡-cong (\x -> just x) ( selection f ) 
         identityR' {t1} {t1} {just f} = ≡-cong (\x -> just x) ( selection f ) 
         identityR' {t1} {t0} {just f} = refl
         identityR' {t0} {t1} {just f} =  {!!}
@@ -145,22 +159,22 @@
         associative {_} {_} {_} {_} {nothing} {g} {h} = refl
         associative {_} {_} {_} {_} {_} {nothing} {h} = {!!}
         associative {_} {_} {_} {_} {_} {g} {nothing} = {!!}
-        associative {t0} {t0} {t0} {t0} {just f} {just g} {just h} = {!!}
+        associative {t0} {t0} {t0} {t0} {just f} {just g} {just h} = refl
         associative {t0} {t0} {t0} {t1} {just f} {just g} {just h} = {!!}
-        associative {t0} {t0} {t1} {t0} {just f} {just g} {just h} = {!!}
+        associative {t0} {t0} {t1} {t0} {just f} {just g} {just h} = refl
         associative {t0} {t0} {t1} {t1} {just f} {just g} {just h} = {!!}
-        associative {t0} {t1} {t0} {t0} {just f} {just g} {just h} = {!!}
-        associative {t0} {t1} {t0} {t1} {just f} {just g} {just h} = {!!}
-        associative {t0} {t1} {t1} {t0} {just f} {just g} {just h} = {!!}
+        associative {t0} {t1} {t0} {t0} {just f} {just g} {just h} = refl
+        associative {t0} {t1} {t0} {t1} {just f} {just g} {just h} = refl
+        associative {t0} {t1} {t1} {t0} {just f} {just g} {just h} = refl
         associative {t0} {t1} {t1} {t1} {just f} {just g} {just h} = {!!}
-        associative {t1} {t0} {t0} {t0} {just f} {just g} {just h} = {!!}
+        associative {t1} {t0} {t0} {t0} {just f} {just g} {just h} = refl
         associative {t1} {t0} {t0} {t1} {just f} {just g} {just h} = {!!}
-        associative {t1} {t0} {t1} {t0} {just f} {just g} {just h} = {!!}
+        associative {t1} {t0} {t1} {t0} {just f} {just g} {just h} = refl
         associative {t1} {t0} {t1} {t1} {just f} {just g} {just h} = {!!}
-        associative {t1} {t1} {t0} {t0} {just f} {just g} {just h} = {!!}
-        associative {t1} {t1} {t0} {t1} {just f} {just g} {just h} = {!!}
-        associative {t1} {t1} {t1} {t0} {just f} {just g} {just h} = {!!}
-        associative {t1} {t1} {t1} {t1} {just f} {just g} {just h} = {!!}
+        associative {t1} {t1} {t0} {t0} {just f} {just g} {just h} = refl
+        associative {t1} {t1} {t0} {t1} {just f} {just g} {just h} = refl
+        associative {t1} {t1} {t1} {t0} {just f} {just g} {just h} = refl
+        associative {t1} {t1} {t1} {t1} {just f} {just g} {just h} = refl