Mercurial > hg > Members > kono > Proof > category

changeset 33:fefebc387eae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add Adj to Universal Mapping
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2013 14:54:52 +0900
parents 7862ad3b000f
children 306aa1873b2f
files universal-mapping.agda
diffstat 1 files changed, 14 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/universal-mapping.agda	Mon Jul 22 14:45:58 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 14:54:52 2013 +0900
@@ -50,5 +50,19 @@
     field
        isAdjection : IsAdjunction A B U 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 } ->
+     ( Adj : Adjunction A B U F η ε ) -> 
+      record { 
+             U = ? 
+           ; F = ? 
+           ; η = ? 
+           ; _*  = ? 
+     }
+Lemma1 adj =  ?
 
 
+