Mercurial > hg > Members > kono > Proof > category

changeset 263:c1b3193097ce

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 Fri, 20 Sep 2013 19:03:57 +0900
parents e1b08c5e4d2e
children 78ce12f8e6b6
files pullback.agda
diffstat 1 files changed, 13 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Fri Sep 20 18:58:32 2013 +0900
+++ b/pullback.agda	Fri Sep 20 19:03:57 2013 +0900
@@ -87,8 +87,8 @@
              ≈⟨ π1fxg=f prod ⟩
                      π1'
              ∎
--- π1fxg=f  prod 
-      π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ]
+      π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → 
+            A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ]
       π2p=π21  {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
              begin
                      ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
@@ -105,4 +105,14 @@
         {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' ]
-      uniqueness1 = {!!}
+      uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} = let open ≈-Reasoning (A) in
+             begin
+                 p1 eq
+             ≈⟨⟩
+                 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq)
+             ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) {!!} ⟩
+                 {!!} o {!!}
+             ≈⟨ {!!} ⟩
+                 p'
+             ∎
+