Mercurial > hg > Members > kono > Proof > category
changeset 53:b4530a807918
start adjunction
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Jul 2013 16:36:31 +0900 |
| parents | 0fc0dbda7b55 |
| children | 5d2a33bb1291 |
| files | universal-mapping.agda |
| diffstat | 1 files changed, 31 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/universal-mapping.agda Tue Jul 23 16:18:21 2013 +0900 +++ b/universal-mapping.agda Tue Jul 23 16:36:31 2013 +0900 @@ -296,3 +296,34 @@ ∎ ) myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor ε myIsNTrans = record { naturality = naturality } + +------ +-- +-- Adjunction Construction from Universal Mapping +-- +----- + +UMAdjunction : {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) ) ) -> + (um : UniversalMapping A B U F' η' ) -> + Adjunction A B U (FunctorF A B U F' η' um) (nat-η A B U F' η' um) (nat-ε A B U F' η' um) +UMAdjunction A B U F' η' um = record { + isAdjunction = record { + adjoint1 = adjoint1 ; + adjoint2 = adjoint2 + } + } where + F : Functor A B + F = FunctorF A B U F' η' um + η : NTrans A A identityFunctor ( U ○ F ) + η = nat-η A B U F' η' um + ε : NTrans B B ( F ○ U ) identityFunctor + ε = nat-ε A B U F' η' um + adjoint1 : { b : Obj B } -> + A [ A [ ( FMap U ( TMap ε b )) o ( TMap η ( FObj U b )) ] ≈ id1 A (FObj U b) ] + adjoint1 = ? + adjoint2 : {a : Obj A} -> + B [ B [ ( TMap ε ( FObj F a )) o ( FMap F ( TMap η a )) ] ≈ id1 B (FObj F a) ] + adjoint2 = ?