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