Mercurial > hg > Members > kono > Proof > category

annotate yoneda.agda @ 180:2d983d843e29

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no yellow on co-Contravariant Functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Aug 2013 11:41:17 +0900
parents f017d892d8c3
children b58453d90db6
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category -- https://github.com/konn/category-agda
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Category.Sets
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import HomReasoning
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import cat-utility
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
8 open import Relation.Binary.Core
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
9 open import Relation.Binary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
10
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} )
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
13 open Functor
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
180
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
15 CF : (a : Obj A) → Functor A Sets
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 CF a = record {
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 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
18 ; FMap = λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) → A [ f o g ]
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 ; isFunctor = record {
180
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
20 identity = identity
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
21 ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 ; ≈-cong = cong1
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 }
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 } where
180
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
25 identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ]
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
26 identity = let open ≈-Reasoning A in {!!}
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
27 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
28 Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ]
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
29 distr1 a b c f g = {!!}
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
30 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₁ ]) ]
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
31 cong1 eq = {!!}
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
34