Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 525:cb35d6b25559

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Mar 2017 10:18:08 +0900
parents d6739779b4ac
children b035cd3be525
comparison
equal deleted inserted replaced
524:d6739779b4ac 525:cb35d6b25559
132 lemma5 : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → 132 lemma5 : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
133 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x) 133 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x)
134 lemma5 refl x = refl -- somehow this is not equal to lemma1 134 lemma5 refl x = refl -- somehow this is not equal to lemma1
135 uniqueness : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → 135 uniqueness : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
136 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] 136 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ]
137 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → 137 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → begin
138 elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ) 138 k h fh=gh x
139 ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩
140 k' x
141 ∎ ) where
142 open import Relation.Binary.PropositionalEquality
143 open ≡-Reasoning
144
139 145
140 open Functor 146 open Functor
141 open NTrans 147 open NTrans
142 148
143 record ΓObj { c₂ } ( I : Set c₂ ) : Set c₂ where 149 record ΓObj { c₂ } ( I : Set c₂ ) : Set c₂ where
163 cong1 : {A B : Obj Sets} {f g : Hom Sets A B} → Sets [ f ≈ g ] → Sets [ map (fmap f) ≈ map (fmap g) ] 169 cong1 : {A B : Obj Sets} {f g : Hom Sets A B} → Sets [ f ≈ g ] → Sets [ map (fmap f) ≈ map (fmap g) ]
164 cong1 refl = refl 170 cong1 refl = refl
165 171
166 open IProduct 172 open IProduct
167 173
174 record slim { c₂ } ( sobj : Set c₂ → Set c₂ ) ( smap : { a b : Set c₂ } ( f : a → b ) → Set c₂ ) : Set c₂ where
175
168 SetsLimit : { c₂ : Level} → Limit Sets Sets Γ 176 SetsLimit : { c₂ : Level} → Limit Sets Sets Γ
169 SetsLimit { c₂} = record { 177 SetsLimit { c₂} = record {
170 a0 = {!!} 178 a0 = slim ΓObj ΓMap
171 ; t0 = record { 179 ; t0 = record {
172 TMap = λ i → Sets [ proj i o e i ] 180 TMap = λ i → Sets [ proj i o e i ]
173 ; isNTrans = record { commute = {!!} } 181 ; isNTrans = record { commute = {!!} }
174 } 182 }
175 ; isLimit = record { 183 ; isLimit = record {
178 ; limit-uniqueness = {!!} 186 ; limit-uniqueness = {!!}
179 } 187 }
180 } where 188 } where
181 eqa : {i j : Obj Sets} (f : Hom Sets i j) → sequ (Obj Sets) (Obj Sets) {!!} {!!} -- {!!} {!!} (FMap Γ f o proj i) ( proj j ) 189 eqa : {i j : Obj Sets} (f : Hom Sets i j) → sequ (Obj Sets) (Obj Sets) {!!} {!!} -- {!!} {!!} (FMap Γ f o proj i) ( proj j )
182 eqa f = {!!} 190 eqa f = {!!}
183 e : (i : Obj Sets) → Hom Sets (FObj (K Sets Sets ( sequ {!!} {!!} {!!} {!!} )) i ) (iproduct (Obj Sets) (λ I → ΓObj (Obj Sets))) 191 e : (i : Obj Sets) → Hom Sets (FObj (K Sets Sets (slim ΓObj ΓMap)) i ) (iproduct (slim ΓObj ΓMap) (λ I → ΓObj (slim ΓObj ΓMap)))
184 e i = λ x → record { pi1 = λ i → record { obj = sequ ? {!!} {!!} {!!} } } 192 e i = λ x → record { pi1 = λ j → record { obj = record {}} }
185 proj : (i : Obj Sets) → ( prod : iproduct (Obj Sets) (λ i → ΓObj (Obj Sets) )) → FObj Γ i 193 proj : (i : Obj Sets) → ( prod : iproduct (slim ΓObj ΓMap) (λ i → ΓObj (slim ΓObj ΓMap))) → FObj Γ i
186 proj i prod = record { obj = {!!} } 194 proj i prod = record { obj = ? }
187 comm1 : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → {!!} ) ] ≈ 195 comm1 : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → {!!} ) ] ≈
188 Sets [ (λ lim → {!!}) o FMap (K Sets Sets {!!}) f ] ] 196 Sets [ (λ lim → {!!}) o FMap (K Sets Sets {!!}) f ] ]
189 comm1 {a} {b} {f} = {!!} 197 comm1 {a} {b} {f} = {!!}