Mercurial > hg > Members > kono > Proof > category
annotate CCCGraph.agda @ 927:2c5ae3015a05
level hell
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 May 2020 16:36:42 +0900 |
| parents | a7332c329b57 |
| children | c1222aa20244 |
| rev | line source |
|---|---|
| 779 | 1 open import Level |
| 2 open import Category | |
| 927 | 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 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
97 open import graph |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
98 module ccc-from-graph {c₁ c₂ : Level} (G : Graph {c₁} {c₂} ) where |
| 787 | 99 |
|
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
100 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
|
101 open Graph |
|
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
102 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
103 data Objs : Set c₁ where |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
104 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
|
105 ⊤ : Objs |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
106 _∧_ : 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
|
107 _<=_ : Objs → Objs → Objs |
|
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
108 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
109 data Arrows : (b c : Objs ) → Set ( c₁ ⊔ c₂ ) |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
110 data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
111 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
|
112 π : {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
|
113 π' : {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
|
114 ε : {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
|
115 _* : {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
|
116 |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
117 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
|
118 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
|
119 ○ : ( 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
|
120 <_,_> : {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
|
121 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
|
122 |
|
911
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 } (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
|
124 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
|
125 ○ a ・ g = ○ _ |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
126 < 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
|
127 iv f g ・ h = iv f ( g ・ h ) |
| 819 | 128 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
129 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
|
130 identityL = refl |
| 819 | 131 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
132 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
|
133 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
|
134 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
|
135 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
|
136 identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR |
| 819 | 137 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
138 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
|
139 (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
|
140 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
|
141 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
|
142 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
|
143 assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) |
| 819 | 144 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
145 -- positive intutionistic calculus |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
146 PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂) |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
147 PL = record { |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
148 Obj = Objs; |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
149 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
|
150 _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
|
151 _≈_ = λ 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
|
152 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
|
153 isCategory = record { |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
154 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
|
155 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
|
156 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
|
157 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
|
158 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
|
159 } |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
160 } where |
|
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 : 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
|
162 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
|
163 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
|
164 |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
165 -------- |
| 819 | 166 -- |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
167 -- Functor from Positive Logic to Sets |
| 819 | 168 -- |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
169 |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
170 -- 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
|
171 -- 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
|
172 |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
173 C = graphtocat.Chain G |
| 819 | 174 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
175 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
176 tr f x y = graphtocat.next 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
|
177 |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
178 fobj : ( a : Objs ) → Set (c₁ ⊔ c₂ ) |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
179 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
|
180 fobj ⊤ = One |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
181 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
|
182 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
|
183 |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
184 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
|
185 amap : { a b : Objs } → Arrow 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
|
186 amap (arrow x) = tr x |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
187 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
|
188 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
|
189 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
|
190 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
|
191 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
|
192 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
|
193 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
|
194 fmap (iv x f) a = amap x ( fmap f a ) |
| 819 | 195 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
196 -- 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
|
197 -- 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
|
198 -- 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
|
199 |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
200 CS : Functor PL (Sets {c₁ ⊔ c₂ }) |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
201 FObj CS a = fobj a |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
202 FMap CS {a} {b} f = fmap {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
|
203 isFunctor CS = isf where |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
204 _+_ = 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
|
205 ++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
|
206 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
|
207 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
|
208 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
|
209 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
|
210 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
|
211 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
|
212 ( 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
|
213 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
|
214 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
|
215 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
|
216 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
|
217 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) |
| 819 | 218 |
| 801 | 219 |
| 818 | 220 --- |
| 221 --- SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap | |
| 222 --- | |
| 223 --- CCC ( SC (CS G)) Sets have to be proved | |
| 224 --- SM can be eliminated if we have | |
| 225 --- sobj (a : vertex g ) → {a} a set have only a | |
| 226 --- smap (a b : vertex g ) → {a} → {b} | |
| 227 | |
| 228 | |
| 229 record CCCObj { c₁ c₂ ℓ : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where | |
| 230 field | |
| 231 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
|
232 ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g |
| 818 | 233 ccc : CCC cat |
| 234 | |
| 235 open CCCObj | |
| 236 | |
| 237 record CCCMap {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 238 field | |
| 239 cmap : Functor (cat A ) (cat B ) | |
| 820 | 240 ccf : CCC (cat A) → CCC (cat B) |
| 241 | |
| 242 open import Category.Cat | |
| 243 | |
| 244 open CCCMap | |
| 245 open import Relation.Binary.Core | |
| 818 | 246 |
| 820 | 247 Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ)) |
| 248 Cart {c₁} {c₂} {ℓ} = record { | |
| 249 Obj = CCCObj {c₁} {c₂} {ℓ} | |
| 250 ; Hom = CCCMap | |
| 824 | 251 ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) } |
| 820 | 252 ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g |
| 253 ; Id = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x } | |
| 254 ; isCategory = record { | |
| 255 isEquivalence = λ {A} {B} → record { | |
| 256 refl = λ {f} → let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f} | |
| 257 ; sym = λ {f} {g} → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g} | |
| 258 ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h} } | |
| 821 | 259 ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_} |
| 260 ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f} | |
| 261 ; 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} | |
| 262 ; 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 | 263 }} |
| 818 | 264 |
| 825 | 265 open import graph |
| 818 | 266 open Graph |
| 267 | |
| 927 | 268 record GMap {c₁ c₂ : Level} (x y : Graph {c₁} {c₂} ) : Set (c₁ ⊔ c₂ ) where |
| 820 | 269 field |
| 818 | 270 vmap : vertex x → vertex y |
| 271 emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b) | |
| 272 | |
| 820 | 273 open GMap |
| 274 | |
| 821 | 275 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) |
| 276 | |
| 824 | 277 data [_]_==_ {c₁ c₂ } (C : Graph {c₁} {c₂} ) {A B : vertex C} (f : edge C A B) |
| 278 : ∀{X Y : vertex C} → edge C X Y → Set (suc (c₁ ⊔ c₂ )) where | |
| 279 mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g | |
| 280 | |
| 281 _=m=_ : ∀ {c₁ c₂ } {C D : Graph {c₁} {c₂} } | |
| 282 → (F G : GMap C D) → Set (suc (c₂ ⊔ c₁)) | |
| 283 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f | |
| 821 | 284 |
| 927 | 285 _&_ : {c₁ c₂ : Level} {x y z : Graph {c₁} {c₂}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z |
| 821 | 286 f & g = record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) } |
| 287 | |
| 927 | 288 Grph : {c₁ c₂ : Level} → Category (suc (c₁ ⊔ c₂)) (c₁ ⊔ c₂) (suc ( c₁ ⊔ c₂)) |
| 289 Grph {c₁} {c₂} = record { | |
| 290 Obj = Graph {c₁} {c₂} | |
| 291 ; Hom = GMap {c₁} {c₂} | |
| 821 | 292 ; _o_ = _&_ |
| 293 ; _≈_ = _=m=_ | |
| 820 | 294 ; Id = record { vmap = λ y → y ; emap = λ f → f } |
| 295 ; isCategory = record { | |
| 824 | 296 isEquivalence = λ {A} {B} → ise |
| 297 ; identityL = λ e → mrefl refl | |
| 298 ; identityR = λ e → mrefl refl | |
| 821 | 299 ; o-resp-≈ = m--resp-≈ |
| 824 | 300 ; associative = λ e → mrefl refl |
| 821 | 301 }} where |
| 927 | 302 msym : {c₁ c₂ : Level} {x y : Graph {c₁} {c₂} } { f g : GMap x y } → f =m= g → g =m= f |
| 824 | 303 msym {_} {_} {x} {y} f=g f = lemma ( f=g f ) where |
| 304 lemma : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f | |
| 305 lemma (mrefl Ff≈Gf) = mrefl (sym Ff≈Gf) | |
| 927 | 306 mtrans : {c₁ c₂ : Level} {x y : Graph {c₁} {c₂} } { f g h : GMap x y } → f =m= g → g =m= h → f =m= h |
| 824 | 307 mtrans {_} {_} {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where |
| 308 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 | |
| 309 lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv eqv₁ ) | |
| 927 | 310 ise : {c₁ c₂ : Level} {x y : Graph {c₁} {c₂}} → IsEquivalence {_} {suc c₁ ⊔ suc c₂ } {_} ( _=m=_ {c₁} {c₂} {x} {y}) |
| 821 | 311 ise = record { |
| 824 | 312 refl = λ f → mrefl refl |
| 821 | 313 ; sym = msym |
| 314 ; trans = mtrans | |
| 315 } | |
| 927 | 316 m--resp-≈ : {c₁ c₂ : Level} {A B C : Graph {c₁} {c₂} } |
| 824 | 317 {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g ) |
| 318 m--resp-≈ {_} {_} {A} {B} {C} {f} {g} {h} {i} f=g h=i e = | |
| 319 lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where | |
| 320 lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) → | |
| 321 [ B ] ϕ == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π | |
| 322 lemma _ _ _ (mrefl refl) (mrefl refl) = mrefl refl | |
| 820 | 323 |
| 821 | 324 --- Forgetful functor |
| 325 | |
| 927 | 326 module forgetful {c₁ c₂ : Level} where |
| 327 | |
| 328 ≃-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
|
329 → { 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
|
330 → { 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
|
331 → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g' |
| 927 | 332 ≃-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
|
333 f' |
|
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' ⟩ |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
335 f |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
336 ≈⟨ eqv ⟩ |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
337 g |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
338 ≈⟨ g=g' ⟩ |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
339 g' |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
340 ∎ ) |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
821
diff
changeset
|
341 |
| 927 | 342 fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂} ) → Obj (Grph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}) |
| 343 fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) } | |
| 344 fmap : {a b : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) } → Hom (Cart ) a b → Hom (Grph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}) ( fobj a ) ( fobj b ) | |
| 345 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
|
346 |
| 927 | 347 UX : Functor (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) |
| 348 FObj UX a = fobj a | |
| 349 FMap UX f = fmap f | |
| 350 isFunctor UX = isf where | |
| 351 isf : IsFunctor Cart Grph fobj fmap | |
| 352 IsFunctor.identity isf {a} {b} {f} e = mrefl refl | |
| 353 IsFunctor.distr isf {a} {b} {c} f = mrefl refl | |
| 354 IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = lemma ( (extensionality Sets ( λ z → lemma4 ( | |
| 355 ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g))) | |
| 356 )))) (f=g e) where | |
| 357 lemma4 : {x y : vertex (fobj b)} → [_]_~_ (cat b) (id1 (cat b) x) (id1 (cat b) y) → x ≡ y | |
| 358 lemma4 (refl eqv) = refl | |
| 359 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 | |
| 360 lemma refl (refl eqv) = mrefl (≡←≈ b eqv) | |
| 824 | 361 |
| 821 | 362 |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
363 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
|
364 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
|
365 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
|
366 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
|
367 |
| 927 | 368 ccc-graph-univ : {c₁ c₂ : Level } → UniversalMapping (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}) (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (forgetful.UX {c₁} {c₂} ) |
| 369 ccc-graph-univ {c₁} {c₂} = record { | |
| 370 F = λ g → csc {!!} ; | |
| 371 η = λ a → record { vmap = λ y → cobj {!!} {!!}; emap = λ f x y → next f (x y) } ; | |
| 372 _* = solution ; | |
|
911
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
373 isUniversalMapping = record { |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
374 universalMapping = {!!} ; |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
375 uniquness = {!!} |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
376 } |
|
b8c5f15ee561
small graph and small category on CCC to graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
825
diff
changeset
|
377 } where |
| 927 | 378 open forgetful {c₁} {c₂} |
| 926 | 379 open ccc-from-graph |
| 927 | 380 csc : Graph {c₁} {c₂} → Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) |
| 381 csc g = record { cat = Sets {c₁ ⊔ c₂} ; ccc = sets {c₁ ⊔ c₂} ; ≡←≈ = λ eq → eq } | |
| 382 cs : (g : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}) → Functor (ccc-from-graph.PL g) (Sets {suc (c₁ ⊔ c₂)}) | |
| 926 | 383 cs g = CS g |
| 927 | 384 pl : (g : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)} ) → Category _ _ _ |
| 926 | 385 pl g = PL g |
| 927 | 386 cobj : {g : Obj (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)})} {c : Obj (Cart)} → Hom Grph g (FObj UX c) → Objs g → Obj (cat c) |
| 914 | 387 cobj {g} {c} f (atom x) = vmap f x |
| 912 | 388 cobj {g} {c} f ⊤ = CCC.１ (ccc c) |
| 914 | 389 cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y) |
| 390 cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) | |
| 927 | 391 c-map : {g : Obj (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)} )} {c : Obj Cart} {A B : Objs g} |
| 926 | 392 → (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) |
| 393 c-map {g} {c} {atom a} {atom x} f y = {!!} | |
| 927 | 394 c-map {g} {c} {⊤} {atom x} f (iv f1 y) = {!!} |
| 395 c-map {g} {c} {a ∧ b} {atom x} f (iv f1 y) = {!!} | |
| 926 | 396 c-map {g} {c} {b <= a} {atom x} f y = {!!} |
| 914 | 397 c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a) |
| 926 | 398 c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f {!!}) (c-map f {!!}) |
| 399 c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!}) | |
| 927 | 400 solution : {g : Obj (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)})} {c : Obj (Cart )} → Hom Grph g (FObj UX c) → Hom (Cart ) {!!} {!!} |
| 401 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
|
402 |
| 912 | 403 |