Mercurial > hg > Members > kono > Proof > category

changeset 383:2a27ab008299

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Maybe Arrow
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Mar 2016 18:43:35 +0900
parents 813cf2e2bd1a
children e2b493fec8c3
files limit-to.agda
diffstat 1 files changed, 67 insertions(+), 86 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sun Mar 13 12:29:42 2016 +0900
+++ b/limit-to.agda	Sun Mar 13 18:43:35 2016 +0900
@@ -40,12 +40,13 @@
    arrow-f :  Arrow
    arrow-g :  Arrow
 
-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 
+arrowSel : (a : TwoObject   ) (b : TwoObject   ) (sel : Maybe TwoObject ) -> Maybe Arrow
+arrowSel _ _ nothing  =   nothing
+arrowSel t0 t0 (just _) =   just id-t0 
+arrowSel t0 t1 (just t0) =  just arrow-f 
+arrowSel t0 t1 (just t1) =  just arrow-g 
+arrowSel t1 t0 (just _) =   nothing
+arrowSel t1 t1 (just _) =   just id-t1 
 
 arrow2Sel : Arrow -> TwoObject
 arrow2Sel id-t0  = t0
@@ -56,49 +57,49 @@
 record Two-Hom   (a : TwoObject   ) (b : TwoObject   ) : Set  where
    field
        Map    : Maybe Arrow 
-       Sel    : TwoObject
+       Sel    : Maybe TwoObject
        selection :  ( arrowSel a b Sel  ) ≡ Map
 
 open Two-Hom
 
-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-hom-iso : {a b : TwoObject} -> (f : Two-Hom a b ) ->  Map f ≡ Map (  record { Map = Map f  ; Sel = Sel f  ; selection = selection f  } )
+two-hom-iso  _ = 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 } 
+Two-id t0  = record { Map = just id-t0 ; Sel = just t0 ; selection = refl } 
+Two-id t1  = record { Map = just id-t1 ; Sel = just t0 ; selection = refl } 
 
-Two-nothing ( a b : TwoObject) : Two-Hom a b
-Two-nothing a b  = record { Map = nothing ; Sel = t0 ; selection = refl }
+Two-nothing : ( a b : TwoObject) -> Two-Hom a b
+Two-nothing a b  = record { Map = nothing ; Sel = nothing  ; selection = refl }
 
 -- arrow composition
 
 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    {a} {b} {c} nothing  ga  =  Two-nothing a c
+twocomp    {a} {b} {c} fa  nothing  = Two-nothing a c
 twocomp   {t0} {t0} {t0} ( just i ) ( just _ ) = Two-id t0
-twocomp   {t0} {t1} {t0} ( just _ ) ( just _ ) = nothing
-twocomp   {t1} {t0} {t0} ( just _ ) ( just _ ) = nothing
-twocomp   {t1} {t0} {t1} ( just _ ) ( just _ ) = nothing
-twocomp   {t1} {t1} {t0} ( just _ ) ( just _ ) = nothing
+twocomp   {t0} {t1} {t0} ( just _ ) ( just _ ) = Two-nothing t0 t0
+twocomp   {t1} {t0} {t0} ( just _ ) ( just _ ) = Two-nothing t1 t0
+twocomp   {t1} {t0} {t1} ( just _ ) ( just _ ) = Two-nothing t1 t1
+twocomp   {t1} {t1} {t0} ( just _ ) ( just _ ) = Two-nothing t1 t0
 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 } 
+... | t0 =    record { Map = just arrow-f ; Sel = just t0 ; selection = refl } 
+... | t1 =    record { Map = just arrow-g ; Sel = just 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 } 
+... | t0 =    record { Map = just arrow-f ; Sel = just t0 ; selection = refl } 
+... | t1 =    record { Map = just arrow-g ; Sel = just 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 )
+_×_ :  {A B C : TwoObject } →  Two-Hom B C →  Two-Hom A B  →  Two-Hom A C 
+_×_   {a} {b} {c} f g  = twocomp {a} {b} {c} ( Map f ) ( Map g )
 
 twocat : {ℓ c₁ c₂ : Level  } ->  Category _ _ _ 
 twocat  = record {
     Obj  = TwoObject  ;
-    Hom = λ a b →  Maybe ( Two-Hom a b )  ; 
+    Hom = λ a b →   Two-Hom a b   ; 
     _o_ =  _×_ ;
-    _≈_ = λ a b →   twomap a ≡ twomap b  ;
+    _≈_ = λ a b →   Map a ≡ Map b  ;
     Id  =  \{a} -> Two-id a ;
     isCategory  = record {
             isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym};
@@ -110,71 +111,51 @@
    } where
         open  import  Relation.Binary.PropositionalEquality
         ≡-cong = Relation.Binary.PropositionalEquality.cong 
