Mercurial > hg > Members > kono > Proof > category
changeset 373:4164586ffdb8
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 06 Mar 2016 02:23:36 +0900 |
| parents | b4855a3ebd34 |
| children | 5641b923201e |
| files | limit-to.agda |
| diffstat | 1 files changed, 3 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Sun Mar 06 02:05:50 2016 +0900 +++ b/limit-to.agda Sun Mar 06 02:23:36 2016 +0900 @@ -78,8 +78,8 @@ lim-to-equ A lim {a} {b} {c} f g two e fe=ge = record { fe=ge = fe=ge ; k = λ {d} h fh=gh → k {d} h fh=gh - ; ek=h = λ {d} {h} {fh=gh} → {!!} - ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!} + ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh + ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' } where Γ = indexFunctor A a b f g two nmap : (x : Obj A) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A A d) x) (FObj Γ x) @@ -134,7 +134,7 @@ k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c k {d} h fh=gh = limit (lim A Γ {c} {nat c e fe=ge }) d (nat d h fh=gh ) ek=h : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) -> A [ A [ e o k h fh=gh ] ≈ h ] - ek=h d h fh=gh = {!!} + ek=h d h fh=gh = ? uniquness : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) -> ( k' : Hom A d c ) -> A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]