Mercurial > hg > Members > kono > Proof > category

changeset 203:1c16d18a8d67

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 01 Sep 2013 15:21:53 +0900
parents 58ee98bbb333
children b2874c5086ea
files yoneda.agda
diffstat 1 files changed, 18 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Sun Sep 01 13:26:30 2013 +0900
+++ b/yoneda.agda	Sun Sep 01 15:21:53 2013 +0900
@@ -277,11 +277,11 @@
              ≡⟨  extensionality (λ g → (
                 begin
                     FMap F g (TMap ha a (Category.Category.Id A)) 
-                ≡⟨  Relation.Binary.PropositionalEquality.cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩
+                ≡⟨  ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩
                     TMap ha b (FMap (y-obj a) g (Category.Category.Id A))
                 ≡⟨⟩
                     TMap ha b ( (A Category.o Category.Category.Id A) g )
-                ≡⟨  Relation.Binary.PropositionalEquality.cong ( TMap ha b ) ( ≈-≡ (IsCategory.identityL  ( Category.isCategory A ))) ⟩
+                ≡⟨  ≡-cong ( TMap ha b ) ( ≈-≡ (IsCategory.identityL  ( Category.isCategory A ))) ⟩
                     TMap ha b g
                 ∎ 
              )) ⟩
@@ -304,6 +304,9 @@
 dom-equivalence : {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → Category.dom A f ≡ Category.dom A g
 dom-equivalence eq = refl
 
+-- dom-equivalence1 : {a b : Obj A} → {f : Hom A a a} -> {g : Hom A a b} → A [ f ≈ g ] → Category.dom A f ≡ Category.dom A g
+-- dom-equivalence1 eq = ?
+
 equive-elm : ∀{n} {a b : Set n} → (f : a ) → a ≡ b → b
 equive-elm f refl  = f
 
@@ -313,10 +316,19 @@
 -- equive-hom : {a b : Obj A } → {f : Hom A a b } → Hom A a b  ≡ Hom A a a → a ≡ b 
 -- equive-hom  {a} {b} {f} eq  = {!!}
 
---YondaLemma2 : {a b : Obj A }  → (λ x → FObj (FObj YonedaFunctor a) x)  ≡ (λ x → FObj (FObj YonedaFunctor b  ) x)  →  
---       {f : Hom A a b } → a ≡ b 
---YondaLemma2 {a} {b} eq  {f}  = ≡-cong (Category.cod ? ) eq
+inv :  {a x : Obj A} ( f : FObj (FObj YonedaFunctor a) x ) →  Obj A
+inv {a} {x} f =  Category.cod A f
+
+--YondaLemma2 : {a b : Obj A }  → (λ x → FObj (FObj YonedaFunctor a) x)  ≡ (λ x → FObj (FObj YonedaFunctor b  ) x)  →     
+--         a ≡ b 
+--YondaLemma2 {a} {b} eq  = ≡-cong inv ?
 
--- inv-yobj =  {a x : Obj A} →  Category.cod A (( FObj (FObj YonedaFunctor a) x))
+inv-yobj :  {a x : Obj A} →  Hom A a x → Obj A
+inv-yobj {a} {x} _ = a
+
+YonedaLemma21 :  (a x : Obj A) { f : ( FObj (FObj YonedaFunctor a) x) } →  Category.cod A f  ≡ a
+YonedaLemma21 a x {f} = refl
+
+---    f ≡  g     f x  ≡ g x
 
 -- I cannot prove this, please help.