-        identityL' : {A B : TwoObject} {f : Maybe ( Two-Hom A B)} →  twomap ( Two-id B × f ) ≡ twomap f
-        identityL' {t0} {t0} {f = nothing}  = refl
-        identityL' {t0} {t1} {f = nothing}  = refl
-        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} = ≡-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 =   let open ≡-Reasoning in
+        identityL' : {A B : TwoObject} {f : Two-Hom A B} →  Map ( Two-id B × f ) ≡ Map f
+        identityL' {t0} {t0} {f} = {!!}
+        identityL' {t1} {t1} {f} = {!!}
+        identityL' {t1} {t0} {f} = {!!}
+        identityL' {t0} {t1} {f} with (Sel f)
+        identityL' {t0} {t1} {f} | nothing =   ?
+        identityL' {t0} {t1} {f} | just 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)
+                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} = ≡-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} =  {!!}
-        o-resp-≈ : {A B C : TwoObject} {f g : Maybe ( Two-Hom A B)} {h i : Maybe (Two-Hom B C)} →
-            twomap f ≡ twomap g → twomap h ≡ twomap i → twomap ( h × f ) ≡ twomap ( i × g )
+        identityL' {t0} {t1} {f} | just t1 =  {!!}
+        identityR' : {A B : TwoObject} {f : Two-Hom A B} →  Map ( f × Two-id A  ) ≡ Map f
+        identityR' {t0} {t0} {f} = {!!}
+        identityR' {t1} {t1} {f} = {!!}
+        identityR' {t1} {t0} {f} = {!!}
+        identityR' {t0} {t1} {f} =  {!!}
+        o-resp-≈ : {A B C : TwoObject} {f g :  Two-Hom A B} {h i : Two-Hom B C} →
+            Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g )
         o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = let open ≡-Reasoning in
               begin
-                twomap (twocomp {a} {b} {c}  ( twomap h ) ( twomap {a} {b} f )  )
-              ≡⟨ ≡-cong (\y -> twomap (twocomp {a} {b} {c}  y  ( twomap {a} {b} f )  )) h≡i  ⟩
-                twomap (twocomp {a} {b} {c}  ( twomap i ) ( twomap {a} {b} f )  )
-              ≡⟨ ≡-cong (\y -> twomap (twocomp {a} {b} {c}  (twomap i)   y  )) f≡g  ⟩
-                twomap (twocomp {a} {b} {c}  ( twomap i ) ( twomap {a} {b} g )  )
+                Map (twocomp {a} {b} {c}  ( Map h ) ( Map {a} {b} f )  )
+              ≡⟨ ≡-cong (\y -> Map (twocomp {a} {b} {c}  y  ( Map {a} {b} f )  )) h≡i  ⟩
+                Map (twocomp {a} {b} {c}  ( Map i ) ( Map {a} {b} f )  )
+              ≡⟨ ≡-cong (\y -> Map (twocomp {a} {b} {c}  (Map i)   y  )) f≡g  ⟩
+                Map (twocomp {a} {b} {c}  ( Map i ) ( Map {a} {b} g )  )
               ∎
-        associative : {A B C D : TwoObject} {f : Maybe (Two-Hom C D)} {g : Maybe (Two-Hom B C)} {h : Maybe (Two-Hom A B)} → twomap ( f × (g × h) ) ≡ twomap ( (f × g) × h )
-        associative {_} {_} {_} {_} {nothing} {g} {h} = refl
-        associative {_} {_} {_} {_} {_} {nothing} {h} = {!!}
-        associative {_} {_} {_} {_} {_} {g} {nothing} = {!!}
-        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} = refl
-        associative {t0} {t0} {t1} {t1} {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} = refl
-        associative {t1} {t0} {t0} {t1} {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} = 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
+        associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h )
+        associative {t0} {t0} {t0} {t0} {f} {g} {h} = {!!}
+        associative {t0} {t0} {t0} {t1} {f} {g} {h} = {!!}
+        associative {t0} {t0} {t1} {t0} {f} {g} {h} = {!!}
+        associative {t0} {t0} {t1} {t1} {f} {g} {h} = {!!}
+        associative {t0} {t1} {t0} {t0} {f} {g} {h} = {!!}
+        associative {t0} {t1} {t0} {t1} {f} {g} {h} = {!!}
+        associative {t0} {t1} {t1} {t0} {f} {g} {h} = {!!}
+        associative {t0} {t1} {t1} {t1} {f} {g} {h} = {!!}
+        associative {t1} {t0} {t0} {t0} {f} {g} {h} = {!!}
+        associative {t1} {t0} {t0} {t1} {f} {g} {h} = {!!}
+        associative {t1} {t0} {t1} {t0} {f} {g} {h} = {!!}
+        associative {t1} {t0} {t1} {t1} {f} {g} {h} = {!!}
+        associative {t1} {t1} {t0} {t0} {f} {g} {h} = {!!}
+        associative {t1} {t1} {t0} {t1} {f} {g} {h} = {!!}
+        associative {t1} {t1} {t1} {t0} {f} {g} {h} = {!!}
+        associative {t1} {t1} {t1} {t1} {f} {g} {h} = {!!}