Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 554:9e6aa4d77c3e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equ version on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 09 Apr 2017 20:24:42 +0900
parents e33282817cb7
children 91d065bcfdc0
comparison
equal deleted inserted replaced
553:e33282817cb7 554:9e6aa4d77c3e
158 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f 158 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f
159 -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } → (x≈y : C [ x ≈ y ] ) → x ≡ y 159 -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } → (x≈y : C [ x ≈ y ] ) → x ≡ y
160 160
161 open Small 161 open Small
162 162
163 ≡cong2 : { c c' : Level } { A B : Set c } { C : Set c' } { a a' : A } { b b' : B } ( f : A → B → C )
164 → a ≡ a'
165 → b ≡ b'
166 → f a b ≡ f a' b'
167 ≡cong2 _ refl refl = refl
168
163 ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) 169 ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
164 (i : Obj C ) →　 Set c₁ 170 (i : Obj C ) →　 Set c₁
165 ΓObj s Γ i = FObj Γ i 171 ΓObj s Γ i = FObj Γ i
166 172
167 ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) 173 ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
168 {i j : Obj C } →　 ( f : I → I ) → ΓObj s Γ i → ΓObj s Γ j 174 {i j : Obj C } →　 ( f : I → I ) → ΓObj s Γ i → ΓObj s Γ j
169 ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f ) 175 ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f )
170 176
171 record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I )→ sobj i → sobj j ) 177 record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I )→ sobj i → sobj j )
172 ( snequ : { i j : OC } → sequ (sobj i) (sobj j) ( smap (λ x → x ) ) ( smap (λ x → x ) ) )
173 : Set c₂ where 178 : Set c₂ where
174 field 179 field
175 snmap : ( i : OC ) → sobj i 180 snmap : ( i : OC ) → sobj i
176 sncommute : { i j : OC } → ( f : I → I ) → smap f ( snmap i ) ≡ snmap j 181 snequ : { i j : OC } → ( f : I → I ) → sequ (sobj i) (sobj j) ( λ x → smap f ( snmap i ) ) ( λ x → snmap j )
177 182
178 open snat 183 open snat
179 184
180 open import HomReasoning 185 open import HomReasoning
181 open NTrans 186 open NTrans
182
183 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 187 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
184 ( Cequ : { i j : Obj C} → sequ (ΓObj s Γ i) (ΓObj s Γ j) ( ΓMap s Γ (λ x → x ) ) ( ΓMap s Γ (λ x → x ) ) ) 188 → NTrans C Sets (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) Γ
185 → NTrans C Sets (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) Cequ ) ) Γ 189 Cone C I s Γ = record {
186 Cone C I s Γ cequ = record { 190 TMap = λ i → λ sn → snmap sn i
187 TMap = λ i → λ sn → snmap sn i
188 ; isNTrans = record { commute = comm1 } 191 ; isNTrans = record { commute = comm1 }
189 } where 192 } where
190 comm1 : {a b : Obj C} {f : Hom C a b} → 193 comm1 : {a b : Obj C} {f : Hom C a b} →
191 Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ 194 Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈
192 Sets [ (λ sn → (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) cequ )) f ] ] 195 Sets [ (λ sn → (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
193 comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin 196 comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin
194 FMap Γ f (snmap sn a ) 197 FMap Γ f (snmap sn a )
195 ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( hom-iso s )) ⟩ 198 ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( hom-iso s )) ⟩
196 FMap Γ ( hom← s ( hom→ s f)) (snmap sn a ) 199 FMap Γ ( hom← s ( hom→ s f)) (snmap sn a )
197 ≡⟨⟩ 200 ≡⟨⟩
198 ΓMap s Γ (hom→ s f) (snmap sn a ) 201 ΓMap s Γ (hom→ s f) (snmap sn a )
199 ≡⟨ sncommute sn (hom→ s f) ⟩ 202 ≡⟨ fe=ge0 (snequ sn (hom→ s f)) ⟩
200 snmap sn b 203 snmap sn b
201 ∎ ) where 204 ∎ ) where
202 open import Relation.Binary.PropositionalEquality 205 open import Relation.Binary.PropositionalEquality
203 open ≡-Reasoning 206 open ≡-Reasoning
204
205 207
206 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 208 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
207 → Limit Sets C Γ 209 → Limit Sets C Γ
208 SetsLimit { c₂} C I s Γ = record { 210 SetsLimit { c₂} C I s Γ = record {
209 a0 = snat (ΓObj s Γ) (ΓMap s Γ) (elem ? refl ) 211 a0 = snat (ΓObj s Γ) (ΓMap s Γ)
210 ; t0 = Cone C I s Γ {!!} 212 ; t0 = Cone C I s Γ
211 ; isLimit = record { 213 ; isLimit = record {
212 limit = limit1 214 limit = limit1
213 ; t0f=t = λ {a t i } → t0f=t {a} {t} {i} 215 ; t0f=t = λ {a t i } → t0f=t {a} {t} {i}
214 ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i} 216 ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i}
215 } 217 }
216 } where 218 } where
219 snat-cong : { snat tnat : snat (ΓObj s Γ) (ΓMap s Γ) }
220 → (( i : Obj C ) → snmap snat i ≡ snmap tnat i )
221 → ( ( i j : Obj C ) ( f : I → I ) → ΓMap s Γ f ( snmap snat i ) ≡ snmap snat j )
222 → ( ( i j : Obj C ) ( f : I → I ) → ΓMap s Γ f ( snmap tnat i ) ≡ snmap tnat j )
223 → snat ≡ tnat
224 snat-cong {s} {t} eq1 eq2 eq3 = begin
225 record { snmap = λ i → snmap s i ; snequ = {!!} }
226 ≡⟨
227 ≡cong2 ( λ x y →
228 record { snmap = λ i → x i ; snequ = {!!} } ) ( extensionality Sets ( λ i → {!!} ) )
229 ( extensionality Sets ( λ x →
230 ( extensionality Sets ( λ i →
231 ( extensionality Sets ( λ j →
232 ( extensionality Sets ( λ f → {!!}
233 ))))))))
234 ⟩
235 record { snmap = {!!} ; snequ = {!!} }
236 ≡⟨ {!!} ⟩
237 record { snmap = λ i → snmap t i ; snequ = {!!} }
238 ∎ where
239 open import Relation.Binary.PropositionalEquality
240 open ≡-Reasoning
217 a0 : Obj Sets 241 a0 : Obj Sets
218 a0 = snat (ΓObj s Γ) (ΓMap s Γ) ( λ {i j } → elem {!!} refl ) 242 a0 = snat (ΓObj s Γ) (ΓMap s Γ)
219 comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 243 comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I )
220 → ΓMap s Γ f (TMap t i x) ≡ TMap t j x 244 → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
221 comm2 {a} {x} t f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ) 245 comm2 {a} {x} t f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
222 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ) {!!}) 246 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))
223 limit1 a t = λ x → record { 247 limit1 a t = λ ( x : a ) → record {
224 snmap = λ i → ( TMap t i ) x 248 snmap = λ i → ( TMap t i ) x
225 ; sncommute = λ f → comm2 t f } 249 ; snequ = λ {i} {j} f → elem (TMap t i x) (comm2 t f ) }
226 t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ {!!}) i o limit1 a t ] ≈ TMap t i ] 250 t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o limit1 a t ] ≈ TMap t i ]
227 t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin 251 t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin
228 ( Sets [ TMap (Cone C I s Γ {!!}) i o limit1 a t ]) x 252 ( Sets [ TMap (Cone C I s Γ ) i o limit1 a t ]) x
229 -- ≡⟨⟩ 253 -- ≡⟨⟩
230 -- snmap ( record { snmap = λ i → ( TMap t i ) x ; sncommute = λ {i j} f → comm2 {a} {x} {i} {j} t f } ) i 254 -- snmap ( record { snmap = λ i → ( TMap t i ) x ; sncommute = λ {i j} f → comm2 {a} {x} {i} {j} t f } ) i
231 ≡⟨⟩ 255 ≡⟨⟩
232 TMap t i x 256 TMap t i x
233 ∎ ) where 257 ∎ ) where
234 open import Relation.Binary.PropositionalEquality 258 open import Relation.Binary.PropositionalEquality
235 open ≡-Reasoning 259 open ≡-Reasoning
236 limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ) {!!} )} → 260 limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ) )} →
237 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ {!!}) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] 261 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
238 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin 262 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin
239 limit1 a t x 263 limit1 a t x
240 ≡⟨⟩ 264 ≡⟨⟩
241 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ f → comm2 t f } 265 record { snmap = λ i → ( TMap t i ) x ; snequ = λ {i} {j} f → elem (TMap t i x) (comm2 t f ) }
242 ≡⟨ {!!} (ΓObj s Γ) (ΓMap s Γ) {!!} {!!} {!!} ⟩ 266 ≡⟨ snat-cong {!!} {!!} {!!} ⟩
243 record { snmap = λ i → snmap (f x ) i ; sncommute = sncommute (f x ) } 267 record { snmap = λ i → snmap (f x ) i ; snequ = snequ (f x) }
244 ≡⟨⟩ 268 ≡⟨⟩
245 f x 269 f x
246 ∎ ) where 270 ∎ ) where
247 open import Relation.Binary.PropositionalEquality 271 open import Relation.Binary.PropositionalEquality
248 open ≡-Reasoning 272 open ≡-Reasoning
249 273
250