Mercurial > hg > Members > kono > Proof > category
changeset 515:221dd46ded35
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 21 Mar 2017 13:18:52 +0900 |
| parents | 1fca61019bdf |
| children | 327dc7372729 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 10 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Tue Mar 21 10:14:04 2017 +0900 +++ b/SetsCompleteness.agda Tue Mar 21 13:18:52 2017 +0900 @@ -124,6 +124,8 @@ fhy=ghy d h y fh=gh = cong ( λ f → f y ) fh=gh fuga : (x : a ) → { fx=gx : f x ≡ g x } → sequ a b f g fuga x { fx=gx } = elem x fx=gx + hoge : sequ a b f g → sequ a b f g + hoge ( elem x eq ) = elem x eq 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 = @@ -133,11 +135,17 @@ elem (h y) (fhy=ghy d h y fh=gh ) ≡⟨⟩ 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 ) ) {?} + ≡⟨ sym ( Category.cong (λ f → fuga (f y ) ) ek'=h ) ⟩ + fuga ( ( λ e → equ e ) ( k' y ) ) {fe=ge0 (k' y)} ≡⟨⟩ ( λ e → fuga ( equ e )) ( k' y ) + ≡⟨⟩ + ( λ e → elem (equ e) (fe=ge0 e )) ( k' y ) ≡⟨ {!!} ⟩ + hoge ( k' y ) + ≡⟨ {!!} ⟩ + ( λ e → e ) ( k' y ) + ≡⟨⟩ k' y ∎ where