Mercurial > hg > Members > kono > Proof > category

comparison yoneda.agda @ 783:bded2347efa4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CCC by equation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Apr 2019 12:03:45 +0900
parents 340708e8d54f
children 232cea484067
comparison
equal deleted inserted replaced
782:db59b8f954aa 783:bded2347efa4
163 -- Yoneda Functor itself 163 -- Yoneda Functor itself
164 -- 164 --
165 ----- 165 -----
166 166
167 YonedaFunctor : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Functor A (SetsAop A) 167 YonedaFunctor : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Functor A (SetsAop A)
168 YonedaFunctor {_} {c₂} {_} A = record { 168 YonedaFunctor A = record {
169 FObj = λ a → y-obj A a 169 FObj = λ a → y-obj A a
170 ; FMap = λ f → y-map A f 170 ; FMap = λ f → y-map A f
171 ; isFunctor = record { 171 ; isFunctor = record {
172 identity = identity 172 identity = identity
173 ; distr = distr1 173 ; distr = distr1
297 297
298 -- Full embedding of Yoneda Functor requires injective on Object, 298 -- Full embedding of Yoneda Functor requires injective on Object,
299 -- 299 --
300 -- But we cannot prove like this 300 -- But we cannot prove like this
301 -- FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b 301 -- FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b
302 -- YondaLemma2 : {a b x : Obj A } → (FObj (FObj YonedaFunctor a) x) ≡ (FObj (FObj YonedaFunctor b ) x) → 302
303 -- a ≡ b 303 open import Relation.Nullary
304 -- YondaLemma2 {a} {b} eq = {!!} 304 open import Data.Empty
305
306 --YondaLemma2 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →
307 -- (a b x : Obj A ) → (FObj (FObj (YonedaFunctor A) a) x) ≡ (FObj (FObj (YonedaFunctor A) b ) x) → a ≡ b
308 --YondaLemma2 A a bx eq = {!!}
309
305 -- N.B = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b 310 -- N.B = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b
311
312 --record Category c₁ c₂ ℓ : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
313 -- infixr 9 _o_
314 -- infix 4 _≈_
315 -- field
316 -- Obj : Set c₁
317 -- Hom : Obj → Obj → Set c₂
318 --YondaLemma31 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →
319 -- (a b x : Obj A ) → Hom A a x ≡ Hom A b x → a ≡ b
320 --YondaLemma31 A a b x eq = {!!}
306 -- 321 --
307 -- Instead we prove only 322 -- Instead we prove only
308 -- inv ( FObj YonedaFunctor a ) ≡ a 323 -- inv ( FObj YonedaFunctor a ) ≡ a
309 324
310 inv : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : FObj (FObj (YonedaFunctor A) a) x) → Obj A 325 inv : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : FObj (FObj (YonedaFunctor A) a) x) → Obj A
312 327
313 YonedaLemma21 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : ( FObj (FObj (YonedaFunctor A ) a) x) ) → inv A f ≡ a 328 YonedaLemma21 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : ( FObj (FObj (YonedaFunctor A ) a) x) ) → inv A f ≡ a
314 YonedaLemma21 A {a} {x} f = refl 329 YonedaLemma21 A {a} {x} f = refl
315 330
316 open import Relation.Binary.HeterogeneousEquality 331 open import Relation.Binary.HeterogeneousEquality
317 --
318 a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 332 a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B
319 a1 refl = refl 333 a1 refl = refl
320 -- 334
321 -- YonedaInjective : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b x : Obj A} 335 -- YondaLemma3 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →
322 -- → FObj (FObj (YonedaFunctor A ) a ) x ≡ FObj (FObj (YonedaFunctor A ) b ) x 336 -- (a b x : Obj A ) → Hom A a x ≅ Hom A b x → a ≡ b
323 -- → a ≡ b 337 -- YondaLemma3 A a b x eq = {!!} -- ≡-cong (inv A) ?
324 -- YonedaInjective A eq = ≡-cong ( λ y → inv A y ) eq 338
339 a2 : ( a b : Set ) (f : a → a ) (g : b → a ) -> f ≅ g → a ≡ b
340 a2 a b f g eq = {!!}
341
342 -- YonedaInjective : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A}
343 -- → FObj (FObj (YonedaFunctor A ) a ) a ≅ FObj (FObj (YonedaFunctor A ) a ) b
344 -- → a ≡ b
345 -- YonedaInjective A {a} {b} eq = {!!}
346
347