Mercurial > hg > Members > kono > Proof > category

comparison src/CCCSets.agda @ 1025:49fbc57ea772

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 Mon, 29 Mar 2021 19:55:41 +0900
parents 447bbacacf64
children 7916bde5e57b
comparison
equal deleted inserted replaced
1024:447bbacacf64 1025:49fbc57ea772
106 true : Bool 106 true : Bool
107 false : Bool 107 false : Bool
108 108
109 ¬f≡t : { c : Level } → ¬ (false {c} ≡ true ) 109 ¬f≡t : { c : Level } → ¬ (false {c} ≡ true )
110 ¬f≡t () 110 ¬f≡t ()
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))
111 115
112 data _∨_ {c c' : Level } (a : Set c) (b : Set c') : Set (c ⊔ c') where 116 data _∨_ {c c' : Level } (a : Set c) (b : Set c') : Set (c ⊔ c') where
113 case1 : a → a ∨ b 117 case1 : a → a ∨ b
114 case2 : b → a ∨ b 118 case2 : b → a ∨ b
115 119
154 ; isEqualizer = SetsIsEqualizer _ _ _ _ } 158 ; isEqualizer = SetsIsEqualizer _ _ _ _ }
155 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}
156 tchar {a} {b} m mono y with lem (image m y ) 160 tchar {a} {b} m mono y with lem (image m y )
157 ... | case1 t = true 161 ... | case1 t = true
158 ... | case2 f = false 162 ... | case2 f = false
163 tcharImg : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (y : a) → tchar m mono y ≡ true → image m y
164 tcharImg m mono y eq with lem (image m y)
165 ... | case1 t = t
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
167 tchar¬Img m mono y eq im with lem (image m y)
168 ... | case2 n = n im
169 img-x : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → image m y → b
170 img-x m {.(m x)} (isImage x) = x
171 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
172 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
173 img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁)
174 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) )
175 ... | refl = HE.refl
176 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
177 img-x-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁)
178 with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) )
179 ... | refl = refl
180 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
181 img-x-cong0 m mono y s t = img-x-cong m mono y y refl s t
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 ) 182 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 )
160 isol {a} {b} m mono = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ; iso→ = {!!} ; iso← = {!!} } ; iso≈L = {!!} } where 183 isol {a} {b} m mono = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ;
184 iso→ = Mono.isMono mono (Sets [ b←s o b→s ]) (id1 Sets _) ( extensionality Sets ( λ x → iso1 x ))
185 ; iso← = extensionality Sets ( λ x → iso2 x) } ; iso≈L = {!!} } where
161 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true)) 186 b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))
162 b→s x with lem (image m (m x) ) 187 b→s x with tchar m mono (m x) | inspect (tchar m mono ) (m x)
163 ... | case1 x₁ = bs1 x₁ refl where 188 ... | true | record { eq = eq1 } = elem (m x) eq1
164 bs1 : {y : a } → image m y → y ≡ m x → sequ a Bool (λ y → tchar m mono y) (λ _ → true) 189 b→s x | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1
165 bs1 (isImage x) eq = elem (m x) {!!} 190 ... | t = ⊥-elim (t (isImage x))
166 ... | case2 n = ⊥-elim (n (isImage x))
167 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b 191 b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
168 b←s (elem y eq) with lem (image m y) 192 b←s (elem y eq) with tchar m mono y | inspect (tchar m mono ) y
169 ... | case1 (isImage x) = x 193 ... | true | record { eq = eq1 } = img-x m (tcharImg m mono y eq1 )
170 ... | case2 t = ⊥-elim ( ¬f≡t eq ) 194 bs=x : (x : b) → (y : a) → y ≡ m x → (eq : tchar m mono y ≡ true ) → b←s (elem y eq) ≡ x
195 bs=x x y refl t with tcharImg m mono y t
196 ... | t1 = {!!}
197 iso1 : (x : b) → ( Sets [ m o (Sets Category.o b←s) b→s ] ) x ≡ ( Sets [ m o Category.Category.Id Sets ] ) x
198 iso1 x with tchar m mono (m x) | inspect (tchar m mono ) (m x)
199 ... | true | record { eq = eq1 } = begin
200 m ( b←s ( elem (m x) eq1 )) ≡⟨⟩
201 m (img-x m (isImage (b←s ( elem (m x) eq1 )) )) ≡⟨ {!!} ⟩
202 m (img-x m (tcharImg m mono (m x) eq1 ) ) ≡⟨ {!!} ⟩
203 m (img-x m (isImage x) ) ≡⟨⟩
204 m x ∎ where open ≡-Reasoning
205 iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x))
206 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
207 iso2 (elem y eq) = {!!}
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 ]) 208 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 ])
172 imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) 209 imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono)
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) → 210 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) →
174 tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y 211 tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ 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 212 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
176 ... | true | case1 x | record { eq = eq1 } = eq1 213 ... | true | record { eq = eqhy } | case1 x | record { eq = eq1 } = eq1
177 ... | true | case2 x | record { eq = eq1 } = {!!} 214 ... | true | record { eq = eqhy } | case2 x | record { eq = eq1 } = ⊥-elim (x (isImage (elem y eqhy)))
178 ... | false | case1 (isImage (elem x eq)) | record { eq = eq1 } = {!!} 215 ... | false | record { eq = eqhy } | case1 (isImage (elem x eq)) | record { eq = eq1 } = ⊥-elim ( ¬x≡t∧x≡f record {fst = eqhy ; snd = eq })
179 ... | false | case2 x | record { eq = eq1 } = eq1 216 ... | false | record { eq = eqhy } | case2 x | record { eq = eq1 } = eq1
180 217
181 218
182 open import graph 219 open import graph
183 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where 220 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where
184 221