Mercurial > hg > Members > kono > Proof > category

comparison src/CCCSets.agda @ 1031:52c98490c877

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sets Topos iso1 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Mar 2021 20:22:20 +0900
parents 76a7d5a8a4e0
children c3b3faa791fa
comparison
equal deleted inserted replaced
1030:76a7d5a8a4e0 1031:52c98490c877
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 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 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) )
167 ... | refl = HE.refl
164 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 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
165 image-iso = {!!} 169 image-iso {a} {b} m mono y i0 i1 = HE.≅-to-≡ (img-cong m mono y y refl i0 i1)
166 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 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
167 tchar¬Img m mono y eq im with lem (image m y) 171 tchar¬Img m mono y eq im with lem (image m y)
168 ... | case2 n = n im 172 ... | case2 n = n im
169 b2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → image m (m x) 173 b2i : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (x : b) → image m (m x)
170 b2i m x = isImage x 174 b2i m x = isImage x