Mercurial > hg > Members > kono > Proof > category
changeset 32:7862ad3b000f
Adjoint
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Jul 2013 14:45:58 +0900 |
| parents | 17b8bafebad7 |
| children | fefebc387eae |
| files | universal-mapping.agda |
| diffstat | 1 files changed, 25 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/universal-mapping.agda Mon Jul 22 14:30:27 2013 +0900 +++ b/universal-mapping.agda Mon Jul 22 14:45:58 2013 +0900 @@ -25,5 +25,30 @@ field isUniversalMapping : IsUniversalMapping A B U F η _* +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 ) + ( η : NTrans A A identityFunctor ( U ○ F ) ) + ( ε : NTrans B B ( F ○ U ) identityFunctor ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + adjoint1 : {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> + A [ A [ ( FMap U ( TMap ε b' )) o ( TMap η ( FObj U b' )) ] ≈ Id {_} {_} {_} {A} (FObj U b') ] + 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 ) + ( η : NTrans A A identityFunctor ( U ○ F ) ) + ( ε : NTrans B B ( F ○ U ) identityFunctor ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + isAdjection : IsAdjunction A B U F η ε + + +