Mercurial > hg > Members > kono > Proof > category
annotate CCChom.agda @ 815:bb9fd483f560
simpler proof of CCC from graph
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 27 Apr 2019 12:17:49 +0900 |
parents | e4986625ddd7 |
children | 4e48b331020a |
rev | line source |
---|---|
779 | 1 open import Level |
2 open import Category | |
784 | 3 module CCChom 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 ( [_] ) |
779 | 10 |
11 open Functor | |
12 | |
13 -- ccc-1 : Hom A a 1 ≅ {*} | |
14 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) | |
15 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c | |
16 | |
785 | 17 data One : Set where |
779 | 18 OneObj : One -- () in Haskell ( or any one object set ) |
19 | |
780 | 20 OneCat : Category Level.zero Level.zero Level.zero |
21 OneCat = record { | |
22 Obj = One ; | |
23 Hom = λ a b → One ; | |
24 _o_ = λ{a} {b} {c} x y → OneObj ; | |
25 _≈_ = λ x y → x ≡ y ; | |
26 Id = λ{a} → OneObj ; | |
27 isCategory = record { | |
28 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; | |
29 identityL = λ{a b f} → lemma {a} {b} {f} ; | |
30 identityR = λ{a b f} → lemma {a} {b} {f} ; | |
31 o-resp-≈ = λ{a b c f g h i} _ _ → refl ; | |
32 associative = λ{a b c d f g h } → refl | |
33 } | |
34 } where | |
785 | 35 lemma : {a b : One } → { f : One } → OneObj ≡ f |
780 | 36 lemma {a} {b} {f} with f |
37 ... | OneObj = refl | |
38 | |
783 | 39 record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) |
40 : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where | |
41 field | |
42 ≅→ : Hom A a b → Hom B a' b' | |
43 ≅← : Hom B a' b' → Hom A a b | |
44 iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] | |
45 iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] | |
787 | 46 cong→ : {f g : Hom A a b } → A [ f ≈ g ] → B [ ≅→ f ≈ ≅→ g ] |
47 cong← : {f g : Hom B a' b'} → B [ f ≈ g ] → A [ ≅← f ≈ ≅← g ] | |
779 | 48 |
783 | 49 |
784 | 50 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (1 : Obj A) |
780 | 51 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where |
779 | 52 field |
785 | 53 ccc-1 : {a : Obj A} {b c : Obj OneCat} → -- Hom A a 1 ≅ {*} |
54 IsoS A OneCat a 1 b c | |
780 | 55 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b ) |
784 | 56 IsoS A (A × A) c (a * b) (c , c ) (a , b ) |
780 | 57 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c |
58 IsoS A A a (c ^ b) (a * b) c | |
788 | 59 nat-2 : {a b c : Obj A} → {f : Hom A (b * c) (b * c) } → {g : Hom A a (b * c) } |
60 → (A × A) [ (A × A) [ IsoS.≅→ ccc-2 f o (g , g) ] ≈ IsoS.≅→ ccc-2 ( A [ f o g ] ) ] | |
789 | 61 nat-3 : {a b c : Obj A} → { k : Hom A c (a ^ b ) } → A [ A [ IsoS.≅→ (ccc-3) (id1 A (a ^ b)) o |
62 (IsoS.≅← (ccc-2 ) (A [ k o (proj₁ ( IsoS.≅→ ccc-2 (id1 A (c * b)))) ] , | |
63 (proj₂ ( IsoS.≅→ ccc-2 (id1 A (c * b) ))))) ] ≈ IsoS.≅→ (ccc-3 ) k ] | |
788 | 64 |
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
65 -------- |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
66 -- CCC satisfies hom natural iso |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
67 -- |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
68 -- ccc-1 : Hom A a 1 ≅ {*} |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
69 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
70 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
71 -- |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
72 -------- |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
73 |
788 | 74 open import CCC |
75 | |
779 | 76 |
784 | 77 record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where |
781 | 78 field |
79 one : Obj A | |
80 _*_ : Obj A → Obj A → Obj A | |
81 _^_ : Obj A → Obj A → Obj A | |
784 | 82 isCCChom : IsCCChom A one _*_ _^_ |
783 | 83 |
84 open import HomReasoning | |
85 | |
784 | 86 CCC→hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) → CCChom A |
87 CCC→hom A c = record { | |
88 one = CCC.1 c | |
89 ; _*_ = CCC._∧_ c | |
90 ; _^_ = CCC._<=_ c | |
91 ; isCCChom = record { | |
787 | 92 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 ; cong← = c105 ; cong→ = c106 } |
93 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 ; cong← = c205; cong→ = c206 } | |
94 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 ; cong← = c305 ; cong→ = c306 } | |
789 | 95 ; nat-2 = nat-2 ; nat-3 = nat-3 |
784 | 96 } |
794 | 97 } module CCC→HOM where |
785 | 98 c101 : {a : Obj A} → Hom A a (CCC.1 c) → Hom OneCat OneObj OneObj |
99 c101 _ = OneObj | |
100 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.1 c) | |
101 c102 {a} OneObj = CCC.○ c a | |
102 c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f | |
103 c103 {a} {OneObj} {OneObj} {OneObj} = refl | |
104 c104 : {a : Obj A} → {f : Hom A a (CCC.1 c)} → A [ (c102 ( c101 f )) ≈ f ] | |
793 | 105 c104 {a} {f} = let open ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) ) |
785 | 106 c201 : { c₁ a b : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b) |
107 c201 f = ( A [ CCC.π c o f ] , A [ CCC.π' c o f ] ) | |
108 c202 : { c₁ a b : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b) | |
109 c202 (f , g ) = CCC.<_,_> c f g | |
110 c203 : { c₁ a b : Obj A} → {f : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ (c201 ( c202 f )) ≈ f ] | |
111 c203 = ( IsCCC.e3a (CCC.isCCC c) , IsCCC.e3b (CCC.isCCC c)) | |
112 c204 : { c₁ a b : Obj A} → {f : Hom A c₁ ((c CCC.∧ a) b)} → A [ (c202 ( c201 f )) ≈ f ] | |
113 c204 = IsCCC.e3c (CCC.isCCC c) | |
114 c301 : { d a b : Obj A} → Hom A a ((c CCC.<= d) b) → Hom A ((c CCC.∧ a) b) d -- a -> d <= b -> (a ∧ b ) -> d | |
115 c301 {d} {a} {b} f = A [ CCC.ε c o CCC.<_,_> c ( A [ f o CCC.π c ] ) ( CCC.π' c ) ] | |
116 c302 : { d a b : Obj A} → Hom A ((c CCC.∧ a) b) d → Hom A a ((c CCC.<= d) b) | |
117 c302 f = CCC._* c f | |
118 c303 : { c₁ a b : Obj A} → {f : Hom A ((c CCC.∧ a) b) c₁} → A [ (c301 ( c302 f )) ≈ f ] | |
119 c303 = IsCCC.e4a (CCC.isCCC c) | |
120 c304 : { c₁ a b : Obj A} → {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f )) ≈ f ] | |
121 c304 = IsCCC.e4b (CCC.isCCC c) | |
787 | 122 c105 : {a : Obj A } {f g : Hom OneCat OneObj OneObj} → _[_≈_] OneCat {OneObj} {OneObj} f g → A [ c102 {a} f ≈ c102 {a} g ] |
123 c105 refl = let open ≈-Reasoning A in refl-hom | |
124 c106 : { a : Obj A } {f g : Hom A a (CCC.1 c)} → A [ f ≈ g ] → _[_≈_] OneCat {OneObj} {OneObj} OneObj OneObj | |
125 c106 _ = refl | |
126 c205 : { a b c₁ : Obj A } {f g : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ f ≈ g ] → A [ c202 f ≈ c202 g ] | |
127 c205 f=g = IsCCC.π-cong (CCC.isCCC c ) (proj₁ f=g ) (proj₂ f=g ) | |
128 c206 : { a b c₁ : Obj A } {f g : Hom A c₁ ((c CCC.∧ a) b)} → A [ f ≈ g ] → (A × A) [ c201 f ≈ c201 g ] | |
129 c206 {a} {b} {c₁} {f} {g} f=g = ( begin | |
130 CCC.π c o f | |
131 ≈⟨ cdr f=g ⟩ | |
132 CCC.π c o g | |
133 ∎ ) , ( begin | |
134 CCC.π' c o f | |
135 ≈⟨ cdr f=g ⟩ | |
136 CCC.π' c o g | |
137 ∎ ) where open ≈-Reasoning A | |
138 c305 : { a b c₁ : Obj A } {f g : Hom A ((c CCC.∧ a) b) c₁} → A [ f ≈ g ] → A [ (c CCC.*) f ≈ (c CCC.*) g ] | |
139 c305 f=g = IsCCC.*-cong (CCC.isCCC c ) f=g | |
140 c306 : { a b c₁ : Obj A } {f g : Hom A a ((c CCC.<= c₁) b)} → A [ f ≈ g ] → A [ c301 f ≈ c301 g ] | |
141 c306 {a} {b} {c₁} {f} {g} f=g = begin | |
142 CCC.ε c o CCC.<_,_> c ( f o CCC.π c ) ( CCC.π' c ) | |
143 ≈⟨ cdr ( IsCCC.π-cong (CCC.isCCC c ) (car f=g ) refl-hom) ⟩ | |
144 CCC.ε c o CCC.<_,_> c ( g o CCC.π c ) ( CCC.π' c ) | |
145 ∎ where open ≈-Reasoning A | |
788 | 146 nat-2 : {a b : Obj A} {c = c₁ : Obj A} {f : Hom A ((c CCC.∧ b) c₁) ((c CCC.∧ b) c₁)} |
147 {g : Hom A a ((c CCC.∧ b) c₁)} → (A × A) [ (A × A) [ c201 f o g , g ] ≈ c201 (A [ f o g ]) ] | |
148 nat-2 {a} {b} {c₁} {f} {g} = ( begin | |
149 ( CCC.π c o f) o g | |
150 ≈↑⟨ assoc ⟩ | |
151 ( CCC.π c ) o (f o g) | |
152 ∎ ) , (sym-hom assoc) where open ≈-Reasoning A | |
789 | 153 nat-3 : {a b : Obj A} {c = c₁ : Obj A} {k : Hom A c₁ ((c CCC.<= a) b)} → |
154 A [ A [ c301 (id1 A ((c CCC.<= a) b)) o c202 (A [ k o proj₁ (c201 (id1 A ((c CCC.∧ c₁) b))) ] , proj₂ (c201 (id1 A ((c CCC.∧ c₁) b)))) ] | |
155 ≈ c301 k ] | |
156 nat-3 {a} {b} { c₁} {k} = begin | |
157 c301 (id1 A ((c CCC.<= a) b)) o c202 ( k o proj₁ (c201 (id1 A ((c CCC.∧ c₁) b))) , proj₂ (c201 (id1 A ((c CCC.∧ c₁) b)))) | |
158 ≈⟨⟩ | |
159 ( CCC.ε c o CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c)) | |
160 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))) | |
161 ≈↑⟨ assoc ⟩ | |
162 (CCC.ε c) o (( CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c)) | |
163 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b))))) | |
164 ≈⟨ cdr (car (IsCCC.π-cong (CCC.isCCC c ) idL refl-hom ) ) ⟩ | |
165 (CCC.ε c) o ( CCC.<_,_> c (CCC.π c) (CCC.π' c) | |
166 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b))))) | |
167 ≈⟨ cdr (car (IsCCC.π-id (CCC.isCCC c))) ⟩ | |
168 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b ) | |
169 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b))))) | |
170 ≈⟨ cdr ( cdr ( IsCCC.π-cong (CCC.isCCC c) (cdr idR) idR )) ⟩ | |
171 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b ) o (CCC.<_,_> c (k o ( CCC.π c )) ( CCC.π' c ))) | |
172 ≈⟨ cdr idL ⟩ | |
173 (CCC.ε c) o (CCC.<_,_> c ( k o (CCC.π c) ) (CCC.π' c)) | |
174 ≈⟨⟩ | |
175 c301 k | |
176 ∎ where open ≈-Reasoning A | |
788 | 177 |
794 | 178 U_b : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( ccc : CCC A ) → (b : Obj A) → Functor A A |
179 FObj (U_b A ccc b) = λ a → (CCC._<=_ ccc a b ) | |
180 FMap (U_b A ccc b) = λ f → CCC._* ccc ( A [ f o CCC.ε ccc ] ) | |
181 isFunctor (U_b A ccc b) = isF where | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
182 _<=_ = CCC._<=_ ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
183 _∧_ = CCC._∧_ ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
184 <_,_> = CCC.<_,_> ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
185 _* = CCC._* ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
186 ε = CCC.ε ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
187 π = CCC.π ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
188 π' = CCC.π' ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
189 isc = CCC.isCCC ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
190 *-cong = IsCCC.*-cong (CCC.isCCC ccc) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
191 π-cong = IsCCC.π-cong (CCC.isCCC ccc) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
192 |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
193 isF : IsFunctor A A ( λ a → (a <= b)) ( λ f → CCC._* ccc ( A [ f o ε ] ) ) |
794 | 194 IsFunctor.≈-cong isF f≈g = IsCCC.*-cong (CCC.isCCC ccc) ( car f≈g ) where open ≈-Reasoning A |
195 -- e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ] | |
196 IsFunctor.identity isF {a} = begin | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
197 (id1 A a o ε ) * |
794 | 198 ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) ( begin |
199 id1 A a o CCC.ε ccc | |
200 ≈⟨ idL ⟩ | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
201 ε |
794 | 202 ≈↑⟨ idR ⟩ |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
203 ε o id1 A ( ( a <= b ) ∧ b ) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
204 ≈↑⟨ cdr ( IsCCC.π-id isc) ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
205 ε o ( < π , π' > ) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
206 ≈↑⟨ cdr ( π-cong idL refl-hom) ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
207 ε o ( < id1 A (a <= b) o π , π' > ) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
208 ∎ ) ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
209 ( ε o ( < id1 A ( a <= b) o π , π' > ) ) * |
794 | 210 ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩ |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
211 id1 A (a <= b) |
794 | 212 ∎ where open ≈-Reasoning A |
213 IsFunctor.distr isF {x} {y} {z} {f} {g} = begin | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
214 ( ( g o f ) o ε ) * |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
215 ≈↑⟨ *-cong assoc ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
216 ( g o (f o ε ) ) * |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
217 ≈↑⟨ *-cong ( cdr (IsCCC.e4a isc) ) ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
218 ( g o ( ε o ( < ( ( f o ε ) * ) o π , π' > ) )) * |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
219 ≈⟨ *-cong assoc ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
220 ( ( g o ε ) o ( < ( ( f o ε ) * ) o π , π' > ) ) * |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
221 ≈↑⟨ IsCCC.distr-* isc ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
222 ( g o ε ) * o ( f o ε ) * |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
223 ∎ where open ≈-Reasoning A |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
224 |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
225 F_b : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( ccc : CCC A ) → (b : Obj A) → Functor A A |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
226 FObj (F_b A ccc b) = λ a → ( CCC._∧_ ccc a b ) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
227 FMap (F_b A ccc b) = λ f → ( CCC.<_,_> ccc (A [ f o CCC.π ccc ] ) ( CCC.π' ccc) ) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
228 isFunctor (F_b A ccc b) = isF where |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
229 _∧_ = CCC._∧_ ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
230 <_,_> = CCC.<_,_> ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
231 π = CCC.π ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
232 π' = CCC.π' ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
233 isc = CCC.isCCC ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
234 π-cong = IsCCC.π-cong (CCC.isCCC ccc) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
235 |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
236 isF : IsFunctor A A ( λ a → (a ∧ b)) ( λ f → < ( A [ f o π ] ) , π' > ) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
237 IsFunctor.≈-cong isF f≈g = π-cong ( car f≈g ) refl-hom where open ≈-Reasoning A |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
238 IsFunctor.identity isF {a} = trans-hom (π-cong idL refl-hom ) (IsCCC.π-id isc) where open ≈-Reasoning A |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
239 IsFunctor.distr isF {x} {y} {z} {f} {g} = begin |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
240 < ( g o f ) o π , π' > |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
241 ≈↑⟨ π-cong assoc refl-hom ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
242 < g o ( f o π ) , π' > |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
243 ≈↑⟨ π-cong (cdr (IsCCC.e3a isc )) refl-hom ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
244 < g o ( π o < ( f o π ) , π' > ) , π' > |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
245 ≈⟨ π-cong assoc ( sym-hom (IsCCC.e3b isc )) ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
246 < ( g o π ) o < ( f o π ) , π' > , π' o < ( f o π ) , π' > > |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
247 ≈↑⟨ IsCCC.distr-π isc ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
248 < ( g o π ) , π' > o < ( f o π ) , π' > |
794 | 249 ∎ where open ≈-Reasoning A |
250 | |
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
251 ------- |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
252 --- U_b and F_b is an adjunction Functor |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
253 ------- |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
254 |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
255 CCCtoAdj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → (b : Obj A ) → coUniversalMapping A A (F_b A ccc b) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
256 CCCtoAdj A ccc b = record { |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
257 U = λ a → a <= b |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
258 ; ε = ε' |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
259 ; _*' = solution |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
260 ; iscoUniversalMapping = record { |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
261 couniversalMapping = couniversalMapping |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
262 ; couniquness = couniquness |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
263 } |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
264 } where |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
265 _<=_ = CCC._<=_ ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
266 <_,_> = CCC.<_,_> ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
267 _* = CCC._* ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
268 ε = CCC.ε ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
269 π = CCC.π ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
270 π' = CCC.π' ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
271 isc = CCC.isCCC ccc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
272 *-cong = IsCCC.*-cong (CCC.isCCC ccc) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
273 ε' : (a : Obj A) → Hom A (FObj (F_b A ccc b) (a <= b)) a |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
274 ε' a = ε |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
275 solution : { b' : Obj A} {a : Obj A} → Hom A (FObj (F_b A ccc b) a) b' → Hom A a (b' <= b) |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
276 solution f = f * |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
277 couniversalMapping : {b = b₁ : Obj A} {a : Obj A} |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
278 {f : Hom A (FObj (F_b A ccc b) a) b₁} → |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
279 A [ A [ ε' b₁ o FMap (F_b A ccc b) (solution f) ] ≈ f ] |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
280 couniversalMapping {c} {a} {f} = IsCCC.e4a isc |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
281 couniquness : {b = b₁ : Obj A} {a : Obj A} |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
282 {f : Hom A (FObj (F_b A ccc b) a) b₁} {g : Hom A a (b₁ <= b)} → |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
283 A [ A [ ε' b₁ o FMap (F_b A ccc b) g ] ≈ f ] → A [ solution f ≈ g ] |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
284 couniquness {c} {a} {f} {g} eq = begin |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
285 f * |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
286 ≈↑⟨ *-cong eq ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
287 ( ε o FMap (F_b A ccc b) g ) * |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
288 ≈⟨⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
289 ( ε o < ( g o π ) , π' > ) * |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
290 ≈⟨ IsCCC.e4b isc ⟩ |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
291 g |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
292 ∎ where open ≈-Reasoning A |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
293 |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
294 |
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
295 ---------- |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
296 --- Hom A 1 ( c ^ b ) ≅ Hom A b c |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
297 ---------- |
794 | 298 |
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
299 c^b=b<=c : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} → |
793 | 300 IsoS A A (CCC.1 ccc ) (CCC._<=_ ccc c b) b c |
794 | 301 c^b=b<=c A ccc {a} {b} {c} = record { |
302 ≅→ = λ f → A [ CCC.ε ccc o CCC.<_,_> ccc ( A [ f o CCC.○ ccc b ] ) ( id1 A b ) ] --- g ’ (g : 1 → b ^ a) of | |
303 ; ≅← = λ f → CCC._* ccc ( A [ f o CCC.π' ccc ] ) --- ┌ f ┐ name of (f : b ^a → 1 ) | |
793 | 304 ; iso→ = iso→ |
305 ; iso← = iso← | |
306 ; cong→ = cong* | |
307 ; cong← = cong2 | |
308 } where | |
309 cc = IsCCChom.ccc-3 ( CCChom.isCCChom (CCC→hom A ccc ) ) | |
310 -- e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] | |
311 iso→ : {f : Hom A b c} → A [ | |
312 (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o (ccc CCC.*) ((A Category.o f) (CCC.π' ccc))) (CCC.○ ccc b) > (Category.Category.Id A)) ≈ f ] | |
313 iso→ {f} = begin | |
314 CCC.ε ccc o (CCC.<_,_> ccc (CCC._* ccc ( f o (CCC.π' ccc)) o (CCC.○ ccc b)) (id1 A b ) ) | |
315 ≈↑⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) refl-hom (IsCCC.e3b (CCC.isCCC ccc) ) ) ⟩ | |
316 CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.○ ccc b) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) | |
317 ≈↑⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) (cdr (IsCCC.e3a (CCC.isCCC ccc))) refl-hom ) ⟩ | |
318 CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o ( CCC.π ccc o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) | |
319 ≈⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) assoc refl-hom ) ⟩ | |
320 CCC.ε ccc o ( CCC.<_,_> ccc ((CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) | |
794 | 321 ≈↑⟨ cdr ( IsCCC.distr-π ( CCC.isCCC ccc ) ) ⟩ |
793 | 322 CCC.ε ccc o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) |
323 ≈⟨ assoc ⟩ | |
324 ( CCC.ε ccc o CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc) ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) | |
325 ≈⟨ car ( IsCCC.e4a (CCC.isCCC ccc) ) ⟩ | |
326 ( f o CCC.π' ccc ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) | |
327 ≈↑⟨ assoc ⟩ | |
328 f o ( CCC.π' ccc o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) | |
329 ≈⟨ cdr (IsCCC.e3b (CCC.isCCC ccc)) ⟩ | |
330 f o id1 A b | |
331 ≈⟨ idR ⟩ | |
332 f | |
333 ∎ where open ≈-Reasoning A | |
334 lemma : {f : Hom A (CCC.1 ccc) ((ccc CCC.<= c) b)} → A [ A [ A [ f o (CCC.○ ccc b) ] o (CCC.π' ccc) ] ≈ A [ f o (CCC.π ccc) ] ] | |
335 lemma {f} = begin | |
336 ( f o (CCC.○ ccc b) ) o (CCC.π' ccc) | |
337 ≈↑⟨ assoc ⟩ | |
338 f o ( (CCC.○ ccc b) o (CCC.π' ccc) ) | |
339 ≈⟨ cdr ( IsCCC.e2 (CCC.isCCC ccc) ) ⟩ | |
340 f o (CCC.○ ccc ( CCC._∧_ ccc (CCC.1 ccc) b ) ) | |
341 ≈↑⟨ cdr ( IsCCC.e2 (CCC.isCCC ccc) ) ⟩ | |
342 f o ( (CCC.○ ccc) (CCC.1 ccc) o (CCC.π ccc) ) | |
343 ≈↑⟨ cdr ( car ( IsCCC.e2 (CCC.isCCC ccc) )) ⟩ | |
344 f o ( id1 A (CCC.1 ccc) o (CCC.π ccc) ) | |
345 ≈⟨ cdr (idL) ⟩ | |
346 f o (CCC.π ccc) | |
347 ∎ where open ≈-Reasoning A | |
348 -- e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ] | |
349 iso← : {f : Hom A (CCC.1 ccc) ((ccc CCC.<= c) b)} → A [ (ccc CCC.*) ((A Category.o (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o f) (CCC.○ ccc b) > | |
350 (Category.Category.Id A))) (CCC.π' ccc)) ≈ f ] | |
351 iso← {f} = begin | |
352 CCC._* ccc (( CCC.ε ccc o ( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b ))) o (CCC.π' ccc)) | |
353 ≈↑⟨ IsCCC.*-cong ( CCC.isCCC ccc ) assoc ⟩ | |
354 CCC._* ccc ( CCC.ε ccc o (( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b )) o (CCC.π' ccc))) | |
794 | 355 ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.distr-π ( CCC.isCCC ccc ) ) ) ⟩ |
793 | 356 CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( (f o (CCC.○ ccc b)) o CCC.π' ccc ) (id1 A b o CCC.π' ccc) ) |
357 ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) lemma idL )) ⟩ | |
358 CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( f o CCC.π ccc ) (CCC.π' ccc) ) | |
359 ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩ | |
360 f | |
361 ∎ where open ≈-Reasoning A | |
362 cong* : {f g : Hom A (CCC.1 ccc) ((ccc CCC.<= c) b)} → | |
363 A [ f ≈ g ] → A [ (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o f) (CCC.○ ccc b) > (Category.Category.Id A)) | |
364 ≈ (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o g) (CCC.○ ccc b) > (Category.Category.Id A)) ] | |
365 cong* {f} {g} f≈g = begin | |
366 CCC.ε ccc o ( CCC.<_,_> ccc ( f o ( CCC.○ ccc b )) (id1 A b )) | |
367 ≈⟨ cdr (IsCCC.π-cong ( CCC.isCCC ccc ) (car f≈g) refl-hom ) ⟩ | |
368 CCC.ε ccc o ( CCC.<_,_> ccc ( g o ( CCC.○ ccc b )) (id1 A b )) | |
369 ∎ where open ≈-Reasoning A | |
370 cong2 : {f g : Hom A b c} → A [ f ≈ g ] → | |
371 A [ (ccc CCC.*) ((A Category.o f) (CCC.π' ccc)) ≈ (ccc CCC.*) ((A Category.o g) (CCC.π' ccc)) ] | |
372 cong2 {f} {g} f≈g = begin | |
373 CCC._* ccc ( f o (CCC.π' ccc) ) | |
374 ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (car f≈g ) ⟩ | |
375 CCC._* ccc ( g o (CCC.π' ccc) ) | |
376 ∎ where open ≈-Reasoning A | |
377 | |
378 | |
787 | 379 |
785 | 380 |
381 open CCChom | |
382 open IsCCChom | |
383 open IsoS | |
384 | |
385 hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A | |
386 hom→CCC A h = record { | |
387 1 = 1 | |
388 ; ○ = ○ | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
389 ; _∧_ = _∧_ |
785 | 390 ; <_,_> = <,> |
391 ; π = π | |
392 ; π' = π' | |
393 ; _<=_ = _<=_ | |
394 ; _* = _* | |
395 ; ε = ε | |
396 ; isCCC = isCCC | |
397 } where | |
398 1 : Obj A | |
399 1 = one h | |
400 ○ : (a : Obj A ) → Hom A a 1 | |
401 ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
402 _∧_ : Obj A → Obj A → Obj A |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
403 _∧_ a b = _*_ h a b |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
404 <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a ∧ b) |
785 | 405 <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g ) |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
406 π : {a b : Obj A } → Hom A (a ∧ b) a |
785 | 407 π {a} {b} = proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) )) |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
408 π' : {a b : Obj A } → Hom A (a ∧ b) b |
785 | 409 π' {a} {b} = proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) )) |
410 _<=_ : (a b : Obj A ) → Obj A | |
411 _<=_ = _^_ h | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
412 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) |
785 | 413 _* = ≅← ( ccc-3 (isCCChom h ) ) |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
414 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a |
785 | 415 ε {a} {b} = ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
416 isCCC : CCC.IsCCC A 1 ○ _∧_ <,> π π' _<=_ _* ε |
785 | 417 isCCC = record { |
418 e2 = e2 | |
419 ; e3a = e3a | |
420 ; e3b = e3b | |
421 ; e3c = e3c | |
422 ; π-cong = π-cong | |
423 ; e4a = e4a | |
424 ; e4b = e4b | |
787 | 425 ; *-cong = *-cong |
785 | 426 } where |
786 | 427 e20 : ∀ ( f : Hom OneCat OneObj OneObj ) → _[_≈_] OneCat {OneObj} {OneObj} f OneObj |
428 e20 OneObj = refl | |
793 | 429 e2 : {a : Obj A} → ∀ { f : Hom A a 1 } → A [ f ≈ ○ a ] |
430 e2 {a} {f} = begin | |
786 | 431 f |
432 ≈↑⟨ iso← ( ccc-1 (isCCChom h )) ⟩ | |
433 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj}) ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f ) | |
434 ≈⟨ ≡-cong {Level.zero} {Level.zero} {Level.zero} {OneCat} {OneObj} {OneObj} ( | |
435 λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) ) ⟩ | |
436 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) OneObj | |
437 ≈⟨⟩ | |
438 ○ a | |
439 ∎ where open ≈-Reasoning A | |
787 | 440 -- |
441 -- g id | |
442 -- a -------------> b * c ------> b * c | |
443 -- | |
444 -- a -------------> b * c ------> b | |
445 -- a -------------> b * c ------> c | |
446 -- | |
447 cong-proj₁ : {a b c d : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₁ f ≈ proj₁ g ] | |
448 cong-proj₁ eq = proj₁ eq | |
788 | 449 cong-proj₂ : {a b c d : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₂ f ≈ proj₂ g ] |
450 cong-proj₂ eq = proj₂ eq | |
785 | 451 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o <,> f g ] ≈ f ] |
786 | 452 e3a {a} {b} {c} {f} {g} = begin |
453 π o <,> f g | |
454 ≈⟨⟩ | |
455 proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o (≅← (ccc-2 (isCCChom h)) (f , g)) | |
788 | 456 ≈⟨ cong-proj₁ (nat-2 (isCCChom h)) ⟩ |
787 | 457 proj₁ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) )) |
458 ≈⟨ cong-proj₁ ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩ | |
459 proj₁ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) )) | |
460 ≈⟨ cong-proj₁ ( iso→ (ccc-2 (isCCChom h))) ⟩ | |
786 | 461 proj₁ ( f , g ) |
462 ≈⟨⟩ | |
463 f | |
464 ∎ where open ≈-Reasoning A | |
785 | 465 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o <,> f g ] ≈ g ] |
788 | 466 e3b {a} {b} {c} {f} {g} = begin |
467 π' o <,> f g | |
468 ≈⟨⟩ | |
469 proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o (≅← (ccc-2 (isCCChom h)) (f , g)) | |
470 ≈⟨ cong-proj₂ (nat-2 (isCCChom h)) ⟩ | |
471 proj₂ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) )) | |
472 ≈⟨ cong-proj₂ ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩ | |
473 proj₂ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) )) | |
474 ≈⟨ cong-proj₂ ( iso→ (ccc-2 (isCCChom h))) ⟩ | |
475 proj₂ ( f , g ) | |
476 ≈⟨⟩ | |
477 g | |
478 ∎ where open ≈-Reasoning A | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
479 e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ] |
788 | 480 e3c {a} {b} {c} {f} = begin |
481 <,> ( π o f ) ( π' o f ) | |
482 ≈⟨⟩ | |
483 ≅← (ccc-2 (isCCChom h)) ( ( proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) ))) o f | |
484 , ( proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b)))) o f ) | |
485 ≈⟨⟩ | |
486 ≅← (ccc-2 (isCCChom h)) (_[_o_] (A × A) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) (f , f ) ) | |
487 ≈⟨ cong← (ccc-2 (isCCChom h)) (nat-2 (isCCChom h)) ⟩ | |
488 ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) o f )) | |
489 ≈⟨ cong← (ccc-2 (isCCChom h)) (cong→ (ccc-2 (isCCChom h)) idL ) ⟩ | |
490 ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) f ) | |
491 ≈⟨ iso← (ccc-2 (isCCChom h)) ⟩ | |
492 f | |
493 ∎ where open ≈-Reasoning A | |
785 | 494 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ <,> f g ≈ <,> f' g' ] |
786 | 495 π-cong {a} {b} {c} {f} {f'} {g} {g'} eq1 eq2 = begin |
496 <,> f g | |
497 ≈⟨⟩ | |
498 ≅← (ccc-2 (isCCChom h)) (f , g) | |
787 | 499 ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 ) ⟩ |
786 | 500 ≅← (ccc-2 (isCCChom h)) (f' , g') |
501 ≈⟨⟩ | |
502 <,> f' g' | |
503 ∎ where open ≈-Reasoning A | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
504 e4a : {a b c : Obj A} → { k : Hom A (c ∧ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] |
786 | 505 e4a {a} {b} {c} {k} = begin |
506 ε o ( <,> ((k *) o π ) π' ) | |
507 ≈⟨⟩ | |
787 | 508 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π')) |
789 | 509 ≈⟨ nat-3 (isCCChom h) ⟩ |
787 | 510 ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k) |
511 ≈⟨ iso→ (ccc-3 (isCCChom h)) ⟩ | |
786 | 512 k |
513 ∎ where open ≈-Reasoning A | |
785 | 514 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ] |
787 | 515 e4b {a} {b} {c} {k} = begin |
516 ( ε o ( <,> ( k o π ) π' ) ) * | |
517 ≈⟨⟩ | |
518 ≅← (ccc-3 (isCCChom h)) ( ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) o (≅← (ccc-2 (isCCChom h)) ( k o π , π'))) | |
789 | 519 ≈⟨ cong← (ccc-3 (isCCChom h)) (nat-3 (isCCChom h)) ⟩ |
787 | 520 ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k) |
521 ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩ | |
522 k | |
523 ∎ where open ≈-Reasoning A | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
524 *-cong : {a b c : Obj A} {f f' : Hom A (a ∧ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ] |
787 | 525 *-cong eq = cong← ( ccc-3 (isCCChom h )) eq |
785 | 526 |
790 | 527 open import Category.Sets |
528 | |
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
529 -- Sets is a CCC |
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
530 |
790 | 531 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
532 | |
533 data One' {l : Level} : Set l where | |
534 OneObj' : One' -- () in Haskell ( or any one object set ) | |
535 | |
536 sets : {l : Level } → CCC (Sets {l}) | |
537 sets {l} = record { | |
538 1 = One' | |
539 ; ○ = λ _ → λ _ → OneObj' | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
540 ; _∧_ = _∧_ |
790 | 541 ; <_,_> = <,> |
542 ; π = π | |
543 ; π' = π' | |
544 ; _<=_ = _<=_ | |
545 ; _* = _* | |
546 ; ε = ε | |
547 ; isCCC = isCCC | |
548 } where | |
549 1 : Obj Sets | |
550 1 = One' | |
551 ○ : (a : Obj Sets ) → Hom Sets a 1 | |
552 ○ a = λ _ → OneObj' | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
553 _∧_ : Obj Sets → Obj Sets → Obj Sets |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
554 _∧_ a b = a /\ b |
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
555 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b) |
790 | 556 <,> 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
|
557 π : {a b : Obj Sets } → Hom Sets (a ∧ b) a |
790 | 558 π {a} {b} = proj₁ |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
559 π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b |
790 | 560 π' {a} {b} = proj₂ |
561 _<=_ : (a b : Obj Sets ) → Obj Sets | |
562 a <= b = b → a | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
563 _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b) |
790 | 564 f * = λ x → λ y → f ( x , y ) |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
565 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a |
790 | 566 ε {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
|
567 isCCC : CCC.IsCCC Sets 1 ○ _∧_ <,> π π' _<=_ _* ε |
790 | 568 isCCC = record { |
569 e2 = e2 | |
570 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} | |
571 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} | |
572 ; e3c = e3c | |
573 ; π-cong = π-cong | |
574 ; e4a = e4a | |
575 ; e4b = e4b | |
576 ; *-cong = *-cong | |
577 } where | |
793 | 578 e2 : {a : Obj Sets} {f : Hom Sets a 1} → Sets [ f ≈ ○ a ] |
579 e2 {a} {f} = extensionality Sets ( λ x → e20 x ) | |
790 | 580 where |
581 e20 : (x : a ) → f x ≡ ○ a x | |
582 e20 x with f x | |
583 e20 x | OneObj' = refl | |
584 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → | |
585 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] | |
586 e3a = refl | |
587 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → | |
588 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] | |
589 e3b = refl | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
590 e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → |
790 | 591 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] |
592 e3c = refl | |
593 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → | |
594 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] | |
595 π-cong refl refl = refl | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
596 e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → |
790 | 597 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] |
598 e4a = refl | |
599 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → | |
600 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] | |
601 e4b = refl | |
795
030c5b87ed78
ccc to adjunction done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
794
diff
changeset
|
602 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → |
790 | 603 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] |
604 *-cong refl = refl | |
787 | 605 |
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
606 module ccc-from-graph where |
787 | 607 |
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
608 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) |
801 | 609 open import discrete |
809
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
610 open graphtocat |
799 | 611 |
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
612 open Graph |
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
613 |
812 | 614 data Objs (G : Graph ) : Set where |
615 atom : (vertex G) → Objs G | |
616 ⊤ : Objs G | |
617 _∧_ : Objs G → Objs G → Objs G | |
618 _<=_ : Objs G → Objs G → Objs G | |
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
619 |
812 | 620 data Arrow (G : Graph ) : Objs G → Objs G → Set where |
621 arrow : {a b : vertex G} → (edge G) a b → Arrow G (atom a) (atom b) | |
622 ○ : (a : Objs G ) → Arrow G a ⊤ | |
623 π : {a b : Objs G } → Arrow G ( a ∧ b ) a | |
624 π' : {a b : Objs G } → Arrow G ( a ∧ b ) b | |
625 ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a | |
814 | 626 <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b) |
627 _* : {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
|
628 |
806 | 629 record SM : Set (suc Level.zero) where |
630 field | |
631 graph : Graph | |
632 sobj : vertex graph → Set | |
633 smap : { a b : vertex graph } → edge graph a b → sobj a → sobj b | |
634 | |
635 open SM | |
803
984d20c10c87
simpler graph to category
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
802
diff
changeset
|
636 |
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
637 -- positive intutionistic calculus |
811 | 638 PL : (G : SM) → Graph |
812 | 639 PL G = record { vertex = Objs (graph G) ; edge = Arrow (graph G) } |
806 | 640 DX : (G : SM) → Category Level.zero Level.zero Level.zero |
811 | 641 DX G = GraphtoCat (PL G) |
801 | 642 |
802
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
643 -- open import Category.Sets |
7bc41fc7b563
graph with positive logic to Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
801
diff
changeset
|
644 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
801 | 645 |
812 | 646 fobj : {G : SM} ( a : Objs (graph G) ) → Set |
806 | 647 fobj {G} (atom x) = sobj G x |
648 fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b ) | |
649 fobj {G} (a <= b) = fobj {G} b → fobj {G} a | |
805 | 650 fobj ⊤ = One' |
812 | 651 amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b |
652 amap {G} {.(atom _)} {.(atom _)} (arrow x) = smap G x | |
653 amap {G} {a} {.⊤} (○ a) _ = OneObj' | |
654 amap {G} {.(b ∧ _)} {b} π ( x , _) = x | |
655 amap {G} {.(_ ∧ b)} {b} π'( _ , x) = x | |
656 amap {G} {.((b <= _) ∧ _)} {b} ε ( f , x ) = f x | |
814 | 657 amap {G} {a} {.(_ ∧ _)} < f , g > x = (amap f x , amap g x) |
658 amap {G} {a} {.(_ <= _)} (f *) x = λ y → amap f ( x , y ) | |
812 | 659 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b |
806 | 660 fmap {G} {a} {a} (id a) = λ z → z |
812 | 661 fmap {G} {a} {b} (next x f ) = Sets [ amap {G} x o fmap f ] |
805 | 662 |
815
bb9fd483f560
simpler proof of CCC from graph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
814
diff
changeset
|
663 -- 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
|
664 -- 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
|
665 -- 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
|
666 |
809
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
667 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
|
668 FObj (CS G) a = fobj a |
0976d576f5f6
<_,_> as function on Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
808
diff
changeset
|
669 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
|
670 isFunctor (CS G) = isf where |
805 | 671 _++_ = Category._o_ (DX G) |
811 | 672 ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) ) |
673 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
|
674 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
|
675 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
|
676 ( 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
|
677 adistr eq x = cong ( λ k → amap x k ) eq |
811 | 678 distr {a} {b} {b} {f} {id b} z = refl |
805 | 679 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
|
680 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
|
681 IsFunctor.≈-cong isf refl = refl |
811 | 682 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) |
801 | 683 |