Mercurial > hg > Members > kono > Proof > category

changeset 384:e2b493fec8c3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tow-hom-iso in twocat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 14 Mar 2016 13:08:36 +0900
parents 2a27ab008299
children ff3803fc0c8a
files limit-to.agda
diffstat 1 files changed, 86 insertions(+), 66 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Sun Mar 13 18:43:35 2016 +0900
+++ b/limit-to.agda	Mon Mar 14 13:08:36 2016 +0900
@@ -40,59 +40,80 @@
    arrow-f :  Arrow
    arrow-g :  Arrow
 
-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 
+record RawHom   (a : TwoObject   ) (b : TwoObject   ) : Set  where
+   field
+       RawMap    : Maybe Arrow 
+       RawSel    : Maybe TwoObject
+
+open RawHom
 
-arrow2Sel : Arrow -> TwoObject
-arrow2Sel id-t0  = t0
-arrow2Sel arrow-f  = t0
-arrow2Sel arrow-g  = t1
-arrow2Sel id-t1  = t0
+arrow2hom : {a b : TwoObject}  -> Maybe Arrow -> RawHom a b
+arrow2hom {t0} {t0} (just id-t0)    =  record { RawMap = just id-t0  ; RawSel = just t0  }
+arrow2hom {t0} {t1} (just arrow-f)  =  record { RawMap = just arrow-f  ; RawSel = just t0  }
+arrow2hom {t0} {t1} (just arrow-g)  =  record { RawMap = just arrow-g  ; RawSel = just t1  }
+arrow2hom {t1} {t1} (just id-t1)    =  record { RawMap = just id-t1  ; RawSel = just t0  }
+arrow2hom {a} {b} _   =  record { RawMap = nothing ; RawSel = nothing  }
+
 
 record Two-Hom   (a : TwoObject   ) (b : TwoObject   ) : Set  where
    field
-       Map    : Maybe Arrow 
-       Sel    : Maybe TwoObject
-       selection :  ( arrowSel a b Sel  ) ≡ Map
+      hom : RawHom a b
+      two-hom-iso :  arrow2hom {a} {b} (RawMap hom)  ≡  hom
+   Map : Maybe Arrow
+   Map = RawMap hom
+   Sel : Maybe TwoObject
+   Sel = RawSel hom
+
+Two-id :  (a : TwoObject ) ->   Two-Hom a a 
+Two-id t0  = record { hom = record { RawMap = just id-t0 ; RawSel = just t0 } ; two-hom-iso = refl }
+Two-id t1  = record { hom = record { RawMap = just id-t1 ; RawSel = just t0 } ; two-hom-iso = refl }
+
+Two-nothing : ( a b : TwoObject) -> Two-Hom a b
+Two-nothing a b  = record { hom = record { RawMap = nothing ; RawSel = nothing  } ; two-hom-iso =  nothing-iso a b }
+ where
+        nothing-iso :  (a b : TwoObject ) ->   arrow2hom {a} {b} nothing  ≡  record { RawMap = nothing ; RawSel = nothing  }
+        nothing-iso t0 t0 = refl
+        nothing-iso t0 t1 = refl
+        nothing-iso t1 t0 = refl
+        nothing-iso t1 t1 = refl
 
 open Two-Hom
 
-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 = 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 = nothing  ; selection = refl }
-
 -- arrow composition
 
-twocomp :  {A B C : TwoObject } → Maybe Arrow -> Maybe Arrow -> Two-Hom A C 
-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 _ ) = 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 = 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 = just t0 ; selection = refl } 
-... | t1 =    record { Map = just arrow-g ; Sel = just t1 ; selection = refl } 
+twocomp :  Maybe Arrow -> Maybe Arrow -> Maybe Arrow
+twocomp (just arrow-f) (just id-t0) = just arrow-f
+twocomp (just arrow-g) (just id-t0) = just arrow-g
+twocomp (just id-t0) (just id-t0) = just id-t0
+twocomp (just id-t1) (just id-t1) = just id-t1
+twocomp _ _ = nothing
 
 _×_ :  {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 )
+_×_   {a} {b} {c} f g  = record { hom = arrow2hom ( twocomp (Map f) (Map g) ); two-hom-iso  = comp-iso a c }
+ where
+    comp-iso :  (a c : TwoObject ) →  arrow2hom (RawMap (arrow2hom {a} {c} (twocomp (Map f) (Map g)))) ≡ arrow2hom {a} {c} (twocomp (Map f) (Map g))
+    comp-iso a c  with (twocomp (Map f) (Map g))
+    comp-iso t0 t0 | nothing = refl
+    comp-iso t0 t1 | nothing = refl
+    comp-iso t1 t0 | nothing = refl
+    comp-iso t1 t1 | nothing = refl
+    comp-iso t0 t0 | just id-t0 = refl
+    comp-iso t0 t1 | just id-t0 = refl
+    comp-iso t1 t0 | just id-t0 = refl
+    comp-iso t1 t1 | just id-t0 = refl
+    comp-iso t0 t0 | just id-t1 = refl
+    comp-iso t0 t1 | just id-t1 = refl
+    comp-iso t1 t0 | just id-t1 = refl
+    comp-iso t1 t1 | just id-t1 = refl
+    comp-iso t1 t1 | just arrow-f = refl
+    comp-iso t0 t0 | just arrow-f = refl
+    comp-iso t0 t1 | just arrow-f = refl
+    comp-iso t1 t0 | just arrow-f = refl
+    comp-iso t1 t1 | just arrow-g = refl
+    comp-iso t0 t0 | just arrow-g = refl
+    comp-iso t0 t1 | just arrow-g = refl
+    comp-iso t1 t0 | just arrow-g = refl
+
 
 twocat : {ℓ c₁ c₂ : Level  } ->  Category _ _ _ 
 twocat  = record {
@@ -103,42 +124,41 @@
     Id  =  \{a} -> Two-id a ;
     isCategory  = record {
             isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym};
-            identityL  = \{a b f} -> identityL' {a} {b} {f} ;
-            identityR  = \{a b f} -> identityR' {a} {b} {f} ;
+            identityL  = \{a b f} -> identityL {a} {b} {f} ;
+            identityR  = \{a b f} -> identityR {a} {b} {f} ;
             o-resp-≈  = \{a b c f g h i} -> o-resp-≈  {a} {b} {c} {f} {g} {h} {i} ;
             associative  = \{a b c d f g h } -> associative  {a} {b} {c} {d} {f} {g} {h}
        } 
    } where
         open  import  Relation.Binary.PropositionalEquality
         ≡-cong = Relation.Binary.PropositionalEquality.cong 
-        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
+        identityL : {A B : TwoObject} {f : Two-Hom A B} →  Map ( Two-id B × f ) ≡ Map f
+        identityL {a} {b} {f} with (Map f)
+        identityL {a} {b} {f} | nothing =   let open ≡-Reasoning in
+              begin
+                {!!}
+              ≡⟨ {!!} ⟩
+                {!!}
+              ≡⟨⟩
+                nothing
+             ∎
+        identityL {a} {b} {f} | just id-t0  =   let open ≡-Reasoning in
               begin
                 {!!}
               ≡⟨ {!!} ⟩
-                Map f
+                just id-t0
              ∎
-        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} =  {!!}
+        identityL {a} {b} {f} | just id-t1  =   {!!}
+        identityL {a} {b} {f} | just arrow-f  =  {!!}
+        identityL {a} {b} {f} | just arrow-g  =  {!!}
+        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
-                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 )  )
-              ∎
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = let open ≡-Reasoning in {!!}
         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} = {!!}