Mercurial > hg > Members > kono > Proof > category

comparison src/CCCSets.agda @ 1029:348b5c6d5670

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Mar 2021 16:03:44 +0900
parents 28569574e3cf
children 76a7d5a8a4e0
comparison
equal deleted inserted replaced
1028:28569574e3cf 1029:348b5c6d5670
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
164 s2i : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (e : sequ a Bool (tchar m mono) (λ _ → true )) → image m (equ e) 164 b2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → image m (m x)
165 b2i m mono x = isImage x
166 i2b : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → {y : a} → image m y → b
167 i2b m mono (isImage x) = x
168 b2i-iso : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → i2b m mono (b2i m mono x) ≡ x
169 b2i-iso m mono x = refl
170 b2s : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → sequ a Bool (tchar m mono) (λ _ → true )
171 b2s m mono x with tchar m mono (m x) | inspect (tchar m mono) (m x)
172 ... | true | record {eq = eq1} = elem (m x) eq1
173 ... | false | record { eq = eq1 } = {!!}
174 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)
165 s2i {a} {b} m mono (elem y eq) with lem (image m y) 175 s2i {a} {b} m mono (elem y eq) with lem (image m y)
166 ... | case1 im = im 176 ... | case1 im = im
167 i2s : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → {y : a} → (i : image m y) → sequ a Bool (tchar m mono) (λ _ → true ) 177
168 i2s {a} {b} m mono {y} i with lem (image m y) | inspect (tchar m mono) y 178
169 ... | case1 (isImage x) | record { eq = eq1 } = elem (m x) eq1
170 ... | case2 n | record { eq = eq1 } = ⊥-elim (n i)
171 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
172 ii : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → {y : a} → (i : image m y) → s2i m mono ( i2s m mono i ) ≅ i
173 ii {a} {b} m mono {y} i with lem (image m y) | inspect (tchar m mono) y
174 ... | case2 n | t = ⊥-elim (n i)
175 ... | case1 (isImage x) | record { eq = eq1 } = {!!}
176 ss : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (e : sequ a Bool (tchar m mono) (λ _ → true )) → i2s m mono ( s2i m mono e ) ≡ e
177 ss = {!!}
178 tcharImg : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (y : a) → tchar m mono y ≡ true → image m y
179 tcharImg m mono y eq with lem (image m y)
180 ... | case1 t = t
181 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
182 tchar¬Img m mono y eq im with lem (image m y)
183 ... | case2 n = n im
184 img-x : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → image m y → b
185 img-x m {.(m x)} (isImage x) = x
186 m-img-x : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → (t : image m y ) → m (img-x m t) ≡ y
187 m-img-x m (isImage x) = refl
188 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
189 img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁)
190 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) )
191 ... | refl = HE.refl
192 img-x-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') → img-x m s ≡ img-x m t
193 img-x-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁)
194 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) )
195 ... | refl = refl
196 img-x-cong0 : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (y : a) → (s t : image m y ) → img-x m s ≡ img-x m t
197 img-x-cong0 m mono y s t = img-x-cong m mono y y refl s t
198 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 ) 179 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 )
199 isol {a} {b} m mono = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ; 180 isol {a} {b} m mono = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ;
200 iso→ = extensionality Sets ( λ x → iso1 x ) 181 iso→ = extensionality Sets ( λ x → iso1 x )
201 ; iso← = extensionality Sets ( λ x → iso2 x) } ; iso≈L = {!!} } where 182 ; iso← = extensionality Sets ( λ x → iso2 x) } ; iso≈L = {!!} } where
202 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true)) 183 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))
203 b→s x with tchar m mono (m x) | inspect (tchar m mono ) (m x) 184 b→s x = {!!}
204 ... | true | record { eq = eq1 } = elem (m x) eq1
205 b→s x | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1
206 ... | t = ⊥-elim (t (isImage x))
207 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b 185 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
208 b←s (elem y eq) with tchar m mono y | inspect (tchar m mono ) y 186 b←s (elem y eq) = {!!}
209 ... | true | record { eq = eq1 } = img-x m (tcharImg m mono y eq1 )
210 i←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) (image m {!!})
211 i←s (elem y eq) = {!!}
212 bs1 : (y : a) → (eq1 : tchar m mono y ≡ true ) → m (b←s ( elem y eq1 )) ≡ y
213 bs1 y eq1 with tcharImg m mono y eq1
214 ... | isImage x = {!!}
215 iso1 : (x : b) → b←s ( b→s x ) ≡ x 187 iso1 : (x : b) → b←s ( b→s x ) ≡ x
216 iso1 x with tchar m mono (m x) | inspect (tchar m mono ) (m x) 188 iso1 x with tchar m mono (m x) | inspect (tchar m mono ) (m x)
217 ... | true | record { eq = eq1 } = begin 189 ... | true | record { eq = eq1 } = begin
218 b←s ( elem (m x) eq1 ) ≡⟨ cong (λ k → k ! ) (Mono.isMono mono {One} (λ _ → b←s ( elem (m x) eq1 ) ) (λ _ → x ) (cong (λ k _ → k ) (bs1 (m x) eq1 ))) ⟩ 190 b←s ( elem (m x) eq1 ) ≡⟨ {!!} ⟩
219 x ∎ where open ≡-Reasoning 191 x ∎ where open ≡-Reasoning
220 iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x)) 192 iso1 x | false | record { eq = eq1 } = {!!}
221 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 193 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
222 iso2 (elem y eq) = {!!} 194 iso2 (elem y eq) = {!!}
223 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 ]) 195 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 ])
224 imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) 196 imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono)
225 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) → 197 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) →