Mercurial > hg > Members > kono > Proof > category
annotate src/HomReasoning.agda @ 1106:270f0ba65b88
unify yoneda functor
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 10 Mar 2023 16:19:46 +0900 |
parents | ac53803b3b2a |
children | 45de2b31bf02 |
rev | line source |
---|---|
56 | 1 module HomReasoning where |
31 | 2 |
3 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
4 | |
5 open import Category -- https://github.com/konn/category-agda | |
6 open import Level | |
7 open Functor | |
8 | |
9 -- F(f) | |
10 -- F(a) ---→ F(b) | |
11 -- | | | |
12 -- |t(a) |t(b) G(f)t(a) = t(b)F(f) | |
13 -- | | | |
14 -- v v | |
15 -- G(a) ---→ G(b) | |
16 -- G(f) | |
17 | |
18 record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) | |
19 ( F G : Functor D C ) | |
20 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A)) | |
21 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where | |
22 field | |
130 | 23 commute : {a b : Obj D} {f : Hom D a b} |
31 | 24 → C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ] |
25 | |
130 | 26 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) |
27 (F G : Functor domain codomain ) | |
31 | 28 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where |
29 field | |
30 TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) | |
31 isNTrans : IsNTrans domain codomain F G TMap | |
32 | |
33 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where | |
949
ac53803b3b2a
reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
948
diff
changeset
|
34 open import Relation.Binary |
31 | 35 |
36 _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b | |
37 x o y = A [ x o y ] | |
38 | |
39 _≈_ : {a b : Obj A } → Rel (Hom A a b) ℓ | |
40 x ≈ y = A [ x ≈ y ] | |
41 | |
42 infixr 9 _o_ | |
43 infix 4 _≈_ | |
44 | |
45 refl-hom : {a b : Obj A } { x : Hom A a b } → x ≈ x | |
46 refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) | |
47 | |
48 trans-hom : {a b : Obj A } { x y z : Hom A a b } → | |
49 x ≈ y → y ≈ z → x ≈ z | |
50 trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c | |
51 | |
52 -- some short cuts | |
53 | |
54 car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → | |
55 x ≈ y → ( x o f ) ≈ ( y o f ) | |
787 | 56 car eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq |
57 | |
58 car1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → | |
59 A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y o f ] ] | |
60 car1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) ) eq | |
31 | 61 |
62 cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → | |
63 x ≈ y → f o x ≈ f o y | |
787 | 64 cdr eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) |
65 | |
66 cdr1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → | |
67 A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f o y ] ] | |
68 cdr1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) ) | |
31 | 69 |
70 id : (a : Obj A ) → Hom A a a | |
71 id a = (Id {_} {_} {_} {A} a) | |
72 | |
479
a5034bdf6f38
Comma Category with A B C
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
460
diff
changeset
|
73 idL : {a b : Obj A } { f : Hom A a b } → id b o f ≈ f |
31 | 74 idL = IsCategory.identityL (Category.isCategory A) |
75 | |
76 idR : {a b : Obj A } { f : Hom A a b } → f o id a ≈ f | |
77 idR = IsCategory.identityR (Category.isCategory A) | |
78 | |
79 sym : {a b : Obj A } { f g : Hom A a b } → f ≈ g → g ≈ f | |
80 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) | |
81 | |
455 | 82 sym-hom = sym |
83 | |
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
84 -- working on another cateogry |
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
85 idL1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A b a } → A [ A [ Id {_} {_} {_} {A} a o f ] ≈ f ] |
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
86 idL1 A = IsCategory.identityL (Category.isCategory A) |
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
87 |
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
88 idR1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b } → A [ A [ f o Id {_} {_} {_} {A} a ] ≈ f ] |
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
89 idR1 A = IsCategory.identityR (Category.isCategory A) |
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
90 |
781 | 91 open import Relation.Binary.PropositionalEquality using ( _≡_ ) |
693 | 92 ≈←≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≡ y ) → x ≈ y |
781 | 93 ≈←≡ _≡_.refl = refl-hom |
75 | 94 |
693 | 95 -- Ho← to prove this? |
96 -- ≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : x ≈ y ) → x ≡ y | |
97 -- ≡←≈ x≈y = irr x≈y | |
98 | |
75 | 99 ≡-cong : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → |
420
3e44951b9bdb
refl in free-monoid trouble
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
299
diff
changeset
|
100 (f : Hom B x y → Hom A x' y' ) → a ≡ b → f a ≈ f b |
781 | 101 ≡-cong f _≡_.refl = ≈←≡ _≡_.refl |
75 | 102 |
67 | 103 -- cong-≈ : { c₁′ c₂′ ℓ′ : Level} {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A } → |
104 -- B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) → f a ≈ f b | |
75 | 105 -- cong-≈ eq f = {!!} |
67 | 106 |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
107 assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} |
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
108 → f o ( g o h ) ≈ ( f o g ) o h |
31 | 109 assoc = IsCategory.associative (Category.isCategory A) |
110 | |
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
111 -- working on another cateogry |
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
112 assoc1 : { c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
113 → A [ A [ f o ( A [ g o h ] ) ] ≈ A [ ( A [ f o g ] ) o h ] ] |
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
114 assoc1 A = IsCategory.associative (Category.isCategory A) |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
115 |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
116 distr : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
117 { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) → {a b c : Obj D} {g : Hom D b c} { f : Hom D a b } |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
118 → A [ FMap T ( D [ g o f ] ) ≈ A [ FMap T g o FMap T f ] ] |
75 | 119 distr T = IsFunctor.distr ( isFunctor T ) |
120 | |
121 resp : {a b c : Obj A} {f g : Hom A a b} {h i : Hom A b c} → f ≈ g → h ≈ i → (h o f) ≈ (i o g) | |
122 resp = IsCategory.o-resp-≈ (Category.isCategory A) | |
123 | |
124 fcong : { c₁ c₂ ℓ : Level} {C : Category c₁ c₂ ℓ} | |
125 { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} {a b : Obj C} {f g : Hom C a b} → (T : Functor C D) → C [ f ≈ g ] → D [ FMap T f ≈ FMap T g ] | |
126 fcong T = IsFunctor.≈-cong (isFunctor T) | |
31 | 127 |
128 open NTrans | |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
129 nat : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
130 {a b : Obj D} {f : Hom D a b} {F G : Functor D A } |
31 | 131 → (η : NTrans D A F G ) |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
67
diff
changeset
|
132 → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] |
130 | 133 nat η = IsNTrans.commute ( isNTrans η ) |
31 | 134 |
460 | 135 nat1 : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} |
136 {a b : Obj D} {F G : Functor D A } | |
137 → (η : NTrans D A F G ) → (f : Hom D a b) | |
138 → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] | |
139 nat1 η f = IsNTrans.commute ( isNTrans η ) | |
140 | |
606 | 141 infix 3 _∎ |
31 | 142 infixr 2 _≈⟨_⟩_ _≈⟨⟩_ |
168 | 143 infixr 2 _≈↑⟨_⟩_ |
31 | 144 infix 1 begin_ |
145 | |
146 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly | |
147 -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } → A [ x ≈ y ] → x ≡ y | |
148 -- ≈-to-≡ refl-hom = refl | |
149 | |
150 data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) : | |
151 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
152 relTo : (x≈y : x ≈ y ) → x IsRelatedTo y | |
153 | |
154 begin_ : { a b : Obj A } { x y : Hom A a b } → | |
155 x IsRelatedTo y → x ≈ y | |
156 begin relTo x≈y = x≈y | |
157 | |
158 _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → | |
159 x ≈ y → y IsRelatedTo z → x IsRelatedTo z | |
160 _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z) | |
161 | |
168 | 162 _≈↑⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → |
163 y ≈ x → y IsRelatedTo z → x IsRelatedTo z | |
164 _ ≈↑⟨ y≈x ⟩ relTo y≈z = relTo (trans-hom ( sym y≈x ) y≈z) | |
165 | |
31 | 166 _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y |
167 _ ≈⟨⟩ x∼y = x∼y | |
168 | |
169 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x | |
170 _∎ _ = relTo refl-hom | |
171 | |
948 | 172 |
1106 | 173 -- examples |
56 | 174 |
175 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
176 { a : Obj A } ( b : Obj A ) → | |
177 ( f : Hom A a b ) | |
178 → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ] | |
179 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) | |
606 | 180 let open ≈-Reasoning (c) in begin |
181 c [ ( Id {_} {_} {_} {c} b ) o g ] | |
56 | 182 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ |
183 g | |
184 ∎ | |
253 | 185 |
186 Lemma62 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
187 { a b : Obj A } → | |
188 ( f g : Hom A a b ) | |
189 → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ A [ (Id {_} {_} {_} {A} b) o g ] ] | |
190 → A [ g ≈ f ] | |
191 Lemma62 A {a} {b} f g 1g=1f = let open ≈-Reasoning A in | |
192 begin | |
193 g | |
194 ≈↑⟨ idL ⟩ | |
195 id b o g | |
196 ≈↑⟨ 1g=1f ⟩ | |
197 id b o f | |
198 ≈⟨ idL ⟩ | |
199 f | |
200 ∎ |