Mercurial > hg > Members > kono > Proof > category
annotate src/CCCSets.agda @ 1028:28569574e3cf
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 30 Mar 2021 15:20:08 +0900 |
| parents | 5ae0290c34b4 |
| children | 348b5c6d5670 |
| rev | line source |
|---|---|
| 999 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 2 module CCCSets where | |
| 3 | |
| 4 open import Level | |
| 5 open import Category | |
| 6 open import HomReasoning | |
| 7 open import cat-utility | |
| 8 open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) | |
| 9 open import Category.Constructions.Product | |
| 10 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 11 open import CCC | |
| 12 | |
| 13 open Functor | |
| 14 | |
| 15 -- ccc-1 : Hom A a 1 ≅ {*} | |
| 16 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) | |
| 17 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c | |
| 18 | |
| 19 open import Category.Sets | |
| 20 | |
| 21 -- Sets is a CCC | |
| 22 | |
| 1018 | 23 open import SetsCompleteness hiding (ki1) |
| 24 | |
| 25 -- import Axiom.Extensionality.Propositional | |
| 26 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ | |
| 999 | 27 |
| 28 data One {c : Level } : Set c where | |
| 1020 | 29 ! : One -- () in Haskell ( or any one object set ) |
| 999 | 30 |
| 31 sets : {c : Level } → CCC (Sets {c}) | |
| 32 sets = record { | |
| 33 １ = One | |
| 1020 | 34 ; ○ = λ _ → λ _ → ! |
| 999 | 35 ; _∧_ = _∧_ |
| 36 ; <_,_> = <,> | |
| 37 ; π = π | |
| 38 ; π' = π' | |
| 39 ; _<=_ = _<=_ | |
| 40 ; _* = _* | |
| 41 ; ε = ε | |
| 42 ; isCCC = isCCC | |
| 43 } where | |
| 44 １ : Obj Sets | |
| 45 １ = One | |
| 46 ○ : (a : Obj Sets ) → Hom Sets a １ | |
| 1020 | 47 ○ a = λ _ → ! |
| 999 | 48 _∧_ : Obj Sets → Obj Sets → Obj Sets |
| 49 _∧_ a b = a /\ b | |
| 50 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b) | |
| 51 <,> f g = λ x → ( f x , g x ) | |
| 52 π : {a b : Obj Sets } → Hom Sets (a ∧ b) a | |
| 53 π {a} {b} = proj₁ | |
| 54 π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b | |
| 55 π' {a} {b} = proj₂ | |
| 56 _<=_ : (a b : Obj Sets ) → Obj Sets | |
| 57 a <= b = b → a | |
| 58 _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b) | |
| 59 f * = λ x → λ y → f ( x , y ) | |
| 60 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a | |
| 61 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x ) | |
| 62 isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε | |
| 63 isCCC = record { | |
| 64 e2 = e2 | |
| 65 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} | |
| 66 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} | |
| 67 ; e3c = e3c | |
| 68 ; π-cong = π-cong | |
| 69 ; e4a = e4a | |
| 70 ; e4b = e4b | |
| 71 ; *-cong = *-cong | |
| 72 } where | |
| 73 e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ] | |
| 74 e2 {a} {f} = extensionality Sets ( λ x → e20 x ) | |
| 75 where | |
| 76 e20 : (x : a ) → f x ≡ ○ a x | |
| 77 e20 x with f x | |
| 1020 | 78 e20 x | ! = refl |
| 999 | 79 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → |
| 80 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] | |
| 81 e3a = refl | |
| 82 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → | |
| 83 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] | |
| 84 e3b = refl | |
| 85 e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → | |
| 86 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] | |
| 87 e3c = refl | |
| 88 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → | |
| 89 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] | |
| 90 π-cong refl refl = refl | |
| 91 e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → | |
| 92 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] | |
| 93 e4a = refl | |
| 94 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → | |
| 95 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] | |
| 96 e4b = refl | |
| 97 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → | |
| 98 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] | |
| 99 *-cong refl = refl | |
| 100 | |
| 1020 | 101 open import Relation.Nullary |
| 102 open import Data.Empty | |
| 1023 | 103 open import equalizer |
| 999 | 104 |
| 1020 | 105 data Bool { c : Level } : Set c where |
| 106 true : Bool | |
| 107 false : Bool | |
| 1023 | 108 |
| 109 ¬f≡t : { c : Level } → ¬ (false {c} ≡ true ) | |
| 110 ¬f≡t () | |
| 1025 | 111 |
| 112 ¬x≡t∧x≡f : { c : Level } → {x : Bool {c}} → ¬ ((x ≡ false) /\ (x ≡ true) ) | |
| 113 ¬x≡t∧x≡f {_} {true} p = ⊥-elim (¬f≡t (sym (proj₁ p))) | |
| 114 ¬x≡t∧x≡f {_} {false} p = ⊥-elim (¬f≡t (proj₂ p)) | |
| 1020 | 115 |
| 1022 | 116 data _∨_ {c c' : Level } (a : Set c) (b : Set c') : Set (c ⊔ c') where |
|
1021
8a78ddfdaa24
... use LEM for Topos Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1020
diff
changeset
|
117 case1 : a → a ∨ b |
|
8a78ddfdaa24
... use LEM for Topos Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1020
diff
changeset
|
118 case2 : b → a ∨ b |
|
8a78ddfdaa24
... use LEM for Topos Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1020
diff
changeset
|
119 |
| 1024 | 120 -- |
| 121 -- m : b → a determins a subset of a as an image | |
| 122 -- b and m-image in a has one to one correspondence with an equalizer (x : b) → (y : a) ≡ m x. | |
| 123 -- so tchar m mono and ker (tchar m mono) is Iso. | |
| 124 -- Finding (x : b) from (y : a) is non constructive. Assuming LEM of image. | |
| 125 -- | |
| 126 data image {c : Level} {a b : Set c} (m : Hom Sets b a) : a → Set c where | |
| 127 isImage : (x : b ) → image m (m x) | |
| 1022 | 128 |
| 129 topos : {c : Level } → ({ c : Level} → (b : Set c) → b ∨ (¬ b)) → Topos (Sets {c}) sets | |
|
1021
8a78ddfdaa24
... use LEM for Topos Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1020
diff
changeset
|
130 topos {c} lem = record { |
| 1023 | 131 Ω = Bool |
| 132 ; ⊤ = λ _ → true | |
| 999 | 133 ; Ker = tker |
| 1020 | 134 ; char = λ m mono → tchar m mono |
| 999 | 135 ; isTopos = record { |
| 1018 | 136 char-uniqueness = λ {a} {b} {h} m mono → extensionality Sets ( λ x → uniq h m mono x ) |
| 137 ; ker-m = imequ | |
| 999 | 138 } |
| 139 } where | |
| 1023 | 140 -- |
| 1024 | 141 -- In Sets, equalizers exist as |
| 1022 | 142 -- data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where |
| 143 -- elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g | |
| 1024 | 144 -- m have to be isomorphic to ker (char m). |
| 145 -- | |
| 1022 | 146 -- i ○ b |
| 147 -- ker (char m) ----→ b -----------→ 1 | |
| 148 -- | ←---- | | | |
| 1024 | 149 -- | j |m | ⊤ char m : a → Ω = {true,false} |
| 150 -- | e ↓ char m ↓ if y : a ≡ m (∃ x : b) → true ( data char ) | |
| 151 -- +-------------→ a -----------→ Ω else false | |
| 1022 | 152 -- h |
| 153 -- | |
| 1023 | 154 tker : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true ) o CCC.○ sets a ]) |
| 999 | 155 tker {a} h = record { |
| 1023 | 156 equalizer-c = sequ a Bool h (λ _ → true ) |
| 1018 | 157 ; equalizer = λ e → equ e |
| 158 ; isEqualizer = SetsIsEqualizer _ _ _ _ } | |
| 1023 | 159 tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c} |
| 1024 | 160 tchar {a} {b} m mono y with lem (image m y ) |
| 1023 | 161 ... | case1 t = true |
| 162 ... | case2 f = false | |
| 1028 | 163 |
| 164 s2i : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (e : sequ a Bool (tchar m mono) (λ _ → true )) → image m (equ e) | |
| 165 s2i {a} {b} m mono (elem y eq) with lem (image m y) | |
| 166 ... | case1 im = im | |
| 167 i2s : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → {y : a} → (i : image m y) → sequ a Bool (tchar m mono) (λ _ → true ) | |
| 168 i2s {a} {b} m mono {y} i with lem (image m y) | inspect (tchar m mono) y | |
| 169 ... | case1 (isImage x) | record { eq = eq1 } = elem (m x) eq1 | |
| 170 ... | case2 n | record { eq = eq1 } = ⊥-elim (n i) | |
| 171 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | |
| 172 ii : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → {y : a} → (i : image m y) → s2i m mono ( i2s m mono i ) ≅ i | |
| 173 ii {a} {b} m mono {y} i with lem (image m y) | inspect (tchar m mono) y | |
| 174 ... | case2 n | t = ⊥-elim (n i) | |
| 175 ... | case1 (isImage x) | record { eq = eq1 } = {!!} | |
| 176 ss : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (e : sequ a Bool (tchar m mono) (λ _ → true )) → i2s m mono ( s2i m mono e ) ≡ e | |
| 177 ss = {!!} | |
| 1025 | 178 tcharImg : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (y : a) → tchar m mono y ≡ true → image m y |
| 179 tcharImg m mono y eq with lem (image m y) | |
| 180 ... | case1 t = t | |
| 181 tchar¬Img : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) (y : a) → tchar m mono y ≡ false → ¬ image m y | |
| 182 tchar¬Img m mono y eq im with lem (image m y) | |
| 183 ... | case2 n = n im | |
| 184 img-x : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → image m y → b | |
| 185 img-x m {.(m x)} (isImage x) = x | |
| 1026 | 186 m-img-x : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → (t : image m y ) → m (img-x m t) ≡ y |
| 187 m-img-x m (isImage x) = refl | |
| 1025 | 188 img-cong : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (y y' : a) → y ≡ y' → (s : image m y ) (t : image m y') → s ≅ t |
| 189 img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁) | |
| 190 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) ) | |
| 191 ... | refl = HE.refl | |
| 192 img-x-cong : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (y y' : a) → y ≡ y' → (s : image m y ) →( t : image m y') → img-x m s ≡ img-x m t | |
| 193 img-x-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁) | |
| 194 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) ) | |
| 195 ... | refl = refl | |
| 196 img-x-cong0 : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (y : a) → (s t : image m y ) → img-x m s ≡ img-x m t | |
| 197 img-x-cong0 m mono y s t = img-x-cong m mono y y refl s t | |
| 1023 | 198 isol : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → IsoL Sets m (λ (e : sequ a Bool (tchar m mono) (λ _ → true )) → equ e ) |
| 1025 | 199 isol {a} {b} m mono = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ; |
| 1026 | 200 iso→ = extensionality Sets ( λ x → iso1 x ) |
| 1025 | 201 ; iso← = extensionality Sets ( λ x → iso2 x) } ; iso≈L = {!!} } where |
| 1023 | 202 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true)) |
| 1025 | 203 b→s x with tchar m mono (m x) | inspect (tchar m mono ) (m x) |
| 204 ... | true | record { eq = eq1 } = elem (m x) eq1 | |
| 205 b→s x | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1 | |
| 206 ... | t = ⊥-elim (t (isImage x)) | |
| 1023 | 207 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b |
| 1025 | 208 b←s (elem y eq) with tchar m mono y | inspect (tchar m mono ) y |
| 209 ... | true | record { eq = eq1 } = img-x m (tcharImg m mono y eq1 ) | |
| 1028 | 210 i←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) (image m {!!}) |
| 211 i←s (elem y eq) = {!!} | |
| 212 bs1 : (y : a) → (eq1 : tchar m mono y ≡ true ) → m (b←s ( elem y eq1 )) ≡ y | |
| 213 bs1 y eq1 with tcharImg m mono y eq1 | |
| 214 ... | isImage x = {!!} | |
| 1026 | 215 iso1 : (x : b) → b←s ( b→s x ) ≡ x |
| 1025 | 216 iso1 x with tchar m mono (m x) | inspect (tchar m mono ) (m x) |
| 1028 | 217 ... | true | record { eq = eq1 } = begin |
| 218 b←s ( elem (m x) eq1 ) ≡⟨ cong (λ k → k ! ) (Mono.isMono mono {One} (λ _ → b←s ( elem (m x) eq1 ) ) (λ _ → x ) (cong (λ k _ → k ) (bs1 (m x) eq1 ))) ⟩ | |
| 1026 | 219 x ∎ where open ≡-Reasoning |
| 1025 | 220 iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x)) |
| 221 iso2 : (x : sequ a Bool (tchar m mono) (λ _ → true) ) → (Sets [ b→s o b←s ]) x ≡ id1 Sets (sequ a Bool (tchar m mono) (λ _ → true)) x | |
| 222 iso2 (elem y eq) = {!!} | |
| 1023 | 223 imequ : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true ) o CCC.○ sets a ]) |
| 1022 | 224 imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) |
| 1023 | 225 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) → |
| 226 tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y | |
| 1025 | 227 uniq {a} {b} h m mono y with h y | inspect h y | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y |
| 228 ... | true | record { eq = eqhy } | case1 x | record { eq = eq1 } = eq1 | |
| 229 ... | true | record { eq = eqhy } | case2 x | record { eq = eq1 } = ⊥-elim (x (isImage (elem y eqhy))) | |
| 230 ... | false | record { eq = eqhy } | case1 (isImage (elem x eq)) | record { eq = eq1 } = ⊥-elim ( ¬x≡t∧x≡f record {fst = eqhy ; snd = eq }) | |
| 231 ... | false | record { eq = eqhy } | case2 x | record { eq = eq1 } = eq1 | |
| 1010 | 232 |
| 999 | 233 |
| 234 open import graph | |
| 235 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where | |
| 236 | |
| 237 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) | |
| 238 open Graph | |
| 239 | |
| 240 V = vertex G | |
| 241 E : V → V → Set c₂ | |
| 242 E = edge G | |
| 243 | |
| 244 data Objs : Set c₁ where | |
| 245 atom : V → Objs | |
| 246 ⊤ : Objs | |
| 247 _∧_ : Objs → Objs → Objs | |
| 248 _<=_ : Objs → Objs → Objs | |
| 249 | |
| 250 data Arrows : (b c : Objs ) → Set (c₁ ⊔ c₂) | |
| 251 data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i | |
| 252 arrow : {a b : V} → E a b → Arrow (atom a) (atom b) | |
| 253 π : {a b : Objs } → Arrow ( a ∧ b ) a | |
| 254 π' : {a b : Objs } → Arrow ( a ∧ b ) b | |
| 255 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a | |
| 256 _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v | |
| 257 | |
| 258 data Arrows where | |
| 259 id : ( a : Objs ) → Arrows a a --- case i | |
| 260 ○ : ( a : Objs ) → Arrows a ⊤ --- case i | |
| 261 <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii | |
| 262 iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv | |
| 263 | |
| 264 _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c | |
| 265 id a ・ g = g | |
| 266 ○ a ・ g = ○ _ | |
| 267 < f , g > ・ h = < f ・ h , g ・ h > | |
| 268 iv f g ・ h = iv f ( g ・ h ) | |
| 269 | |
| 270 | |
| 271 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f | |
| 272 identityL = refl | |
| 273 | |
| 274 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f | |
| 275 identityR {a} {a} {id a} = refl | |
| 276 identityR {a} {⊤} {○ a} = refl | |
| 277 identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR | |
| 278 identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR | |
| 279 | |
| 280 assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → | |
| 281 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) | |
| 282 assoc≡ (id a) g h = refl | |
| 283 assoc≡ (○ a) g h = refl | |
| 284 assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h) | |
| 285 assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) | |
| 286 | |
| 287 -- positive intutionistic calculus | |
| 288 PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂) | |
| 289 PL = record { | |
| 290 Obj = Objs; | |
| 291 Hom = λ a b → Arrows a b ; | |
| 292 _o_ = λ{a} {b} {c} x y → x ・ y ; | |
| 293 _≈_ = λ x y → x ≡ y ; | |
| 294 Id = λ{a} → id a ; | |
| 295 isCategory = record { | |
| 296 isEquivalence = record {refl = refl ; trans = trans ; sym = sym} ; | |
| 297 identityL = λ {a b f} → identityL {a} {b} {f} ; | |
| 298 identityR = λ {a b f} → identityR {a} {b} {f} ; | |
| 299 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; | |
| 300 associative = λ{a b c d f g h } → assoc≡ f g h | |
| 301 } | |
| 302 } where | |
| 303 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → | |
| 304 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) | |
| 305 o-resp-≈ refl refl = refl | |
| 306 -------- | |
| 307 -- | |
| 308 -- Functor from Positive Logic to Sets | |
| 309 -- | |
| 310 | |
| 311 -- open import Category.Sets | |
| 312 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂ | |
| 313 | |
| 314 open import Data.List | |
| 315 | |
| 316 C = graphtocat.Chain G | |
| 317 | |
| 318 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b | |
| 319 tr f x y = graphtocat.next f (x y) | |
| 320 | |
| 321 fobj : ( a : Objs ) → Set (c₁ ⊔ c₂) | |
| 322 fobj (atom x) = ( y : vertex G ) → C y x | |
| 323 fobj ⊤ = One | |
| 324 fobj (a ∧ b) = ( fobj a /\ fobj b) | |
| 325 fobj (a <= b) = fobj b → fobj a | |
| 326 | |
| 327 fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b | |
| 328 amap : { a b : Objs } → Arrow a b → fobj a → fobj b | |
| 329 amap (arrow x) y = tr x y -- tr x | |
| 330 amap π ( x , y ) = x | |
| 331 amap π' ( x , y ) = y | |
| 332 amap ε (f , x ) = f x | |
| 333 amap (f *) x = λ y → fmap f ( x , y ) | |
| 334 fmap (id a) x = x | |
| 1020 | 335 fmap (○ a) x = ! |
| 999 | 336 fmap < f , g > x = ( fmap f x , fmap g x ) |
| 337 fmap (iv x f) a = amap x ( fmap f a ) | |
| 338 | |
| 339 -- CS is a map from Positive logic to Sets | |
| 340 -- Sets is CCC, so we have a cartesian closed category generated by a graph | |
| 341 -- as a sub category of Sets | |
| 342 | |
| 343 CS : Functor PL (Sets {c₁ ⊔ c₂}) | |
| 344 FObj CS a = fobj a | |
| 345 FMap CS {a} {b} f = fmap {a} {b} f | |
| 346 isFunctor CS = isf where | |
| 347 _+_ = Category._o_ PL | |
| 348 ++idR = IsCategory.identityR ( Category.isCategory PL ) | |
| 349 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) | |
| 350 distr {a} {a₁} {a₁} {f} {id a₁} z = refl | |
| 351 distr {a} {a₁} {⊤} {f} {○ a₁} z = refl | |
| 352 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) | |
| 353 distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr {a} {b} {d} {f} {g} z) x where | |
| 354 adistr : fmap (g + f) z ≡ fmap g (fmap f z) → | |
| 355 ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) | |
| 356 adistr eq x = cong ( λ k → amap x k ) eq | |
| 357 isf : IsFunctor PL Sets fobj fmap | |
| 358 IsFunctor.identity isf = extensionality Sets ( λ x → refl ) | |
| 359 IsFunctor.≈-cong isf refl = refl | |
| 360 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) | |
| 361 | |
| 362 |