Mercurial > hg > Members > kono > Proof > category
annotate CCCGraph.agda @ 817:177162990879
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 28 Apr 2019 12:37:34 +0900 |
| parents | CCChom.agda@4e48b331020a |
| children | bc244fc604c8 |
| rev | line source |
|---|---|
| 779 | 1 open import Level |
| 2 open import Category | |
| 817 | 3 module CCCgraph where |
| 779 | 4 |
| 5 open import HomReasoning | |
| 6 open import cat-utility | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
7 open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) |
| 784 | 8 open import Category.Constructions.Product |
| 790 | 9 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 817 | 10 open import CCC |
| 779 | 11 |
| 12 open Functor | |
| 13 | |
| 14 -- ccc-1 : Hom A a 1 ≅ {*} | |
| 15 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) | |
| 16 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c | |
| 17 | |
| 790 | 18 open import Category.Sets |
| 19 | |
|
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
20 -- Sets is a CCC |
|
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
21 |
| 790 | 22 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
| 23 | |
| 817 | 24 data One {l : Level} : Set l where |
| 25 OneObj : One -- () in Haskell ( or any one object set ) | |
| 790 | 26 |
| 27 sets : {l : Level } → CCC (Sets {l}) | |
| 28 sets {l} = record { | |
| 817 | 29 １ = One |
| 30 ; ○ = λ _ → λ _ → OneObj | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
31 ; _∧_ = _∧_ |
| 790 | 32 ; <_,_> = <,> |
| 33 ; π = π | |
| 34 ; π' = π' | |
| 35 ; _<=_ = _<=_ | |
| 36 ; _* = _* | |
| 37 ; ε = ε | |
| 38 ; isCCC = isCCC | |
| 39 } where | |
| 40 １ : Obj Sets | |
| 817 | 41 １ = One |
| 790 | 42 ○ : (a : Obj Sets ) → Hom Sets a １ |
| 817 | 43 ○ a = λ _ → OneObj |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
44 _∧_ : Obj Sets → Obj Sets → Obj Sets |
|
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
45 _∧_ a b = a /\ b |
|
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
46 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b) |
| 790 | 47 <,> f g = λ x → ( f x , g x ) |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
48 π : {a b : Obj Sets } → Hom Sets (a ∧ b) a |
| 790 | 49 π {a} {b} = proj₁ |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
50 π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b |
| 790 | 51 π' {a} {b} = proj₂ |
| 52 _<=_ : (a b : Obj Sets ) → Obj Sets | |
| 53 a <= b = b → a | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
54 _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b) |
| 790 | 55 f * = λ x → λ y → f ( x , y ) |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
56 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a |
| 790 | 57 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x ) |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
58 isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε |
| 790 | 59 isCCC = record { |
| 60 e2 = e2 | |
| 61 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} | |
| 62 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} | |
| 63 ; e3c = e3c | |
| 64 ; π-cong = π-cong | |
| 65 ; e4a = e4a | |
| 66 ; e4b = e4b | |
| 67 ; *-cong = *-cong | |
| 68 } where | |
| 793 | 69 e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ] |
| 70 e2 {a} {f} = extensionality Sets ( λ x → e20 x ) | |
| 790 | 71 where |
| 72 e20 : (x : a ) → f x ≡ ○ a x | |
| 73 e20 x with f x | |
| 817 | 74 e20 x | OneObj = refl |
| 790 | 75 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → |
| 76 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] | |
| 77 e3a = refl | |
| 78 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → | |
| 79 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] | |
| 80 e3b = refl | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
81 e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → |
| 790 | 82 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] |
| 83 e3c = refl | |
| 84 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → | |
| 85 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] | |
| 86 π-cong refl refl = refl | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
87 e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → |
| 790 | 88 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] |
| 89 e4a = refl | |
| 90 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → | |
| 91 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] | |
| 92 e4b = refl | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
93 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → |
| 790 | 94 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] |
| 95 *-cong refl = refl | |
| 787 | 96 |
|
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
97 module ccc-from-graph where |
| 787 | 98 |
|
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
99 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) |
| 801 | 100 open import discrete |
|
809
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
101 open graphtocat |
| 799 | 102 |
|
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
103 open Graph |
|
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
104 |
| 816 | 105 data Objs (G : Graph ) : Set where -- formula |
| 812 | 106 atom : (vertex G) → Objs G |
| 107 ⊤ : Objs G | |
| 108 _∧_ : Objs G → Objs G → Objs G | |
| 109 _<=_ : Objs G → Objs G → Objs G | |
|
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
110 |
| 816 | 111 data Arrow (G : Graph ) : Objs G → Objs G → Set where --- proof |
| 812 | 112 arrow : {a b : vertex G} → (edge G) a b → Arrow G (atom a) (atom b) |
| 113 ○ : (a : Objs G ) → Arrow G a ⊤ | |
| 114 π : {a b : Objs G } → Arrow G ( a ∧ b ) a | |
| 115 π' : {a b : Objs G } → Arrow G ( a ∧ b ) b | |
| 116 ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a | |
| 814 | 117 <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b) |
| 118 _* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b ) | |
|
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
119 |
| 817 | 120 record SM {v : Level} : Set (suc v) where |
| 806 | 121 field |
| 817 | 122 graph : Graph {v} |
| 806 | 123 sobj : vertex graph → Set |
| 124 smap : { a b : vertex graph } → edge graph a b → sobj a → sobj b | |
| 125 | |
| 126 open SM | |
|
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
127 |
|
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
128 -- positive intutionistic calculus |
| 811 | 129 PL : (G : SM) → Graph |
| 812 | 130 PL G = record { vertex = Objs (graph G) ; edge = Arrow (graph G) } |
| 806 | 131 DX : (G : SM) → Category Level.zero Level.zero Level.zero |
| 811 | 132 DX G = GraphtoCat (PL G) |
| 801 | 133 |
|
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
134 -- open import Category.Sets |
|
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
135 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
| 801 | 136 |
| 812 | 137 fobj : {G : SM} ( a : Objs (graph G) ) → Set |
| 806 | 138 fobj {G} (atom x) = sobj G x |
| 139 fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b ) | |
| 140 fobj {G} (a <= b) = fobj {G} b → fobj {G} a | |
| 817 | 141 fobj ⊤ = One |
| 812 | 142 amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b |
| 816 | 143 amap {G} (arrow x) = smap G x |
| 817 | 144 amap (○ a) _ = OneObj |
| 816 | 145 amap π ( x , _) = x |
| 146 amap π'( _ , x) = x | |
| 147 amap ε ( f , x ) = f x | |
| 148 amap < f , g > x = (amap f x , amap g x) | |
| 149 amap (f *) x = λ y → amap f ( x , y ) | |
| 812 | 150 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b |
| 816 | 151 fmap {G} {a} (id a) = λ z → z |
| 152 fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ] | |
| 805 | 153 |
|
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
154 -- CS is a map from Positive logic to Sets |
|
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
155 -- Sets is CCC, so we have a cartesian closed category generated by a graph |
|
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
156 -- as a sub category of Sets |
|
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
157 |
|
809
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
158 CS : (G : SM ) → Functor (DX G) (Sets {Level.zero}) |
|
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
159 FObj (CS G) a = fobj a |
|
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
160 FMap (CS G) {a} {b} f = fmap {G} {a} {b} f |
|
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
161 isFunctor (CS G) = isf where |
| 805 | 162 _++_ = Category._o_ (DX G) |
| 811 | 163 ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) ) |
| 164 distr : {a b c : Obj (DX G)} { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z) | |
|
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
165 distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = adistr (distr {a} {b} {d} {f} {g} z ) x where |
|
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
166 adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) → |
|
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
167 ( x : Arrow (graph G) d c ) → fmap ( next x (g ++ f) ) z ≡ fmap ( next x g ) (fmap f z ) |
|
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
168 adistr eq x = cong ( λ k → amap x k ) eq |
| 811 | 169 distr {a} {b} {b} {f} {id b} z = refl |
| 805 | 170 isf : IsFunctor (DX G) Sets fobj fmap |
|
809
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
171 IsFunctor.identity isf = extensionality Sets ( λ x → refl ) |
|
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
172 IsFunctor.≈-cong isf refl = refl |
| 811 | 173 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) |
| 801 | 174 |
| 817 | 175 --- record CCCObj { c₁ c₂ ℓ : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where |
| 176 --- field | |
| 177 --- cat : Category c₁ c₂ ℓ | |
| 178 --- ccc : CCC cat | |
| 179 --- | |
| 180 --- open CCCObj | |
| 181 --- | |
| 182 --- record CCCMap {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 183 --- field | |
| 184 --- cmap : Functor (cat A ) (cat B ) | |
| 185 --- ccf : {A B : CCCObj {c₁} {c₂} {ℓ} } → CCC (cat A) → CCC (cat B) | |
| 186 --- | |
| 187 --- Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ)) | |
| 188 --- Cart {c₁} {c₂} {ℓ} = record { | |
| 189 --- Obj = CCCObj {c₁} {c₂} {ℓ} | |
| 190 --- ; Hom = CCCMap | |
| 191 --- ; _o_ = {!!} | |
| 192 --- ; _≈_ = {!!} | |
| 193 --- ; Id = {!!} | |
| 194 --- ; isCategory = record { | |
| 195 --- identityL = {!!} | |
| 196 --- ; identityR = {!!} | |
| 197 --- ; o-resp-≈ = {!!} | |
| 198 --- ; associative = {!!} | |
| 199 --- }} | |
| 200 --- | |
| 201 --- open import discrete | |
| 202 --- open Graph | |
| 203 --- | |
| 204 --- record Gmap {v : Level} (x y : Graph {v} ) : Set (suc v) where | |
| 205 --- vmap : vertex x → vertex y | |
| 206 --- emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b) | |
| 207 --- | |
| 208 --- Grp : {v : Level} → Category (suc v) v v | |
| 209 --- Grp {v} = record { | |
| 210 --- Obj = Graph {v} | |
| 211 --- ; Hom = {!!} | |
| 212 --- ; _o_ = {!!} | |
| 213 --- ; _≈_ = {!!} | |
| 214 --- ; Id = {!!} | |
| 215 --- ; isCategory = record { | |
| 216 --- identityL = {!!} | |
| 217 --- ; identityR = {!!} | |
| 218 --- ; o-resp-≈ = {!!} | |
| 219 --- ; associative = {!!} | |
| 220 --- }} | |
| 221 --- | |
| 222 --- UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁}) | |
| 223 --- UX = {!!} | |
| 224 --- | |
| 225 --- open ccc-from-graph | |
| 226 --- | |
| 227 --- sm : {v : Level } → Graph {v} → SM {v} | |
| 228 --- SM.graph (sm g) = g | |
| 229 --- SM.sobj (sm g) = {!!} | |
| 230 --- SM.smap (sm g) = {!!} | |
| 231 --- | |
| 232 --- HX : {v : Level } ( x : Obj (Grp {v}) ) → Obj (Grp {v}) | |
| 233 --- HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ; ccc = sets } ) | |
| 234 --- | |
| 235 --- | |
| 236 --- | |
| 237 --- |