Mercurial > hg > Members > kono > Proof > category

changeset 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 db59b8f954aa
children f27d966939f8
files CCC.agda applicative.agda monad→monoidal.agda monoid-monad.agda system-f.agda yoneda.agda
diffstat 6 files changed, 168 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/CCC.agda	Fri Mar 08 18:09:11 2019 +0900
+++ b/CCC.agda	Wed Apr 17 12:03:45 2019 +0900
@@ -4,8 +4,8 @@
 
 open import HomReasoning
 open import cat-utility
-open import Data.Product renaming (_×_ to _∧_)
-open import Category.Constructions.Product
+-- open import Data.Product renaming (_×_ to _∧_)
+-- open import Category.Constructions.Product
 open  import  Relation.Binary.PropositionalEquality
 
 open Functor
@@ -14,14 +14,6 @@
 --   ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
 --   ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
 
-record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
-          :  Set ( c₁  ⊔  c₂ ⊔ ℓ ⊔  c₁'  ⊔  c₂' ⊔ ℓ' ) where
-      field
-           ≅→ :  Hom A a b   → Hom B a' b'
-           ≅← :  Hom B a' b' → Hom A a b
-           iso→  : {f : Hom B a' b' }  → B [ ≅→ ( ≅← f) ≈ f ]
-           iso←  : {f : Hom A a b }    → A [ ≅← ( ≅→ f) ≈ f ]
-
 data One {c : Level} : Set c where
   OneObj : One   -- () in Haskell ( or any one object set )
 
@@ -44,14 +36,22 @@
          lemma {a} {b} {f} with f
          ... | OneObj = refl
 
+record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
+          :  Set ( c₁  ⊔  c₂ ⊔ ℓ ⊔  c₁'  ⊔  c₂' ⊔ ℓ' ) where
+      field
+           ≅→ :  Hom A a b   → Hom B a' b'
+           ≅← :  Hom B a' b' → Hom A a b
+           iso→  : {f : Hom B a' b' }  → B [ ≅→ ( ≅← f) ≈ f ]
+           iso←  : {f : Hom A a b }    → A [ ≅← ( ≅→ f) ≈ f ]
 
-record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A)
+
+record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) ( _×_ : {a b c : Obj A ) → Hom A c a  → Hom A c b → Hom A (a * b) )
           ( _*_ : Obj A → Obj A → Obj A  ) ( _^_ : Obj A → Obj A → Obj A  ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field
-       ccc-1 : {a : Obj A}     →  --   Hom A a one ≅ {*}
-                          IsoS A OneCat  a one OneObj OneObj  
+       ccc-1 : {a : Obj A}     →  --   Hom A a １ ≅ {*}
+                          IsoS A OneCat  a １ OneObj OneObj  
        ccc-2 : {a b c : Obj A} →  --  Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
-                          IsoS A (A × A) c (a * b) (c , c) (a , b)
+                          IsoS A A c (a * b) {!!} {!!}
        ccc-3 : {a b c : Obj A} →  -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c
                           IsoS A A  a (c ^ b) (a * b) c
         
@@ -61,11 +61,77 @@
        one : Obj A
        _*_ : Obj A → Obj A → Obj A
        _^_ : Obj A → Obj A → Obj A  
-       isCCC : IsCCC A one _*_ _^_
+       _×_ : Obj A → Obj A → Obj A  
+       isCCC : IsCCC A one _×_  _*_ _^_
+
+open import HomReasoning 
+
+record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+         ( １ : Obj A )
+         ( ○ : (a : Obj A ) → Hom A a １ )
+          ( _∧_ : Obj A → Obj A → Obj A  ) 
+          ( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  ) 
+          ( π : {a b : Obj A } → Hom A (a ∧ b) a ) 
+          ( π' : {a b : Obj A } → Hom A (a ∧ b) b ) 
+          ( _<=_ : (a b : Obj A ) → Obj A ) 
+          ( _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) ) 
+          ( ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a )
+             :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+     field
+       -- cartesian
+       e2  : {a : Obj A} → ∀ ( f : Hom A a １ ) →  A [ f ≈ ○ a ]
+       e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o < f , g > ] ≈ f ]
+       e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π' o < f , g > ] ≈ g ]
+       e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } →  A [ < A [ π o h ] , A [ π' o h  ] >  ≈ h ]
+       π-congl :  {a b c : Obj A} → { f f' : Hom A c a }{ g : Hom A c b } → A [ f ≈ f' ]  →  A [ < f , g >  ≈ < f' , g > ] 
+       π-congr :  {a b c : Obj A} → { f : Hom A c a }{ g g' : Hom A c b } → A [ g ≈ g' ]  →  A [ < f , g >  ≈ < f , g' > ] 
+       -- closed
+       e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } →  A [ A [ ε o < A [ (h *) o π ]  ,  π' > ] ≈ h ]
+       e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o < A [ k o  π ]  ,  π' > ] ) * ≈ k ]
 
-record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A) ( oneT : ( a : Obj A ) → Hom A a one )
-          ( _*_ : Obj A → Obj A → Obj A  ) ( _^_ : Obj A → Obj A → Obj A  ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+     e'2 : A [ ○ １ ≈ id1 A １ ]
+     e'2 = let open  ≈-Reasoning A in begin
+            ○ １
+        ≈↑⟨ e2 (id1 A １ ) ⟩
+           id1 A １
+        ∎
+     e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [  ○ b o f ] ≈ ○ a ]
+     e''2 {a} {b} {f} = let open  ≈-Reasoning A in begin
+           ○ b o f
+        ≈⟨ e2 (○ b o f) ⟩
+           ○ a
+        ∎
+     distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ]  ≈  < A [ f o h ] , A [ g o h ] > ]
+     distr {a} {b} {c} {d} {f} {g} {h} = let open  ≈-Reasoning A in begin
+            < f , g > o h
+        ≈↑⟨ e3c ⟩
+            < π o  < f , g > o h  , π' o  < f , g > o h  >
+        ≈⟨ π-congl assoc ⟩
+            < ( π o  < f , g > ) o h  , π' o  < f , g > o h  >
+        ≈⟨ π-congl (car e3a ) ⟩
+            < f o h  , π' o  < f , g > o h  >
+        ≈⟨ π-congr assoc ⟩
+            < f o h  , (π' o  < f , g > ) o h  >
+        ≈⟨  π-congr (car e3b ) ⟩
+            < f o h ,  g o h  >
+        ∎
+     _×_ :  {  a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e )
+     f × g  = λ h →  < A [ f o A [ π o h  ] ] , A [ g o A [ π' o h ] ] >
+
+record EqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field
-       e2  : {a : Obj A} { f : Hom A a one } →  A [ f ≈ oneT a ]
-       e3a : {!!}
+         １ : Obj A 
+         ○ : (a : Obj A ) → Hom A a １ 
+         _∧_ : Obj A → Obj A → Obj A   
+         <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  
+         π : {a b : Obj A } → Hom A (a ∧ b) a 
+         π' : {a b : Obj A } → Hom A (a ∧ b) b  
+         _<=_ : (a b : Obj A ) → Obj A 
+         _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
+         ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
+         isEqCCC : IsEqCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε 
 
+
+
+
+
--- a/applicative.agda	Fri Mar 08 18:09:11 2019 +0900
+++ b/applicative.agda	Wed Apr 17 12:03:45 2019 +0900
@@ -9,6 +9,7 @@
 open import Relation.Binary.Core
 open import Relation.Binary
 open import monoidal
+open import Relation.Binary.PropositionalEquality  hiding ( [_] )
 
 -----
 --
--- a/monad→monoidal.agda	Fri Mar 08 18:09:11 2019 +0900
+++ b/monad→monoidal.agda	Wed Apr 17 12:03:45 2019 +0900
@@ -16,7 +16,7 @@
 open import applicative 
 open import Category.Cat
 open import Category.Sets
-import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality  hiding ( [_] )
 
 -----
 --
--- a/monoid-monad.agda	Fri Mar 08 18:09:11 2019 +0900
+++ b/monoid-monad.agda	Wed Apr 17 12:03:45 2019 +0900
@@ -19,16 +19,21 @@
 
 
 record ≡-Monoid c : Set (suc c) where
-  infixl 7 _∙_
+  infixl 7 _*_
   field
     Carrier  : Set c
-    _∙_      : Op₂ Carrier
+    _*_      : Op₂ Carrier
     ε        : Carrier   -- id in Monoid
-    isMonoid : IsMonoid _≡_ _∙_ ε
+    isMonoid : IsMonoid _≡_ _*_ ε
 
 postulate M : ≡-Monoid c
 open ≡-Monoid
 
+infixl 7 _∙_
+
+_∙_   : ( m m' : Carrier M ) → Carrier M
+_∙_ m m' = _*_ M m m'
+
 A = Sets {c}
 
 -- T : A → (M x A)
@@ -36,7 +41,7 @@
 T : Functor A A
 T = record {
         FObj = λ a → (Carrier M) × a
-        ; FMap = λ f → map ( λ x → x ) f
+        ; FMap = λ f p → (proj₁ p , f (proj₂ p )) 
         ; isFunctor = record {
              identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
              ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
@@ -71,7 +76,7 @@
 -- μ : (m,(m',a)) → (m*m,a)
 
 muMap : (a : Obj A  ) → FObj T ( FObj T a ) → Σ (Carrier M) (λ x → a )
-muMap a ( m , ( m' , x ) ) = ( _∙_ M m  m'  ,  x )
+muMap a ( m , ( m' , x ) ) = ( m ∙ m' ,  x )
 
 Lemma-MM2 :  {a b : Obj A} {f : Hom A a b} →
         A [ A [ FMap T f o (λ x → muMap a x) ] ≈
@@ -96,13 +101,13 @@
 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b}  {x :  Σ A B } →  (((proj₁ x) , proj₂ x ) ≡ x )
 Lemma-MM33 =  _≡_.refl
 
-Lemma-MM34 : ∀( x : Carrier M  ) → ( (M ∙ ε M) x ≡ x  )
+Lemma-MM34 : ∀( x : Carrier M  ) → ε M ∙ x ≡ x  
 Lemma-MM34  x = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
 
-Lemma-MM35 : ∀( x : Carrier M  ) → ((M ∙ x) (ε M))  ≡ x
+Lemma-MM35 : ∀( x : Carrier M  ) → x ∙ ε M ≡ x
 Lemma-MM35  x = ( proj₂  ( IsMonoid.identity ( isMonoid M )) ) x
 
-Lemma-MM36 : ∀( x y z : Carrier M ) → ((M ∙ (M ∙ x) y) z)  ≡ (_∙_ M  x (_∙_ M y z ) )
+Lemma-MM36 : ∀( x y z : Carrier M ) → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z ) 
 Lemma-MM36  x y z = ( IsMonoid.assoc ( isMonoid M ))  x y z
 
 -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming )
@@ -115,13 +120,13 @@
                (∀ x y z  → f x y z ≡ g x y z )  → ( f ≡ g ) 
 extensionality30 eq = extensionality ( λ x → extensionality ( λ y → extensionality (eq x y) ) )
 
-Lemma-MM9  : ( λ(x : Carrier M) → ( M ∙ ε M ) x )  ≡ ( λ(x : Carrier M) → x ) 
+Lemma-MM9  :  (λ(x : Carrier M) → ( ε M ∙ x ))  ≡ ( λ(x : Carrier M) → x  )
 Lemma-MM9  = extensionality Lemma-MM34
 
-Lemma-MM10 : ( λ x →   ((M ∙ x) (ε M)))  ≡ ( λ x → x ) 
+Lemma-MM10 : ( λ x →   (x ∙ ε M))  ≡ ( λ x → x ) 
 Lemma-MM10  = extensionality Lemma-MM35
 
-Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z))  ≡ (λ x y z → ( _∙_ M  x (_∙_ M y z ) ))
+Lemma-MM11 : (λ x y z → ((x ∙ y ) ∙ z))  ≡ (λ x y z → ( x ∙ (y ∙ z ) ))
 Lemma-MM11 = extensionality30 Lemma-MM36 
 
 MonoidMonad : Monad A 
@@ -140,7 +145,7 @@
                 begin
                      TMap μ a o TMap η ( FObj T a )
                 ≈⟨⟩
-                    ( λ x → ((M ∙ ε M) (proj₁ x) , proj₂ x ))
+                    ( λ x →   ε M ∙ (proj₁ x) , proj₂ x )
                 ≈⟨  cong ( λ f → ( λ x →  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
                     ( λ (x : FObj T a) → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
@@ -153,7 +158,7 @@
                 begin
                      TMap μ a o (FMap T (TMap η a ))
                 ≈⟨⟩
-                    ( λ x → (M ∙ proj₁ x) (ε M) , proj₂ x )
+                    ( λ x → ( proj₁ x ∙ (ε M) , proj₂ x ))
                 ≈⟨  cong ( λ f → ( λ x →  ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 )  ⟩
                     ( λ x → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
@@ -166,11 +171,11 @@
                 begin
                       TMap μ a o TMap μ ( FObj T a ) 
                 ≈⟨⟩
-                      ( λ x → (M ∙ (M ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x)))
+                      ( λ x → (proj₁ x) ∙ (proj₁ (proj₂ x)) ∙ (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x)))
                 ≈⟨ cong ( λ f → ( λ x → 
                          (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x)))  )) ,  proj₂ (proj₂ (proj₂ x)) )
                          )) Lemma-MM11  ⟩
-                      ( λ x → (M ∙ proj₁ x) ((M ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
+                      ( λ x → ( proj₁ x) ∙(( proj₁ (proj₂ x)) ∙ (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
                 ≈⟨⟩
                       TMap μ a o FMap T (TMap μ a)
                 ∎
--- a/system-f.agda	Fri Mar 08 18:09:11 2019 +0900
+++ b/system-f.agda	Wed Apr 17 12:03:45 2019 +0900
@@ -12,6 +12,8 @@
 T X = λ(x y : X) → x
 
 F : {l : Level} (X : Set l) → Bool X
+
+
 F X = λ(x y : X) → y
 
 D : {l : Level} → {U : Set l} → U → U → Bool U → U
@@ -27,7 +29,7 @@
 _×_ {l} U V =  {X : Set l} → (U → V → X)  → X 
  
 <_,_> : {l : Level} {U V : Set l} → U → V → (U ×  V) 
-<_,_> {l} {U} {V} u v = λ X  → λ(x : U → V → X) → x u v
+<_,_> {l} {U} {V} u v = λ x → x u v 
 
 π1 : {l : Level} {U V : Set l} → (U ×  V) → U
 π1 {l} {U} {V}  t = t {U} (λ(x : U) → λ(y : V) → x)
@@ -44,8 +46,8 @@
 hoge : {l : Level} {U V : Set l} → U → V  → (U ×  V)
 hoge u v = < u , v >
 
--- lemma08 :  {l : Level} {U V : Set l } → {u : U } →  (t : U ×  V)  → < π1 t  , π2 t > ≡ t
--- lemma08 t = refl
+--lemma08 :  {l : Level} {X U V : Set l } → {x : X } → {u : U } →  (t : U ×  V)  → < π1 t  , π2 t > x ≡ t x
+--lemma08 t = refl
 
 -- Emp definision is still wrong...
 
@@ -62,8 +64,8 @@
 Emp  : {l : Level } → Set (suc l)
 Emp {l} = {X : Set l} → X 
 
--- ε :  {l : Level} {U : Set l} → Emp {l} → U
--- ε {l} {U} t =  t U
+ε :  {l : Level} {U : Set l} → Emp {l} → U
+ε {l} {U} t =  t {U}
 
 -- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} ) → (ε {l} {U → V} t) u ≡ ε {l} {V} t
 -- lemma103 u t = refl
@@ -88,10 +90,10 @@
 _+_ {l} U V = {X : Set l} → ( U → X ) → (V → X) → X
 
 ι1 : {l : Level } {U V : Set l} →  U →  U + V
-ι1 {l} {U} {V} u = λ{X} → λ(x : U → X) → λ(y : V → X ) → x u
+ι1 {l} {U} {V} u = λ x y → x u -- λ{X} → λ(x : U → X) → λ(y : V → X ) → x u
 
 ι2 : {l : Level } {U V : Set l} →  V →  U + V
-ι2 {l} {U} {V} v = λ{X} → λ(x : U → X) → λ(y : V → X ) → y v
+ι2 {l} {U} {V} v = λ x y → y v --λ{X} → λ(x : U → X) → λ(y : V → X ) → y v
 
 δ : {l : Level} { U V R S : Set l } → (R → U) → (S → U) → ( R + S ) → U
 δ {l} {U} {V} {R} {S} u v t = t {U} (λ(x : R) → u x) ( λ(y : S) → v y)
@@ -107,7 +109,7 @@
 _××_ {l} U V =  {X : Set l} → (U → V → X)  → X 
 
 <<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} → U → V → (U  ××   V) 
-<<_,_>> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v
+<<_,_>> {l} {U} {V} u v = λ x → x u v -- λ{X} → λ(x : U → V → X) → x u v
 
 
 Int : {l : Level } ( X : Set l ) → Set l
@@ -143,6 +145,9 @@
 ItInt : {l : Level} {X : Set l} → Int X → (X → Int X ) → ( Int X → Int X ) → Int X → Int X
 ItInt {l} {X} u g f t = λ z s → t (u z s) ( λ (w : X) → (f (g w)) z s )
 
+copy_int : {l l' : Level } { X X' : Set l } → Int (X → (X → X) → X) → Int X
+copy_int {_} {_} {X} {X'} x = It Zero S x
+
 R : {l : Level} { U X : Set l}   → U → ( U → Int X →  U ) → Int _ → U 
 R {l} {U} {X} u v t =  π1 ( It {suc l} {U ×  Int X} (< u , Zero >) (λ (x : U × Int X) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
 
@@ -159,6 +164,20 @@
 lemma22 : {l : Level} {X : Set l} ( x y : Int X ) → add x y  ≡ add'' x y
 lemma22 x y = refl
 
+lemma21 : {l : Level} {X : Set l} ( x y : Int X ) → add x Zero  ≡ x
+lemma21 x y = refl
+
+postulate extensionality : {l : Level } → Relation.Binary.PropositionalEquality.Extensionality l l
+
+--lemma23 : {l : Level} {X : Set l} ( x y : Int X ) → add x (S y)  ≡ S ( add x y )
+--lemma23 x y = extensionality ( λ z → {!!} )
+--   where
+--       lemma24 : {!!}
+--       lemma24 = {!!}
+
+-- lemma23 : {l : Level} {X : Set l} ( x y : Int X ) → add x y  ≡ add y x
+-- lemma23 x y = {!!}
+
 -- bad adder which modifies input type
 mul' : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X
 mul' {l} {X} x y = It Zero (add x) y
@@ -183,7 +202,7 @@
 
 
 -- lemma14 : {l : Level} {X : Set l} → (x y : Int X) → mul x y  ≡ mul y x
--- lemma14 x y = It {!!} {!!} {!!}
+-- lemma14 x y = {!!} -- It {!!} {!!} {!!}
 
 lemma15 : {l : Level} {X : Set l} (x y : Int X) → mul {l} {X} n2 n3  ≡ mul {l} {X} n3 n2
 lemma15 x y = refl
--- a/yoneda.agda	Fri Mar 08 18:09:11 2019 +0900
+++ b/yoneda.agda	Wed Apr 17 12:03:45 2019 +0900
@@ -165,7 +165,7 @@
 -----
 
 YonedaFunctor :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  → Functor A (SetsAop A)
-YonedaFunctor {_} {c₂} {_} A = record {
+YonedaFunctor A = record {
          FObj = λ a → y-obj A a
        ; FMap = λ f → y-map A f
        ; isFunctor = record {
@@ -299,10 +299,25 @@
 --
 -- But we cannot prove like this
 --     FObj YonedaFunctor a   ≡ FObj YonedaFunctor b → a  ≡ b
---     YondaLemma2 : {a b x : Obj A }  → (FObj (FObj YonedaFunctor a) x)  ≡ (FObj (FObj YonedaFunctor b  ) x)  →     
---         a ≡ b 
---     YondaLemma2 {a} {b} eq  = {!!}
+
+open import Relation.Nullary
+open import Data.Empty
+
+--YondaLemma2 :  {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )   →
+--     (a b x : Obj A )  → (FObj (FObj (YonedaFunctor A) a) x)  ≡ (FObj (FObj (YonedaFunctor A) b ) x)  → a ≡ b 
+--YondaLemma2 A a bx eq = {!!}
+
 --       N.B     = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b
+
+--record Category c₁ c₂ ℓ : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+--  infixr 9 _o_
+--  infix  4 _≈_
+--  field
+--    Obj : Set c₁
+--    Hom : Obj → Obj → Set c₂
+--YondaLemma31 :  {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )   →
+--     (a b x : Obj A )  → Hom A a x  ≡ Hom A b x  → a ≡ b 
+--YondaLemma31 A a b x eq = {!!}
 --
 -- Instead we prove only
 --     inv ( FObj YonedaFunctor a )  ≡ a
@@ -314,11 +329,19 @@
 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
--- 
--- YonedaInjective :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b x : Obj A}
---      → FObj (FObj (YonedaFunctor A ) a ) x ≡ FObj (FObj (YonedaFunctor A ) b ) x
---      → a ≡ b
--- YonedaInjective A eq =  ≡-cong ( λ y → inv A y ) eq
+
+-- YondaLemma3 :  {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )   →
+--     (a b x : Obj A )  → Hom A a x  ≅ Hom A b x  → a ≡ b 
+-- YondaLemma3 A a b x eq = {!!} -- ≡-cong (inv A) ?
+
+a2 :  ( a b : Set ) (f : a → a ) (g : b → a ) -> f ≅ g → a ≡ b
+a2 a b f g eq = {!!}
+
+-- YonedaInjective :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A}
+--          → FObj (FObj (YonedaFunctor A ) a ) a  ≅ FObj (FObj (YonedaFunctor A ) a ) b
+--          → a ≡ b
+-- YonedaInjective A {a} {b} eq = {!!}
+
+