Mercurial > hg > Members > kono > Proof > category

changeset 34:306aa1873b2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
trying...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2013 15:16:56 +0900
parents fefebc387eae
children 4ac419251f86
files universal-mapping.agda
diffstat 1 files changed, 6 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/universal-mapping.agda	Mon Jul 22 14:54:52 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 15:16:56 2013 +0900
@@ -15,7 +15,6 @@
        universalMapping :   {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> 
                      A [ A [ FMap U ( f * ) o η a' ]  ≈ f ]
 
-
 record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  ( U : Functor B A )
                  ( F : Obj A -> Obj B )
@@ -27,7 +26,6 @@
 
 open NTrans
 open import Category.Cat
-
 record IsAdjunction  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  ( U : Functor B A )
                  ( F : Functor A B )
@@ -40,7 +38,6 @@
        adjoint2 :   {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> 
                      B [ B [ ( TMap ε ( FObj F a' ))  o ( FMap F ( TMap η a' )) ]  ≈ Id {_} {_} {_} {B} (FObj F a') ]
 
-
 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  ( U : Functor B A )
                  ( F : Functor A B )
@@ -50,19 +47,17 @@
     field
        isAdjection : IsAdjunction A B U F η ε
 
+open Adjunction
+open UniversalMapping
 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 } ->
-     ( Adj : Adjunction A B U F η ε ) -> 
-      record { 
-             U = ? 
-           ; F = ? 
-           ; η = ? 
-           ; _*  = ? 
-     }
-Lemma1 adj =  ?
+      Adjunction A B U F η ε  -> UniversalMapping A B U (FObj F) ?  ?
+Lemma1 = ?
 
 
 
+
+