Mercurial > hg > Members > kono > Proof > category
diff code-data.agda @ 356:500c813af3c9
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 |
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 ∎