Mercurial > hg > Members > kono > Proof > category

comparison src/CCCSets.agda @ 1024:447bbacacf64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Mar 2021 08:11:58 +0900
parents 227e1fe321ea
children 49fbc57ea772
comparison
equal deleted inserted replaced
1023:227e1fe321ea 1024:447bbacacf64
111 111
112 data _∨_ {c c' : Level } (a : Set c) (b : Set c') : Set (c ⊔ c') where 112 data _∨_ {c c' : Level } (a : Set c) (b : Set c') : Set (c ⊔ c') where
113 case1 : a → a ∨ b 113 case1 : a → a ∨ b
114 case2 : b → a ∨ b 114 case2 : b → a ∨ b
115 115
116 data char {c : Level} {a b : Set c} (m : Hom Sets b a) : a → Set c where 116 --
117 isChar : (x : b ) → char m (m x) 117 -- m : b → a determins a subset of a as an image
118 -- b and m-image in a has one to one correspondence with an equalizer (x : b) → (y : a) ≡ m x.
119 -- so tchar m mono and ker (tchar m mono) is Iso.
120 -- Finding (x : b) from (y : a) is non constructive. Assuming LEM of image.
121 --
122 data image {c : Level} {a b : Set c} (m : Hom Sets b a) : a → Set c where
123 isImage : (x : b ) → image m (m x)
118 124
119 topos : {c : Level } → ({ c : Level} → (b : Set c) → b ∨ (¬ b)) → Topos (Sets {c}) sets 125 topos : {c : Level } → ({ c : Level} → (b : Set c) → b ∨ (¬ b)) → Topos (Sets {c}) sets
120 topos {c} lem = record { 126 topos {c} lem = record {
121 Ω = Bool 127 Ω = Bool
122 ; ⊤ = λ _ → true 128 ; ⊤ = λ _ → true
126 char-uniqueness = λ {a} {b} {h} m mono → extensionality Sets ( λ x → uniq h m mono x ) 132 char-uniqueness = λ {a} {b} {h} m mono → extensionality Sets ( λ x → uniq h m mono x )
127 ; ker-m = imequ 133 ; ker-m = imequ
128 } 134 }
129 } where 135 } where
130 -- 136 --
137 -- In Sets, equalizers exist as
131 -- data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where 138 -- data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where
132 -- elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g 139 -- elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g
140 -- m have to be isomorphic to ker (char m).
141 --
133 -- i ○ b 142 -- i ○ b
134 -- ker (char m) ----→ b -----------→ 1 143 -- ker (char m) ----→ b -----------→ 1
135 -- | ←---- | | 144 -- | ←---- | |
136 -- | j |m | ⊤ char m : a → Ω = {1,⊥} 145 -- | j |m | ⊤ char m : a → Ω = {true,false}
137 -- | e ↓ char m ↓ if y : a ≡ m (∃ x : b) → 1 146 -- | e ↓ char m ↓ if y : a ≡ m (∃ x : b) → true ( data char )
138 -- +-------------→ a -----------→ Ω else ⊥ 147 -- +-------------→ a -----------→ Ω else false
139 -- h 148 -- h
140 -- 149 --
141 tker : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true ) o CCC.○ sets a ]) 150 tker : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true ) o CCC.○ sets a ])
142 tker {a} h = record { 151 tker {a} h = record {
143 equalizer-c = sequ a Bool h (λ _ → true ) 152 equalizer-c = sequ a Bool h (λ _ → true )
144 ; equalizer = λ e → equ e 153 ; equalizer = λ e → equ e
145 ; isEqualizer = SetsIsEqualizer _ _ _ _ } 154 ; isEqualizer = SetsIsEqualizer _ _ _ _ }
146 tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c} 155 tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c}
147 tchar {a} {b} m mono y with lem (char m y ) 156 tchar {a} {b} m mono y with lem (image m y )
148 ... | case1 t = true 157 ... | case1 t = true
149 ... | case2 f = false 158 ... | case2 f = false
150 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 ) 159 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 )
151 isol {a} {b} m mono = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ; iso→ = {!!} ; iso← = {!!} } ; iso≈L = {!!} } where 160 isol {a} {b} m mono = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ; iso→ = {!!} ; iso← = {!!} } ; iso≈L = {!!} } where
152 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true)) 161 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))
153 b→s x with lem (char m (m x) ) 162 b→s x with lem (image m (m x) )
154 ... | case1 x₁ = bs1 x₁ refl where 163 ... | case1 x₁ = bs1 x₁ refl where
155 bs1 : {y : a } → char m y → y ≡ m x → sequ a Bool (λ y → tchar m mono y) (λ _ → true) 164 bs1 : {y : a } → image m y → y ≡ m x → sequ a Bool (λ y → tchar m mono y) (λ _ → true)
156 bs1 (isChar x) eq = elem (m x) {!!} 165 bs1 (isImage x) eq = elem (m x) {!!}
157 ... | case2 n = ⊥-elim (n (isChar x)) 166 ... | case2 n = ⊥-elim (n (isImage x))
158 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b 167 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
159 b←s (elem y eq) with lem (char m y) 168 b←s (elem y eq) with lem (image m y)
160 ... | case1 (isChar x) = x 169 ... | case1 (isImage x) = x
161 ... | case2 t = ⊥-elim ( ¬f≡t eq ) 170 ... | case2 t = ⊥-elim ( ¬f≡t eq )
162 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 ]) 171 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 ])
163 imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) 172 imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono)
164 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) → 173 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) →
165 tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y 174 tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y
166 uniq {a} {b} h m mono y with h y | lem (char (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y 175 uniq {a} {b} h m mono y with h y | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y
167 ... | true | case1 x | record { eq = eq1 } = eq1 176 ... | true | case1 x | record { eq = eq1 } = eq1
168 ... | true | case2 x | record { eq = eq1 } = {!!} 177 ... | true | case2 x | record { eq = eq1 } = {!!}
169 ... | false | case1 x | record { eq = eq1 } = {!!} 178 ... | false | case1 (isImage (elem x eq)) | record { eq = eq1 } = {!!}
170 ... | false | case2 x | record { eq = eq1 } = eq1 179 ... | false | case2 x | record { eq = eq1 } = eq1
171 180
172 181
173 open import graph 182 open import graph
174 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where 183 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where