Mercurial > hg > Members > kono > Proof > category

changeset 61:af7ddd9f9122

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
unity done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Jul 2013 23:23:56 +0900
parents 45118051b829
children c5277284919e
files nat.agda
diffstat 1 files changed, 10 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Wed Jul 24 23:16:21 2013 +0900
+++ b/nat.agda	Wed Jul 24 23:23:56 2013 +0900
@@ -291,7 +291,16 @@
            assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
            assoc1 = {!!}
            unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-           unity1 = {!!}
+           unity1 {a} = let open ≈-Reasoning (A) in
+             begin
+               TMap μ a o TMap η ( FObj T a )
+             ≈⟨⟩
+               (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F  a ))
+             ≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩
+               id (FObj U ( FObj F a ))
+             ≈⟨⟩
+               id (FObj T a)
+             ∎
            unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
            unity2 {a} = let open ≈-Reasoning (A) in
              begin