Mercurial > hg > Members > kono > Proof > category

changeset 35:4ac419251f86

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
f∗ = ε(b)F(f),
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2013 16:04:23 +0900
parents 306aa1873b2f
children ad997bd9788b
files universal-mapping.agda
diffstat 1 files changed, 16 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/universal-mapping.agda	Mon Jul 22 15:16:56 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 16:04:23 2013 +0900
@@ -49,13 +49,23 @@
 
 open Adjunction
 open UniversalMapping
+
+Solution : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+                 ( U : Functor B A )
+                 ( F : Functor A B )
+                 ( ε : NTrans B B  ( F ○  U ) identityFunctor ) ->
+     { a : Obj A}{ b : Obj B} -> ( f : Hom A a (FObj U b) ) ->  Hom B (FObj F a ) b 
+Solution  A B U F ε {a} {b} f = B [ TMap ε b o FMap F f ]
+
 Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-                 { U : Functor B A }
-                 { F : Functor A B }
-                 { η : NTrans A A identityFunctor ( U ○  F ) }
-                 { ε : NTrans B B  ( F ○  U ) identityFunctor } ->
-      Adjunction A B U F η ε  -> UniversalMapping A B U (FObj F) ?  ?
-Lemma1 = ?
+                 ( U : Functor B A )
+                 ( F : Functor A B )
+                 ( η : NTrans A A identityFunctor ( U ○  F ) )
+                 ( ε : NTrans B B  ( F ○  U ) identityFunctor ) ->
+      Adjunction A B U F η ε  -> UniversalMapping A B U (FObj F) (TMap η) (Solution A B U F ε )
+Lemma1 A B U F η ε adj = record {
+         isUniversalMapping = {!!}
+      }