Mercurial > hg > Members > kono > Proof > category

changeset 990:ac4db33b466f

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 22:49:03 +0900
parents e1df57b34712
children e7848ad0c6f9
files src/yoneda.agda
diffstat 1 files changed, 26 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/src/yoneda.agda	Fri Mar 05 19:08:11 2021 +0900
+++ b/src/yoneda.agda	Fri Mar 05 22:49:03 2021 +0900
@@ -313,54 +313,49 @@
              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 = {!!}
+postulate
+        eqObj0 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A}  → Hom A a b ≡ Hom A a' b' → a ≡ a'
+        eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A}  → Hom A a b ≡ Hom A a' b' → b ≡ b'
+        eqHom0 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → f ≡ f'
+        eqHom1 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → g ≡ g'
+        -- eqTMap : { y b : Obj A} { x z : Obj Sets} → {g h : NTrans (Category.op A) Sets (y-obj b) ? } {w : {!!} } → TMap g x {!!} ≡ TMap h x w → g ≡ h
 
 -- 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 = extensionality A (λ z →  begin
-             TMap g _ z ≡⟨ {!!} ⟩
-             TMap h _ z ∎ ) where  open ≡-Reasoning 
+             TMap g _ z ≡⟨  eqHom1 (cong (λ k → k z ) yg=yh ) ⟩
+             TMap h _ z ∎ ) where
+     open ≡-Reasoning 
+     ylem11 : {x : Obj A}  (z : FObj y x) → A [ f  o TMap g _ z ] ≡ A [ f o TMap h _ z ]
+     ylem11  z = (cong (λ k → k z ) yg=yh )
 
 -- 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 {a} {b} {x} {y} g h f gy=hy =  begin
-             g  ≈⟨ {!!} ⟩
-             h  ∎  where  open ≈-Reasoning SetsAop
+Yoneda-surjective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z →  begin
+             TMap g _ z  ≡⟨   {!!}  ⟩
+             ( Sets [ Sets [ FMap y {!!} o FMap y f ] o TMap g _  ] ) (id1 A _) ≡⟨ {!!} ⟩
+             ( Sets [  FMap y {!!} o Sets [ FMap y f  o TMap g _  ]  ] ) (id1 A _) ≡⟨ {!!} ⟩
+             ( Sets [  FMap y {!!}  o Sets [ TMap g _ o FMap (FObj YonedaFunctor _) f ]  ] ) (id1 A _) ≡⟨ {!!} ⟩
+             ( Sets [  FMap y {!!}  o Sets [ TMap h _ o FMap (FObj YonedaFunctor _) f ]  ] ) (id1 A _) ≡⟨ {!!} ⟩
+             ( Sets [ FMap y z o TMap g _  ] ) (id1 A _) ≡⟨ {!!} ⟩
+             ( Sets [ TMap g _ o FMap (FObj YonedaFunctor _) z ]) (id1 A _) ≡⟨ {!!} ⟩
+             TMap h _ z ∎ ) where
+     open ≡-Reasoning 
+     ylem12 : {y : Obj A} → TMap g y f ≡ TMap h y f
+     ylem12 = yg=yh
+     ylem10 : {y : Obj A} → (λ z  → TMap g y (A [ f o z ])) ≡ (λ z → TMap h y (A [ f o z ] ))
+     ylem10 = yg=yh
 
 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
+Yoneda-full-embed {a} {b} eq = eqObj1 A ylem1 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 )