Mercurial > hg > Members > kono > Proof > category

changeset 987:99c91423b871

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 10:20:20 +0900
parents e2e11014b0f8
children d81341fad6e1
files src/SetsCompleteness.agda src/yoneda.agda
diffstat 2 files changed, 105 insertions(+), 91 deletions(-) [+]
line wrap: on
line diff
--- a/src/SetsCompleteness.agda	Thu Mar 04 18:51:10 2021 +0900
+++ b/src/SetsCompleteness.agda	Fri Mar 05 10:20:20 2021 +0900
@@ -202,31 +202,28 @@
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
--- data cequ {c : Level} (A B : Set c)  ( f g : A → B ) :  Set c where
---     casef : (a : A) → {!!}
-
-record  cequ {c : Level} (A B : Set c)  ( f g : A → B ) :  Set c where
-   field
-      q : B → B
-      qo : (a : A) → q (f a) ≡ q (g a)
+data cequ {c : Level} {A B : Set c} ( f g : A → B )  :   Set c where
+    celem : (b : B)  → (a : A) → f a ≡  b → g a ≡ b →  cequ f g 
 
-data cequ' {c : Level} {A B : Set c} ( f g : A → B ) : {a : A } → (f a ≡ g a) →  Set c where
-    celem : {a : A } → (f=g : f a ≡ g a) →  cequ' f g f=g
+record  cequ' {c : Level} {A B : Set c} ( f g : A → B )  :   Set c where
+   field
+      cb : B
+      celem' : (a : A ) → f a ≡ cb → g a ≡ cb 
 
-c-equ  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b ) → (x : b) →  cequ a b f g 
-c-equ {_} {a} {b} f g x = record { q = {!!} ; qo = {!!} }
+c-equ  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } ( f g : Hom (Sets {c₂}) a b ) → b → cequ f g
+c-equ {_} {a} {b} f g = {!!} 
 
-SetsIsCoEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsCoEqualizer Sets (λ x → c-equ {c₂} f g x) f g
+SetsIsCoEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsCoEqualizer Sets (c-equ f g) f g
 SetsIsCoEqualizer {c₂} a b f g = record {
                ef=eg  = extensionality Sets {!!}
              ; k = k 
              ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq}
              ; uniqueness  = {!!}
        } where
-          k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets (cequ a b f g) d
+          k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets {!!} d
           k = {!!}
           ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] }
-           →   Sets [ Sets [ k h eq o c-equ f g ] ≈ h ]
+           →   Sets [ Sets [ k h eq o {!!} ] ≈ h ]
           ke=h = {!!}
 
 open Functor
--- a/src/yoneda.agda	Thu Mar 04 18:51:10 2021 +0900
+++ b/src/yoneda.agda	Fri Mar 05 10:20:20 2021 +0900
@@ -9,8 +9,7 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 open import Category.Sets
-module yoneda where 
--- { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
+module yoneda { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) where
 
 open import HomReasoning
 open import cat-utility
@@ -25,20 +24,20 @@
 
 open Functor
 
-YObj : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))
-YObj {_} {c₂} A = Functor (Category.op A) (Sets {c₂})
-YHom : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  (f : YObj A ) → (g : YObj A ) →  Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))
-YHom {_} {c₂} A f g = NTrans (Category.op A) (Sets {c₂}) f g
+YObj : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))
+YObj  = Functor (Category.op A) (Sets {c₂})
+YHom : ( f : YObj  ) → (g : YObj  ) →  Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))
+YHom  f g = NTrans (Category.op A) (Sets {c₂}) f g
 
 open NTrans 
-Yid : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : YObj A } → YHom A a a
-Yid {_} {c₂} A {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where
-   isNTrans1 : {a : YObj A } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x )
+Yid : {a : YObj } → YHom a a
+Yid {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where
+   isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x )
    isNTrans1 {a} = record { commute = refl  }
 
-_+_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b c : YObj A} → YHom A b c → YHom A a b → YHom A a c
-_+_ {_} {c₂} {_} {A} {a} {b} {c} f g  = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1  } where
-   commute1 :  (a b c : YObj A ) (f : YHom A b c)  (g : YHom A a b ) 
+_+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c
+_+_ {a} {b} {c} f g  = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1  } where
+   commute1 :  (a b c : YObj ) (f : YHom b c)  (g : YHom a b ) 
             (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) →
                         Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈
                         Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ]
@@ -58,13 +57,13 @@
    isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) 
    isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h }
 
-_==_  :  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : YObj A} → YHom A a b → YHom A a b → Set (c₂ ⊔ c₁)
-_==_  {_} { c₂} {_} {A} f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ]
+_==_  :  {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁)
+_==_  f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ]
 
 infix  4 _==_
 
