Mercurial > hg > Members > kono > Proof > category

comparison src/CCCSets.agda @ 1021:8a78ddfdaa24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... use LEM for Topos Sets
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Mar 2021 13:17:37 +0900
parents d7e89e26700e
children 2f7e4ad86fc6
comparison
equal deleted inserted replaced
1020:d7e89e26700e 1021:8a78ddfdaa24
123 record Char {c : Level } {a b : Obj (Sets {c})} (m : Hom Sets b a) (mono : Mono Sets m) : Set c where 123 record Char {c : Level } {a b : Obj (Sets {c})} (m : Hom Sets b a) (mono : Mono Sets m) : Set c where
124 field 124 field
125 cb : b 125 cb : b
126 cl : (y : a) → m cb ≡ y 126 cl : (y : a) → m cb ≡ y
127 127
128 topos : {c : Level } → ( {a b : Obj (Sets {c})} (m : Hom Sets b a) (mono : Mono Sets m) → Dec (Char m mono )) → Topos (Sets {c}) sets 128 data _∨_ {c : Level } (a b : Set c) : Set c where
129 topos {c} dec = record { 129 case1 : a → a ∨ b
130 case2 : b → a ∨ b
131
132 record Choice {c : Level } (b : Set c) : Set c where
133 field
134 choice : ¬ (¬ b ) → b
135
136 lem2choice : {c : Level } → {b : Set c} → b ∨ (¬ b) → Choice b
137 lem2choice {c} {b} lem with lem
138 ... | case1 x = record { choice = λ y → x }
139 ... | case2 x = record { choice = λ y → ⊥-elim (y x ) }
140
141 topos : {c : Level } → ( (b : Set c) → b ∨ (¬ b)) → Topos (Sets {c}) sets
142 topos {c} lem = record {
130 Ω = CL {c} 143 Ω = CL {c}
131 ; ⊤ = λ _ → c1 ! 144 ; ⊤ = λ _ → c1 !
132 ; Ker = tker 145 ; Ker = tker
133 ; char = λ m mono → tchar m mono 146 ; char = λ m mono → tchar m mono
134 ; isTopos = record { 147 ; isTopos = record {
145 tchar {a} {b} m mono x = c1 ! 158 tchar {a} {b} m mono x = c1 !
146 selem : {a : Obj (Sets {c})} → (x : sequ a CL (λ x₁ → c1 !) (λ _ → c1 ! )) → a 159 selem : {a : Obj (Sets {c})} → (x : sequ a CL (λ x₁ → c1 !) (λ _ → c1 ! )) → a
147 selem (elem x eq) = x 160 selem (elem x eq) = x
148 k-tker : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → Hom Sets b (b /\ sequ a CL (tchar m mono) (λ _ → c1 ! )) 161 k-tker : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → Hom Sets b (b /\ sequ a CL (tchar m mono) (λ _ → c1 ! ))
149 k-tker {a} {b} m mono x = record { fst = x ; snd = elem (m x) refl } 162 k-tker {a} {b} m mono x = record { fst = x ; snd = elem (m x) refl }
150 bb : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → Iso Sets b (b /\ sequ a CL (tchar m mono) (λ _ → c1 !)) 163 kr : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → Hom Sets (b /\ sequ a CL (tchar m mono) (λ _ → c1 ! )) b
151 bb {a} {b} m mono = record { ≅→ = λ x → record { fst = x ; snd = elem (m x) refl } ; ≅← = proj₁ ; iso→ = extensionality Sets ( λ x → refl ) 164 kr {a} {b} m mono = proj₁
152 ; iso← = {!!} } where
153 bb1 : (x : b /\ sequ a CL (tchar m mono) (λ _ → c1 !) ) → elem (m (proj₁ x)) refl ≡ proj₂ x
154 bb1 (x , elem y eq) = {!!}
155 ss : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → Iso Sets (b /\ sequ a CL (tchar m mono) (λ _ → c1 !)) (sequ a CL (tchar m mono) (λ _ → c1 !))
156 ss {a} {b} m mono = record { ≅→ = λ x → elem (m (proj₁ x)) refl ; ≅← = ss1 ; iso→ = extensionality Sets ( λ x → {!!} )
157 ; iso← = extensionality Sets ( λ x → {!!} ) } where
158 ss1 : Hom Sets (sequ a CL (tchar m mono) (λ _ → c1 !)) (b /\ sequ a CL (tchar m mono) (λ _ → c1 !))
159 ss1 (elem x eq) = record { fst = {!!} ; snd = elem x eq }
160 imequ : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → c1 ! ) o CCC.○ sets a ]) 165 imequ : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → c1 ! ) o CCC.○ sets a ])
161 imequ {a} {b} m mono = record { 166 imequ {a} {b} m mono with lem b
167 ... | case2 n = record {
162 fe=ge = extensionality Sets ( λ x → refl ) 168 fe=ge = extensionality Sets ( λ x → refl )
163 ; k = {!!} -- λ h eq y → proj₁ (k-tker {!!} {!!} {!!} ) 169 ; k = λ h eq y → ?
170 ; ek=h = {!!}
171 ; uniqueness = {!!}
172 }
173 ... | case1 x = record {
174 fe=ge = extensionality Sets ( λ x → refl )
175 ; k = λ h eq y → proj₁ (k-tker m mono x )
164 ; ek=h = {!!} 176 ; ek=h = {!!}
165 ; uniqueness = {!!} 177 ; uniqueness = {!!}
166 } 178 }
167 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a CL) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → c1 ! ≡ h x 179 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a CL) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → c1 ! ≡ h x
168 uniq {a} {b} h m mono x with h x 180 uniq {a} {b} h m mono x with h x