Mercurial > hg > Members > kono > Proof > category
diff equalizer.agda @ 222:0bc85361b7d0
iso of equalizer
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 05 Sep 2013 01:23:53 +0900 |
| parents | ea0407fb8f02 |
| children | 8b3aeba14b5e |
line wrap: on
line diff
--- a/equalizer.agda Wed Sep 04 20:35:43 2013 +0900 +++ b/equalizer.agda Thu Sep 05 01:23:53 2013 +0900 @@ -69,6 +69,89 @@ id1 A a ∎ +equalizer-eq-e : { a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {a} f g) → (eq : A [ f ≈ g ] ) → + A [ k eqa (id1 A a) (f1=g1 eq) ≈ id1 A a ] → + A [ e eqa ≈ id1 A a ] +equalizer-eq-e {a} {b} {f} {g} eqa eq k=1 = let open ≈-Reasoning (A) in + begin + e eqa + ≈↑⟨ idR ⟩ + e eqa o id1 A a + ≈↑⟨ cdr k=1 ⟩ + e eqa o k eqa (id1 A a) (f1=g1 eq) + ≈⟨ ek=h eqa ⟩ + id1 A a + ∎ + +-- e eqa f g f +-- c ----------> a ------->b +-- |^ +-- || +-- h || h-1 +-- v| +-- c' + +equalizer+iso : {a b c c' : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) → (h-1 : Hom A c' c ) → (h : Hom A c c' ) → + A [ A [ h-1 o h ] ≈ id1 A c ] → A [ A [ h o h-1 ] ≈ id1 A c' ] + → Equalizer A {c'} f g +equalizer+iso {a} {b} {c} {c'} {f} {g} eqa h-1 h h-1-id h-id = record { + e = A [ e eqa o h-1 ] ; + fe=ge = fe=ge1 ; + k = λ j eq → A [ h o k eqa j eq ] ; + ek=h = ek=h1 ; + uniqueness = uniqueness1 + } where + fe=ge1 : A [ A [ f o A [ e eqa o h-1 ] ] ≈ A [ g o A [ e eqa o h-1 ] ] ] + fe=ge1 = let open ≈-Reasoning (A) in + begin + f o ( e eqa o h-1 ) + ≈⟨ assoc ⟩ + (f o e eqa ) o h-1 + ≈⟨ car (fe=ge eqa) ⟩ + (g o e eqa ) o h-1 + ≈↑⟨ assoc ⟩ + g o ( e eqa o h-1 ) + ∎ + ek=h1 : {d : Obj A} {j : Hom A d a} {eq : A [ A [ f o j ] ≈ A [ g o j ] ]} → + A [ A [ A [ e eqa o h-1 ] o A [ h o k eqa j eq ] ] ≈ j ] + ek=h1 {d} {j} {eq} = let open ≈-Reasoning (A) in + begin + (e eqa o h-1 ) o ( h o k eqa j eq ) + ≈↑⟨ assoc ⟩ + e eqa o ( h-1 o ( h o k eqa j eq )) + ≈⟨ cdr assoc ⟩ + e eqa o (( h-1 o h ) o k eqa j eq ) + ≈⟨ cdr (car (h-1-id )) ⟩ + e eqa o (id1 A c o k eqa j eq ) + ≈⟨ cdr idL ⟩ + e eqa o (k eqa j eq ) + ≈⟨ ek=h eqa ⟩ + j + ∎ + uniqueness1 : {d : Obj A} {h' : Hom A d a} {eq : A [ A [ f o h' ] ≈ A [ g o h' ] ]} {j : Hom A d c'} → + A [ A [ A [ e eqa o h-1 ] o j ] ≈ h' ] → + A [ A [ h o k eqa h' eq ] ≈ j ] + uniqueness1 {d} {h'} {eq} {j} ej=h = let open ≈-Reasoning (A) in + begin + h o k eqa h' eq + ≈⟨ cdr (uniqueness eqa ( + begin + e eqa o ( h-1 o j ) + ≈⟨ assoc ⟩ + (e eqa o h-1 ) o j + ≈⟨ ej=h ⟩ + h' + ∎ + )) ⟩ + h o ( h-1 o j ) + ≈⟨ assoc ⟩ + (h o h-1 ) o j + ≈⟨ car h-id ⟩ + id1 A c' o j + ≈⟨ idL ⟩ + j + ∎ + -- e eqa f g f -- c ----------> a ------->b -- ^ ---> d ---> @@ -269,18 +352,43 @@ → Hom A c c' --- != id1 A c equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (fe=ge eqa) +f1=gh : { a b c d : Obj A } {f g : Hom A a b } → { e : Hom A c a } → { h : Hom A d c } → + (eq : A [ A [ f o e ] ≈ A [ g o e ] ] ) → A [ A [ f o A [ e o h ] ] ≈ A [ g o A [ e o h ] ] ] +f1=gh {a} {b} {c} {d} {f} {g} {e} {h} eq = let open ≈-Reasoning (A) in + begin + f o ( e o h ) + ≈⟨ assoc ⟩ + (f o e ) o h + ≈⟨ car eq ⟩ + (g o e ) o h + ≈↑⟨ assoc ⟩ + g o ( e o h ) + ∎ + -- -- -- e eqa f g f -- c ----------> a ------->b -- equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) - → A [ A [ equalizer-iso eqa eqa' o equalizer-iso eqa' eqa ] ≈ id1 A c' ] -equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' = let open ≈-Reasoning (A) in + { h : Hom A a c } → A [ A [ h o e eqa ] ≈ id1 A c ] → A [ A [ k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) ] ≈ id1 A c ] +equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' {h} rev = let open ≈-Reasoning (A) in begin - k eqa' (e eqa) (fe=ge eqa) o k eqa (e eqa' ) (fe=ge eqa' ) - ≈⟨ {!!} ⟩ - id1 A c' + k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) + ≈↑⟨ idL ⟩ + (id1 A c) o ( k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) ) + ≈↑⟨ car rev ⟩ + ( h o e eqa ) o ( k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) ) + ≈↑⟨ assoc ⟩ + h o ( e eqa o ( k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) ) ) + ≈⟨ cdr assoc ⟩ + h o (( e eqa o k eqa (e eqa' ) (fe=ge eqa')) o k eqa' (e eqa ) (fe=ge eqa) ) + ≈⟨ cdr ( car (ek=h eqa) ) ⟩ + h o ( e eqa' o k eqa' (e eqa ) (fe=ge eqa) ) + ≈⟨ cdr (ek=h eqa' ) ⟩ + h o e eqa + ≈⟨ rev ⟩ + id1 A c ∎ -- ke = e' k'e' = e → k k' = 1 , k' k = 1 @@ -289,9 +397,9 @@ -- x e = e -> x = id? -lemma-equ1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b) → +lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → ( {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → EqEqualizer A {c} f g -lemma-equ1 A {a} {b} {c} f g eqa = record { +lemma-equ1 {a} {b} {c} f g eqa = record { α = λ f g → e (eqa f g ) ; -- Hom A c a γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h o (e ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d δ = λ {a} f → k (eqa f f) (id1 A a) (lemma-equ2 f); -- Hom A a c @@ -342,30 +450,32 @@ ≈⟨ ek=h (eqa f g) ⟩ h o e (eqa (f o h ) ( g o h )) ∎ - lemma-equ6 : {d : Obj A} {k₁ : Hom A d c} → A [ - A [ k (eqa f g) (A [ A [ e (eqa f g) o k₁ ] o e (eqa (A [ f o A [ e (eqa f g) o k₁ ] ]) (A [ g o A [ e (eqa f g) o k₁ ] ])) ]) - (lemma-equ4 {a} {b} {c} f g (A [ e (eqa f g) o k₁ ])) o - k (eqa (A [ f o A [ e (eqa f g) o k₁ ] ]) (A [ f o A [ e (eqa f g) o k₁ ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ e (eqa f g) o k₁ ] ])) ] - ≈ k₁ ] - lemma-equ6 {d} {k₁} = let open ≈-Reasoning (A) in + lemma-equ6 : {d : Obj A} {j : Hom A d c} → A [ + A [ k (eqa f g) (A [ A [ e (eqa f g) o j ] o e (eqa (A [ f o A [ e (eqa f g) o j ] ]) (A [ g o A [ e (eqa f g) o j ] ])) ]) + (lemma-equ4 {a} {b} {c} f g (A [ e (eqa f g) o j ])) o + k (eqa (A [ f o A [ e (eqa f g) o j ] ]) (A [ f o A [ e (eqa f g) o j ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ e (eqa f g) o j ] ])) ] + ≈ j ] + lemma-equ6 {d} {j} = let open ≈-Reasoning (A) in begin - ( k (eqa f g) (( ( e (eqa f g) o k₁ ) o e (eqa (( f o ( e (eqa f g) o k₁ ) )) (( g o ( e (eqa f g) o k₁ ) ))) )) - (lemma-equ4 {a} {b} {c} f g (( e (eqa f g) o k₁ ))) o - k (eqa (( f o ( e (eqa f g) o k₁ ) )) (( f o ( e (eqa f g) o k₁ ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o k₁ ) ))) ) + ( k (eqa f g) (( ( e (eqa f g) o j ) o e (eqa (( f o ( e (eqa f g) o j ) )) (( g o ( e (eqa f g) o j ) ))) )) + (lemma-equ4 {a} {b} {c} f g (( e (eqa f g) o j ))) o + k (eqa (( f o ( e (eqa f g) o j ) )) (( f o ( e (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o j ) ))) ) ≈⟨ car ( uniqueness (eqa f g) ( begin - e (eqa f g) o k₁ + e (eqa f g) o j ≈⟨ {!!} ⟩ - (e (eqa f g) o k₁) o e (eqa (f o e (eqa f g) o k₁) (g o e (eqa f g) o k₁)) + (e (eqa f g) o j) o e (eqa (f o e (eqa f g) o j) (g o e (eqa f g) o j)) ∎ )) ⟩ - k₁ o k (eqa (( f o ( e (eqa f g) o k₁ ) )) (( f o ( e (eqa f g) o k₁ ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o k₁ ) ))) - ≈⟨ cdr ( uniqueness (eqa (( f o ( e (eqa f g) o k₁ ) )) (( f o ( e (eqa f g) o k₁ ) ))) ( begin - e (eqa (f o e (eqa f g) o k₁) (f o e (eqa f g) o k₁)) o id1 A d + j o k (eqa (( f o ( e (eqa f g) o j ) )) (( f o ( e (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o j ) ))) + ≈⟨ cdr ( uniqueness (eqa (( f o ( e (eqa f g) o j ) )) (( f o ( e (eqa f g) o j ) ))) ( begin + e (eqa (f o e (eqa f g) o j) (f o e (eqa f g) o j)) o id1 A d + ≈⟨ idR ⟩ + e (eqa (f o e (eqa f g) o j) (f o e (eqa f g) o j)) ≈⟨ {!!} ⟩ - id1 A d + id1 A d ∎ )) ⟩ - k₁ o id1 A d + j o id1 A d ≈⟨ idR ⟩ - k₁ + j ∎