Mercurial > hg > Members > kono > Proof > category
annotate src/CCCSets.agda @ 1115:5620d4a85069
safe rewriting nearly finished
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Jul 2024 11:44:58 +0900 |
| parents | 0211d99f29fc |
| children |
| rev | line source |
|---|---|
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
1 {-# OPTIONS --with-K --cubical-compatible --allow-unsolved-metas #-} |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
2 --- {-# OPTIONS --allow-unsolved-metas #-} |
| 999 | 3 module CCCSets where |
| 4 | |
| 5 open import Level | |
| 6 open import Category | |
| 7 open import HomReasoning | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
8 open import Definitions |
| 999 | 9 open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> ) |
| 10 open import Category.Constructions.Product | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
11 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 999 | 12 open import CCC |
| 13 | |
| 14 open Functor | |
| 15 | |
| 16 -- ccc-1 : Hom A a 1 ≅ {*} | |
| 17 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) | |
| 18 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c | |
| 19 | |
| 20 open import Category.Sets | |
| 21 | |
| 22 -- Sets is a CCC | |
| 23 | |
| 1018 | 24 open import SetsCompleteness hiding (ki1) |
| 25 | |
| 26 -- import Axiom.Extensionality.Propositional | |
| 27 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ | |
| 999 | 28 |
| 29 data One {c : Level } : Set c where | |
| 1020 | 30 ! : One -- () in Haskell ( or any one object set ) |
| 999 | 31 |
| 32 sets : {c : Level } → CCC (Sets {c}) | |
| 33 sets = record { | |
| 34 １ = One | |
| 1020 | 35 ; ○ = λ _ → λ _ → ! |
| 999 | 36 ; _∧_ = _∧_ |
| 37 ; <_,_> = <,> | |
| 38 ; π = π | |
| 39 ; π' = π' | |
| 40 ; _<=_ = _<=_ | |
| 41 ; _* = _* | |
| 42 ; ε = ε | |
| 43 ; isCCC = isCCC | |
| 44 } where | |
| 45 １ : Obj Sets | |
| 46 １ = One | |
| 47 ○ : (a : Obj Sets ) → Hom Sets a １ | |
| 1020 | 48 ○ a = λ _ → ! |
| 999 | 49 _∧_ : Obj Sets → Obj Sets → Obj Sets |
| 50 _∧_ a b = a /\ b | |
| 51 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b) | |
| 52 <,> f g = λ x → ( f x , g x ) | |
| 53 π : {a b : Obj Sets } → Hom Sets (a ∧ b) a | |
| 54 π {a} {b} = proj₁ | |
| 55 π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b | |
| 56 π' {a} {b} = proj₂ | |
| 57 _<=_ : (a b : Obj Sets ) → Obj Sets | |
| 58 a <= b = b → a | |
| 59 _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b) | |
| 60 f * = λ x → λ y → f ( x , y ) | |
| 61 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a | |
| 62 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x ) | |
| 63 isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε | |
| 64 isCCC = record { | |
| 65 e2 = e2 | |
| 66 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} | |
| 67 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} | |
| 68 ; e3c = e3c | |
| 69 ; π-cong = π-cong | |
| 70 ; e4a = e4a | |
| 71 ; e4b = e4b | |
| 72 ; *-cong = *-cong | |
| 73 } where | |
| 74 e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ] | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
75 e2 {a} {f} = ? -- extensionality Sets ( λ x → e20 x ) |
| 999 | 76 where |
| 77 e20 : (x : a ) → f x ≡ ○ a x | |
| 78 e20 x with f x | |
| 1020 | 79 e20 x | ! = refl |
| 999 | 80 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → |
| 81 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
82 e3a _ = refl |
| 999 | 83 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → |
| 84 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
85 e3b _ = refl |
| 999 | 86 e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} → |
| 87 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
88 e3c _ = refl |
| 999 | 89 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → |
| 90 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
91 π-cong = ? |
| 999 | 92 e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} → |
| 93 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
94 e4a _ = refl |
| 999 | 95 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → |
| 96 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
97 e4b _ = refl |
| 999 | 98 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → |
| 99 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
100 *-cong = ? |
| 999 | 101 |
| 1020 | 102 open import Relation.Nullary |
| 103 open import Data.Empty | |
| 1023 | 104 open import equalizer |
| 999 | 105 |
| 1020 | 106 data Bool { c : Level } : Set c where |
| 107 true : Bool | |
| 108 false : Bool | |
| 1023 | 109 |
| 110 ¬f≡t : { c : Level } → ¬ (false {c} ≡ true ) | |
| 111 ¬f≡t () | |
| 1025 | 112 |
| 113 ¬x≡t∧x≡f : { c : Level } → {x : Bool {c}} → ¬ ((x ≡ false) /\ (x ≡ true) ) | |
| 114 ¬x≡t∧x≡f {_} {true} p = ⊥-elim (¬f≡t (sym (proj₁ p))) | |
| 115 ¬x≡t∧x≡f {_} {false} p = ⊥-elim (¬f≡t (proj₂ p)) | |
| 1020 | 116 |
| 1022 | 117 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
|
118 case1 : a → a ∨ b |
|
8a78ddfdaa24
... use LEM for Topos Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1020
diff
changeset
|
119 case2 : b → a ∨ b |
|
8a78ddfdaa24
... use LEM for Topos Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1020
diff
changeset
|
120 |
| 1034 | 121 --------------------------------------------- |
| 122 -- | |
| 123 -- a binary Topos of Sets | |
| 1024 | 124 -- |
| 125 -- m : b → a determins a subset of a as an image | |
| 126 -- b and m-image in a has one to one correspondence with an equalizer (x : b) → (y : a) ≡ m x. | |
| 127 -- so tchar m mono and ker (tchar m mono) is Iso. | |
| 128 -- Finding (x : b) from (y : a) is non constructive. Assuming LEM of image. | |
| 129 -- | |
| 130 data image {c : Level} {a b : Set c} (m : Hom Sets b a) : a → Set c where | |
| 131 isImage : (x : b ) → image m (m x) | |
| 1022 | 132 |
| 133 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
|
134 topos {c} lem = record { |
| 1023 | 135 Ω = Bool |
| 136 ; ⊤ = λ _ → true | |
| 999 | 137 ; Ker = tker |
| 1020 | 138 ; char = λ m mono → tchar m mono |
| 999 | 139 ; isTopos = record { |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
140 char-uniqueness = λ {a} {b} {h} → ? -- extensionality Sets ( λ x → uniq h x ) |
| 1075 | 141 ; char-iso = iso-m |
| 142 ; ker-m = ker-iso | |
| 999 | 143 } |
| 144 } where | |
| 1023 | 145 -- |
| 1024 | 146 -- In Sets, equalizers exist as |
| 1022 | 147 -- data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where |
| 148 -- elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g | |
| 1024 | 149 -- m have to be isomorphic to ker (char m). |
| 150 -- | |
| 1034 | 151 -- b→s ○ b |
| 1022 | 152 -- ker (char m) ----→ b -----------→ 1 |
| 153 -- | ←---- | | | |
| 1034 | 154 -- | b←s |m | ⊤ char m : a → Ω = {true,false} |
| 1024 | 155 -- | e ↓ char m ↓ if y : a ≡ m (∃ x : b) → true ( data char ) |
| 156 -- +-------------→ a -----------→ Ω else false | |
| 1022 | 157 -- h |
| 158 -- | |
| 1023 | 159 tker : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true ) o CCC.○ sets a ]) |
| 999 | 160 tker {a} h = record { |
| 1023 | 161 equalizer-c = sequ a Bool h (λ _ → true ) |
| 1018 | 162 ; equalizer = λ e → equ e |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
163 ; isEqualizer = SetsIsEqualizer _ _ _ _ ? } |
| 1023 | 164 tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c} |
| 1024 | 165 tchar {a} {b} m mono y with lem (image m y ) |
| 1023 | 166 ... | case1 t = true |
| 167 ... | case2 f = false | |
| 1034 | 168 -- 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 ]) |
| 169 -- imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) | |
| 1069 | 170 uniq : {a : Obj (Sets {c})} (h : Hom Sets a Bool) (y : a) → |
| 1034 | 171 tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
172 uniq = ? |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
173 -- 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 |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
174 -- ... | true | record { eq = eqhy } | case1 x | record { eq = eq1 } = eq1 |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
175 -- ... | true | record { eq = eqhy } | case2 x | record { eq = eq1 } = ⊥-elim (x (isImage (elem y eqhy))) |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
176 -- ... | false | record { eq = eqhy } | case1 (isImage (elem x eq)) | record { eq = eq1 } = ⊥-elim ( ¬x≡t∧x≡f record {fst = eqhy ; snd = eq }) |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
177 -- ... | false | record { eq = eqhy } | case2 x | record { eq = eq1 } = eq1 |
| 1034 | 178 |
| 179 -- technical detail of equalizer-image isomorphism (isol) below | |
| 1031 | 180 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 181 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 | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
182 img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁) = ? |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
183 -- with cong (λ k → k ! ) ? -- ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ? ) -- ( extensionality Sets ( λ _ → eq )) ) |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
184 -- ... | refl = HE.refl |
| 1032 | 185 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 |
| 186 image-uniq {a} {b} m mono y i0 i1 = HE.≅-to-≡ (img-cong m mono y y refl i0 i1) | |
| 1030 | 187 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 |
| 188 tchar¬Img m mono y eq im with lem (image m y) | |
| 189 ... | case2 n = n im | |
| 190 b2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → image m (m x) | |
| 191 b2i m x = isImage x | |
| 192 i2b : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → image m y → b | |
| 193 i2b m (isImage x) = x | |
| 1032 | 194 img-mx=y : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → (im : image m y ) → m (i2b m im) ≡ y |
| 195 img-mx=y m (isImage x) = refl | |
| 1030 | 196 b2i-iso : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → i2b m (b2i m x) ≡ x |
| 197 b2i-iso m x = refl | |
| 1029 | 198 b2s : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → sequ a Bool (tchar m mono) (λ _ → true ) |
| 199 b2s m mono x with tchar m mono (m x) | inspect (tchar m mono) (m x) | |
| 200 ... | true | record {eq = eq1} = elem (m x) eq1 | |
| 1030 | 201 ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1 |
| 202 ... | t = ⊥-elim (t (isImage x)) | |
| 1029 | 203 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 | 204 s2i {a} {b} m mono (elem y eq) with lem (image m y) |
| 205 ... | case1 im = im | |
| 1075 | 206 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 ]) |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
207 ker-iso {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m isol ? where -- (extensionality Sets ( λ x → iso4 x)) where |
| 1023 | 208 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true)) |
| 1030 | 209 b→s x = b2s m mono x |
| 1023 | 210 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b |
| 1030 | 211 b←s (elem y eq) = i2b m (s2i m mono (elem y eq)) |
| 1032 | 212 iso3 : (s : sequ a Bool (tchar m mono) (λ _ → true)) → m (b←s s) ≡ equ s |
| 213 iso3 (elem y eq) with lem (image m y) | |
| 214 ... | case1 (isImage x) = refl | |
| 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 |
| 1030 | 218 b←s ( elem (m x) eq1 ) ≡⟨⟩ |
| 1032 | 219 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 | 220 i2b m (isImage x) ≡⟨⟩ |
| 1026 | 221 x ∎ where open ≡-Reasoning |
| 1030 | 222 iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x)) |
| 1075 | 223 iso4 : (x : b ) → (Sets [ Equalizer.equalizer (tker (tchar m mono)) o b→s ]) x ≡ m x |
| 224 iso4 x = begin | |
| 225 equ (b2s m mono x) ≡⟨ sym (iso3 (b2s m mono x)) ⟩ | |
| 226 m (b←s (b2s m mono x)) ≡⟨ cong (λ k → m k ) (iso1 x) ⟩ | |
| 227 m x ∎ where open ≡-Reasoning | |
| 1025 | 228 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 | 229 iso2 (elem y eq) = begin |
| 230 b→s ( b←s (elem y eq)) ≡⟨⟩ | |
| 231 b2s m mono ( i2b m (s2i m mono (elem y eq))) ≡⟨⟩ | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
232 b2s m mono x ≡⟨ equ-inject ? _ _ (iso21 x ) ⟩ |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
233 elem (m x) eq1 ≡⟨ equ-inject ? _ _ mx=y ⟩ |
| 1032 | 234 elem y eq ∎ where |
| 235 open ≡-Reasoning | |
| 236 x : b | |
| 237 x = i2b m (s2i m mono (elem y eq)) | |
| 238 eq1 : tchar m mono (m x) ≡ true | |
| 239 eq1 with lem (image m (m x)) | |
| 240 ... | case1 t = refl | |
| 241 ... | case2 n = ⊥-elim (n (isImage x)) | |
| 242 mx=y : m x ≡ y | |
| 243 mx=y = img-mx=y m (s2i m mono (elem y eq)) | |
| 244 iso21 : (x : b) → equ (b2s m mono x ) ≡ m x | |
| 245 iso21 x with tchar m mono (m x) | inspect (tchar m mono) (m x) | |
| 246 ... | true | record {eq = eq1} = refl | |
| 247 ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1 | |
| 248 ... | t = ⊥-elim (t (isImage x)) | |
| 1075 | 249 isol : Iso Sets b (Equalizer.equalizer-c (tker (tchar m mono))) |
| 250 isol = record { ≅→ = b→s ; ≅← = b←s ; | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
251 iso→ = ? -- extensionality Sets ( λ x → iso1 x ) |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
252 ; iso← = ? } -- extensionality Sets ( λ x → iso2 x) } |
|
1094
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
253 |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
254 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) → |
|
1095
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1094
diff
changeset
|
255 (i : Iso Sets a a' ) → Sets [ p ≈ Sets [ q o Iso.≅→ i ] ] → Sets [ tchar p mp ≈ tchar q mq ] |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
256 iso-m {a} {a'} {b} p q mp mq i ei = ? -- extensionality Sets (λ y → iso-m1 y ) where |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
257 where |
|
1094
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 -- 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
|
260 -- a'------------→ a -----------→ 1 |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
261 -- | ⟵------------ | | |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
262 -- 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
|
263 -- | ↓ 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
|
264 -- +-------------→ b -----------→ Ω else false |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
265 -- 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
|
266 -- |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
267 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
|
268 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
|
269 ... | case1 (isImage x) | case1 x₁ = refl |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
270 ... | 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
|
271 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
|
272 iso-m4 = begin |
|
1095
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1094
diff
changeset
|
273 q ( Iso.≅→ i x ) ≡⟨ sym ( cong ( λ k → k x) ei ) ⟩ |
|
1094
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 ) ) |
|
1095
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1094
diff
changeset
|
277 ... | case2 not | case1 (isImage x) = ⊥-elim ( not ( subst (λ k → image p k) iso-m3 ( isImage ( Iso.≅← i x ) ) )) where |
|
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1094
diff
changeset
|
278 iso-m3 : p (Iso.≅← i x) ≡ q x |
|
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1094
diff
changeset
|
279 iso-m3 = begin |
|
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1094
diff
changeset
|
280 p (Iso.≅← i x) ≡⟨ cong ( λ k → k (Iso.≅← i x) ) ei ⟩ |
|
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1094
diff
changeset
|
281 q (Iso.≅→ i (Iso.≅← i x)) ≡⟨ cong (λ k → q k) (cong (λ k1 → k1 x) (Iso.iso← i)) ⟩ |
|
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1094
diff
changeset
|
282 q x ∎ where open ≡-Reasoning |
|
1094
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
283 ... | case2 x | case2 not = refl |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
284 |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
285 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
|
286 A = Sets {c} |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
287 Ω = Bool |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
288 １ = One |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
289 ⊤ = λ _ → true |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
290 ○ = λ _ → λ _ → ! |
|
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
291 _⊢_ : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) → Set (suc c ) |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
292 _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ A [ Poly.f p o h ] ≈ A [ ⊤ o ○ c ] ] |
|
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
293 → A [ Poly.f q ∙ h ≈ A [ ⊤ o ○ c ] ] |
|
1094
bcaa8f66ec09
iso-char in Sets Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1076
diff
changeset
|
294 tl01 : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) |
| 1068 | 295 → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
296 tl01 {a} {b} p q p<q q<p = ? where -- extensionality Sets t1011 where |
| 1068 | 297 open ≡-Reasoning |
| 298 t1011 : (s : b ) → Poly.f p s ≡ Poly.f q s | |
| 299 t1011 x with Poly.f p x | inspect ( Poly.f p) x | |
| 300 ... | true | record { eq = eq1 } = sym tt1 where | |
| 301 tt1 : Poly.f q _ ≡ true | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
302 tt1 = cong (λ k → k !) (p<q _ ? ) -- ( extensionality Sets (λ x → eq1) )) |
| 1068 | 303 ... | false | record { eq = eq1 } with Poly.f q x | inspect (Poly.f q) x |
| 304 ... | true | record { eq = eq2 } = ⊥-elim ( ¬x≡t∧x≡f record { fst = eq1 ; snd = tt1 } ) where | |
| 305 tt1 : Poly.f p _ ≡ true | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
306 tt1 = cong (λ k → k !) (q<p _ ? ) -- ( extensionality Sets (λ x → eq2) )) |
| 1068 | 307 ... | false | eq2 = refl |
| 308 | |
| 309 | |
| 999 | 310 open import graph |
| 311 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where | |
| 312 | |
| 313 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) | |
| 314 open Graph | |
| 315 | |
| 316 V = vertex G | |
| 317 E : V → V → Set c₂ | |
| 318 E = edge G | |
| 319 | |
| 320 data Objs : Set c₁ where | |
| 321 atom : V → Objs | |
| 322 ⊤ : Objs | |
| 323 _∧_ : Objs → Objs → Objs | |
| 324 _<=_ : Objs → Objs → Objs | |
| 325 | |
| 326 data Arrows : (b c : Objs ) → Set (c₁ ⊔ c₂) | |
| 327 data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i | |
| 328 arrow : {a b : V} → E a b → Arrow (atom a) (atom b) | |
| 329 π : {a b : Objs } → Arrow ( a ∧ b ) a | |
| 330 π' : {a b : Objs } → Arrow ( a ∧ b ) b | |
| 331 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a | |
| 332 _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v | |
| 333 | |
| 334 data Arrows where | |
| 335 id : ( a : Objs ) → Arrows a a --- case i | |
| 336 ○ : ( a : Objs ) → Arrows a ⊤ --- case i | |
| 337 <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii | |
| 338 iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv | |
| 339 | |
| 340 _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c | |
| 341 id a ・ g = g | |
| 342 ○ a ・ g = ○ _ | |
| 343 < f , g > ・ h = < f ・ h , g ・ h > | |
| 344 iv f g ・ h = iv f ( g ・ h ) | |
| 345 | |
| 346 | |
| 347 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f | |
| 348 identityL = refl | |
| 349 | |
| 350 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f | |
| 351 identityR {a} {a} {id a} = refl | |
| 352 identityR {a} {⊤} {○ a} = refl | |
| 353 identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR | |
| 354 identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR | |
| 355 | |
| 356 assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → | |
| 357 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) | |
| 358 assoc≡ (id a) g h = refl | |
| 359 assoc≡ (○ a) g h = refl | |
| 360 assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h) | |
| 361 assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) | |
| 362 | |
| 363 -- positive intutionistic calculus | |
| 364 PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂) | |
| 365 PL = record { | |
| 366 Obj = Objs; | |
| 367 Hom = λ a b → Arrows a b ; | |
| 368 _o_ = λ{a} {b} {c} x y → x ・ y ; | |
| 369 _≈_ = λ x y → x ≡ y ; | |
| 370 Id = λ{a} → id a ; | |
| 371 isCategory = record { | |
| 372 isEquivalence = record {refl = refl ; trans = trans ; sym = sym} ; | |
| 373 identityL = λ {a b f} → identityL {a} {b} {f} ; | |
| 374 identityR = λ {a b f} → identityR {a} {b} {f} ; | |
| 375 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; | |
| 376 associative = λ{a b c d f g h } → assoc≡ f g h | |
| 377 } | |
| 378 } where | |
| 379 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → | |
| 380 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) | |
| 381 o-resp-≈ refl refl = refl | |
| 382 -------- | |
| 383 -- | |
| 384 -- Functor from Positive Logic to Sets | |
| 385 -- | |
| 386 | |
| 387 -- open import Category.Sets | |
| 388 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂ | |
| 389 | |
| 390 open import Data.List | |
| 391 | |
| 392 C = graphtocat.Chain G | |
| 393 | |
| 394 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b | |
| 395 tr f x y = graphtocat.next f (x y) | |
| 396 | |
| 397 fobj : ( a : Objs ) → Set (c₁ ⊔ c₂) | |
| 398 fobj (atom x) = ( y : vertex G ) → C y x | |
| 399 fobj ⊤ = One | |
| 400 fobj (a ∧ b) = ( fobj a /\ fobj b) | |
| 401 fobj (a <= b) = fobj b → fobj a | |
| 402 | |
| 403 fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b | |
| 404 amap : { a b : Objs } → Arrow a b → fobj a → fobj b | |
| 405 amap (arrow x) y = tr x y -- tr x | |
| 406 amap π ( x , y ) = x | |
| 407 amap π' ( x , y ) = y | |
| 408 amap ε (f , x ) = f x | |
| 409 amap (f *) x = λ y → fmap f ( x , y ) | |
| 410 fmap (id a) x = x | |
| 1020 | 411 fmap (○ a) x = ! |
| 999 | 412 fmap < f , g > x = ( fmap f x , fmap g x ) |
| 413 fmap (iv x f) a = amap x ( fmap f a ) | |
| 414 | |
| 415 -- CS is a map from Positive logic to Sets | |
| 416 -- Sets is CCC, so we have a cartesian closed category generated by a graph | |
| 417 -- as a sub category of Sets | |
| 418 | |
| 419 CS : Functor PL (Sets {c₁ ⊔ c₂}) | |
| 420 FObj CS a = fobj a | |
| 421 FMap CS {a} {b} f = fmap {a} {b} f | |
| 422 isFunctor CS = isf where | |
| 423 _+_ = Category._o_ PL | |
| 424 ++idR = IsCategory.identityR ( Category.isCategory PL ) | |
| 425 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) | |
| 426 distr {a} {a₁} {a₁} {f} {id a₁} z = refl | |
| 427 distr {a} {a₁} {⊤} {f} {○ a₁} z = refl | |
| 428 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) | |
| 429 distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr {a} {b} {d} {f} {g} z) x where | |
| 430 adistr : fmap (g + f) z ≡ fmap g (fmap f z) → | |
| 431 ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) | |
| 432 adistr eq x = cong ( λ k → amap x k ) eq | |
| 433 isf : IsFunctor PL Sets fobj fmap | |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
434 IsFunctor.identity isf = ? -- extensionality Sets ( λ x → refl ) |
| 999 | 435 IsFunctor.≈-cong isf refl = refl |
|
1115
5620d4a85069
safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1095
diff
changeset
|
436 IsFunctor.distr isf {a} {b} {c} {g} {f} = ? -- extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) |
| 999 | 437 |
| 438 |