Mercurial > hg > Members > kono > Proof > category

changeset 57:c6f66c21230c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
nat and functor comp
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Jul 2013 21:19:27 +0900
parents 83ff8d48fdca
children f321a207f711
files cat-utility.agda nat.agda
diffstat 2 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Wed Jul 24 20:47:28 2013 +0900
+++ b/cat-utility.agda	Wed Jul 24 21:19:27 2013 +0900
@@ -98,9 +98,9 @@
                (FMap F (TMap n b )) o  (FMap F (FMap G f))
             ∎
 
-Nat*Functor :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (C : Category c₁'' c₂'' ℓ'')
-    (F : Functor A B) -> { G H : Functor B C } -> ( n : NTrans B C G H ) -> NTrans A C (G ○  F) (H ○ F)
-Nat*Functor A B C F {G} {H} n = record {
+Nat*Functor :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
+    { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○  F) (H ○ F)
+Nat*Functor A {B} C {G} {H} n F = record {
        TMap  = \a -> TMap n (FObj F a)
        ; isNTrans = record {
             naturality = naturality
@@ -108,9 +108,7 @@
     } where
          naturality : {a b : Obj A} {f : Hom A a b} 
             → C [ C [ ( FMap H (FMap F f )) o  ( TMap n (FObj F a)) ]  ≈ C [ (TMap n (FObj F b )) o  (FMap G (FMap F f))  ] ]
-         naturality  {a} {b} {f}  = {!!}
-
-
+         naturality  {a} {b} {f}  =  IsNTrans.naturality ( isNTrans n) 
 
 record Kleisli  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
                  ( T : Functor A A )
--- a/nat.agda	Wed Jul 24 20:47:28 2013 +0900
+++ b/nat.agda	Wed Jul 24 21:19:27 2013 +0900
@@ -271,4 +271,6 @@
                     unity1 = {!!};
                     unity2 = {!!}
               }
-      } 
+      } where
+         UεF : {!!}
+         UεF = Functor*Nat B A U ( Nat*Functor ? {?} ? ε F)