Mercurial > hg > Members > kono > Proof > category
changeset 514:1fca61019bdf
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 21 Mar 2017 10:14:04 +0900 |
| parents | e73c3e73a87b |
| children | 221dd46ded35 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 7 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Tue Mar 21 09:38:57 2017 +0900 +++ b/SetsCompleteness.agda Tue Mar 21 10:14:04 2017 +0900 @@ -91,7 +91,7 @@ -- | . g -- |k . -- | . h - -- d + --y : d data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where @@ -122,8 +122,8 @@ ek=h {d} {h} {eq} = refl fhy=ghy : (d : Obj Sets ) ( h : Hom Sets d a ) (y : d ) → (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]) → f (h y) ≡ g (h y) fhy=ghy d h y fh=gh = cong ( λ f → f y ) fh=gh - fuga : {d : Obj Sets} { y : d } { k' : Hom Sets d (sequ a b f g)} → Hom Sets a {!!} - fuga = {!!} + fuga : (x : a ) → { fx=gx : f x ≡ g x } → sequ a b f g + fuga x { fx=gx } = elem x fx=gx repl : {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)} → ( y : d ) → Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → k h fh=gh y ≡ k' y repl {d} {h} {fh=gh} {k'} y ek'=h = @@ -131,10 +131,10 @@ k h fh=gh y ≡⟨⟩ elem (h y) (fhy=ghy d h y fh=gh ) - ≡⟨ {!!} ⟩ - fuga (h y ) - ≡⟨ sym ( Category.cong (λ f → fuga (f y ) ) ek'=h ) ⟩ - fuga ( ( λ e → equ e ) ( k' y ) ) + ≡⟨⟩ + fuga (h y ) {fhy=ghy d h y fh=gh } + ≡⟨ sym ( Category.cong (λ f → fuga (f y ) ) ek'=h ) ⟩ + fuga ( ( λ e → equ e ) ( k' y ) ) {?} ≡⟨⟩ ( λ e → fuga ( equ e )) ( k' y ) ≡⟨ {!!} ⟩