Mercurial > hg > Members > kono > Proof > category
changeset 262:e1b08c5e4d2e
uniqueness remains
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 20 Sep 2013 18:58:32 +0900 |
| parents | a2477147dfec |
| children | c1b3193097ce |
| files | pullback.agda |
| diffstat | 1 files changed, 56 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Fri Sep 20 16:55:22 2013 +0900 +++ b/pullback.agda Fri Sep 20 18:58:32 2013 +0900 @@ -21,6 +21,7 @@ -- ab -------> b -- ^ π2 -- | +-- | equalizer (f π1) (g π1) = ( π1' × π2' ) -- d -- @@ -43,13 +44,63 @@ 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 = {!!} + commute1 = let open ≈-Reasoning (A) in + begin + f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) + ≈⟨ assoc ⟩ + ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) + ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩ + ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) + ≈↑⟨ assoc ⟩ + g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) + ∎ + lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → + A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ] + lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in + begin + ( f o π1 ) o (prod × π1') π2' + ≈↑⟨ assoc ⟩ + f o ( π1 o (prod × π1') π2' ) + ≈⟨ cdr (π1fxg=f prod) ⟩ + f o π1' + ≈⟨ eq ⟩ + g o π2' + ≈↑⟨ cdr (π2fxg=g prod) ⟩ + g o ( π2 o (prod × π1') π2' ) + ≈⟨ assoc ⟩ + ( g o π2 ) o (prod × π1') π2' + ∎ 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 + p1 {d'} { π1' } { π2' } eq = + let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 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 [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ] + π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in + begin + ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq + ≈⟨⟩ + ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) + ≈↑⟨ assoc ⟩ + π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) + ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ + π1 o (_×_ prod π1' π2' ) + ≈⟨ π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 = {!!} -- π2fxg=g prod + π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 + ≈⟨⟩ + ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) + ≈↑⟨ assoc ⟩ + π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) + ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ + π2 o (_×_ prod π1' π2' ) + ≈⟨ π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' ] ]} → {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' ]} →