Mercurial > hg > Members > kono > Proof > category

annotate code-data.agda @ 790:1e7319868d77

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sets is CCC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Apr 2019 23:42:19 +0900
parents 3d41a8edbf63
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category -- https://github.com/konn/category-agda
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 --open import Category.HomReasoning
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import HomReasoning
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import cat-utility
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Category.Cat
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 module code-data { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
10 -- DataObj is a set of code segment with reverse computation
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 record DataObj : Set (c₁ ⊔ c₂ ⊔ ℓ) where
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 field
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 dom : Obj A
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 codom : Obj A
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 code : Hom A dom codom
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 rev-code : Hom A codom dom
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
17 id-left : A [ A [ code o rev-code ] ≈ id1 A codom ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
18 id-right : A [ A [ rev-code o code ] ≈ id1 A dom ]
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 open DataObj
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
22 -- DataHom is a set of data segment with computational continuation
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 record isDataHom (a : DataObj ) (b : DataObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 field
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
25 continuation : Hom A (codom a) (dom b)
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 data-dom = a
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 data-codom = b
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 open isDataHom
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 DataHom : (a : DataObj ) (b : DataObj ) → Set (c₁ ⊔ c₂ ⊔ ℓ)
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 DataHom = λ a b → isDataHom a b
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 DataId : { a : DataObj } → DataHom a a
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 DataId {a} = record {
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
36 continuation = rev-code a
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 }
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 _∙_ : {a b c : DataObj } → DataHom b c → DataHom a b → DataHom a c
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
40 _∙_ {a} {b} {c} g f = record { continuation = A [ continuation g o A [ code b o continuation f ] ] }
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 _≗_ : {a : DataObj } {b : DataObj } (f g : DataHom a b ) → Set ℓ
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
43 _≗_ {a} {b} f g = A [ continuation f ≈ continuation g ]
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 open import Relation.Binary.Core
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
47 isDataCategory : IsCategory DataObj DataHom _≗_ _∙_ DataId
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
48 isDataCategory = record { isEquivalence = isEquivalence
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 ; identityL = \{a} {b} {f} -> identityL a b f
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 ; identityR = \{a} {b} {f} -> identityR a b f
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 ; o-resp-≈ = \{a} {b} {c} {f} {g} {h} {i} -> o-resp {a} {b} {c} {f} {g} {h} {i}
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 ; associative = \{a} {b} {c} {d} {f} {g} {h} -> associative a b c d f g h
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 }
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 where
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 open ≈-Reasoning (A)
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 o-resp : {A B C : DataObj} {f g : DataHom A B} {h i : DataHom B C} → f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 o-resp {a} {b} {c} {f} {g} {h} {i} f≗g h≗i = begin
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
58 continuation (h ∙ f)
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 ≈⟨⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
60 continuation h o code b o continuation f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
61 ≈⟨ cdr ( cdr ( f≗g )) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
62 continuation h o code b o continuation g
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 ≈⟨ car h≗i ⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
64 continuation i o code b o continuation g
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 ≈⟨⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
66 continuation (i ∙ g)
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 ∎
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 associative : (a b c d : DataObj) (f : DataHom c d) (g : DataHom b c) (h : DataHom a b) → (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 associative a b c d f g h = begin
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
70 continuation (f ∙ (g ∙ h))
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 ≈⟨⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
72 continuation f o code c o continuation g o code b o continuation h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
73 ≈⟨ cdr assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
74 continuation f o (code c o continuation g) o code b o continuation h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
75 ≈⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
76 (continuation f o code c o continuation g) o code b o continuation h
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 ≈⟨⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
78 continuation ((f ∙ g) ∙ h)
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 ∎
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 identityL : (a : DataObj) (b : DataObj) (f : DataHom a b) → (DataId ∙ f) ≗ f
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 identityL a b f = begin
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
82 continuation (DataId ∙ f)
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 ≈⟨⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
84 rev-code b o code b o continuation f
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 ≈⟨ assoc ⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
86 (rev-code b o code b ) o continuation f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
87 ≈⟨ car ( id-right b) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
88 id1 A (dom b) o continuation f
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 ≈⟨ idL ⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
90 continuation f
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 ∎
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 identityR : (a : DataObj) (b : DataObj) (f : DataHom a b) → (f ∙ DataId ) ≗ f
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 identityR a b f = begin
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
94 continuation (f ∙ DataId)
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 ≈⟨⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
96 ( continuation f o ( code a o rev-code a ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
97 ≈⟨ cdr (id-left a) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
98 ( continuation f o id1 A (codom a) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
99 ≈⟨ idR ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
100 continuation f
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 ∎
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 isEquivalence : {a : DataObj } {b : DataObj } →
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 IsEquivalence {_} {_} {DataHom a b } _≗_
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 record { refl = refl-hom
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 ; sym = sym
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 ; trans = trans-hom
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
108 }
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 DataCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 DataCategory =
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 record { Obj = DataObj
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 ; Hom = DataHom
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 ; _o_ = _∙_
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 ; _≈_ = _≗_
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 ; Id = DataId
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
116 ; isCategory = isDataCategory
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 }
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 open Functor
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 open NTrans
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 F : Obj A -> Obj DataCategory
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 F d = record {
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 dom = d
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 ; codom = d
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 ; code = id1 A d
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 ; rev-code = id1 A d
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 ; id-left = idL
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
131 ; id-right = idR
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 } where open ≈-Reasoning (A)
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 U : Functor DataCategory A
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 U = record {
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 FObj = \d -> codom d
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
137 ; FMap = \f -> A [ code ( data-codom f ) o continuation f ]
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 ; isFunctor = record {
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 ≈-cong = \{a} {b} {f} {g} -> ≈-cong-1 {a} {b} {f} {g}
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 ; identity = \{a} -> identity-1 {a}
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 ; distr = \{a b c f g} -> distr-1 {a} {b} {c} {f} {g}
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 }
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 } where
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 open ≈-Reasoning (A)
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 ≈-cong-1 : {a : Obj DataCategory} {b : Obj DataCategory} {f g : Hom DataCategory a b} → DataCategory [ f ≈ g ] →
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
146 A [ A [ code (data-codom f) o continuation f ] ≈ A [ code (data-codom g) o continuation g ] ]
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 ≈-cong-1 {a} {b} {f} {g} f≈g = begin
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
148 code (data-codom f) o continuation f
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 ≈⟨⟩
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
150 code b o continuation f
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
151 ≈⟨ cdr f≈g ⟩
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
152 code b o continuation g
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 ≈⟨⟩
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
154 code (data-codom g) o continuation g
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 ∎
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
156 identity-1 : {a : Obj DataCategory} → A [ A [ code (data-codom (DataId {a})) o continuation (DataId {a}) ] ≈ id1 A (codom a) ]
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 identity-1 {a} = begin
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
158 code (data-codom (DataId {a} )) o continuation (DataId {a} )
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 ≈⟨⟩
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 code a o rev-code a
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 ≈⟨ id-left a ⟩
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 id1 A (codom a)
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 ∎
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 distr-1 : {a b c : Obj DataCategory} {f : Hom DataCategory a b} {g : Hom DataCategory b c} →
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
165 A [ A [ code (data-codom ( g ∙ f )) o continuation ( g ∙ f ) ] ≈
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
166 A [ A [ code (data-codom g) o continuation g ] o A [ code (data-codom f) o continuation f ] ] ]
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 distr-1 {a} {b} {c} {f} {g} = begin
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
168 code (data-codom (g ∙ f )) o continuation ( g ∙ f )
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 ≈⟨⟩
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
170 code c o continuation g o code b o continuation f
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 ≈⟨ assoc ⟩
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
172 (code c o continuation g ) o code b o continuation f
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 ≈⟨⟩
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
174 ( code (data-codom g) o continuation g ) o ( code (data-codom f) o continuation f )
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 ∎
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 eta-map : (a : Obj A) → Hom A a ( FObj U (F a) )
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 eta-map a = id1 A a
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 357
diff changeset
181 Lemma1 : UniversalMapping A DataCategory U
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 Lemma1 = record {
690
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 357
diff changeset
183 F = F ;
3d41a8edbf63 fix universal mapping done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 357
diff changeset
184 η = eta-map ;
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 _* = solution ;
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 isUniversalMapping = record {
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187 universalMapping = \{a} {b} {f} -> universalMapping {a} {b} {f} ;
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188 uniquness = \{a} {b} {f} {g} -> uniqueness {a} {b} {f} {g}
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
189 }
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190 } where
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
191 open ≈-Reasoning (A)
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192 solution : {a : Obj A} {b : Obj DataCategory} → Hom A a (FObj U b) → Hom DataCategory (F a) b
356
500c813af3c9 history to continuation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 355
diff changeset
193 solution {a} {b} f = record { continuation = A [ rev-code b o f ] }
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
194 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 ]
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 universalMapping {a} {b} {f} = begin
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196 FMap U (solution {a} {b} f) o eta-map a
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 ≈⟨⟩
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
198 (code b o ( rev-code b o f)) o id1 A a
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
199 ≈⟨ idR ⟩
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
200 code b o ( rev-code b o f)
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
201 ≈⟨ assoc ⟩
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
202 (code b o rev-code b ) o f
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
203 ≈⟨ car (id-left b) ⟩
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
204 id1 A (codom b) o f
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
205 ≈⟨ idL ⟩
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
206 f
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
207 ∎
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
208 uniqueness : {a : Obj A} {b : Obj DataCategory} {f : Hom A a (FObj U b)}
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
209 {g : Hom DataCategory (F a) b} →
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
210 A [ A [ FMap U g o eta-map a ] ≈ f ] →
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
211 DataCategory [ solution f ≈ g ]
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
212 uniqueness {a} {b} {f} {g} Uη≈f = begin
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
213 continuation (solution {a} {b} f)
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
214 ≈⟨⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
215 rev-code b o f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
216 ≈⟨ sym ( cdr Uη≈f ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
217 rev-code b o ( code b o continuation g ) o id1 A (codom (F a))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
218 ≈⟨ sym ( cdr assoc) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
219 rev-code b o code b o continuation g o id1 A (codom (F a))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
220 ≈⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
221 (rev-code b o code b ) o continuation g o id1 A (codom (F a))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
222 ≈⟨ car ( id-right b ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
223 id (dom b) o continuation g o id1 A (codom (F a))
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
224 ≈⟨ idL ⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
225 ( continuation g ) o id1 A (codom (F a))
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
226 ≈⟨ idR ⟩
357
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 356
diff changeset
227 continuation g
355
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
228 ∎
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
229
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
230
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
231
8fd085379380 add DataCategory Universal mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
232