Mercurial > hg > Members > kono > Proof > category
annotate src/CCCSets.agda @ 1094:bcaa8f66ec09
iso-char in Sets Topos
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 18 May 2021 01:06:43 +0900 |
| parents | 5e89bbb4cf53 |
| children | 0211d99f29fc |
| 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 |
| 1034 | 120 --------------------------------------------- |
| 121 -- | |
| 122 -- a binary Topos of Sets | |
| 1024 | 123 -- |
| 124 -- m : b → a determins a subset of a as an image | |
| 125 -- b and m-image in a has one to one correspondence with an equalizer (x : b) → (y : a) ≡ m x. | |
| 126 -- so tchar m mono and ker (tchar m mono) is Iso. | |
| 127 -- Finding (x : b) from (y : a) is non constructive. Assuming LEM of image. | |
| 128 -- | |
| 129 data image {c : Level} {a b : Set c} (m : Hom Sets b a) : a → Set c where | |
| 130 isImage : (x : b ) → image m (m x) | |
| 1022 | 131 |
| 132 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
|
133 topos {c} lem = record { |
| 1023 | 134 Ω = Bool |
| 135 ; ⊤ = λ _ → true | |
| 999 | 136 ; Ker = tker |
| 1020 | 137 ; char = λ m mono → tchar m mono |
| 999 | 138 ; isTopos = record { |
| 1069 | 139 char-uniqueness = λ {a} {b} {h} → extensionality Sets ( λ x → uniq h x ) |
| 1075 | 140 ; char-iso = iso-m |
| 141 ; ker-m = ker-iso | |
| 999 | 142 } |
| 143 } where | |
| 1023 | 144 -- |
| 1024 | 145 -- In Sets, equalizers exist as |
| 1022 | 146 -- data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where |
| 147 -- elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g | |
| 1024 | 148 -- m have to be isomorphic to ker (char m). |
| 149 -- | |
| 1034 | 150 -- b→s ○ b |
| 1022 | 151 -- ker (char m) ----→ b -----------→ 1 |
| 152 -- | ←---- | | | |
| 1034 | 153 -- | b←s |m | ⊤ char m : a → Ω = {true,false} |
| 1024 | 154 -- | e ↓ char m ↓ if y : a ≡ m (∃ x : b) → true ( data char ) |
| 155 -- +-------------→ a -----------→ Ω else false | |
| 1022 | 156 -- h |
| 157 -- | |
| 1023 | 158 tker : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true ) o CCC.○ sets a ]) |
| 999 | 159 tker {a} h = record { |
| 1023 | 160 equalizer-c = sequ a Bool h (λ _ → true ) |
| 1018 | 161 ; equalizer = λ e → equ e |
| 162 ; isEqualizer = SetsIsEqualizer _ _ _ _ } | |
| 1023 | 163 tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c} |
| 1024 | 164 tchar {a} {b} m mono y with lem (image m y ) |
| 1023 | 165 ... | case1 t = true |
| 166 ... | case2 f = false | |
| 1034 | 167 -- 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 ]) |
| 168 -- imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) | |
| 1069 | 169 uniq : {a : Obj (Sets {c})} (h : Hom Sets a Bool) (y : a) → |
| 1034 | 170 tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y |
| 1069 | 171 uniq {a} h 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 |
| 1034 | 172 ... | true | record { eq = eqhy } | case1 x | record { eq = eq1 } = eq1 |
| 173 ... | true | record { eq = eqhy } | case2 x | record { eq = eq1 } = ⊥-elim (x (isImage (elem y eqhy))) | |
| 174 ... | false | record { eq = eqhy } | case1 (isImage (elem x eq)) | record { eq = eq1 } = ⊥-elim ( ¬x≡t∧x≡f record {fst = eqhy ; snd = eq }) | |
| 175 ... | false | record { eq = eqhy } | case2 x | record { eq = eq1 } = eq1 | |
| 176 | |
| 177 -- technical detail of equalizer-image isomorphism (isol) below | |
| 1031 | 178 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 179 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 | |
| 180 img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁) | |
| 181 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) ) | |
| 182 ... | refl = HE.refl | |
| 1032 | 183 image-uniq : {a b : Obj (Sets {c})} (m : Hom Sets b a) → (mono : Mono Sets m ) (y : a) → (i0 i1 : image m y ) → i0 ≡ i1 |
| 184 image-uniq {a} {b} m mono y i0 i1 = HE.≅-to-≡ (img-cong m mono y y refl i0 i1) | |
| 1030 | 185 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 |
| 186 tchar¬Img m mono y eq im with lem (image m y) | |
| 187 ... | case2 n = n im | |
| 188 b2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → image m (m x) | |
| 189 b2i m x = isImage x | |
| 190 i2b : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → image m y → b | |
| 191 i2b m (isImage x) = x | |
| 1032 | 192 img-mx=y : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → (im : image m y ) → m (i2b m im) ≡ y |
| 193 img-mx=y m (isImage x) = refl | |
| 1030 | 194 b2i-iso : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → i2b m (b2i m x) ≡ x |
| 195 b2i-iso m x = refl | |
| 1029 | 196 b2s : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → sequ a Bool (tchar m mono) (λ _ → true ) |
| 197 b2s m mono x with tchar m mono (m x) | inspect (tchar m mono) (m x) | |
| 198 ... | true | record {eq = eq1} = elem (m x) eq1 | |
| 1030 | 199 ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1 |
| 200 ... | t = ⊥-elim (t (isImage x)) | |
| 1029 | 201 s2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (e : sequ a Bool (tchar m mono) (λ _ → true )) → image m (equ e) |
| 1028 | 202 s2i {a} {b} m mono (elem y eq) with lem (image m y) |
| 203 ... | case1 im = im | |
| 1075 | 204 ker-iso : {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 ]) |
| 205 ker-iso {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m isol (extensionality Sets ( λ x → iso4 x)) where | |
| 1023 | 206 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true)) |
| 1030 | 207 b→s x = b2s m mono x |
| 1023 | 208 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b |
| 1030 | 209 b←s (elem y eq) = i2b m (s2i m mono (elem y eq)) |
| 1032 | 210 iso3 : (s : sequ a Bool (tchar m mono) (λ _ → true)) → m (b←s s) ≡ equ s |
| 211 iso3 (elem y eq) with lem (image m y) | |
| 212 ... | case1 (isImage x) = refl | |
| 1026 | 213 iso1 : (x : b) → b←s ( b→s x ) ≡ x |
| 1025 | 214 iso1 x with tchar m mono (m x) | inspect (tchar m mono ) (m x) |
| 1028 | 215 ... | true | record { eq = eq1 } = begin |
| 1030 | 216 b←s ( elem (m x) eq1 ) ≡⟨⟩ |
| 1032 | 217 i2b m (s2i m mono (elem (m x ) eq1 )) ≡⟨ cong (λ k → i2b m k) (image-uniq m mono (m x) (s2i m mono (elem (m x ) eq1 )) (isImage x) ) ⟩ |
| 1030 | 218 i2b m (isImage x) ≡⟨⟩ |
| 1026 | 219 x ∎ where open ≡-Reasoning |
| 1030 | 220 iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x)) |
| 1075 | 221 iso4 : (x : b ) → (Sets [ Equalizer.equalizer (tker (tchar m mono)) o b→s ]) x ≡ m x |
| 222 iso4 x = begin | |
| 223 equ (b2s m mono x) ≡⟨ sym (iso3 (b2s m mono x)) ⟩ | |
| 224 m (b←s (b2s m mono x)) ≡⟨ cong (λ k → m k ) (iso1 x) ⟩ | |
| 225 m x ∎ where open ≡-Reasoning | |
| 1025 | 226 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 |
| 1032 | 227 iso2 (elem y eq) = begin |
| 228 b→s ( b←s (elem y eq)) ≡⟨⟩ | |
| 229 b2s m mono ( i2b m (s2i m mono (elem y eq))) ≡⟨⟩ | |
| 230 b2s m mono x ≡⟨ elm-cong _ _ (iso21 x ) ⟩ | |
| 231 elem (m x) eq1 ≡⟨ elm-cong _ _ mx=y ⟩ | |
| 232 elem y eq ∎ where | |
| 233 open ≡-Reasoning | |
| 234 x : b | |
| 235 x = i2b m (s2i m mono (elem y eq)) | |
| 236 eq1 : tchar m mono (m x) ≡ true | |
| 237 eq1 with lem (image m (m x)) | |
| 238 ... | case1 t = refl | |
| 239 ... | case2 n = ⊥-elim (n (isImage x)) | |
| 240 mx=y : m x ≡ y | |
| 241 mx=y = img-mx=y m (s2i m mono (elem y eq)) | |
| 242 iso21 : (x : b) → equ (b2s m mono x ) ≡ m x | |
| 243 iso21 x with tchar m mono (m x) | inspect (tchar m mono) (m x) | |
| 244 ... | true | record {eq = eq1} = refl | |
| 245 ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1 | |
| 246 ... | t = ⊥-elim (t (isImage x)) | |
| 1075 | 247 isol : Iso Sets b (Equalizer.equalizer-c (tker (tchar m mono))) |
| 248 isol = record { ≅→ = b→s ; ≅← = b←s ; | |
| 249 iso→ = extensionality Sets ( λ x → iso1 x ) | |
|
1094
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
250 ; iso← = extensionality Sets ( λ x → iso2 x) } |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
251 |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
252 iso-m : {a a' b : Obj Sets} (p : Hom Sets a b) (q : Hom Sets a' b) (mp : Mono Sets p) (mq : Mono Sets q) → |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
253 Iso Sets a a' → Sets [ tchar p mp ≈ tchar q mq ] |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
254 iso-m {a} {a'} {b} p q mp mq i = extensionality Sets (λ y → iso-m1 y ) where |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
255 -- |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
256 -- Iso.≅← i x ○ a mq : q ( f x ) ≡ q ( g x ) → f x ≡ g x |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
257 -- a'------------→ a -----------→ 1 |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
258 -- | ⟵------------ | | |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
259 -- q| Iso.≅→ i |p | ⊤ char m : a → Ω = {true,false} |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
260 -- | ↓ char m ↓ if y : a ≡ m (∃ x : b) → true ( data char ) |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
261 -- +-------------→ b -----------→ Ω else false |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
262 -- q ( Iso.≅→ i x ) ≡ y ≡ p x |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
263 -- |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
264 iso-m1 : (y : b) → tchar p mp y ≡ tchar q mq y |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
265 iso-m1 y with lem (image p y) | lem (image q y) |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
266 ... | case1 (isImage x) | case1 x₁ = refl |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
267 ... | case1 (isImage x) | case2 not = ⊥-elim ( not iso-m2 ) where |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
268 iso-m3 : image p y -- → p x ≣ y |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
269 iso-m3 = isImage x |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
270 iso-m4 : q ( Iso.≅→ i x ) ≡ p x |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
271 iso-m4 = begin |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
272 q ( Iso.≅→ i x ) ≡⟨ {!!} ⟩ |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
273 p ( Iso.≅← i ( Iso.≅→ i x) ) ≡⟨ {!!} ⟩ |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
274 p x ∎ where open ≡-Reasoning |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
275 iso-m2 : image q (p x) |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
276 iso-m2 = subst (λ k → image q k) iso-m4 ( isImage ( Iso.≅→ i x ) ) |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
277 ... | case2 x | case1 (isImage x₁) = {!!} |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
278 ... | case2 x | case2 not = refl |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
279 |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
280 open import Polynominal (Sets {c} ) (sets {c}) |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
281 A = Sets {c} |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
282 Ω = Bool |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
283 １ = One |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
284 ⊤ = λ _ → true |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
285 ○ = λ _ → λ _ → ! |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
286 _⊢_ : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) → Set (suc c ) |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
287 _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p o h ≈ ⊤ o ○ c ] |
| 1068 | 288 → A [ Poly.f q ∙ h ≈ ⊤ o ○ c ] |
|
1094
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
289 tl01 : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) |
| 1068 | 290 → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] |
|
1094
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
291 tl01 {a} {b} p q p<q q<p = extensionality Sets t1011 where |
| 1068 | 292 open ≡-Reasoning |
| 293 t1011 : (s : b ) → Poly.f p s ≡ Poly.f q s | |
| 294 t1011 x with Poly.f p x | inspect ( Poly.f p) x | |
| 295 ... | true | record { eq = eq1 } = sym tt1 where | |
| 296 tt1 : Poly.f q _ ≡ true | |
| 297 tt1 = cong (λ k → k !) (p<q _ ( extensionality Sets (λ x → eq1) )) | |
| 298 ... | false | record { eq = eq1 } with Poly.f q x | inspect (Poly.f q) x | |
| 299 ... | true | record { eq = eq2 } = ⊥-elim ( ¬x≡t∧x≡f record { fst = eq1 ; snd = tt1 } ) where | |
| 300 tt1 : Poly.f p _ ≡ true | |
| 301 tt1 = cong (λ k → k !) (q<p _ ( extensionality Sets (λ x → eq2) )) | |
| 302 ... | false | eq2 = refl | |
| 303 | |
| 304 | |
| 999 | 305 open import graph |
| 306 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where | |
| 307 | |
| 308 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) | |
| 309 open Graph | |
| 310 | |
| 311 V = vertex G | |
| 312 E : V → V → Set c₂ | |
| 313 E = edge G | |
| 314 | |
| 315 data Objs : Set c₁ where | |
| 316 atom : V → Objs | |
| 317 ⊤ : Objs | |
| 318 _∧_ : Objs → Objs → Objs | |
| 319 _<=_ : Objs → Objs → Objs | |
| 320 | |
| 321 data Arrows : (b c : Objs ) → Set (c₁ ⊔ c₂) | |
| 322 data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i | |
| 323 arrow : {a b : V} → E a b → Arrow (atom a) (atom b) | |
| 324 π : {a b : Objs } → Arrow ( a ∧ b ) a | |
| 325 π' : {a b : Objs } → Arrow ( a ∧ b ) b | |
| 326 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a | |
| 327 _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v | |
| 328 | |
| 329 data Arrows where | |
| 330 id : ( a : Objs ) → Arrows a a --- case i | |
| 331 ○ : ( a : Objs ) → Arrows a ⊤ --- case i | |
| 332 <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii | |
| 333 iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv | |
| 334 | |
| 335 _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c | |
| 336 id a ・ g = g | |
| 337 ○ a ・ g = ○ _ | |
| 338 < f , g > ・ h = < f ・ h , g ・ h > | |
| 339 iv f g ・ h = iv f ( g ・ h ) | |
| 340 | |
| 341 | |
| 342 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f | |
| 343 identityL = refl | |
| 344 | |
| 345 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f | |
| 346 identityR {a} {a} {id a} = refl | |
| 347 identityR {a} {⊤} {○ a} = refl | |
| 348 identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR | |
| 349 identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR | |
| 350 | |
| 351 assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → | |
| 352 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) | |
| 353 assoc≡ (id a) g h = refl | |
| 354 assoc≡ (○ a) g h = refl | |
| 355 assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h) | |
| 356 assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) | |
| 357 | |
| 358 -- positive intutionistic calculus | |
| 359 PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂) | |
| 360 PL = record { | |
| 361 Obj = Objs; | |
| 362 Hom = λ a b → Arrows a b ; | |
| 363 _o_ = λ{a} {b} {c} x y → x ・ y ; | |
| 364 _≈_ = λ x y → x ≡ y ; | |
| 365 Id = λ{a} → id a ; | |
| 366 isCategory = record { | |
| 367 isEquivalence = record {refl = refl ; trans = trans ; sym = sym} ; | |
| 368 identityL = λ {a b f} → identityL {a} {b} {f} ; | |
| 369 identityR = λ {a b f} → identityR {a} {b} {f} ; | |
| 370 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; | |
| 371 associative = λ{a b c d f g h } → assoc≡ f g h | |
| 372 } | |
| 373 } where | |
| 374 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → | |
| 375 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) | |
| 376 o-resp-≈ refl refl = refl | |
| 377 -------- | |
| 378 -- | |
| 379 -- Functor from Positive Logic to Sets | |
| 380 -- | |
| 381 | |
| 382 -- open import Category.Sets | |
| 383 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂ | |
| 384 | |
| 385 open import Data.List | |
| 386 | |
| 387 C = graphtocat.Chain G | |
| 388 | |
| 389 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b | |
| 390 tr f x y = graphtocat.next f (x y) | |
| 391 | |
| 392 fobj : ( a : Objs ) → Set (c₁ ⊔ c₂) | |
| 393 fobj (atom x) = ( y : vertex G ) → C y x | |
| 394 fobj ⊤ = One | |
| 395 fobj (a ∧ b) = ( fobj a /\ fobj b) | |
| 396 fobj (a <= b) = fobj b → fobj a | |
| 397 | |
| 398 fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b | |
| 399 amap : { a b : Objs } → Arrow a b → fobj a → fobj b | |
| 400 amap (arrow x) y = tr x y -- tr x | |
| 401 amap π ( x , y ) = x | |
| 402 amap π' ( x , y ) = y | |
| 403 amap ε (f , x ) = f x | |
| 404 amap (f *) x = λ y → fmap f ( x , y ) | |
| 405 fmap (id a) x = x | |
| 1020 | 406 fmap (○ a) x = ! |
| 999 | 407 fmap < f , g > x = ( fmap f x , fmap g x ) |
| 408 fmap (iv x f) a = amap x ( fmap f a ) | |
| 409 | |
| 410 -- CS is a map from Positive logic to Sets | |
| 411 -- Sets is CCC, so we have a cartesian closed category generated by a graph | |
| 412 -- as a sub category of Sets | |
| 413 | |
| 414 CS : Functor PL (Sets {c₁ ⊔ c₂}) | |
| 415 FObj CS a = fobj a | |
| 416 FMap CS {a} {b} f = fmap {a} {b} f | |
| 417 isFunctor CS = isf where | |
| 418 _+_ = Category._o_ PL | |
| 419 ++idR = IsCategory.identityR ( Category.isCategory PL ) | |
| 420 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) | |
| 421 distr {a} {a₁} {a₁} {f} {id a₁} z = refl | |
| 422 distr {a} {a₁} {⊤} {f} {○ a₁} z = refl | |
| 423 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) | |
| 424 distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr {a} {b} {d} {f} {g} z) x where | |
| 425 adistr : fmap (g + f) z ≡ fmap g (fmap f z) → | |
| 426 ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) | |
| 427 adistr eq x = cong ( λ k → amap x k ) eq | |
| 428 isf : IsFunctor PL Sets fobj fmap | |
| 429 IsFunctor.identity isf = extensionality Sets ( λ x → refl ) | |
| 430 IsFunctor.≈-cong isf refl = refl | |
| 431 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) | |
| 432 | |
| 433 |