Mercurial > hg > Members > kono > Proof > category
annotate universal-mapping.agda @ 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 |
| rev | line source |
|---|---|
| 31 | 1 module universal-mapping where |
| 2 | |
| 3 open import Category -- https://github.com/konn/category-agda | |
| 4 open import Level | |
| 5 open import Category.HomReasoning | |
| 6 | |
| 7 open Functor | |
| 8 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 9 ( U : Functor B A ) | |
| 10 ( F : Obj A -> Obj B ) | |
| 11 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
| 12 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b ) | |
| 13 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 14 field | |
| 36 | 15 universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> |
| 31 | 16 A [ A [ FMap U ( f * ) o η a' ] ≈ f ] |
| 17 | |
| 18 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 19 ( U : Functor B A ) | |
| 20 ( F : Obj A -> Obj B ) | |
| 21 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
| 22 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b ) | |
| 23 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 24 field | |
| 25 isUniversalMapping : IsUniversalMapping A B U F η _* | |
| 26 | |
| 32 | 27 open NTrans |
| 28 open import Category.Cat | |
| 29 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 30 ( U : Functor B A ) | |
| 31 ( F : Functor A B ) | |
| 32 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 33 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 34 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 35 field | |
| 36 adjoint1 : {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> | |
| 37 A [ A [ ( FMap U ( TMap ε b' )) o ( TMap η ( FObj U b' )) ] ≈ Id {_} {_} {_} {A} (FObj U b') ] | |
| 38 adjoint2 : {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> | |
| 39 B [ B [ ( TMap ε ( FObj F a' )) o ( FMap F ( TMap η a' )) ] ≈ Id {_} {_} {_} {B} (FObj F a') ] | |
| 31 | 40 |
| 32 | 41 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 42 ( U : Functor B A ) | |
| 43 ( F : Functor A B ) | |
| 44 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 45 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 46 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 47 field | |
| 48 isAdjection : IsAdjunction A B U F η ε | |
| 49 | |
| 34 | 50 open Adjunction |
| 51 open UniversalMapping | |
| 35 | 52 |
| 53 Solution : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 54 ( U : Functor B A ) | |
| 55 ( F : Functor A B ) | |
| 56 ( ε : NTrans B B ( F ○ U ) identityFunctor ) -> | |
| 36 | 57 { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) -> Hom B (FObj F a ) b |
| 35 | 58 Solution A B U F ε {a} {b} f = B [ TMap ε b o FMap F f ] |
| 59 | |
|
33
fefebc387eae
add Adj to Universal Mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
60 Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 35 | 61 ( U : Functor B A ) |
| 62 ( F : Functor A B ) | |
| 63 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 64 ( ε : NTrans B B ( F ○ U ) identityFunctor ) -> | |
| 36 | 65 Adjunction A B U F η ε -> UniversalMapping A B U (FObj F) (TMap η) (Solution A B U F ε) |
| 35 | 66 Lemma1 A B U F η ε adj = record { |
| 36 | 67 isUniversalMapping = record { |
| 68 universalMapping = univeralMapping | |
| 69 } | |
| 70 } where | |
| 71 univeralMapping : {!!} | |
| 72 univeralMapping = {!!} |