Mercurial > hg > Members > kono > Proof > category
changeset 36:ad997bd9788b
isUniversalMapping
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Jul 2013 16:47:45 +0900 |
| parents | 4ac419251f86 |
| children | 2f5f5b4d62fa |
| files | universal-mapping.agda |
| diffstat | 1 files changed, 9 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/universal-mapping.agda Mon Jul 22 16:04:23 2013 +0900 +++ b/universal-mapping.agda Mon Jul 22 16:47:45 2013 +0900 @@ -12,7 +12,7 @@ ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where field - universalMapping : {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> + 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₂' ℓ') @@ -54,7 +54,7 @@ ( 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 + { 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₂' ℓ') @@ -62,12 +62,11 @@ ( F : Functor A B ) ( η : NTrans A A identityFunctor ( U ○ F ) ) ( ε : NTrans B B ( F ○ U ) identityFunctor ) -> - Adjunction A B U F η ε -> UniversalMapping A B U (FObj F) (TMap η) (Solution A B U F ε ) + Adjunction A B U F η ε -> UniversalMapping A B U (FObj F) (TMap η) (Solution A B U F ε) Lemma1 A B U F η ε adj = record { - isUniversalMapping = {!!} - } - - - - - + isUniversalMapping = record { + universalMapping = univeralMapping + } + } where + univeralMapping : {!!} + univeralMapping = {!!}