Mercurial > hg > Members > kono > Proof > category
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 ∎