Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 691:917e51be9bbf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
change argument of Limit and K
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Nov 2017 09:56:40 +0900
parents bd8f7346f252
children 984518c56e96
comparison
equal deleted inserted replaced
690:3d41a8edbf63 691:917e51be9bbf
50 pi1 : ( i : I ) → pi0 i 50 pi1 : ( i : I ) → pi0 i
51 51
52 open iproduct 52 open iproduct
53 53
54 SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) 54 SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets )
55 → IProduct ( Sets { c₂} ) I ai 55 → IProduct I ( Sets { c₂} ) ai
56 SetsIProduct I fi = record { 56 SetsIProduct I fi = record {
57 iprod = iproduct I fi 57 iprod = iproduct I fi
58 ; pi = λ i prod → pi1 prod i 58 ; pi = λ i prod → pi1 prod i
59 ; isIProduct = record { 59 ; isIProduct = record {
60 iproduct = iproduct1 60 iproduct = iproduct1
191 191
192 open import HomReasoning 192 open import HomReasoning
193 open NTrans 193 open NTrans
194 194
195 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 195 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
196 → NTrans C Sets (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ 196 → NTrans C Sets (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ
197 Cone C I s Γ = record { 197 Cone C I s Γ = record {
198 TMap = λ i → λ sn → snmap sn i 198 TMap = λ i → λ sn → snmap sn i
199 ; isNTrans = record { commute = comm1 } 199 ; isNTrans = record { commute = comm1 }
200 } where 200 } where
201 comm1 : {a b : Obj C} {f : Hom C a b} → 201 comm1 : {a b : Obj C} {f : Hom C a b} →
202 Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ 202 Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈
203 Sets [ (λ sn → (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] 203 Sets [ (λ sn → (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
204 comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin 204 comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin
205 FMap Γ f (snmap sn a ) 205 FMap Γ f (snmap sn a )
206 ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( hom-iso s )) ⟩ 206 ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( hom-iso s )) ⟩
207 FMap Γ ( hom← s ( hom→ s f)) (snmap sn a ) 207 FMap Γ ( hom← s ( hom→ s f)) (snmap sn a )
208 ≡⟨⟩ 208 ≡⟨⟩
212 ∎ ) where 212 ∎ ) where
213 open import Relation.Binary.PropositionalEquality 213 open import Relation.Binary.PropositionalEquality
214 open ≡-Reasoning 214 open ≡-Reasoning
215 215
216 216
217 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 217 SetsLimit : { c₁ c₂ ℓ : Level} ( I : Set c₁ ) ( C : Category c₁ c₂ ℓ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
218 → Limit Sets C Γ 218 → Limit C Sets Γ
219 SetsLimit {c₁} C I s Γ = record { 219 SetsLimit {c₁} I C s Γ = record {
220 a0 = snat (ΓObj s Γ) (ΓMap s Γ) 220 a0 = snat (ΓObj s Γ) (ΓMap s Γ)
221 ; t0 = Cone C I s Γ 221 ; t0 = Cone C I s Γ
222 ; isLimit = record { 222 ; isLimit = record {
223 limit = limit1 223 limit = limit1
224 ; t0f=t = λ {a t i } → t0f=t {a} {t} {i} 224 ; t0f=t = λ {a t i } → t0f=t {a} {t} {i}
225 ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i} 225 ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i}
226 } 226 }
227 } where 227 } where
228 comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I) 228 comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K C Sets a) Γ) (f : I)
229 → ΓMap s Γ f (TMap t i x) ≡ TMap t j x 229 → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
230 comm2 {a} {x} t f = ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) ) 230 comm2 {a} {x} t f = ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) )
231 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) 231 limit1 : (a : Obj Sets) → NTrans C Sets (K C Sets a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))
232 limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ; 232 limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ;
233 sncommute = λ i j f → comm2 t f } 233 sncommute = λ i j f → comm2 t f }
234 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 ] 234 t0f=t : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ]
235 t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin 235 t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin
236 ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x 236 ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x
237 ≡⟨⟩ 237 ≡⟨⟩
238 TMap t i x 238 TMap t i x
239 ∎ ) where 239 ∎ ) where
240 open import Relation.Binary.PropositionalEquality 240 open import Relation.Binary.PropositionalEquality
241 open ≡-Reasoning 241 open ≡-Reasoning
242 limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} → 242 limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} →
243 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] 243 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
244 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin 244 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin
245 limit1 a t x 245 limit1 a t x
246 ≡⟨⟩ 246 ≡⟨⟩
247 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ i j f → comm2 t f } 247 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ i j f → comm2 t f }
275 open IsLimit 275 open IsLimit
276 open IProduct 276 open IProduct
277 277
278 SetsCompleteness : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) → Complete (Sets {c₁}) C 278 SetsCompleteness : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) → Complete (Sets {c₁}) C
279 SetsCompleteness {c₁} {c₂} C I s = record { 279 SetsCompleteness {c₁} {c₂} C I s = record {
280 climit = λ Γ → SetsLimit {c₁} C I s Γ 280 climit = λ Γ → SetsLimit {c₁} I C s Γ
281 ; cequalizer = λ {a} {b} f g → record { equalizer-c = sequ a b f g ; 281 ; cequalizer = λ {a} {b} f g → record { equalizer-c = sequ a b f g ;
282 equalizer = ( λ e → equ e ) ; 282 equalizer = ( λ e → equ e ) ;
283 isEqualizer = SetsIsEqualizer a b f g } 283 isEqualizer = SetsIsEqualizer a b f g }
284 ; cproduct = λ J fi → SetsIProduct J fi 284 ; cproduct = λ J fi → SetsIProduct J fi
285 } where 285 } where