Mercurial > hg > Members > kono > Proof > category
annotate CCCGraph.agda @ 860:d3cf372ac8cd
give update idempotent
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 05 Apr 2020 11:53:00 +0900 |
| parents | a115daa7d30e |
| children | 484f19f16712 32c11e2fdf82 |
| 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 | |
| 826 | 20 ------------------------------------------------------ |
|
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
21 -- Sets is a CCC |
| 826 | 22 ------------------------------------------------------ |
|
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
23 |
| 790 | 24 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
| 25 | |
| 817 | 26 data One {l : Level} : Set l where |
| 27 OneObj : One -- () in Haskell ( or any one object set ) | |
| 790 | 28 |
| 29 sets : {l : Level } → CCC (Sets {l}) | |
| 30 sets {l} = record { | |
| 817 | 31 １ = One |
| 32 ; ○ = λ _ → λ _ → OneObj | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
33 ; _∧_ = _∧_ |
| 790 | 34 ; <_,_> = <,> |
| 35 ; π = π | |
| 36 ; π' = π' | |
| 37 ; _<=_ = _<=_ | |
| 38 ; _* = _* | |
| 39 ; ε = ε | |
| 40 ; isCCC = isCCC | |
| 41 } where | |
| 42 １ : Obj Sets | |
| 817 | 43 １ = One |
| 790 | 44 ○ : (a : Obj Sets ) → Hom Sets a １ |
| 817 | 45 ○ a = λ _ → OneObj |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
46 _∧_ : Obj Sets → Obj Sets → Obj Sets |
|
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
47 _∧_ a b = a /\ b |
|
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
48 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b) |
| 790 | 49 <,> 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
|
50 π : {a b : Obj Sets } → Hom Sets (a ∧ b) a |
| 790 | 51 π {a} {b} = proj₁ |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
52 π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b |
| 790 | 53 π' {a} {b} = proj₂ |
| 54 _<=_ : (a b : Obj Sets ) → Obj Sets | |
| 55 a <= b = b → a | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
56 _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b) |
| 790 | 57 f * = λ x → λ y → f ( x , y ) |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
58 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a |
| 790 | 59 ε {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
|
60 isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε |
| 790 | 61 isCCC = record { |
| 62 e2 = e2 | |
| 63 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} | |
| 64 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} | |
| 65 ; e3c = e3c | |
| 66 ; π-cong = π-cong | |
| 67 ; e4a = e4a | |
| 68 ; e4b = e4b | |
| 69 ; *-cong = *-cong | |
| 70 } where | |
| 793 | 71 e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ] |
| 72 e2 {a} {f} = extensionality Sets ( λ x → e20 x ) | |
| 790 | 73 where |
| 74 e20 : (x : a ) → f x ≡ ○ a x | |
| 75 e20 x with f x | |
| 817 | 76 e20 x | OneObj = refl |
| 790 | 77 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → |
| 78 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] | |
| 79 e3a = refl | |
| 80 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → | |
| 81 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] | |
| 82 e3b = refl | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
83 e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → |
| 790 | 84 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] |
| 85 e3c = refl | |
| 86 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → | |
| 87 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] | |
| 88 π-cong refl refl = refl | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
89 e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → |
| 790 | 90 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] |
| 91 e4a = refl | |
| 92 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → | |
| 93 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] | |
| 94 e4b = refl | |
|
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
95 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → |
| 790 | 96 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] |
| 97 *-cong refl = refl | |
| 787 | 98 |
| 830 | 99 module sets-from-graph where |
| 787 | 100 |
| 826 | 101 ------------------------------------------------------ |
| 102 -- CCC generated from a graph | |
| 103 ------------------------------------------------------ | |
| 104 | |
|
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
105 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) |
| 825 | 106 open import graph |
|
809
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
107 open graphtocat |
| 799 | 108 |
|
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
109 open Graph |
|
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
110 |
| 821 | 111 data Objs (G : Graph {Level.zero} {Level.zero} ) : Set where -- formula |
| 812 | 112 atom : (vertex G) → Objs G |
| 113 ⊤ : Objs G | |
| 114 _∧_ : Objs G → Objs G → Objs G | |
| 115 _<=_ : Objs G → Objs G → Objs G | |
|
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
116 |
| 816 | 117 data Arrow (G : Graph ) : Objs G → Objs G → Set where --- proof |
| 812 | 118 arrow : {a b : vertex G} → (edge G) a b → Arrow G (atom a) (atom b) |
| 119 ○ : (a : Objs G ) → Arrow G a ⊤ | |
| 120 π : {a b : Objs G } → Arrow G ( a ∧ b ) a | |
| 121 π' : {a b : Objs G } → Arrow G ( a ∧ b ) b | |
| 122 ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a | |
| 814 | 123 <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b) |
| 124 _* : {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
|
125 |
| 817 | 126 record SM {v : Level} : Set (suc v) where |
| 806 | 127 field |
| 821 | 128 graph : Graph {v} {v} |
| 806 | 129 sobj : vertex graph → Set |
| 130 smap : { a b : vertex graph } → edge graph a b → sobj a → sobj b | |
| 131 | |
| 132 open SM | |
|
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
133 |
|
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
134 -- positive intutionistic calculus |
| 811 | 135 PL : (G : SM) → Graph |
| 812 | 136 PL G = record { vertex = Objs (graph G) ; edge = Arrow (graph G) } |
| 806 | 137 DX : (G : SM) → Category Level.zero Level.zero Level.zero |
| 811 | 138 DX G = GraphtoCat (PL G) |
| 801 | 139 |
|
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
140 -- open import Category.Sets |
|
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
141 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
| 801 | 142 |
| 812 | 143 fobj : {G : SM} ( a : Objs (graph G) ) → Set |
| 806 | 144 fobj {G} (atom x) = sobj G x |
| 145 fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b ) | |
| 146 fobj {G} (a <= b) = fobj {G} b → fobj {G} a | |
| 817 | 147 fobj ⊤ = One |
| 812 | 148 amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b |
| 816 | 149 amap {G} (arrow x) = smap G x |
| 817 | 150 amap (○ a) _ = OneObj |
| 816 | 151 amap π ( x , _) = x |
| 152 amap π'( _ , x) = x | |
| 153 amap ε ( f , x ) = f x | |
| 154 amap < f , g > x = (amap f x , amap g x) | |
| 155 amap (f *) x = λ y → amap f ( x , y ) | |
| 812 | 156 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b |
| 816 | 157 fmap {G} {a} (id a) = λ z → z |
| 158 fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ] | |
| 805 | 159 |
|
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
160 -- 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
|
161 -- 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
|
162 -- 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
|
163 |
|
809
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
164 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
|
165 FObj (CS G) a = fobj a |
|
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
166 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
|
167 isFunctor (CS G) = isf where |
| 805 | 168 _++_ = Category._o_ (DX G) |
| 811 | 169 ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) ) |
| 170 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
|
171 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
|
172 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
|
173 ( 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
|
174 adistr eq x = cong ( λ k → amap x k ) eq |
| 811 | 175 distr {a} {b} {b} {f} {id b} z = refl |
| 805 | 176 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
|
177 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
|
178 IsFunctor.≈-cong isf refl = refl |
| 811 | 179 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) |
| 801 | 180 |
| 830 | 181 |
| 826 | 182 ------------------------------------------------------ |
| 183 -- Cart Category of CCC and CCC preserving Functor | |
| 184 ------------------------------------------------------ | |
| 185 | |
| 818 | 186 --- |
| 187 --- SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap | |
| 188 --- | |
| 189 --- CCC ( SC (CS G)) Sets have to be proved | |
| 190 --- SM can be eliminated if we have | |
| 191 --- sobj (a : vertex g ) → {a} a set have only a | |
| 192 --- smap (a b : vertex g ) → {a} → {b} | |
| 193 | |
| 194 | |
| 195 record CCCObj { c₁ c₂ ℓ : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where | |
| 196 field | |
| 197 cat : Category c₁ c₂ ℓ | |
| 198 ccc : CCC cat | |
| 199 | |
| 200 open CCCObj | |
| 201 | |
| 202 record CCCMap {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 203 field | |
| 204 cmap : Functor (cat A ) (cat B ) | |
| 820 | 205 ccf : CCC (cat A) → CCC (cat B) |
| 206 | |
| 207 open import Category.Cat | |
| 208 | |
| 209 open CCCMap | |
| 210 open import Relation.Binary.Core | |
| 818 | 211 |
| 820 | 212 Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ)) |
| 213 Cart {c₁} {c₂} {ℓ} = record { | |
| 214 Obj = CCCObj {c₁} {c₂} {ℓ} | |
| 215 ; Hom = CCCMap | |
| 824 | 216 ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) } |
| 820 | 217 ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g |
| 218 ; Id = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x } | |
| 219 ; isCategory = record { | |
| 220 isEquivalence = λ {A} {B} → record { | |
| 221 refl = λ {f} → let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f} | |
| 222 ; sym = λ {f} {g} → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g} | |
| 223 ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h} } | |
| 821 | 224 ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_} |
| 225 ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f} | |
| 226 ; o-resp-≈ = λ {x} {y} {z} {f} {g} {h} {i} → IsCategory.o-resp-≈ ( Category.isCategory CAT) {cat x}{cat y}{cat z} {cmap f} {cmap g} {cmap h} {cmap i} | |
| 227 ; associative = λ {a} {b} {c} {d} {f} {g} {h} → let open ≈-Reasoning (CAT) in assoc {cat a} {cat b} {cat c} {cat d} {cmap f} {cmap g} {cmap h} | |
| 824 | 228 }} |
| 818 | 229 |
| 826 | 230 ------------------------------------------------------ |
| 231 -- Grph Category of Graph and Graph mapping | |
| 232 ------------------------------------------------------ | |
| 233 | |
| 825 | 234 open import graph |
| 818 | 235 open Graph |
| 236 | |
| 825 | 237 record GMap {v v' : Level} (x y : Graph {v} {v'} ) : Set (suc (v ⊔ v') ) where |
| 820 | 238 field |
| 818 | 239 vmap : vertex x → vertex y |
| 240 emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b) | |
| 241 | |
| 820 | 242 open GMap |
| 243 | |
| 821 | 244 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) |
| 245 | |
| 824 | 246 data [_]_==_ {c₁ c₂ } (C : Graph {c₁} {c₂} ) {A B : vertex C} (f : edge C A B) |
| 247 : ∀{X Y : vertex C} → edge C X Y → Set (suc (c₁ ⊔ c₂ )) where | |
| 248 mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g | |
| 249 | |
| 250 _=m=_ : ∀ {c₁ c₂ } {C D : Graph {c₁} {c₂} } | |
| 251 → (F G : GMap C D) → Set (suc (c₂ ⊔ c₁)) | |
| 252 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f | |
| 821 | 253 |
| 254 _&_ : {v v' : Level} {x y z : Graph {v} {v'}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z | |
| 255 f & g = record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) } | |
| 256 | |
| 829 | 257 Grph : {v v' : Level} → Category (suc (v ⊔ v')) (suc (v ⊔ v')) (suc ( v ⊔ v')) |
| 826 | 258 Grph {v} {v'} = record { |
| 821 | 259 Obj = Graph {v} {v'} |
| 260 ; Hom = GMap {v} {v'} | |
| 261 ; _o_ = _&_ | |
| 262 ; _≈_ = _=m=_ | |
| 820 | 263 ; Id = record { vmap = λ y → y ; emap = λ f → f } |
| 264 ; isCategory = record { | |
| 824 | 265 isEquivalence = λ {A} {B} → ise |
| 266 ; identityL = λ e → mrefl refl | |
| 267 ; identityR = λ e → mrefl refl | |
| 821 | 268 ; o-resp-≈ = m--resp-≈ |
| 824 | 269 ; associative = λ e → mrefl refl |
| 821 | 270 }} where |
| 824 | 271 msym : {v v' : Level} {x y : Graph {v} {v'} } { f g : GMap x y } → f =m= g → g =m= f |
| 272 msym {_} {_} {x} {y} f=g f = lemma ( f=g f ) where | |
| 273 lemma : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f | |
| 274 lemma (mrefl Ff≈Gf) = mrefl (sym Ff≈Gf) | |
| 275 mtrans : {v v' : Level} {x y : Graph {v} {v'} } { f g h : GMap x y } → f =m= g → g =m= h → f =m= h | |
| 276 mtrans {_} {_} {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where | |
| 277 lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f} → [ y ] p == q → [ y ] q == r → [ y ] p == r | |
| 278 lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv eqv₁ ) | |
| 279 ise : {v v' : Level} {x y : Graph {v} {v'}} → IsEquivalence {_} {suc v ⊔ suc v' } {_} ( _=m=_ {v} {v'} {x} {y}) | |
| 821 | 280 ise = record { |
| 824 | 281 refl = λ f → mrefl refl |
| 821 | 282 ; sym = msym |
| 283 ; trans = mtrans | |
| 284 } | |
| 824 | 285 m--resp-≈ : {v v' : Level} {A B C : Graph {v} {v'} } |
| 286 {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g ) | |
| 287 m--resp-≈ {_} {_} {A} {B} {C} {f} {g} {h} {i} f=g h=i e = | |
| 288 lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where | |
| 289 lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) → | |
| 290 [ B ] ϕ == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π | |
| 291 lemma _ _ _ (mrefl refl) (mrefl refl) = mrefl refl | |
| 820 | 292 |
| 826 | 293 ------------------------------------------------------ |
| 294 --- CCC → Grph Forgetful functor | |
| 295 ------------------------------------------------------ | |
| 821 | 296 |
|
822
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
297 ≃-cong : {c₁ c₂ ℓ : Level} (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B } |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
298 → { f f' : Hom B a b } |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
299 → { g g' : Hom B a' b' } |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
300 → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g' |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
301 ≃-cong B {a} {b} {a'} {b'} {f} {f'} {g} {g'} (refl {g2} eqv) f=f' g=g' = let open ≈-Reasoning B in refl {_} {_} {_} {B} {a'} {b'} {f'} {g'} ( begin |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
302 f' |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
303 ≈↑⟨ f=f' ⟩ |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
304 f |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
305 ≈⟨ eqv ⟩ |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
306 g |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
307 ≈⟨ g=g' ⟩ |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
308 g' |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
309 ∎ ) |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
310 |
| 826 | 311 fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} ) → Obj (Grph {c₁} {c₂}) |
| 824 | 312 fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) } |
| 826 | 313 fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {c₁} {c₂}) ( fobj a ) ( fobj b ) |
| 824 | 314 fmap f = record { vmap = FObj (cmap f) ; emap = FMap (cmap f) } |
|
822
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
315 |
| 823 | 316 UX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) → {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g ) |
| 826 | 317 → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}) |
| 823 | 318 FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡ ) a = fobj a |
| 319 FMap (UX ≈-to-≡) f = fmap f | |
| 320 isFunctor (UX {c₁} {c₂} {ℓ} ≈-to-≡) = isf where | |
| 824 | 321 -- if we don't need ≈-cong ( i.e. f ≈ g → UX f =m= UX g ), all lemmas are not necessary |
|
822
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
322 open import HomReasoning |
| 826 | 323 isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}) fobj fmap |
| 824 | 324 IsFunctor.identity isf {a} {b} {f} e = mrefl refl |
| 325 IsFunctor.distr isf f = mrefl refl | |
| 326 IsFunctor.≈-cong isf {a} {b} {f} {g} eq {x} {y} e = lemma (extensionality Sets ( λ z → lemma4 ( | |
| 327 ≃-cong (cat b) (eq (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g))) | |
| 328 ))) (eq e) where | |
| 329 lemma4 : {x y : vertex (fobj b) } → [_]_~_ (cat b) (id1 (cat b) x) (id1 (cat b) y) → x ≡ y | |
| 330 lemma4 (refl eqv) = refl | |
| 331 lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e | |
| 332 lemma refl (refl eqv) = mrefl ( ≈-to-≡ (cat b) eqv ) | |
| 333 | |
| 821 | 334 |
| 817 | 335 --- |
| 336 --- open ccc-from-graph | |
| 337 --- | |
| 338 --- sm : {v : Level } → Graph {v} → SM {v} | |
| 339 --- SM.graph (sm g) = g | |
| 340 --- SM.sobj (sm g) = {!!} | |
| 341 --- SM.smap (sm g) = {!!} | |
| 342 --- | |
| 826 | 343 --- HX : {v : Level } ( x : Obj (Grph {v}) ) → Obj (Grph {v}) |
| 817 | 344 --- HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ; ccc = sets } ) |
| 345 --- | |
| 346 --- | |
| 347 --- | |
| 348 --- |