Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 608:7194ba55df56

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
freyd2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 12 Jun 2017 10:50:02 +0900
parents caab94e897e6
children 855e497a9c8f
comparison
equal deleted inserted replaced
607:caab94e897e6 608:7194ba55df56
173 smap0 : { i j : OC } → (f : I ) → sobj i → sobj j 173 smap0 : { i j : OC } → (f : I ) → sobj i → sobj j
174 smap0 {i} {j} f x = smap f x 174 smap0 {i} {j} f x = smap f x
175 175
176 open snat 176 open snat
177 177
178 ≡cong2 : { c c' : Level } { A B : Set c } { C : Set c' } { a a' : A } { b b' : B } ( f : A → B → C )
179 → a ≡ a'
180 → b ≡ b'
181 → f a b ≡ f a' b'
182 ≡cong2 _ refl refl = refl
183
184 open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' )
185
178 snat-cong : { c : Level } { I OC : Set c } { SObj : OC → Set c } { SMap : { i j : OC } → (f : I )→ SObj i → SObj j } 186 snat-cong : { c : Level } { I OC : Set c } { SObj : OC → Set c } { SMap : { i j : OC } → (f : I )→ SObj i → SObj j }
179 ( s t : snat SObj SMap ) 187 ( s t : snat SObj SMap )
180 → ( ( λ i → snmap s i ) ≡ ( λ i → snmap t i ) ) 188 → ( ( λ i → snmap s i ) ≡ ( λ i → snmap t i ) )
181 → ( ( λ i j f → smap0 s f ( snmap s i ) ≡ snmap s j ) ≡ ( ( λ i j f → smap0 t f ( snmap t i ) ≡ snmap t j ) ) ) 189 → ( ( λ i j f → smap0 s f ( snmap s i ) ≡ snmap s j ) ≡ ( ( λ i j f → smap0 t f ( snmap t i ) ≡ snmap t j ) ) )
182 → s ≡ t 190 → s ≡ t
183 snat-cong s t refl refl = {!!} 191 snat-cong s t refl refl = {!!}
184 192
185 open import HomReasoning 193 open import HomReasoning
186 open NTrans 194 open NTrans
236 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] 244 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
237 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin 245 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin
238 limit1 a t x 246 limit1 a t x
239 ≡⟨⟩ 247 ≡⟨⟩
240 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ i j f → comm2 t f } 248 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ i j f → comm2 t f }
241 ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets ( λ i → eq1 x i )) (eq2 x ) ⟩ 249 ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets ( λ i → eq1 x i )) {!!} ⟩
242 record { snmap = λ i → snmap (f x ) i ; sncommute = λ i j f' → sncommute (f x ) i j f' } 250 record { snmap = λ i → snmap (f x ) i ; sncommute = λ i j f' → sncommute (f x ) i j f' }
243 ≡⟨⟩ 251 ≡⟨⟩
244 f x 252 f x
245 ∎ ) where 253 ∎ ) where
246 open import Relation.Binary.PropositionalEquality 254 open import Relation.Binary.PropositionalEquality