Mercurial > hg > Members > kono > Proof > category

changeset 356:500c813af3c9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
history to continuation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 11 May 2015 16:59:33 +0900
parents 8fd085379380
children 71c817f28bc6
files code-data.agda
diffstat 1 files changed, 49 insertions(+), 47 deletions(-) [+]
line wrap: on
line diff
--- a/code-data.agda	Mon May 11 11:16:24 2015 +0900
+++ b/code-data.agda	Mon May 11 16:59:33 2015 +0900
@@ -7,6 +7,7 @@
 
 module code-data { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
 
+-- DataObj is a set of code segment with reverse computation
 record DataObj : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
    field
       dom : Obj A
@@ -17,9 +18,10 @@
 
 open DataObj
 
+-- DataHom is a set of data segment with computational continuation 
 record isDataHom (a : DataObj ) (b : DataObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
    field
-      history : Hom A (codom a) (dom b)
+      continuation : Hom A (codom a) (dom b)
    data-dom = a
    data-codom = b
 
@@ -30,14 +32,14 @@
 
 DataId : { a : DataObj } → DataHom a a
 DataId {a} = record {
-      history = rev-code a
+      continuation = rev-code a
    }
 
 _∙_ :  {a b c : DataObj } → DataHom b c → DataHom a b → DataHom a c
-_∙_ {a} {b} {c} g f = record { history = A [ history g o A [ code b o history f ] ] }
+_∙_ {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 history f ]  ≈  A [ code b o history g ]  ]
+_≗_ {a} {b} f g = A [  A [ code b o continuation f ]  ≈  A [ code b o continuation g ]  ]
 
 open import Relation.Binary.Core
 
@@ -52,53 +54,53 @@
          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 history (h ∙ f) 
+                code c o continuation (h ∙ f) 
            ≈⟨⟩
-                code c o history h o code b o history f
+                code c o continuation h o code b o continuation f
            ≈⟨ cdr ( cdr ( f≗g ) ) ⟩
-                code c o history h o code b o history g
+                code c o continuation h o code b o continuation g
            ≈⟨ assoc ⟩
-                (code c o history h ) o code b o history g
+                (code c o continuation h ) o code b o continuation g
            ≈⟨ car h≗i ⟩
-                (code c o history i ) o code b o history g
+                (code c o continuation i ) o code b o continuation g
            ≈⟨ sym assoc ⟩
-                code c o history i o code b o history g
+                code c o continuation i o code b o continuation g
            ≈⟨⟩
-                code c o history (i ∙ g)
+                code c o 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 history (f ∙ (g ∙ h))
+               code d o continuation (f ∙ (g ∙ h))
            ≈⟨⟩
-               code d o history f o code c o  history g  o code b o history h  
+               code d o continuation f o code c o  continuation g  o code b o continuation h  
            ≈⟨ cdr (cdr assoc ) ⟩
-               code d o history f o (code c o  history g)  o code b o history h  
+               code d o continuation f o (code c o  continuation g)  o code b o continuation h  
            ≈⟨ cdr assoc ⟩
-               code d o (history f o code c o history g) o code b o history h
+               code d o (continuation f o code c o continuation g) o code b o continuation h
            ≈⟨⟩
-               code d o history ((f ∙ g) ∙ h) 
+               code d o continuation ((f ∙ g) ∙ h) 
            ∎
          identityL : (a : DataObj) (b : DataObj) (f : DataHom a b) → (DataId ∙ f) ≗ f
          identityL a b f  = begin
-              code b o history (DataId ∙ f) 
+              code b o continuation (DataId ∙ f) 
            ≈⟨⟩
-               code b o ( rev-code b o  (code b o history f ))
+               code b o ( rev-code b o  (code b o continuation f ))
            ≈⟨ assoc ⟩
-               (code b o  rev-code b ) o  ( code b o history f )
+               (code b o  rev-code b ) o  ( code b o continuation f )
            ≈⟨ car (id-left b )  ⟩
-               id1 A (codom b) o  ( code b o history f )
+               id1 A (codom b) o  ( code b o continuation f )
            ≈⟨ idL ⟩
-              code b o history f 
+              code b o continuation f 
            ∎
          identityR : (a : DataObj) (b : DataObj) (f : DataHom a b) → (f ∙ DataId  ) ≗ f
          identityR a b f  = begin
-               code b o history (f ∙ DataId) 
+               code b o continuation (f ∙ DataId) 
            ≈⟨⟩
-               code b o ( history f  o ( code a   o rev-code a ) )
+               code b o ( continuation f  o ( code a   o rev-code a ) )
            ≈⟨ cdr (cdr (id-left a)) ⟩
-               code b o ( history f  o id1 A (codom a) )
+               code b o ( continuation f  o id1 A (codom a) )
            ≈⟨ cdr idR ⟩
-               code b o history f
+               code b o continuation f
            ∎
          isEquivalence : {a : DataObj } {b : DataObj } →
                IsEquivalence {_} {_} {DataHom a b } _≗_
@@ -106,7 +108,7 @@
            record { refl  = refl-hom
              ; sym   = sym
              ; trans = trans-hom
-             } 
+           } 
 DataCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
 DataCategory =
   record { Obj = DataObj
@@ -134,7 +136,7 @@
 U : Functor  DataCategory A
 U = record {
       FObj = \d -> codom  d
-    ; FMap = \f -> A [ code ( data-codom f ) o history f ] 
+    ; FMap = \f -> A [ code ( data-codom f ) o continuation f ] 
     ; isFunctor = record {
              ≈-cong   =  \{a} {b} {f} {g} -> ≈-cong-1 {a} {b} {f} {g}
              ; identity = \{a} -> identity-1 {a}
@@ -143,35 +145,35 @@
  } where
     open ≈-Reasoning (A) 
     ≈-cong-1 :  {a : Obj DataCategory} {b : Obj DataCategory} {f g : Hom DataCategory a b} → DataCategory [ f ≈ g ] → 
-         A [ A [ code (data-codom f) o history f ] ≈ A [ code (data-codom g) o history g ] ]
+         A [ A [ code (data-codom f) o continuation f ] ≈ A [ code (data-codom g) o continuation g ] ]
     ≈-cong-1 {a} {b} {f} {g}  f≈g =  begin
-              code (data-codom f) o history f 
+              code (data-codom f) o continuation f 
            ≈⟨⟩
-              code b o history f 
+              code b o continuation f 
            ≈⟨ f≈g ⟩
-              code b o history g 
+              code b o continuation g 
            ≈⟨⟩
-              code (data-codom g) o history g 
+              code (data-codom g) o continuation g 
            ∎
-    identity-1 :  {a : Obj DataCategory} → A [ A [ code (data-codom (DataId {a})) o history (DataId {a}) ] ≈ id1 A (codom a) ]
+    identity-1 :  {a : Obj DataCategory} → A [ A [ code (data-codom (DataId {a})) o continuation (DataId {a}) ] ≈ id1 A (codom a) ]
     identity-1 {a} =   begin
-              code (data-codom (DataId {a} )) o history (DataId  {a} )
+              code (data-codom (DataId {a} )) o continuation (DataId  {a} )
            ≈⟨⟩
                code a o  rev-code a
            ≈⟨ id-left a ⟩
               id1 A (codom a)
            ∎
     distr-1 :  {a b c : Obj DataCategory} {f : Hom DataCategory a b} {g : Hom DataCategory b c} → 
-             A [ A [ code (data-codom ( g ∙ f )) o history ( g ∙ f ) ] ≈
-                A [ A [ code (data-codom g) o history g ] o A [ code (data-codom f) o history f ] ] ]
+             A [ A [ code (data-codom ( g ∙ f )) o continuation ( g ∙ f ) ] ≈
+                A [ A [ code (data-codom g) o continuation g ] o A [ code (data-codom f) o continuation f ] ] ]
     distr-1 {a} {b} {c} {f} {g} =  begin
-               code (data-codom (g ∙ f )) o history ( g ∙ f ) 
+               code (data-codom (g ∙ f )) o continuation ( g ∙ f ) 
            ≈⟨⟩
-                code c o history g o  code b o history f
+                code c o continuation g o  code b o continuation f
            ≈⟨ assoc ⟩
-                (code c o history g ) o  code b o history f
+                (code c o continuation g ) o  code b o continuation f
            ≈⟨⟩
-               ( code (data-codom g) o history g ) o ( code (data-codom f) o history f )
+               ( code (data-codom g) o continuation g ) o ( code (data-codom f) o continuation f )
            ∎
 
 eta-map :   (a : Obj A) → Hom A a ( FObj U (F a) )
@@ -188,7 +190,7 @@
   } where
     open ≈-Reasoning (A) 
     solution :  {a : Obj A} {b : Obj DataCategory} → Hom A a (FObj U b) → Hom DataCategory (F a) b
-    solution {a} {b} f = record { history = A [ rev-code b o f ]  }
+    solution {a} {b} f = record { continuation = A [ rev-code b o f ]  }
     universalMapping :  {a : Obj A} {b : Obj DataCategory} {f : Hom A a (FObj U b)} → A [ A [ FMap U (solution {a} {b} f) o eta-map a ] ≈ f ]
     universalMapping {a} {b} {f} = begin
                 FMap U (solution {a} {b} f) o eta-map a 
@@ -208,19 +210,19 @@
         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 history (solution {a} {b} f)
+               code b o 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 history g ) o id1 A (codom (F a))
+               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 history g ) o id1 A (codom (F a))
+               (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 history g ) o id1 A (codom (F a))
+               id1 A (codom b ) o ( code b o continuation g ) o id1 A (codom (F a))
            ≈⟨ idL ⟩
-               ( code b o history g ) o id1 A (codom (F a))
+               ( code b o continuation g ) o id1 A (codom (F a))
            ≈⟨ idR ⟩
-               code b o history g
+               code b o continuation g
            ∎