-isSetsAop :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → IsCategory (YObj A) (YHom A) _==_ _+_ ( Yid A )
-isSetsAop {_} {c₂} {_} A =  
+isSetsAop : IsCategory (YObj) (YHom) _==_ _+_ ( Yid )
+isSetsAop  =  
   record  { isEquivalence =  record {refl = refl ; trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1  {_} {_} {i} {j}}
         ; identityL = refl
         ; identityR = refl
@@ -72,22 +71,22 @@
         ; associative = refl
         } where 
             open ≈-Reasoning (Sets {c₂}) 
-            sym1 : {a b : YObj A } {i j : YHom A a b } → i == j → j == i
+            sym1 : {a b : YObj } {i j : YHom a b } → i == j → j == i
             sym1 {a} {b} {i} {j} eq {x} = sym eq 
-            trans1 : {a b : YObj A } {i j k : YHom A a b} → i == j → j == k → i == k
+            trans1 : {a b : YObj } {i j k : YHom a b} → i == j → j == k → i == k
             trans1 {a} {b} {i} {j} {k} i=j j=k {x} =  trans-hom i=j j=k
-            o-resp-≈ : {A₁ B C : YObj A} {f g : YHom A A₁ B} {h i : YHom A B C} → 
+            o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → 
                 f == g → h == i → h + f == i + g
             o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = resp  f=g h=i
 
-SetsAop :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  → Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁)
-SetsAop {_} {c₂} {_} A  =
-  record { Obj = YObj A
-         ; Hom = YHom A
+SetsAop :  Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁)
+SetsAop  =
+  record { Obj = YObj
+         ; Hom = YHom
          ; _o_ = _+_
          ; _≈_ = _==_
-         ; Id  = Yid A
-         ; isCategory = isSetsAop A
+         ; Id  = Yid
+         ; isCategory = isSetsAop 
          }
 
 -- A is Locally small
@@ -105,8 +104,8 @@
 
 open import Function
 
-y-obj :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  (a : Obj A) → Functor (Category.op A) (Sets {c₂})
-y-obj {_} {c₂} {_} A a = record {
+y-obj :  (a : Obj A) → Functor (Category.op A) (Sets {c₂})
+y-obj a = record {
         FObj = λ b → Hom (Category.op A) a b  ;
         FMap =   λ {b c : Obj A } → λ ( f : Hom  A c b ) → λ (g : Hom  A b a ) →  (Category.op A) [ f o g ] ;
         isFunctor = record {
@@ -140,21 +139,21 @@
 --
 ----
 
-y-tmap :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → 
-     FObj (y-obj A a) x → FObj (y-obj A b ) x 
-y-tmap {_} {c₂} {_} A  a b f x = λ ( g : Hom A x a ) → A [ f o g ]  --  ( h : Hom A x b ) 
+y-tmap :   ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → 
+     FObj (y-obj a) x → FObj (y-obj b ) x 
+y-tmap a b f x = λ ( g : Hom A x a ) → A [ f o g ]  --  ( h : Hom A x b ) 
 
-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) 
-y-map  {_} {c₂} {_} A  {a} {b} f = record { TMap =  y-tmap A a b f ; isNTrans = isNTrans1 {a} {b} f } where
+y-map :  {a b : Obj A } → (f : Hom A a b ) → YHom (y-obj a) (y-obj b) 
+y-map  {a} {b} f = record { TMap =  y-tmap  a b f ; isNTrans = isNTrans1 {a} {b} f } where
    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 ) →
-        Sets [ Sets [ FMap (y-obj A b) g o y-tmap A a b f a₁ ] ≈
-        Sets [ y-tmap A a b f b₁ o FMap (y-obj A a) g ] ]
+        Sets [ Sets [ FMap (y-obj b) g o y-tmap  a b f a₁ ] ≈
+        Sets [ y-tmap  a b f b₁ o FMap (y-obj a) g ] ]
    lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ {_} {_} {_} {A} ( begin
                 A [ A [ f o x ] o g ]
              ≈↑⟨ assoc ⟩
                 A [ f o A [ x  o g ] ]
              ∎ ) )
-   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 )
+   isNTrans1 : {a b : Obj A } →  (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) (y-obj b) (y-tmap  a b f )
    isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } 
 
 -----
@@ -163,10 +162,10 @@
 --
 -----
 
