Mercurial > hg > Members > kono > Proof > category

changeset 302:c5b2656dbec6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
looped.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 30 Oct 2013 19:35:14 +0900
parents 93cf0a6c21fe
children 7f40d6a51c72
files pullback.agda
diffstat 1 files changed, 32 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Sun Sep 29 14:43:47 2013 +0900
+++ b/pullback.agda	Wed Oct 30 19:35:14 2013 +0900
@@ -44,7 +44,8 @@
               π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21  {d} {π1'} {π2'} {eq} ;
               uniqueness = uniqueness1
       } where
-      commute1 :  A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ]
+      commute1 :  A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] 
+                    ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ]
       commute1 = let open ≈-Reasoning (A) in
              begin
                     f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
@@ -102,7 +103,8 @@
              ≈⟨ π2fxg=g prod ⟩
                      π2'
              ∎
-      uniqueness1 :  {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
+      uniqueness1 :  {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} 
+         {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
         {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
         {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
         A [ p1 eq ≈ p' ]
@@ -331,10 +333,35 @@
       ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
       ip-cong : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
                 → ( ∀ (i : I ) →  A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ]
-      -- another form of uniquness
-      ip-uniquness1 : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I }  → ( product' : Hom A q p ) 
-          → A [ A [ ( pi i )  o product' ] ≈  (qi i) ]
+   -- another form of uniquness
+   ip-uniquness1 : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) 
+          → ( ∀ { i : I } →  A [ A [ ( pi i )  o product' ] ≈  (qi i) ] )
           → A [ product'  ≈ product qi ]
+   ip-uniquness1 {a} qi product' eq =  let  open ≈-Reasoning (A) in begin
+           product'
+         ≈↑⟨ ip-uniqueness ⟩
+           product (λ i₁ → A [ pi i₁ o product' ])
+         ≈⟨ ip-cong ( λ i → begin
+           pi i o product'
+         ≈⟨ eq {i} ⟩
+           qi i
+         ∎ ) ⟩
+           product qi
+         ∎ 
+   pif=q1' :   { i : I } → { qi : (j : I ) →  Hom A p (ai j) } → A [ pi i ≈  qi i ]
+   pif=q1' {i} {qi} = let  open ≈-Reasoning (A) in begin
+           pi i
+         ≈↑⟨ idR ⟩
+           pi i o id1 A p
+         ≈⟨ cdr ( ip-uniquness1 {p} qi (id1 A p) ( begin
+           pi ? o id1 A p
+         ≈⟨ {!!} ⟩
+           qi ?
+         ∎ )) ⟩
+           pi i o product qi
+         ≈⟨ pif=q {p} qi {i} ⟩
+           qi i
+         ∎ 
 
 open IProduct
 open Equalizer