changeset 357:71c817f28bc6

fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 12 May 2015 11:17:38 +0900
parents 500c813af3c9
children cf9c0f12cec5
files code-data.agda
diffstat 1 files changed, 45 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/code-data.agda	Mon May 11 16:59:33 2015 +0900
+++ b/code-data.agda	Tue May 12 11:17:38 2015 +0900
@@ -14,7 +14,8 @@
       codom : Obj A
       code : Hom A dom codom
       rev-code : Hom A codom dom
-      id-left  :  A [ A [ code  o rev-code ]  ≈  id1 A codom ]
+      id-left   :  A [ A [ code  o rev-code ]  ≈  id1 A codom ]
+      id-right  :  A [ A [ rev-code  o code ]  ≈  id1 A dom ]
 
 open DataObj
 
@@ -39,12 +40,12 @@
 _∙_ {a} {b} {c} g f = record { continuation = A [ continuation g o A [ code b o continuation f ] ] }
 
 _≗_ : {a : DataObj } {b : DataObj } (f g : DataHom a b ) → Set ℓ 
-_≗_ {a} {b} f g = A [  A [ code b o continuation f ]  ≈  A [ code b o continuation g ]  ]
+_≗_ {a} {b} f g = A [  continuation f ≈  continuation g ]
 
 open import Relation.Binary.Core
 
-iDataCategory : IsCategory DataObj DataHom _≗_ _∙_  DataId 
-iDataCategory  = record  { isEquivalence =  isEquivalence 
+isDataCategory : IsCategory DataObj DataHom _≗_ _∙_  DataId 
+isDataCategory  = record  { isEquivalence =  isEquivalence 
                     ; 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}
@@ -54,53 +55,49 @@
          open ≈-Reasoning (A) 
          o-resp :  {A B C : DataObj} {f g : DataHom A B} {h i : DataHom B C} → f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
          o-resp {a} {b} {c} {f} {g} {h} {i} f≗g h≗i =  begin
-                code c o continuation (h ∙ f) 
+                continuation (h ∙ f) 
            ≈⟨⟩
-                code c o continuation h o code b o continuation f
-           ≈⟨ cdr ( cdr ( f≗g ) ) ⟩
-                code c o continuation h o code b o continuation g
-           ≈⟨ assoc ⟩
-                (code c o continuation h ) o code b o continuation g
+                continuation h o code b o continuation f
+           ≈⟨  cdr ( cdr ( f≗g ))  ⟩
+                continuation h o code b o continuation g
            ≈⟨ car h≗i ⟩
-                (code c o continuation i ) o code b o continuation g
-           ≈⟨ sym assoc ⟩
-                code c o continuation i o code b o continuation g
+                continuation i  o code b o continuation g
            ≈⟨⟩
-                code c o continuation (i ∙ g)
+                continuation (i ∙ g)

          associative : (a b c d : DataObj)  (f : DataHom c d) (g : DataHom b c) (h : DataHom a b) → (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
          associative a b c d f g h  = begin
-               code d o continuation (f ∙ (g ∙ h))
+               continuation (f ∙ (g ∙ h))
            ≈⟨⟩
-               code d o continuation f o code c o  continuation g  o code b o continuation h  
-           ≈⟨ cdr (cdr assoc ) ⟩
-               code d o continuation f o (code c o  continuation g)  o code b o continuation h  
-           ≈⟨ cdr assoc ⟩
-               code d o (continuation f o code c o continuation g) o code b o continuation h
+               continuation f o code c o  continuation g  o code b o continuation h  
+           ≈⟨ cdr assoc  ⟩
+               continuation f o (code c o  continuation g)  o code b o continuation h  
+           ≈⟨ assoc ⟩
+               (continuation f o code c o continuation g) o code b o continuation h
            ≈⟨⟩
-               code d o continuation ((f ∙ g) ∙ h) 
+               continuation ((f ∙ g) ∙ h) 

          identityL : (a : DataObj) (b : DataObj) (f : DataHom a b) → (DataId ∙ f) ≗ f
          identityL a b f  = begin
-              code b o continuation (DataId ∙ f) 
+              continuation (DataId ∙ f) 
            ≈⟨⟩
-               code b o ( rev-code b o  (code b o continuation f ))
+              rev-code b o code b o continuation f 
            ≈⟨ assoc ⟩
-               (code b o  rev-code b ) o  ( code b o continuation f )
-           ≈⟨ car (id-left b )  ⟩
-               id1 A (codom b) o  ( code b o continuation f )
+               (rev-code b  o  code b ) o continuation f 
+           ≈⟨ car ( id-right b) ⟩
+               id1 A (dom b) o continuation f 
            ≈⟨ idL ⟩
-              code b o continuation f 
+              continuation f

          identityR : (a : DataObj) (b : DataObj) (f : DataHom a b) → (f ∙ DataId  ) ≗ f
          identityR a b f  = begin
-               code b o continuation (f ∙ DataId) 
+               continuation (f ∙ DataId) 
            ≈⟨⟩
-               code b o ( continuation f  o ( code a   o rev-code a ) )
-           ≈⟨ cdr (cdr (id-left a)) ⟩
-               code b o ( continuation f  o id1 A (codom a) )
-           ≈⟨ cdr idR ⟩
-               code b o continuation f
+               ( continuation f  o ( code a   o rev-code a ) )
+           ≈⟨ cdr (id-left a) ⟩
+               ( continuation f  o id1 A (codom a) )
+           ≈⟨ idR ⟩
+               continuation f

          isEquivalence : {a : DataObj } {b : DataObj } →
                IsEquivalence {_} {_} {DataHom a b } _≗_
@@ -116,7 +113,7 @@
          ; _o_ = _∙_ 
          ; _≈_ = _≗_
          ; Id  =  DataId 
-         ; isCategory = iDataCategory
+         ; isCategory = isDataCategory
           }
 
 
@@ -131,6 +128,7 @@
       ; code  = id1 A d
       ; rev-code  = id1 A d
       ; id-left = idL
+      ; id-right = idR
    }  where open ≈-Reasoning (A)  
 
 U : Functor  DataCategory A
