Mercurial > hg > Members > kono > Proof > category
annotate CCCGraph.agda @ 936:d13e0981e667
η on Graph to CCC
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 15 May 2020 20:10:09 +0900 |
parents | 92f8f57467e3 |
children | 2385fdd6818b |
rev | line source |
---|---|
779 | 1 open import Level |
2 open import Category | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
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 | |
931 | 24 data One {c : Level } : Set c where |
817 | 25 OneObj : One -- () in Haskell ( or any one object set ) |
790 | 26 |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
27 sets : {c : Level } → CCC (Sets {c}) |
929
1e8ed7dedc03
... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
928
diff
changeset
|
28 sets = record { |
817 | 29 1 = 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 1 : Obj Sets | |
817 | 41 1 = One |
790 | 42 ○ : (a : Obj Sets ) → Hom Sets a 1 |
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 1 ○ _∧_ <,> π π' _<=_ _* ε |
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 1} → 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 |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
97 |
933
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
98 |
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
99 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
100 open import graph |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
101 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where |
787 | 102 |
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
103 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) |
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
104 open Graph |
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
105 |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
106 data Objs : Set (suc c₁) where |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
107 atom : (vertex G) → Objs |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
108 ⊤ : Objs |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
109 _∧_ : Objs → Objs → Objs |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
110 _<=_ : Objs → Objs → Objs |
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
111 |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
112 data Arrows : (b c : Objs ) → Set (suc c₁ ⊔ c₂) |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
113 data Arrow : Objs → Objs → Set (suc c₁ ⊔ c₂) where --- case i |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
114 arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
115 π : {a b : Objs } → Arrow ( a ∧ b ) a |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
116 π' : {a b : Objs } → Arrow ( a ∧ b ) b |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
117 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
118 _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
119 |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
120 data Arrows where |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
121 id : ( a : Objs ) → Arrows a a --- case i |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
122 ○ : ( a : Objs ) → Arrows a ⊤ --- case i |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
123 <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
124 iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv |
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
125 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
126 _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
127 id a ・ g = g |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
128 ○ a ・ g = ○ _ |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
129 < f , g > ・ h = < f ・ h , g ・ h > |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
130 iv f g ・ h = iv f ( g ・ h ) |
819 | 131 |
933
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
132 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
133 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
134 identityL = refl |
819 | 135 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
136 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
137 identityR {a} {a} {id a} = refl |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
138 identityR {a} {⊤} {○ a} = refl |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
139 identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
140 identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR |
819 | 141 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
142 assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
143 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
144 assoc≡ (id a) g h = refl |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
145 assoc≡ (○ a) g h = refl |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
146 assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
147 assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) |
819 | 148 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
149 -- positive intutionistic calculus |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
150 PL : Category (suc c₁) (suc c₁ ⊔ c₂) (suc c₁ ⊔ c₂) |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
151 PL = record { |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
152 Obj = Objs; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
153 Hom = λ a b → Arrows a b ; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
154 _o_ = λ{a} {b} {c} x y → x ・ y ; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
155 _≈_ = λ x y → x ≡ y ; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
156 Id = λ{a} → id a ; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
157 isCategory = record { |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
158 isEquivalence = record {refl = refl ; trans = trans ; sym = sym} ; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
159 identityL = λ {a b f} → identityL {a} {b} {f} ; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
160 identityR = λ {a b f} → identityR {a} {b} {f} ; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
161 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
162 associative = λ{a b c d f g h } → assoc≡ f g h |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
163 } |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
164 } where |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
165 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
166 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
167 o-resp-≈ refl refl = refl |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
168 |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
169 -------- |
819 | 170 -- |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
171 -- Functor from Positive Logic to Sets |
819 | 172 -- |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
173 |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
174 -- open import Category.Sets |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
175 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂ |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
176 |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
177 open import Data.List |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
178 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
179 C = graphtocat.Chain G |
819 | 180 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
181 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
182 tr f x y = graphtocat.next f (x y) |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
183 |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
184 fobj : ( a : Objs ) → Set (c₁ ⊔ c₂) |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
185 fobj (atom x) = ( y : vertex G ) → C y x |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
186 fobj ⊤ = One |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
187 fobj (a ∧ b) = ( fobj a /\ fobj b) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
188 fobj (a <= b) = fobj b → fobj a |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
189 |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
190 fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
191 amap : { a b : Objs } → Arrow a b → fobj a → fobj b |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
192 amap (arrow x) y = tr x y -- tr x |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
193 amap π ( x , y ) = x |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
194 amap π' ( x , y ) = y |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
195 amap ε (f , x ) = f x |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
196 amap (f *) x = λ y → fmap f ( x , y ) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
197 fmap (id a) x = x |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
198 fmap (○ a) x = OneObj |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
199 fmap < f , g > x = ( fmap f x , fmap g x ) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
200 fmap (iv x f) a = amap x ( fmap f a ) |
819 | 201 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
202 -- CS is a map from Positive logic to Sets |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
203 -- Sets is CCC, so we have a cartesian closed category generated by a graph |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
204 -- as a sub category of Sets |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
205 |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
206 CS : Functor PL (Sets {c₁ ⊔ c₂}) |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
207 FObj CS a = fobj a |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
208 FMap CS {a} {b} f = fmap {a} {b} f |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
209 isFunctor CS = isf where |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
210 _+_ = Category._o_ PL |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
211 ++idR = IsCategory.identityR ( Category.isCategory PL ) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
212 distr : {a b c : Obj PL} { f : Hom PL a b } { g : Hom PL b c } → (z : fobj a ) → fmap (g + f) z ≡ fmap g (fmap f z) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
213 distr {a} {a₁} {a₁} {f} {id a₁} z = refl |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
214 distr {a} {a₁} {⊤} {f} {○ a₁} z = refl |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
215 distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k → j , k ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
216 distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr {a} {b} {d} {f} {g} z) x where |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
217 adistr : fmap (g + f) z ≡ fmap g (fmap f z) → |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
218 ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
219 adistr eq x = cong ( λ k → amap x k ) eq |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
220 isf : IsFunctor PL Sets fobj fmap |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
221 IsFunctor.identity isf = extensionality Sets ( λ x → refl ) |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
222 IsFunctor.≈-cong isf refl = refl |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
223 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) |
819 | 224 |
818 | 225 --- |
226 --- SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap | |
227 --- | |
228 --- CCC ( SC (CS G)) Sets have to be proved | |
229 --- SM can be eliminated if we have | |
230 --- sobj (a : vertex g ) → {a} a set have only a | |
231 --- smap (a b : vertex g ) → {a} → {b} | |
232 | |
233 | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
234 record CCCObj {c₁ c₂ ℓ : Level} : Set (suc (ℓ ⊔ (c₂ ⊔ c₁))) where |
818 | 235 field |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
236 cat : Category c₁ c₂ ℓ |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
237 ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g |
818 | 238 ccc : CCC cat |
239 | |
240 open CCCObj | |
241 | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
242 record CCCMap {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (A : CCCObj {c₁} {c₂} {ℓ} ) (B : CCCObj {c₁′} {c₂′}{ℓ′} ) : Set (suc (ℓ′ ⊔ (c₂′ ⊔ c₁′) ⊔ ℓ ⊔ (c₂ ⊔ c₁))) where |
818 | 243 field |
244 cmap : Functor (cat A ) (cat B ) | |
820 | 245 ccf : CCC (cat A) → CCC (cat B) |
246 | |
247 open import Category.Cat | |
248 | |
249 open CCCMap | |
250 open import Relation.Binary.Core | |
818 | 251 |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
252 Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (ℓ ⊔ (c₂ ⊔ c₁))) (suc (ℓ ⊔ c₁ ⊔ c₂)) |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
253 Cart {c₁} {c₂} {ℓ} = record { |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
254 Obj = CCCObj {c₁} {c₂} {ℓ} |
820 | 255 ; Hom = CCCMap |
824 | 256 ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) } |
820 | 257 ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g |
258 ; Id = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x } | |
259 ; isCategory = record { | |
260 isEquivalence = λ {A} {B} → record { | |
261 refl = λ {f} → let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f} | |
262 ; sym = λ {f} {g} → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g} | |
263 ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h} } | |
821 | 264 ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_} |
265 ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f} | |
266 ; 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} | |
267 ; 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 | 268 }} |
818 | 269 |
825 | 270 open import graph |
818 | 271 open Graph |
272 | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
273 record GMap {c₁ c₂ c₁' c₂' : Level} (x : Graph {c₁} {c₂} ) (y : Graph {c₁'} {c₂'} ) : Set (c₁ ⊔ c₂ ⊔ c₁' ⊔ c₂') where |
820 | 274 field |
818 | 275 vmap : vertex x → vertex y |
276 emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b) | |
277 | |
820 | 278 open GMap |
279 | |
821 | 280 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) |
281 | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
282 data [_]_==_ {c₁ c₂ : Level} (C : Graph {c₁} {c₂}) {A B : vertex C} (f : edge C A B) |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
283 : ∀{X Y : vertex C} → edge C X Y → Set (c₁ ⊔ c₂ ) where |
824 | 284 mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g |
285 | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
286 _=m=_ : {c₁ c₂ c₁' c₂' : Level} {C : Graph {c₁} {c₂} } {D : Graph {c₁'} {c₂'} } |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
287 → (F G : GMap C D) → Set (c₁ ⊔ c₂ ⊔ c₁' ⊔ c₂') |
824 | 288 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f |
821 | 289 |
934
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
290 _&_ : {c₁ c₂ c₁' c₂' c₁'' c₂'' : Level} {x : Graph {c₁} {c₂}} {y : Graph {c₁'} {c₂'}} {z : Graph {c₁''} {c₂''} } ( f : GMap y z ) ( g : GMap x y ) → GMap x z |
821 | 291 f & g = record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) } |
292 | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
293 Grph : {c₁ c₂ : Level} → Category (suc (c₁ ⊔ c₂)) (c₁ ⊔ c₂) (c₁ ⊔ c₂) |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
294 Grph {c₁} {c₂} = record { |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
295 Obj = Graph {c₁} {c₂} |
929
1e8ed7dedc03
... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
928
diff
changeset
|
296 ; Hom = GMap |
821 | 297 ; _o_ = _&_ |
298 ; _≈_ = _=m=_ | |
820 | 299 ; Id = record { vmap = λ y → y ; emap = λ f → f } |
300 ; isCategory = record { | |
824 | 301 isEquivalence = λ {A} {B} → ise |
302 ; identityL = λ e → mrefl refl | |
303 ; identityR = λ e → mrefl refl | |
821 | 304 ; o-resp-≈ = m--resp-≈ |
824 | 305 ; associative = λ e → mrefl refl |
821 | 306 }} where |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
307 msym : {x y : Graph {c₁} {c₂} } { f g : GMap x y } → f =m= g → g =m= f |
929
1e8ed7dedc03
... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
928
diff
changeset
|
308 msym {x} {y} f=g f = lemma ( f=g f ) where |
824 | 309 lemma : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f |
310 lemma (mrefl Ff≈Gf) = mrefl (sym Ff≈Gf) | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
311 mtrans : {x y : Graph {c₁} {c₂} } { f g h : GMap x y } → f =m= g → g =m= h → f =m= h |
929
1e8ed7dedc03
... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
928
diff
changeset
|
312 mtrans {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where |
824 | 313 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 |
314 lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv eqv₁ ) | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
315 ise : {x y : Graph {c₁} {c₂} } → IsEquivalence {_} {c₁ ⊔ c₂} {_} ( _=m=_ {_} {_} {_} {_} {x} {y}) |
821 | 316 ise = record { |
824 | 317 refl = λ f → mrefl refl |
821 | 318 ; sym = msym |
319 ; trans = mtrans | |
320 } | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
321 m--resp-≈ : {A B C : Graph {c₁} {c₂} } |
824 | 322 {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g ) |
929
1e8ed7dedc03
... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
928
diff
changeset
|
323 m--resp-≈ {A} {B} {C} {f} {g} {h} {i} f=g h=i e = |
824 | 324 lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where |
325 lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) → | |
326 [ B ] ϕ == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π | |
327 lemma _ _ _ (mrefl refl) (mrefl refl) = mrefl refl | |
820 | 328 |
821 | 329 --- Forgetful functor |
330 | |
934
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
331 module forgetful {c₁ c₂ : Level} where |
927 | 332 |
333 ≃-cong : {c₁ c₂ ℓ : Level} (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B } | |
822
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
334 → { 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
|
335 → { 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
|
336 → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g' |
927 | 337 ≃-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 |
822
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
338 f' |
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
339 ≈↑⟨ f=f' ⟩ |
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
340 f |
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
341 ≈⟨ eqv ⟩ |
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
342 g |
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
343 ≈⟨ g=g' ⟩ |
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
344 g' |
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
345 ∎ ) |
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
346 |
934
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
347 -- Grph does not allow morph on different level graphs |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
348 -- simply assumes we have iso to the another level. This may means same axiom on CCCs results the same CCCs. |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
349 postulate |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
350 g21 : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} → Graph {c₁} {c₂} |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
351 m21 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁} {c₂} g (g21 g) |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
352 m12 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {c₁} {c₂} {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} (g21 g) g |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
353 giso→ : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} } |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
354 → {a b : vertex g } → {e : edge g a b } → (m12 g & m21 g) =m= id1 Grph g |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
355 giso← : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} } |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
356 → {a b : vertex (g21 g) } → {e : edge (g21 g) a b } → (m21 g & m12 g ) =m= id1 Grph (g21 g) |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
357 -- Grph [ Grph [ m21 g o m12 g ] ≈ id1 Grph (g21 g) ] |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
358 |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
359 fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
360 fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) } |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
361 fmap : {a b : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂} ) } → Hom (Cart ) a b → Hom (Grph {c₁} {c₂}) (g21 ( fobj a )) (g21 ( fobj b )) |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
362 fmap {a} {b} f = record { |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
363 vmap = λ e → vmap (m21 (fobj b)) (FObj (cmap f) (vmap (m12 (fobj a)) e )) |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
364 ; emap = λ e → emap (m21 (fobj b)) (FMap (cmap f) (emap (m12 (fobj a)) e )) } |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
365 |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
366 UX : Functor (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂}) |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
367 FObj UX a = g21 (fobj a) |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
368 FMap UX f = fmap f |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
369 isFunctor UX = isf where |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
370 isf : IsFunctor Cart Grph (λ z → g21 (fobj z)) fmap |
935 | 371 eff : (a : Obj Cart) (f : vertex (g21 (fobj a)) ) → edge (g21 (fobj a)) f f |
372 eff a f = {!!} | |
373 IsFunctor.identity isf {a} {b} {f} = begin | |
374 fmap (id1 Cart a) | |
375 ≈⟨⟩ | |
376 fmap {a} {a} (record { cmap = identityFunctor ; ccf = λ x → x }) | |
377 ≈⟨⟩ | |
378 record { vmap = λ e → vmap (m21 (fobj a)) (vmap (m12 (fobj a)) e ) ; emap = λ e → emap (m21 (fobj a)) (emap (m12 (fobj a)) e )} | |
379 ≈⟨ giso← {fobj a} {f} {f} {eff a f } ⟩ | |
380 record { vmap = λ y → y ; emap = λ f → f } | |
381 ≈⟨⟩ | |
382 id1 Grph (g21 (fobj a)) | |
383 ∎ where open ≈-Reasoning Grph | |
384 IsFunctor.distr isf {a} {b} {c} {f} {g} = begin | |
385 fmap ( Cart [ g o f ] ) | |
386 ≈⟨ {!!} ⟩ | |
387 Grph [ fmap g o fmap f ] | |
388 ∎ where open ≈-Reasoning Grph | |
934
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
389 IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} where -- lemma ( (extensionality Sets ( λ z → lemma4 ( |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
390 -- ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g))) |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
391 -- )))) (f=g e) where |
927 | 392 lemma4 : {x y : vertex (fobj b)} → [_]_~_ (cat b) (id1 (cat b) x) (id1 (cat b) y) → x ≡ y |
393 lemma4 (refl eqv) = refl | |
934
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
394 -- lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ g21 (fobj b)] emap (fmap f) {!!} == emap (fmap g) {!!} |
cce9e539486e
workaround on forget functor level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
933
diff
changeset
|
395 -- lemma = {!!} -- refl (refl eqv) = mrefl (≡←≈ b eqv) |
824 | 396 |
821 | 397 |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
398 open ccc-from-graph.Objs |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
399 open ccc-from-graph.Arrow |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
400 open ccc-from-graph.Arrows |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
401 open graphtocat.Chain |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
402 |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
403 Sets0 : {c₂ : Level } → Category (suc c₂) c₂ c₂ |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
404 Sets0 {c₂} = Sets {c₂} |
930 | 405 |
933
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
406 ccc-graph-univ : {c₁ c₂ : Level} → UniversalMapping (Grph {c₁} {c₂}) (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) forgetful.UX |
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
407 ccc-graph-univ {c₁} {c₂} = record { |
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
408 F = F ; |
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
409 η = η ; -- λ a → record { vmap = λ y → graphtocat.Chain {!!} {!!} {!!} ; emap = λ f x → {!!} } ; -- |
927 | 410 _* = solution ; |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
411 isUniversalMapping = record { |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
412 universalMapping = {!!} ; |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
413 uniquness = {!!} |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
414 } |
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
415 } where |
929
1e8ed7dedc03
... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
928
diff
changeset
|
416 open forgetful |
926 | 417 open ccc-from-graph |
935 | 418 -- η : Hom Grph a (FObj UX (F a)) |
936 | 419 -- f : edge g x y -----------------------------------> m21 (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph |
935 | 420 -- Graph g x ----------------------> y : vertex g ↑ |
421 -- arrow f : Hom (PL g) (atom x) (atom y) | | |
422 -- PL g atom x ------------------> atom y : Obj (PL g) | UX : Functor Sets Graph | |
423 -- | | | |
424 -- | Functor (CS g) | | |
425 -- ↓ | | |
426 -- Sets ((z : vertx g) → C z x) ----> ((z : vertx g) → C z y) = h : Hom Sets (fobj (atom x)) (fobj (atom y)) | |
427 -- | |
428 cs : {c₁ c₂ : Level} → (g : Graph {c₁} {c₂} ) → Functor (ccc-from-graph.PL g) (Sets {_}) | |
429 cs g = CS g | |
933
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
430 F : Obj (Grph {c₁} {c₂}) → Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) |
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
431 F g = record { cat = Sets {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } |
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
432 η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a)) |
936 | 433 η a = record { vmap = λ y → vm y ; emap = λ f → em f } where |
434 fo : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} | |
435 fo = forgetful.fobj {c₁} {c₂} (F a) | |
436 vm : (y : vertex a ) → vertex (g21 fo) | |
437 vm y = vmap (m21 fo) (ccc-from-graph.fobj a (atom y)) | |
438 em : { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) (vm x) (vm y) | |
439 em {x} {y} f = emap (m21 fo) (ccc-from-graph.fmap a (iv (arrow f) (id _))) | |
440 | |
935 | 441 -- k : ( y : vertex a) → Set (c₁ ⊔ c₂) |
442 -- k y = ( e : vertex a ) → graphtocat.Chain a e y | |
443 -- mm : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)} | |
444 -- mm = forgetful.fobj {c₁} {c₂} (F a) | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
445 pl : {c₁ c₂ : Level} → (g : Graph {c₁} {c₂} ) → Category _ _ _ |
926 | 446 pl g = PL g |
933
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
447 cobj : {g : Obj (Grph {c₁} {c₂} ) } {c : Obj Cart} → Hom Grph g (FObj UX c) → Objs g → Obj (cat c) |
e702aa8be9dd
level try and CCC bad approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
932
diff
changeset
|
448 cobj {g} {c} f (atom x) = {!!} -- vmap f x |
912 | 449 cobj {g} {c} f ⊤ = CCC.1 (ccc c) |
914 | 450 cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y) |
451 cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) | |
932
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
452 c-map : {g : Obj (Grph )} {c : Obj Cart} {A B : Objs g} |
f19425b54aba
introduce detailed level on CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
931
diff
changeset
|
453 → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl g) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B) |
926 | 454 c-map {g} {c} {atom a} {atom x} f y = {!!} |
927 | 455 c-map {g} {c} {⊤} {atom x} f (iv f1 y) = {!!} |
456 c-map {g} {c} {a ∧ b} {atom x} f (iv f1 y) = {!!} | |
926 | 457 c-map {g} {c} {b <= a} {atom x} f y = {!!} |
914 | 458 c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a) |
926 | 459 c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f {!!}) (c-map f {!!}) |
460 c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!}) | |
935 | 461 solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c |
929
1e8ed7dedc03
... simpler level on CCC Graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
928
diff
changeset
|
462 solution {g} {c} f = {!!} -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} } |
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
463 |
912 | 464 |