Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 533:c3dcea3a92a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use sequ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 29 Mar 2017 11:59:59 +0900
parents d5d7163f2a1d
children a90889cc2988
comparison
equal deleted inserted replaced
532:d5d7163f2a1d 533:c3dcea3a92a7
100 elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g 100 elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g
101 101
102 equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b f g ) → a 102 equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b f g ) → a
103 equ (elem x eq) = x 103 equ (elem x eq) = x
104 104
105 fe=ge0 : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } →
106 (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
107 fe=ge0 (elem x eq ) = eq
108
105 open sequ 109 open sequ
106 110
107 -- equalizer-c = sequ a b f g 111 -- equalizer-c = sequ a b f g
108 -- ; equalizer = λ e → equ e 112 -- ; equalizer = λ e → equ e
109 113
112 fe=ge = fe=ge 116 fe=ge = fe=ge
113 ; k = k 117 ; k = k
114 ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq} 118 ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq}
115 ; uniqueness = uniqueness 119 ; uniqueness = uniqueness
116 } where 120 } where
117 fe=ge0 : (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
118 fe=ge0 (elem x eq ) = eq
119 fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] 121 fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
120 fe=ge = extensionality Sets (fe=ge0 ) 122 fe=ge = extensionality Sets (fe=ge0 )
121 k : {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g) 123 k : {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
122 k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) eq ) 124 k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) eq )
123 ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e ) o k h eq ] ≈ h ] 125 ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e ) o k h eq ] ≈ h ]
176 open import HomReasoning 178 open import HomReasoning
177 179
178 open NTrans 180 open NTrans
179 open IsEqualizer 181 open IsEqualizer
180 182
183 SetsLimit-c : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) → Obj Sets
184 SetsLimit-c {_} {_} {_} {C} {I} s Γ = sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (iproduct I (λ j → ΓObj s Γ j) ) {!!} {!!}
185
181 SetsNat : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 186 SetsNat : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
182 → NTrans C Sets (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ)) ) Γ 187 → NTrans C Sets (K Sets C ( SetsLimit-c s Γ ) ) Γ
183 SetsNat C I s Γ = record { 188 SetsNat C I s Γ = record {
184 TMap = λ i → Sets [ proj i o e ] 189 TMap = λ i → Sets [ proj i o e ]
185 ; isNTrans = record { commute = comm1 } 190 ; isNTrans = record { commute = comm1 }
186 } where 191 } where
187 e : Hom Sets (slim (ΓObj s Γ) (ΓMap s Γ)) (iproduct I (λ j → ΓObj s Γ j)) 192 e : Hom Sets ( SetsLimit-c s Γ ) (iproduct I (λ j → ΓObj s Γ j))
188 e = λ x → record { pi1 = λ j → slim-obj x j } 193 e = λ x → record { pi1 = λ j → slim-obj (equ x) j }
189 iid : {i : Obj C } → Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i) 194 iid : {i : Obj C } → Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i)
190 iid {i} = FMap Γ ( small-iso s ) 195 iid {i} = FMap Γ ( small-iso s )
191 proj : (i : Obj C ) → ( prod : iproduct I (λ j → ΓObj s Γ j )) → FObj Γ i 196 proj : (i : Obj C ) → ( prod : iproduct I (λ j → ΓObj s Γ j )) → FObj Γ i
192 proj i prod = iid ( pi1 prod ( small→ s i ) ) 197 proj i prod = iid ( pi1 prod ( small→ s i ) )
193 equa : {b : Obj Sets } ( e : slim (ΓObj s Γ) (ΓMap s Γ) → iproduct I (λ j → ΓObj s Γ j) ) → ( f g : Hom Sets (iproduct I (λ j → ΓObj s Γ j)) b ) → 198 equa : {b : Obj Sets } ( e : slim (ΓObj s Γ) (ΓMap s Γ) → iproduct I (λ j → ΓObj s Γ j) ) → ( f g : Hom Sets (iproduct I (λ j → ΓObj s Γ j)) b ) →
194 IsEqualizer Sets e f g 199 IsEqualizer Sets e f g
195 equa e f g = {!!} -- SetsIsEqualizer ? ? ? ? 200 equa e f g = {!!} -- SetsIsEqualizer ? ? ? ?
196 comm2 : {a b : Obj C} {f : Hom C a b} → ( x : slim (ΓObj s Γ) (ΓMap s Γ) ) → (Sets [ FMap Γ f o Sets [ proj a o e ] ]) x ≡ (Sets [ proj b o e ]) x
197 comm2 {a} {b} {f} x = begin
198 (FMap Γ f ) ( ( proj a o e ) x )
199 ≡⟨⟩
200 (FMap Γ f ) ( iid ( slim-obj x (small→ s a) ))
201 ≡⟨ {!!} ⟩
202 iid ( slim-obj x ( small→ s b ) )
203 ∎ where
204 open import Relation.Binary.PropositionalEquality
205 open ≡-Reasoning
206 comm1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o Sets [ proj a o e ] ] ≈ 201 comm1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o Sets [ proj a o e ] ] ≈
207 Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ] 202 Sets [ Sets [ proj b o e ] o FMap (K Sets C ( SetsLimit-c s Γ ) ) f ] ]
208 comm1 {a} {b} {f} = begin 203 comm1 {a} {b} {f} = begin
209 Sets [ FMap Γ f o Sets [ proj a o e ] ] 204 Sets [ FMap Γ f o Sets [ proj a o e ] ]
210 ≈⟨ assoc ⟩ 205 ≈⟨ assoc ⟩
211 Sets [ Sets [ FMap Γ f o proj a ] o e ] 206 Sets [ Sets [ FMap Γ f o proj a ] o e ]
212 ≈⟨ fe=ge (equa e ( Sets [ FMap Γ f o proj a ] ) (proj b )) ⟩ 207 ≈⟨ fe=ge0 {!!} ⟩
213 Sets [ proj b o e ] 208 Sets [ proj b o e ]
214 ≈↑⟨ idR ⟩ 209 ≈↑⟨ idR ⟩
215 Sets [ Sets [ proj b o e ] o id1 Sets (slim (ΓObj s Γ) (ΓMap s Γ)) ] 210 Sets [ Sets [ proj b o e ] o id1 Sets ( SetsLimit-c s Γ) ]
216 ≈⟨⟩ 211 ≈⟨⟩
217 Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] 212 Sets [ Sets [ proj b o e ] o FMap (K Sets C (SetsLimit-c s Γ)) f ]
218 ∎ where 213 ∎ where
219 open ≈-Reasoning Sets 214 open ≈-Reasoning Sets
220 215
221 216
222 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 217 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
223 → Limit Sets C Γ 218 → Limit Sets C Γ
224 SetsLimit { c₂} C I s Γ = record { 219 SetsLimit { c₂} C I s Γ = record {
225 a0 = slim (ΓObj s Γ) (ΓMap s Γ) 220 a0 = slim (ΓObj s Γ) (ΓMap s Γ)
226 ; t0 = SetsNat C I s Γ 221 ; t0 = {!!} -- SetsNat C I s Γ
227 ; isLimit = record { 222 ; isLimit = record {
228 limit = limit1 223 limit = limit1
229 ; t0f=t = {!!} 224 ; t0f=t = {!!}
230 ; limit-uniqueness = {!!} 225 ; limit-uniqueness = {!!}
231 } 226 }