Mercurial > hg > Members > kono > Proof > category
changeset 43:5506abc832c7
uniqness
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Jul 2013 00:29:17 +0900 |
| parents | 9694f93977ca |
| children | a626fdd909c3 |
| files | universal-mapping.agda |
| diffstat | 1 files changed, 26 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/universal-mapping.agda Mon Jul 22 21:29:26 2013 +0900 +++ b/universal-mapping.agda Tue Jul 23 00:29:17 2013 +0900 @@ -51,16 +51,14 @@ field isAdjunction : IsAdjunction A B U F η ε +-- +-- Adjunction yields solution of universal mapping +-- +-- + 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 ) @@ -68,17 +66,20 @@ ( ε : NTrans B B ( F ○ U ) identityFunctor ) -> Adjunction A B U F η ε -> UniversalMapping A B U (FObj F) (TMap η) Lemma1 A B U F η ε adj = record { - _* = Solution A B U F ε ; + _* = solution ; isUniversalMapping = record { - universalMapping = universalMapping + universalMapping = universalMapping; + unique-universalMapping = uniqness } } where + solution : { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) -> Hom B (FObj F a ) b + solution {_} {b} f = B [ TMap ε b o FMap F f ] universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> - A [ A [ FMap U ( Solution A B U F ε f ) o TMap η a' ] ≈ f ] + A [ A [ FMap U ( solution f) o TMap η a' ] ≈ f ] universalMapping a b {f} = let open ≈-Reasoning (A) in begin - FMap U ( Solution A B U F ε f ) o TMap η a + FMap U ( solution f) o TMap η a ≈⟨⟩ FMap U ( B [ TMap ε b o FMap F f ] ) o TMap η a ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩ @@ -94,8 +95,22 @@ ≈⟨ idL ⟩ f ∎ + uniqness : (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g : Hom B (FObj F a') b') -> + A [ A [ FMap U g o TMap η a' ] ≈ f ] -> B [ solution f ≈ g ] + uniqness a b f g = {!!} +-- +-- +-- Universal mapping yields Adjunction +-- +-- + + +-- +-- F is an functor +-- + FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Obj A -> Obj B )