Mercurial > hg > Members > kono > Proof > category

comparison yoneda.agda @ 830:232cea484067

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to CCC again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Mar 2020 14:26:39 +0900
parents bded2347efa4
children
comparison
equal deleted inserted replaced
829:6c5cfb9b333e 830:232cea484067
89 ; Id = Yid A 89 ; Id = Yid A
90 ; isCategory = isSetsAop A 90 ; isCategory = isSetsAop A
91 } 91 }
92 92
93 -- A is Locally small 93 -- A is Locally small
94 postulate ≈-≡ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y 94 postulate ≡←≈ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y
95 95
96 import Relation.Binary.PropositionalEquality 96 import Relation.Binary.PropositionalEquality
97 -- 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 ) 97 -- 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 )
98 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ 98 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
99 99
115 distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; 115 distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ;
116 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) 116 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq )
117 } 117 }
118 } where 118 } where
119 lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x 119 lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x
120 lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} idL 120 lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≡←≈ {_} {_} {_} {A} idL
121 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ 121 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→
122 Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x 122 Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x
123 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin 123 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≡←≈ {_} {_} {_} {A} ( begin
124 Category.op A [ Category.op A [ g o f ] o x ] 124 Category.op A [ Category.op A [ g o f ] o x ]
125 ≈↑⟨ assoc ⟩ 125 ≈↑⟨ assoc ⟩
126 Category.op A [ g o Category.op A [ f o x ] ] 126 Category.op A [ g o Category.op A [ f o x ] ]
127 ≈⟨⟩ 127 ≈⟨⟩
128 ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) 128 ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x )
129 ∎ ) 129 ∎ )
130 lemma-y-obj3 : {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → A [ f ≈ g ] → Category.op A [ f o x ] ≡ Category.op A [ g o x ] 130 lemma-y-obj3 : {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → A [ f ≈ g ] → Category.op A [ f o x ] ≡ Category.op A [ g o x ]
131 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin 131 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≡←≈ {_} {_} {_} {A} ( begin
132 Category.op A [ f o x ] 132 Category.op A [ f o x ]
133 ≈⟨ resp refl-hom eq ⟩ 133 ≈⟨ resp refl-hom eq ⟩
134 Category.op A [ g o x ] 134 Category.op A [ g o x ]
135 ∎ ) 135 ∎ )
136 136
148 y-map : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → (f : Hom A a b ) → YHom A (y-obj A a) (y-obj A b) 148 y-map : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → (f : Hom A a b ) → YHom A (y-obj A a) (y-obj A b)
149 y-map {_} {c₂} {_} A {a} {b} f = record { TMap = y-tmap A a b f ; isNTrans = isNTrans1 {a} {b} f } where 149 y-map {_} {c₂} {_} A {a} {b} f = record { TMap = y-tmap A a b f ; isNTrans = isNTrans1 {a} {b} f } where
150 lemma-y-obj4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) → 150 lemma-y-obj4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) →
151 Sets [ Sets [ FMap (y-obj A b) g o y-tmap A a b f a₁ ] ≈ 151 Sets [ Sets [ FMap (y-obj A b) g o y-tmap A a b f a₁ ] ≈
152 Sets [ y-tmap A a b f b₁ o FMap (y-obj A a) g ] ] 152 Sets [ y-tmap A a b f b₁ o FMap (y-obj A a) g ] ]
153 lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ {_} {_} {_} {A} ( begin 153 lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≡←≈ {_} {_} {_} {A} ( begin
154 A [ A [ f o x ] o g ] 154 A [ A [ f o x ] o g ]
155 ≈↑⟨ assoc ⟩ 155 ≈↑⟨ assoc ⟩
156 A [ f o A [ x o g ] ] 156 A [ f o A [ x o g ] ]
157 ∎ ) ) 157 ∎ ) )
158 isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) (y-obj A b) (y-tmap A a b f ) 158 isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) (y-obj A b) (y-tmap A a b f )
175 175
176 } 176 }
177 } where 177 } where
178 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop A [ y-map A f ≈ y-map A g ] 178 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop A [ y-map A f ≈ y-map A g ]
179 ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning (A) in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) 179 ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning (A) in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] )
180 extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin 180 extensionality A ( λ h → ≡←≈ {_} {_} {_} {A} ( begin
181 A [ f o h ] 181 A [ f o h ]
182 ≈⟨ resp refl-hom eq ⟩ 182 ≈⟨ resp refl-hom eq ⟩
183 A [ g o h ] 183 A [ g o h ]
184 ∎ 184 ∎
185 ) ) 185 ) )
186 identity : {a : Obj A} → SetsAop A [ y-map A (id1 A a) ≈ id1 (SetsAop A) (y-obj A a ) ] 186 identity : {a : Obj A} → SetsAop A [ y-map A (id1 A a) ≈ id1 (SetsAop A) (y-obj A a ) ]
187 identity {a} = let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) 187 identity {a} = let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
188 extensionality A ( λ g → ≈-≡ {_} {_} {_} {A} ( begin 188 extensionality A ( λ g → ≡←≈ {_} {_} {_} {A} ( begin
189 A [ id1 A a o g ] 189 A [ id1 A a o g ]
190 ≈⟨ idL ⟩ 190 ≈⟨ idL ⟩
191 g 191 g
192 ∎ 192 ∎
193 ) ) 193 ) )
194 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop A [ y-map A (A [ g o f ]) ≈ SetsAop A [ y-map A g o y-map A f ] ] 194 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop A [ y-map A (A [ g o f ]) ≈ SetsAop A [ y-map A g o y-map A f ] ]
195 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] ) 195 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] )
196 extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin 196 extensionality A ( λ h → ≡←≈ {_} {_} {_} {A} ( begin
197 A [ A [ g o f ] o h ] 197 A [ A [ g o f ] o h ]
198 ≈↑⟨ assoc ⟩ 198 ≈↑⟨ assoc ⟩
199 A [ g o A [ f o h ] ] 199 A [ g o A [ f o h ] ]
200 ∎ 200 ∎
201 ) ) 201 ) )
275 FMap F g (TMap ha a (Category.Category.Id A)) 275 FMap F g (TMap ha a (Category.Category.Id A))
276 ≡⟨ ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩ 276 ≡⟨ ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩
277 TMap ha b (FMap (y-obj A a) g (Category.Category.Id A)) 277 TMap ha b (FMap (y-obj A a) g (Category.Category.Id A))
278 ≡⟨⟩ 278 ≡⟨⟩
279 TMap ha b ( (A Category.o Category.Category.Id A) g ) 279 TMap ha b ( (A Category.o Category.Category.Id A) g )
280 ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL ( Category.isCategory A ))) ⟩ 280 ≡⟨ ≡-cong ( TMap ha b ) ( ≡←≈ {_} {_} {_} {A} (IsCategory.identityL ( Category.isCategory A ))) ⟩
281 TMap ha b g 281 TMap ha b g
282 ∎ 282 ∎
283 )) ⟩ 283 )) ⟩
284 TMap ha b 284 TMap ha b
285 ∎ 285 ∎