Mercurial > hg > Members > kono > Proof > category

changeset 59:a6e31588e2a6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
UεF
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Jul 2013 22:45:57 +0900
parents f321a207f711
children 45118051b829
files nat.agda
diffstat 1 files changed, 3 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Wed Jul 24 22:32:53 2013 +0900
+++ b/nat.agda	Wed Jul 24 22:45:57 2013 +0900
@@ -259,8 +259,9 @@
 open Adjunction
 
 lemma11 :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'}
-                 ( U : Functor B A ) ( F : Functor A B ) -> NTrans A A ? ? -> NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
-lemma11 U F n = {!!}
+                 ( U : Functor B A ) ( F : Functor A B ) -> NTrans A A ( U ○  ((F  ○  U) ○  F )) ( U ○  (identityFunctor ○ F) ) 
+                         -> NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
+lemma11 U F n = record { isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }}
 
 UεF :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  ( U : Functor B A )