Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 589:6584db867bd0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 May 2017 09:55:10 +0900
parents 11b5eeb4a9e7
children 2c5d8c3c9086
comparison
equal deleted inserted replaced
588:11b5eeb4a9e7 589:6584db867bd0
179 record slim { c₂ } { I OC : Set c₂ } 179 record slim { c₂ } { I OC : Set c₂ }
180 ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I ) → sobj i → sobj j ) 180 ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I ) → sobj i → sobj j )
181 : Set c₂ where 181 : Set c₂ where
182 field 182 field
183 slequ : (i j : OC) (f : I → I ) → sequ (sproduct OC sobj) (sobj j) (λ x → smap f (proj x i) ) (λ x → proj x j ) 183 slequ : (i j : OC) (f : I → I ) → sequ (sproduct OC sobj) (sobj j) (λ x → smap f (proj x i) ) (λ x → proj x j )
184 slprod : sproduct OC sobj 184 slprod : {i : OC } → sproduct OC sobj
185 slprod {i} = equ ( slequ i i slid )
185 186
186 open slim 187 open slim
187 188
188 open import HomReasoning 189 open import HomReasoning
189 open NTrans 190 open NTrans
190 191
191 cone-equ : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 192 cone-equ : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
192 → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) 193 → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) )
193 → sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (FObj Γ b) (λ x → FMap Γ (hom← s f) (proj (slprod x) a) ) (λ x → proj (slprod x) b ) 194 → sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (FObj Γ b) (λ x → FMap Γ (hom← s f) (proj (slprod x {a}) a) ) (λ x → proj (slprod x {b}) b )
194 cone-equ C I s Γ a b f se = elem se {!!} -- (( fe=ge0 (slequ se a b f )) ) 195 cone-equ C I s Γ a b f se = elem se {!!} -- (( fe=ge0 (slequ se a b f )) )
196
197 cone-equ' : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
198 → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) )
199 → FMap Γ (hom← s f) (proj (equ (slequ se a b f )) a) ≡ proj (equ (slequ se a b f)) b
200 cone-equ' C I s Γ a b f se = fe=ge0 (slequ se a b f )
195 201
196 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 202 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
197 → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ))) Γ 203 → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ))) Γ
198 Cone C I s Γ = record { 204 Cone C I s Γ = record {
199 TMap = λ i → λ se → proj ( equ {_} { sproduct (Obj C) (ΓObj s Γ)} {FObj Γ i} 205 TMap = λ i → λ se → proj ( equ {_} { sproduct (Obj C) (ΓObj s Γ)} {FObj Γ i}
201 ; isNTrans = record { commute = commute1 } 207 ; isNTrans = record { commute = commute1 }
202 } where 208 } where
203 commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (slprod se) a) ] 209 commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (slprod se) a) ]
204 ≈ Sets [ (λ se → proj (slprod se) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ] 210 ≈ Sets [ (λ se → proj (slprod se) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
205 commute1 {a} {b} {f} = extensionality Sets ( λ se → begin 211 commute1 {a} {b} {f} = extensionality Sets ( λ se → begin
206 (Sets [ FMap Γ f o (λ se → proj (slprod se) a) ]) se 212 (Sets [ FMap Γ f o (λ se → proj (slprod se {a}) a) ]) se
207 ≡⟨⟩ 213 ≡⟨⟩
208 FMap Γ f (proj (slprod se) a ) 214 FMap Γ f (proj (slprod se) a )
209 ≡⟨ ≡cong ( λ g → FMap Γ g (proj (slprod se) a)) (sym ( hom-iso s ) ) ⟩ 215 ≡⟨ ≡cong ( λ g → FMap Γ g (proj (slprod se) a)) (sym ( hom-iso s ) ) ⟩
210 FMap Γ (hom← s ( hom→ s f)) (proj (slprod se) a) 216 FMap Γ (hom← s ( hom→ s f)) (proj (slprod se {a}) a)
211 ≡⟨ fe=ge0 (cone-equ C I s Γ a b ( hom→ s f) se ) ⟩ 217 ≡⟨ fe=ge0 (cone-equ C I s Γ a b ( hom→ s f) se ) ⟩
212 proj (slprod se) b 218 proj (slprod se {b}) b
213 ≡⟨⟩ 219 ≡⟨⟩
214 (Sets [ (λ se → proj (slprod se) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se 220 (Sets [ (λ se → proj (slprod se {b}) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
215 ∎ ) where 221 ∎ ) where
216 open import Relation.Binary.PropositionalEquality 222 open import Relation.Binary.PropositionalEquality
217 open ≡-Reasoning 223 open ≡-Reasoning
218 224
219 225
235 iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) ( begin 241 iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) ( begin
236 (λ x₁ → ΓMap s Γ f (proj x₁ i)) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) 242 (λ x₁ → ΓMap s Γ f (proj x₁ i)) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x)
237 ≈⟨ car (nat t) ⟩ 243 ≈⟨ car (nat t) ⟩
238 (λ x₁ → proj x₁ j) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) 244 (λ x₁ → proj x₁ j) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x)
239 ∎ 245 ∎
240 ) x 246 ) x }
241 ; slprod = record { proj = λ i → TMap t i x } }
242 where open ≈-Reasoning (Sets { c₂}) 247 where open ≈-Reasoning (Sets { c₂})