Mercurial > hg > Members > kono > Proof > category

comparison src/CCCSets.agda @ 1032:c3b3faa791fa sets-topos

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
topos of Sets done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Mar 2021 23:30:55 +0900
parents 52c98490c877
children 40c39d3e6a75
comparison
equal deleted inserted replaced
1031:52c98490c877 1032:c3b3faa791fa
158 ; isEqualizer = SetsIsEqualizer _ _ _ _ } 158 ; isEqualizer = SetsIsEqualizer _ _ _ _ }
159 tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c} 159 tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c}
160 tchar {a} {b} m mono y with lem (image m y ) 160 tchar {a} {b} m mono y with lem (image m y )
161 ... | case1 t = true 161 ... | case1 t = true
162 ... | case2 f = false 162 ... | case2 f = false
163
163 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 164 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
164 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 165 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
165 img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁) 166 img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁)
166 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) ) 167 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) )
167 ... | refl = HE.refl 168 ... | refl = HE.refl
168 image-iso : {a b : Obj (Sets {c})} (m : Hom Sets b a) → (mono : Mono Sets m ) (y : a) → (i0 i1 : image m y ) → i0 ≡ i1 169 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
169 image-iso {a} {b} m mono y i0 i1 = HE.≅-to-≡ (img-cong m mono y y refl i0 i1) 170 image-uniq {a} {b} m mono y i0 i1 = HE.≅-to-≡ (img-cong m mono y y refl i0 i1)
170 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 171 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
171 tchar¬Img m mono y eq im with lem (image m y) 172 tchar¬Img m mono y eq im with lem (image m y)
172 ... | case2 n = n im 173 ... | case2 n = n im
173 b2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → image m (m x) 174 b2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → image m (m x)
174 b2i m x = isImage x 175 b2i m x = isImage x
175 i2b : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → image m y → b 176 i2b : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → image m y → b
176 i2b m (isImage x) = x 177 i2b m (isImage x) = x
178 img-mx=y : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → (im : image m y ) → m (i2b m im) ≡ y
179 img-mx=y m (isImage x) = refl
177 b2i-iso : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → i2b m (b2i m x) ≡ x 180 b2i-iso : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → i2b m (b2i m x) ≡ x
178 b2i-iso m x = refl 181 b2i-iso m x = refl
179 b2s : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → sequ a Bool (tchar m mono) (λ _ → true ) 182 b2s : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → sequ a Bool (tchar m mono) (λ _ → true )
180 b2s m mono x with tchar m mono (m x) | inspect (tchar m mono) (m x) 183 b2s m mono x with tchar m mono (m x) | inspect (tchar m mono) (m x)
181 ... | true | record {eq = eq1} = elem (m x) eq1 184 ... | true | record {eq = eq1} = elem (m x) eq1
182 ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1 185 ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1
183 ... | t = ⊥-elim (t (isImage x)) 186 ... | t = ⊥-elim (t (isImage x))
184 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) 187 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)
185 s2i {a} {b} m mono (elem y eq) with lem (image m y) 188 s2i {a} {b} m mono (elem y eq) with lem (image m y)
186 ... | case1 im = im 189 ... | case1 im = im
187 s2ii : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → (eq1 : tchar m mono (m x) ≡ true)
188 → s2i m mono (elem (m x ) eq1) ≡ isImage x
189 s2ii m mono x eq1 with lem (image m (m x))
190 ... | case1 im = s2ii0 where
191 s2ii0 : im ≡ isImage x
192 s2ii0 = image-iso m mono (m x) im (isImage x)
193 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 ) 190 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 )
194 isol {a} {b} m mono = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ; 191 isol {a} {b} m mono = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ;
195 iso→ = extensionality Sets ( λ x → iso1 x ) 192 iso→ = extensionality Sets ( λ x → iso1 x )
196 ; iso← = extensionality Sets ( λ x → iso2 x) } ; iso≈L = {!!} } where 193 ; iso← = extensionality Sets ( λ x → iso2 x) } ; iso≈L = extensionality Sets ( λ s → iso3 s ) } where
197 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true)) 194 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))
198 b→s x = b2s m mono x 195 b→s x = b2s m mono x
199 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b 196 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
200 b←s (elem y eq) = i2b m (s2i m mono (elem y eq)) 197 b←s (elem y eq) = i2b m (s2i m mono (elem y eq))
198 iso3 : (s : sequ a Bool (tchar m mono) (λ _ → true)) → m (b←s s) ≡ equ s
199 iso3 (elem y eq) with lem (image m y)
200 ... | case1 (isImage x) = refl
201 iso1 : (x : b) → b←s ( b→s x ) ≡ x 201 iso1 : (x : b) → b←s ( b→s x ) ≡ x
202 iso1 x with tchar m mono (m x) | inspect (tchar m mono ) (m x) 202 iso1 x with tchar m mono (m x) | inspect (tchar m mono ) (m x)
203 ... | true | record { eq = eq1 } = begin 203 ... | true | record { eq = eq1 } = begin
204 b←s ( elem (m x) eq1 ) ≡⟨⟩ 204 b←s ( elem (m x) eq1 ) ≡⟨⟩
205 i2b m (s2i m mono (elem (m x ) eq1 )) ≡⟨ cong (λ k → i2b m k) (s2ii m mono x eq1 ) ⟩ 205 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) ) ⟩
206 i2b m (isImage x) ≡⟨⟩ 206 i2b m (isImage x) ≡⟨⟩
207 x ∎ where open ≡-Reasoning 207 x ∎ where open ≡-Reasoning
208 iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x)) 208 iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x))
209 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 209 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
210 iso2 (elem y eq) = {!!} 210 iso2 (elem y eq) = begin
211 b→s ( b←s (elem y eq)) ≡⟨⟩
212 b2s m mono ( i2b m (s2i m mono (elem y eq))) ≡⟨⟩
213 b2s m mono x ≡⟨ elm-cong _ _ (iso21 x ) ⟩
214 elem (m x) eq1 ≡⟨ elm-cong _ _ mx=y ⟩
215 elem y eq ∎ where
216 open ≡-Reasoning
217 x : b
218 x = i2b m (s2i m mono (elem y eq))
219 eq1 : tchar m mono (m x) ≡ true
220 eq1 with lem (image m (m x))
221 ... | case1 t = refl
222 ... | case2 n = ⊥-elim (n (isImage x))
223 mx=y : m x ≡ y
224 mx=y = img-mx=y m (s2i m mono (elem y eq))
225 iso21 : (x : b) → equ (b2s m mono x ) ≡ m x
226 iso21 x with tchar m mono (m x) | inspect (tchar m mono) (m x)
227 ... | true | record {eq = eq1} = refl
228 ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1
229 ... | t = ⊥-elim (t (isImage x))
211 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 ]) 230 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 ])
212 imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) 231 imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono)
213 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) → 232 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) →
214 tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y 233 tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y
215 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 234 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