Mercurial > hg > Members > kono > Proof > category
annotate yoneda.agda @ 181:b58453d90db6
contravariant functor
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 28 Aug 2013 13:26:01 +0900 |
| parents | 2d983d843e29 |
| children | 346e8eb35ec3 |
| rev | line source |
|---|---|
| 178 | 1 open import Category -- https://github.com/konn/category-agda |
| 2 open import Level | |
| 3 open import Category.Sets | |
| 4 module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where | |
| 5 | |
| 6 open import HomReasoning | |
| 7 open import cat-utility | |
| 179 | 8 open import Relation.Binary.Core |
| 9 open import Relation.Binary | |
| 10 | |
| 178 | 11 |
| 12 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} ) | |
| 179 | 13 open Functor |
| 178 | 14 |
| 181 | 15 -- A is Locally small |
| 16 postulate ≈-≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y | |
| 17 | |
| 18 import Relation.Binary.PropositionalEquality | |
| 19 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) | |
| 20 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ | |
| 21 | |
| 22 | |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
23 CF : (a : Obj A) → Functor A Sets |
| 178 | 24 CF a = record { |
| 25 FObj = λ b → Hom A a b | |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
26 ; FMap = λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) → A [ f o g ] |
| 178 | 27 ; isFunctor = record { |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
28 identity = identity |
|
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
29 ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g |
| 178 | 30 ; ≈-cong = cong1 |
| 31 } | |
| 32 } where | |
| 181 | 33 lemma-CF1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x |
| 34 lemma-CF1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL | |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
35 identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ] |
| 181 | 36 identity {b} = extensionality lemma-CF1 |
| 37 lemma-CF2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → (x : Hom A a a₁ )→ A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x | |
| 38 lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin | |
| 39 A [ A [ g o f ] o x ] | |
| 40 ≈↑⟨ assoc ⟩ | |
| 41 A [ g o A [ f o x ] ] | |
| 42 ≈⟨⟩ | |
| 43 ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) | |
| 44 ∎ ) | |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
45 distr1 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → |
|
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
46 Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ] |
| 181 | 47 distr1 a b c f g = extensionality ( λ x → lemma-CF2 a b c f g x ) |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
48 cong1 : {A₁ B : Obj A} {f g : Hom A A₁ B} → A [ f ≈ g ] → Sets [ (λ g₁ → A [ f o g₁ ]) ≈ (λ g₁ → A [ g o g₁ ]) ] |
| 181 | 49 cong1 eq = extensionality ( λ x → ( ≈-≡ ( |
| 50 (IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))) eq ))) | |
| 178 | 51 |
| 52 | |
| 179 | 53 |