-YonedaFunctor :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  → Functor A (SetsAop A)
-YonedaFunctor A = record {
-         FObj = λ a → y-obj A a
-       ; FMap = λ f → y-map A f
+YonedaFunctor :  Functor A SetsAop 
+YonedaFunctor  = record {
+         FObj = λ a → y-obj a
+       ; FMap = λ f → y-map f
        ; isFunctor = record {
              identity =  identity
              ; distr = distr1
@@ -174,24 +173,24 @@
 
         } 
   } where
-        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop A [ y-map A f ≈ y-map A g ]
-        ≈-cong {a} {b} {f} {g} eq  =  let open ≈-Reasoning (A) in  -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
+        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map  f ≈ y-map  g ]
+        ≈-cong {a} {b} {f} {g} eq  =  let open ≈-Reasoning A in  -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
              extensionality A ( λ h → ≈-≡ {_} {_} {_} {A}  ( begin
                 A [ f o h ]
              ≈⟨ resp refl-hom eq ⟩
                 A [ g o h ]
              ∎
           ) ) 
-        identity : {a : Obj A} → SetsAop A [ y-map A (id1 A a) ≈ id1 (SetsAop A) (y-obj A a )  ]
-        identity  {a} =  let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
+        identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a )  ]
+        identity  {a} =  let open ≈-Reasoning A in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
              extensionality A ( λ g →  ≈-≡ {_} {_} {_} {A}  ( begin
                 A [ id1 A a o g ] 
              ≈⟨ idL ⟩
                 g
              ∎
           ) )  
-        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 ] ]
-        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₁ ] ] )
+        distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-map (A [ g o f ]) ≈ SetsAop [ y-map g o y-map f ] ]
+        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₁ ] ] )
            extensionality A ( λ h →  ≈-≡ {_} {_} {_} {A}  ( begin
                 A [ A [ g o f ]  o h ]
              ≈↑⟨ assoc  ⟩
@@ -208,35 +207,35 @@
 --      x ∈ F(a) , (g : Hom A b a)  → ( FMap F g ) x
 ------
 
-F2Natmap :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a : Obj A} → {F : Obj ( SetsAop A) } 
-     → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj A a) b) (FObj F b)
-F2Natmap  A {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x
+F2Natmap :  {a : Obj A} → {F : Obj SetsAop  } 
+     → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj a) b) (FObj F b)
+F2Natmap  {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x
 
-F2Nat :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a : Obj A} → {F : Obj (SetsAop A )} →  FObj F a  → Hom (SetsAop A) (y-obj A a) F
-F2Nat {_} {c₂}  A {a} {F} x = record { TMap = F2Natmap A {a} {F} {x} ; isNTrans = isNTrans1 } where
+F2Nat :   {a : Obj A} → {F : Obj SetsAop } →  FObj F a  → Hom SetsAop (y-obj a) F
+F2Nat  {a} {F} x = record { TMap = F2Natmap {a} {F} {x} ; isNTrans = isNTrans1 } where
    commute1 : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} (g : Hom A  a₁ a) →
                 (Sets [ FMap F f o  FMap F g ]) x ≡ FMap F (A [ g o  f ] ) x
    commute1 g =  let open ≈-Reasoning (Sets) in
             cong ( λ f → f x ) ( sym ( distr F )  )
    commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → 
-        Sets [ Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] ]
+        Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap  {a} {F} {x} b o FMap (y-obj  a) f ] ]
    commute {a₁} {b} {f} =  let open ≈-Reasoning (Sets) in
              begin
-                Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ]
+                Sets [ FMap F f o F2Natmap  {a} {F} {x} a₁ ]
              ≈⟨⟩
                 Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ]
              ≈⟨ extensionality A  ( λ (g : Hom A  a₁ a) → commute1 {a₁} {b} {f} g ) ⟩
-                Sets [  (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj A a) f ] 
+                Sets [  (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj  a) f ] 
              ≈⟨⟩
-                Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] 
+                Sets [ F2Natmap  {a} {F} {x} b o FMap (y-obj  a) f ] 
              ∎
-   isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) F (F2Natmap A {a} {F})
+   isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj  a) F (F2Natmap  {a} {F})
    isNTrans1 = record { commute = λ {a₁ b f}  →  commute {a₁} {b} {f} } 
 
 
 --  F(a) <- Nat(h_a,F)
-Nat2F :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj (SetsAop A) } →  Hom (SetsAop A) (y-obj A a) F  → FObj F a 
-Nat2F A {a} {F} ha =  ( TMap ha a ) (id1 A a)
+Nat2F :    {a : Obj A} → {F : Obj SetsAop  } →  Hom SetsAop  (y-obj  a) F  → FObj F a 
+Nat2F  {a} {F} ha =  ( TMap ha a ) (id1 A a)
 
 ----
 --
