Mercurial > hg > Members > kono > Proof > category

changeset 989:e1df57b34712

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Mar 2021 19:08:11 +0900
parents d81341fad6e1
children ac4db33b466f
files src/yoneda.agda
diffstat 1 files changed, 63 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/src/yoneda.agda	Fri Mar 05 10:55:45 2021 +0900
+++ b/src/yoneda.agda	Fri Mar 05 19:08:11 2021 +0900
@@ -291,27 +291,76 @@
      → SetsAop [ F2Nat  {a'} {FObj YonedaFunctor  a} f ≈ FMap YonedaFunctor  f ]
 YondaLemma1 {a} {a'} {f} = refl
 
-open import  Relation.Binary.HeterogeneousEquality hiding ([_])
-a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
-a1 refl = refl
-
 domF : (y :  Obj SetsAop) → {x : Obj (Category.op A)} → FObj y x → Obj A
 domF y {x} z = x
 
--- faithful (injective )
+YondaLemma2 :  {a a' b : Obj A } (f : Hom A a  a' ) →  NTrans (Category.op A) Sets (FObj YonedaFunctor a) (FObj YonedaFunctor a')
+YondaLemma2 f =  FMap YonedaFunctor  f
+
+YondaLemma3 :  {a a' b : Obj A } (f : Hom A a  a' ) → Hom A b a →  Hom A b a'
+YondaLemma3 {a} {a'} {b} f = TMap  (FMap YonedaFunctor  f) b 
+
+-- YondaLemma4 :  {a a' b : Obj A }  → (f : Hom A a  a' ) → Hom ? (id1 A b) f
+-- YondaLemma4 {a} {a'} {b} f = Hom A b a →  Hom A b a'
+
+_^ : {a a' b : Obj A } → (f : Hom A a  a' )  → Hom A b a →  Hom A b a' 
+_^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f
+
+f-unique : {a a' b : Obj A } (f : Hom A a  a' ) →  f ^ ≡ TMap  (FMap YonedaFunctor  f) b
+f-unique {a} {a'} {b} f  =  extensionality A  (λ g → begin
+             (f ^ ) g ≡⟨⟩
+             (FMap (FObj YonedaFunctor a') g) f ≡⟨⟩
+             A [ f o g ] ≡⟨⟩
+             TMap  (FMap YonedaFunctor  f) b g ∎  ) where  open ≡-Reasoning 
+
+--             {!!}  ≡⟨ Relation.Binary.PropositionalEquality.sym (cong (λ k → k (A [ f o z ])) (IsNTrans.commute (isNTrans (invY f))))  ⟩
+-- FObj (FObj YonedaFunctor a) c
+-- c  : Obj (Category.op A)
+-- g  : Category.Category.Hom A c a'
+invY : {a a' b : Obj A } (f : Hom A a  a' ) → Hom SetsAop (FObj YonedaFunctor a') (FObj YonedaFunctor a)
+invY  {a} {a'} {b} f = record { TMap = λ c g → A [ {!!} o g ] ; isNTrans = record { commute = {!!} } }
+
+inv1 :  {a a' b : Obj A } (f : Hom A a  a' ) → SetsAop [ SetsAop [ invY {a} {a'} {b} f o FMap YonedaFunctor  f ] ≈ id1 SetsAop _ ]
+inv1  {a} {a'} {b} f =  extensionality A (λ z →  begin
+             TMap (invY f) (domF (FObj YonedaFunctor a) z) (A [ f o z ] ) ≡⟨ {!!} ⟩
+             TMap (invY f) (domF (FObj YonedaFunctor a) z) ((FMap (FObj YonedaFunctor a') z) f) ≡⟨ {!!} ⟩
+             FMap (FObj YonedaFunctor a) z (TMap (invY f) _ f ) ≡⟨ {!!} ⟩
+             z ∎ ) where  open  ≡-Reasoning
+
+inv2 :  {a a' b : Obj A } (f : Hom A a  a' ) → SetsAop [ SetsAop [ FMap YonedaFunctor  f o invY {a} {a'} {b} f ] ≈ id1 SetsAop _ ]
+inv2  {a} {a'} {b} f = {!!}
+
+-- full (injective )
 Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a))  (f : Hom A a b )
     → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ]
     → SetsAop [  g ≈ h ]
-Yoneda-injective {a} {b} {x} {y} g h f yg=yh = begin
-             g   ≈⟨ {!!} ⟩
-             SetsAop [ {!!} o   SetsAop [ F2Nat f o g ] ] ≈⟨ {!!} ⟩
-             h  ∎  where  open ≈-Reasoning SetsAop
+Yoneda-injective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z →  begin
+             TMap g _ z ≡⟨ {!!} ⟩
+             TMap h _ z ∎ ) where  open ≡-Reasoning 
 
--- full (surjective)
+-- faithful (surjective)
 Yoneda-surjective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop (FObj YonedaFunctor b) y) (f : Hom A a b )
     → SetsAop [ SetsAop [ g o FMap YonedaFunctor f ] ≈ SetsAop [ h o FMap YonedaFunctor f ] ]
     → SetsAop [  g ≈ h ]
-Yoneda-surjective g h f gy=hy = {!!}
+Yoneda-surjective {a} {b} {x} {y} g h f gy=hy =  begin
+             g  ≈⟨ {!!} ⟩
+             h  ∎  where  open ≈-Reasoning SetsAop
+
+open import  Relation.Binary.HeterogeneousEquality as HE using (_≅_) 
+
+Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b
+Yoneda-full-embed {a} {b} eq = ylem2 where
+     ylem1 : Hom A a a ≡ Hom A a b
+     ylem1 = cong (λ k → FObj k a) eq
+     ylem3 : (f :  Hom A a a ) → Hom A a b
+     ylem3 f = subst ( λ k → k ) ylem1 f
+     postulate 
+        ylem0 :  Hom A a a ≡ Hom A a b → a ≡ b -- I still don't know how to do it
+        ylem2 :  Category.cod A (id1 A a) ≡ b
+     -- ylem2 = begin
+     --         Category.cod A (id1 A a) ≡⟨ HE.cong (λ k → Category.cod A k) (ylem4 (id1 A a)) ⟩
+     --         Category.cod A (ylem3 (id1 A a)) ≡⟨⟩
+     --         b ∎  where  open ≡-Reasoning 
 
 --  F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality )
 
@@ -319,6 +368,9 @@
 --
 -- But we cannot prove like this
 --     FObj YonedaFunctor a   ≡ FObj YonedaFunctor b → a  ≡ b
+a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
+a1 HE.refl = refl
+
 
 open import Relation.Nullary
 open import Data.Empty