@@ -150,7 +148,7 @@
               code (data-codom f) o continuation f 
            ≈⟨⟩
               code b o continuation f 
-           ≈⟨ f≈g ⟩
+           ≈⟨ cdr f≈g ⟩
               code b o continuation g 
            ≈⟨⟩
               code (data-codom g) o continuation g 
@@ -210,19 +208,21 @@
         A [ A [ FMap U g o eta-map a ] ≈ f ] →
         DataCategory [ solution f ≈ g ]
     uniqueness {a} {b} {f} {g} Uη≈f  =  begin
-               code b o continuation (solution {a} {b} f)
+               continuation (solution {a} {b} f)
            ≈⟨⟩
-               code b o ( rev-code b o f)
-           ≈⟨ sym ( cdr ( cdr  Uη≈f   )) ⟩
-               code b o  rev-code b o ( code b o continuation g ) o id1 A (codom (F a))
-           ≈⟨ assoc ⟩
-               (code b o  rev-code b ) o ( code b o continuation g ) o id1 A (codom (F a))
-           ≈⟨ car ( id-left b) ⟩
-               id1 A (codom b ) o ( code b o continuation g ) o id1 A (codom (F a))
+               rev-code b o f
+           ≈⟨ sym (  cdr  Uη≈f   ) ⟩
+               rev-code b o ( code b o continuation g ) o id1 A (codom (F a))
+           ≈⟨  sym ( cdr assoc) ⟩
+               rev-code b o code b o continuation g o id1 A (codom (F a))
+           ≈⟨  assoc ⟩
+               (rev-code b o  code b ) o continuation g  o id1 A (codom (F a))
+           ≈⟨  car ( id-right b ) ⟩
+               id (dom b) o continuation g o id1 A (codom (F a))
            ≈⟨ idL ⟩
-               ( code b o continuation g ) o id1 A (codom (F a))
+               ( continuation g ) o id1 A (codom (F a))
            ≈⟨ idR ⟩
-               code b o continuation g
+               continuation g