@@ -244,9 +243,9 @@
 --
 ----
 
-F2Nat→Nat2F :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a : Obj A } → {F : Obj (SetsAop A)} → (fa : FObj F a) 
-    →  Nat2F A {a} {F} (F2Nat A {a} {F} fa) ≡ fa 
-F2Nat→Nat2F A {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) (
+F2Nat→Nat2F :     {a : Obj A } → {F : Obj SetsAop } → (fa : FObj F a) 
+    →  Nat2F  {a} {F} (F2Nat  {a} {F} fa) ≡ fa 
+F2Nat→Nat2F  {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) (
              -- FMap F (Category.Category.Id A) fa ≡ fa
              begin
                ( FMap F (id1 A _ )) 
@@ -254,7 +253,7 @@
                 id1 Sets (FObj F a)
              ∎ )
 
-open  import  Relation.Binary.PropositionalEquality
+-- open  import  Relation.Binary.PropositionalEquality
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong 
 
@@ -262,18 +261,18 @@
 --     ha : NTrans (op A) Sets (y-obj {a}) F
 --                FMap F  g  o TMap ha a ≈   TMap ha b  o FMap (y-obj {a}) g
 
-Nat2F→F2Nat :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a : Obj A } → {F : Obj (SetsAop A)} → (ha : Hom (SetsAop A) (y-obj A a) F) 
-     →  SetsAop A [ F2Nat A {a} {F} (Nat2F A {a} {F} ha) ≈ ha ]
-Nat2F→F2Nat A {a} {F} ha {b} = let open ≡-Reasoning in
+Nat2F→F2Nat :  {a : Obj A } → {F : Obj SetsAop } → (ha : Hom SetsAop  (y-obj  a) F) 
+     →  SetsAop  [ F2Nat  {a} {F} (Nat2F  {a} {F} ha) ≈ ha ]
+Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in
              begin
-                TMap (F2Nat A {a} {F} (Nat2F A {a} {F} ha)) b
+                TMap (F2Nat  {a} {F} (Nat2F {a} {F} ha)) b
              ≡⟨⟩
                 (λ g → FMap F g (TMap ha a (Category.Category.Id A)))
              ≡⟨  extensionality A  (λ g → (
                 begin
                     FMap F g (TMap ha a (Category.Category.Id A)) 
                 ≡⟨  ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩
-                    TMap ha b (FMap (y-obj A a) g (Category.Category.Id A))
+                    TMap ha b (FMap (y-obj a) g (Category.Category.Id A))
                 ≡⟨⟩
                     TMap ha b ( (A Category.o Category.Category.Id A) g )
                 ≡⟨  ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL  ( Category.isCategory A ))) ⟩
@@ -288,9 +287,31 @@
 --    that is FMapp Yoneda is injective and surjective
 
 --  λ b g → (A Category.o f₁) g
-YondaLemma1 :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a a' : Obj A } {f : FObj (FObj (YonedaFunctor A) a) a' } 
-     → SetsAop A [ F2Nat A {a'} {FObj (YonedaFunctor A) a} f ≈ FMap (YonedaFunctor A) f ]
-YondaLemma1 A {a} {a'} {f} = refl
+YondaLemma1 :  {a a' : Obj A } {f : FObj (FObj YonedaFunctor  a) a' } 
+     → 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 )
+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 g _ z ≡⟨ {!!} ⟩
+             TMap h _ z ∎ )) where  open ≡-Reasoning
+
+-- full (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 = {!!}
 
 --  F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality )
 
@@ -321,15 +342,11 @@
 -- Instead we prove only
 --     inv ( FObj YonedaFunctor a )  ≡ a
 
-inv :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a x : Obj A} ( f : FObj (FObj (YonedaFunctor A) a) x)  →  Obj A
-inv A {a} f =  Category.cod A f
+inv :   {a x : Obj A} ( f : FObj (FObj YonedaFunctor  a) x)  →  Obj A
+inv {a} f =  Category.cod A f
 
-YonedaLemma21 :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a x : Obj A} ( f : ( FObj (FObj (YonedaFunctor A ) a) x) ) →  inv A f  ≡ a
-YonedaLemma21 A {a} {x} f = refl
-
-open import  Relation.Binary.HeterogeneousEquality
-a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
-a1 refl = refl
+YonedaLemma21 :  {a x : Obj A} ( f : ( FObj (FObj YonedaFunctor  a) x) ) →  inv f  ≡ a
+YonedaLemma21  {a} {x} f = refl
 
 -- YondaLemma3 :  {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )   →
 --     (a b x : Obj A )  → Hom A a x  ≅ Hom A b x  → a ≡ b