Mercurial > hg > Members > kono > Proof > category

changeset 188:f4c9d7cbcbb9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Yoneda Functor Constructed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2013 10:14:59 +0900
parents 47d6a9bc3933
children c6ce3115cb1b
files yoneda.agda
diffstat 1 files changed, 26 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Thu Aug 29 00:54:15 2013 +0900
+++ b/yoneda.agda	Thu Aug 29 10:14:59 2013 +0900
@@ -159,6 +159,8 @@
          ; isCategory = isSetsAop
          }
 
+postulate extensionality1 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂
+
 YonedaFunctor : Functor A SetsAop
 YonedaFunctor = record {
          FObj = λ a → CF {a}
@@ -170,11 +172,32 @@
         } 
   } where
         ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-nat f ≈ y-nat g ]
-        ≈-cong {a} {b} {f} {g} eq = {!!} -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
+        ≈-cong {a} {b} {f} {g} eq =  let open ≈-Reasoning (A) in  -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
+           extensionality1 ( λ x → extensionality (
+             λ h →  ≈-≡  ( begin
+                A [ f o h ]
+             ≈⟨ resp refl-hom eq ⟩
+                A [ g o h ]
+             ∎
+          ) )  )
         identity : {a : Obj A} → SetsAop [ y-nat (id1 A a) ≈ id1 SetsAop (CF {a} )  ]
-        identity  {a} = {!!} -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
+        identity  {a} =  let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
+           extensionality1 ( λ x → extensionality (
+             λ g →  ≈-≡  ( 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 [ y-nat (A [ g o f ]) ≈ SetsAop [ y-nat g o y-nat f ] ]
-        distr1 {a} {b} {c} {f} {g} = {!!} -- (λ x g₁ → (A [  (A [ g o f]  o g₁ ]) ≡ (λ x x₁ → A [  g .o A [ f o x₁ ] ] )
+        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₁ ] ] )
+           extensionality1 ( λ x → extensionality (
+             λ h →  ≈-≡  ( begin
+                A [ A [ g o f ]  o h ]
+             ≈↑⟨ assoc  ⟩
+                A [  g o A [ f o h ] ]
+             ∎
+          ) )  )