Mercurial > hg > Members > kono > Proof > category

changeset 261:a2477147dfec

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
pull back continue
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 20 Sep 2013 16:55:22 +0900
parents a87d3ea9efe4
children e1b08c5e4d2e
files pullback.agda
diffstat 1 files changed, 25 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Fri Sep 20 15:39:50 2013 +0900
+++ b/pullback.agda	Fri Sep 20 16:55:22 2013 +0900
@@ -24,30 +24,34 @@
 --     d   
 --
 
-pullback-from :  (a b c ab : Obj A) 
+open Equalizer
+open Product
+open Pullback
+
+pullback-from :  (a b c ab d : Obj A) 
       ( f : Hom A a c )    ( g : Hom A b c )
-      ( π1 : Hom A ab a )  ( π2 : Hom A ab b )
+      ( π1 : Hom A ab a )  ( π2 : Hom A ab b ) ( e : Hom A d ab )
       ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g ) 
-      ( prod : Product A a b ab π1 π2 ) → Pullback A a b c ab f g π1 π2
-pullback-from  a b c ab f g π1 π2  eqa prod =  record {
+      ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g 
+          ( A [  π1 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] )
+          ( A [  π2 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] ) 
+pullback-from  a b c ab d f g π1 π2 e eqa prod =  record {
               commute = commute1 ;
               p = p1 ; 
-              π1p=π1 = π1p=π11 ; 
-              π2p=π2 = π2p=π21 ;
+              π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11  {d} {π1'} {π2'} {eq} ; 
+              π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21  {d} {π1'} {π2'} {eq} ; 
               uniqueness = uniqueness1
       } where 
-      commute1 : A [ A [ f  o π1 ] ≈ A [ g  o π2 ] ]
-      commute1 = ?
-      p1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → A [ A [ f  o π1' ] ≈ A [ g  o π2' ] ] → Hom A d ab
-      p1 {d} { π1' } { π2' } eq  = ?
-      π1p=π11 :  { 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 [ π1  o p1 eq ] ≈  π1' ] 
-      π1p=π11  { d }  { π1' } { π2' } { eq }  = ?
-      π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 [ π2  o p1 eq ] ≈  π2' ] 
-      π2p=π21  { d }  { π1' } { π2' } { eq }  = ?
-      uniqueness1 : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f  o π1' ] ≈ A [ g  o π2' ] ]  } 
-             →  { π1p=π1' : A [ A [ π1  o p' ] ≈  π1' ] }
-             →  { π2p=π2' : A [ A [ π2  o p' ] ≈  π2' ] }
-             →  A [ p1 eq  ≈ p' ]
-      uniqueness1 { d } p' { π1' } { π2' } { eq }{ π1p=π1' } { π2p=π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 = {!!}
+      p1 :  {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d
+      p1 {d'} { π1' } { π2' } eq  = -- _×_ prod π1' π2'
+      π1p=π11 :   {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 [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ]
+      π1p=π11   = {!!} -- π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  = {!!} -- π2fxg=g  prod 
+      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' ]
+      uniqueness1 = {!!}