Mercurial > hg > Members > kono > Proof > category

changeset 41:e9fa5c95eff7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isFunctor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2013 19:07:31 +0900
parents c34b1cfe9fdc
children 9694f93977ca
files category.ind universal-mapping.agda
diffstat 2 files changed, 14 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/category.ind	Mon Jul 22 18:13:57 2013 +0900
+++ b/category.ind	Mon Jul 22 19:07:31 2013 +0900
@@ -205,7 +205,7 @@
 $ η(a): a->UF(a)$ 
 
 put 
-\[    F(f) = (η(b)f)* \]
+\[    F(f) = (η(U(b))f)* \]
 \[ ε : FU -> 1_B        \]
 \[  ε(b) = (1_{U(b)})* \]
 
--- a/universal-mapping.agda	Mon Jul 22 18:13:57 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 19:07:31 2013 +0900
@@ -95,3 +95,16 @@
               ∎
 
 
+FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
+                 ( U : Functor B A )
+                 ( F : Obj A -> Obj B )
+                 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) ->
+       UniversalMapping A B U F η   -> Functor A B
+FunctorF A B U F η um = record {
+              FObj = F;
+              FMap = \f ->  (_* um)  (A [  η (Category.cod A f )   o f ])   ;
+              isFunctor = isFunctor1
+       } where
+         isFunctor1 : ?
+         isFunctor1 = ?
+