Mercurial > hg > Members > kono > Proof > category
annotate universal-mapping.agda @ 38:999e637d14c7
reasoning
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Jul 2013 17:17:42 +0900 |
| parents | 2f5f5b4d62fa |
| children | 77c3a5292a2f |
| 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 | |
| 37 | 8 |
| 31 | 9 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 10 ( U : Functor B A ) | |
| 11 ( F : Obj A -> Obj B ) | |
| 12 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
| 13 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b ) | |
| 14 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 15 field | |
| 36 | 16 universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> |
| 37 | 17 A [ A [ FMap U ( f * ) o η a' ] ≈ f ] |
| 18 | |
| 31 | 19 |
| 20 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 21 ( U : Functor B A ) | |
| 22 ( F : Obj A -> Obj B ) | |
| 23 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) | |
| 24 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 37 | 25 infixr 11 _* |
| 31 | 26 field |
| 37 | 27 _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b |
| 31 | 28 isUniversalMapping : IsUniversalMapping A B U F η _* |
| 29 | |
| 32 | 30 open NTrans |
| 31 open import Category.Cat | |
| 32 record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 33 ( U : Functor B A ) | |
| 34 ( F : Functor A B ) | |
| 35 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 36 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 37 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 38 field | |
| 39 adjoint1 : {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> | |
| 40 A [ A [ ( FMap U ( TMap ε b' )) o ( TMap η ( FObj U b' )) ] ≈ Id {_} {_} {_} {A} (FObj U b') ] | |
| 41 adjoint2 : {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> | |
| 42 B [ B [ ( TMap ε ( FObj F a' )) o ( FMap F ( TMap η a' )) ] ≈ Id {_} {_} {_} {B} (FObj F a') ] | |
| 31 | 43 |
| 32 | 44 record Adjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 45 ( U : Functor B A ) | |
| 46 ( F : Functor A B ) | |
| 47 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 48 ( ε : NTrans B B ( F ○ U ) identityFunctor ) | |
| 49 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where | |
| 50 field | |
| 51 isAdjection : IsAdjunction A B U F η ε | |
| 52 | |
| 34 | 53 open Adjunction |
| 54 open UniversalMapping | |
| 35 | 55 |
| 56 Solution : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 57 ( U : Functor B A ) | |
| 58 ( F : Functor A B ) | |
| 59 ( ε : NTrans B B ( F ○ U ) identityFunctor ) -> | |
| 36 | 60 { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) -> Hom B (FObj F a ) b |
| 35 | 61 Solution A B U F ε {a} {b} f = B [ TMap ε b o FMap F f ] |
| 62 | |
|
33
fefebc387eae
add Adj to Universal Mapping
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
32
diff
changeset
|
63 Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
| 35 | 64 ( U : Functor B A ) |
| 65 ( F : Functor A B ) | |
| 66 ( η : NTrans A A identityFunctor ( U ○ F ) ) | |
| 67 ( ε : NTrans B B ( F ○ U ) identityFunctor ) -> | |
| 37 | 68 Adjunction A B U F η ε -> UniversalMapping A B U (FObj F) (TMap η) |
| 35 | 69 Lemma1 A B U F η ε adj = record { |
| 37 | 70 _* = Solution A B U F ε ; |
| 36 | 71 isUniversalMapping = record { |
| 37 | 72 universalMapping = universalMapping |
| 36 | 73 } |
| 74 } where | |
| 37 | 75 universalMapping : (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> |
| 76 A [ A [ FMap U ( Solution A B U F ε f ) o TMap η a' ] ≈ f ] | |
| 38 | 77 universalMapping a b {f} = |
| 78 let open ≈-Reasoning (A) in | |
| 79 begin | |
| 80 A [ FMap U ( Solution A B U F ε f ) o TMap η a ] | |
| 81 ≈⟨ ? ⟩ | |
| 82 f | |
| 83 ∎ | |
| 84 | |
| 85 |