Mercurial > hg > Members > kono > Proof > category
changeset 955:5c8694236ff3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 21 Feb 2021 04:23:24 +0900 |
| parents | 6aa6cbf630a0 |
| children | 468288f3dfe5 |
| files | src/equalizer.agda |
| diffstat | 1 files changed, 30 insertions(+), 175 deletions(-) [+] |
line wrap: on
line diff
--- a/src/equalizer.agda Sun Feb 21 03:34:36 2021 +0900 +++ b/src/equalizer.agda Sun Feb 21 04:23:24 2021 +0900 @@ -23,27 +23,8 @@ -- -- Burroni's Flat Equational Definition of Equalizer -- -record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where - field - α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (e : Hom A c a ) → Hom A c a - γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c - δ : {a b c : Obj A } → (e : Hom A c a ) → (f : Hom A a b) → Hom A a c - cong-α : {a b c : Obj A } → { e : Hom A c a } - → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ α f g e ≈ α f g' e ] - cong-γ : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] - → A [ γ {a} {b} {c} {d} f g h ≈ γ f g h' ] - cong-δ : {a b c : Obj A } → {e : Hom A c a} → {f f' : Hom A a b} → A [ f ≈ f' ] → A [ δ e f ≈ δ e f' ] - b1 : A [ A [ f o α {a} {b} {c} f g e ] ≈ A [ g o α {a} {b} {c} f g e ] ] - b2 : {d : Obj A } → {h : Hom A d a } → A [ A [ ( α {a} {b} {c} f g e ) o (γ {a} {b} {c} f g h) ] ≈ A [ h o α (A [ f o h ]) (A [ g o h ]) (id1 A d) ] ] - b3 : {a b d : Obj A} → (f : Hom A a b ) → {h : Hom A d a } → A [ A [ α {a} {b} {d} f f h o δ {a} {b} {d} h f ] ≈ id1 A a ] - -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ] - b4 : {d : Obj A } {k : Hom A d c} → - A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g e o k ] ) o ( δ {d} {b} {d} (id1 A d) (A [ f o A [ α {a} {b} {c} f g e o k ] ] ) )] ≈ k ] - -- A [ α f g o β f g h ] ≈ h - β : { d a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c - β {d} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ {d} {b} {d} (id1 A d) (A [ f o h ]) ] -record Burroni' { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where +record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where field equ : {a b : Obj A } → (f g : Hom A a b) → Obj A α : {a b : Obj A } → (f g : Hom A a b) → Hom A (equ f g) a @@ -57,6 +38,8 @@ b3 : {d : Obj A} → {h : Hom A d a } → A [ A [ α f f o δ f f (≈-Reasoning.refl-hom A) ] ≈ id1 A a ] b4 : {d : Obj A } {h : Hom A d a } {k : Hom A d (equ f g)} → A [ A [ γ f g ( A [ α f g o k ] ) o ( δ (A [ f o A [ α f g o k ] ] ) (A [ g o A [ α f g o k ] ] ) b1k )] ≈ k ] + β : { d a b : Obj A} → (f g : Hom A a b) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d (equ f g) + β {d} {a} {b} f g h eq = A [ γ f g h o δ (A [ f o h ]) (A [ g o h ]) eq ] open Equalizer open IsEqualizer @@ -264,185 +247,57 @@ -- ---- -lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) - → ( eqa-e : {a b c : Obj A} → (f g : Hom A a b) → Hom A c a ) - → ( eqa : {a b c : Obj A} → (f g : Hom A a b) → IsEqualizer A (eqa-e f g) f g ) - → Burroni A {c} {a} {b} f g (eqa-e f g) -lemma-equ1 {a} {b} {c} f g eqa-e eqa = record { - α = λ {a} {b} {c} f g e → equalizer1 (eqa {a} {b} {c} f g ) ; -- Hom A c a - γ = λ {a} {b} {c} {d} f g h → k (eqa {a} {b} {c} f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) - (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d - δ = λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f ) {a} (id1 A a) (f1=f1 f); -- Hom A a c - cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ; - cong-γ = λ {a} {_} {c} {d} {f} {g} {h} {h'} eq → cong-γ1 {a} {c} {d} {f} {g} {h} {h'} eq ; - cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {f} {f'} f=f' ; - b1 = fe=ge (eqa {a} {b} {c} f g ) ; - b2 = λ {d} {h} → lemma-b2 {d} {h}; - b3 = lemma-b3 ; - b4 = lemma-b4 - } where - -- - -- e eqa f g f - -- c ---------→ a ------→b - -- ^ g - -- | - -- |k₁ = e eqa (f o (e (eqa f g))) (g o (e (eqa f g)))) - -- | - -- d - -- - -- - -- e o id1 ≈ e → k e ≈ id - - lemma-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer1 (eqa f f ) o k (eqa f f) (id1 A a) (f1=f1 f) ] ≈ id1 A a ] - lemma-b3 {a} {b} {d} f {h} = let open ≈-Reasoning (A) in - begin - equalizer1 (eqa f f) o k (eqa f f) (id a) (f1=f1 f) - ≈⟨ ek=h (eqa f f ) ⟩ - id a - ∎ - lemma-equ4 : {a b c d : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → - A [ A [ f o A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ] ] ] - lemma-equ4 {a} {b} {c} {d} f g h = let open ≈-Reasoning (A) in - begin - f o ( h o equalizer1 (eqa (f o h) ( g o h ))) - ≈⟨ assoc ⟩ - (f o h) o equalizer1 (eqa (f o h) ( g o h )) - ≈⟨ fe=ge (eqa (A [ f o h ]) (A [ g o h ])) ⟩ - (g o h) o equalizer1 (eqa (f o h) ( g o h )) - ≈↑⟨ assoc ⟩ - g o ( h o equalizer1 (eqa (f o h) ( g o h ))) - ∎ - cong-α1 : {a b c : Obj A } → { e : Hom A c a } - → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ equalizer1 (eqa {a} {b} {c} f g ) ≈ equalizer1 (eqa {a} {b} {c} f g' ) ] - cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = begin - equalizer1 (eqa f g) - ≈↑⟨ ek=h (eqa f g') ⟩ - equalizer1 (eqa f g') o k (eqa f g') (eqa-e f g) {!!} - ≈⟨ cdr ( uniqueness (eqa f g') {!!}) ⟩ - equalizer1 (eqa f g') o id1 A c - ≈⟨ idR ⟩ - equalizer1 (eqa f g') - ∎ where open ≈-Reasoning (A) - cong-γ1 : {a c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] → - A [ k (eqa f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ) )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) - ≈ k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ) )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ] - cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' = let open ≈-Reasoning (A) in begin - k (eqa f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) - ≈⟨ {!!} ⟩ - k (eqa f g) (A [ h o (eqa-e (A [ f o h' ]) (A [ g o h' ])) ] ) {!!} - ≈⟨ uniqueness (eqa f g) ( begin - eqa-e f g o k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) - ≈⟨ ek=h (eqa f g ) ⟩ - h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) - ≈↑⟨ car h=h' ⟩ - h o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) - ∎ )⟩ - k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) - ∎ - cong-δ1 : {a b c : Obj A} {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f ) (id1 A a) (f1=f1 f) ≈ - k (eqa {a} {b} {c} f' f' ) (id1 A a) (f1=f1 f') ] - cong-δ1 {a} {b} {c} {f} {f'} f=f' = let open ≈-Reasoning (A) in - begin - k (eqa {a} {b} {c} f f ) (id a) (f1=f1 f) - ≈⟨ uniqueness (eqa f f) ( begin - eqa-e f f o k (eqa {a} {b} {c} f' f' ) (id a) (f1=f1 f') - ≈⟨ {!!} ⟩ -- ≈⟨ ek=h (eqa {a} {b} {c} f' f' ) ⟩ - eqa-e f' f' o k (eqa {a} {b} {c} f' f' ) (id a) (f1=f1 f') - ≈⟨ ek=h (eqa {a} {b} {c} f' f' ) ⟩ - id a - ∎ )⟩ - k (eqa {a} {b} {c} f' f' ) (id a) (f1=f1 f') - ∎ - - lemma-b2 : {d : Obj A} {h : Hom A d a} → A [ - A [ equalizer1 (eqa f g) o k (eqa f g) (A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ] - ≈ A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ] ] - lemma-b2 {d} {h} = let open ≈-Reasoning (A) in - begin - equalizer1 (eqa f g) o k (eqa f g) (h o equalizer1 (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} {c} f g h) - ≈⟨ ek=h (eqa f g) ⟩ - h o equalizer1 (eqa (f o h ) ( g o h )) - ∎ - - lemma-b4 : {d : Obj A} {j : Hom A d c} → A [ - A [ k (eqa f g) (A [ A [ equalizer1 (eqa f g) o j ] o - equalizer1 (eqa (A [ f o A [ equalizer1 (eqa f g ) o j ] ]) (A [ g o A [ equalizer1 (eqa f g ) o j ] ])) ]) - (lemma-equ4 {a} {b} {c} f g (A [ equalizer1 (eqa f g) o j ])) - o k (eqa (A [ f o A [ equalizer1 (eqa f g) o j ] ]) (A [ f o A [ equalizer1 (eqa f g) o j ] ])) - (id1 A d) (f1=f1 (A [ f o A [ equalizer1 (eqa f g) o j ] ])) ] - ≈ j ] - lemma-b4 {d} {j} = let open ≈-Reasoning (A) in - begin - ( k (eqa f g) (( ( equalizer1 (eqa f g) o j ) o equalizer1 (eqa (( f o ( equalizer1 (eqa f g ) o j ) )) (( g o ( equalizer1 (eqa f g ) o j ) ))) )) - (lemma-equ4 {a} {b} {c} f g (( equalizer1 (eqa f g) o j ))) o - k (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer1 (eqa f g) o j ) ))) ) - ≈⟨ car ((uniqueness (eqa f g) ( begin - equalizer1 (eqa f g) o j - ≈↑⟨ idR ⟩ - (equalizer1 (eqa f g) o j ) o id d - ≈⟨ {!!} ⟩ -- here we decide e (fej) (gej)' is id d - ((equalizer1 (eqa f g) o j) o equalizer1 (eqa (f o equalizer1 (eqa f g ) o j) (g o equalizer1 (eqa f g ) o j))) - ∎ ))) ⟩ - j o k (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer1 (eqa f g) o j ) ))) - ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) ( begin - equalizer1 (eqa (f o equalizer1 (eqa f g ) o j) (f o equalizer1 (eqa f g ) o j)) o id d - ≈⟨ idR ⟩ - equalizer1 (eqa (f o equalizer1 (eqa f g ) o j) (f o equalizer1 (eqa f g ) o j)) - ≈⟨ {!!} ⟩ -- here we decide e (fej) (fej)' is id d - id d - ∎ ))) ⟩ - j o id d - ≈⟨ idR ⟩ - j - ∎ +lemma-equ1 : {a b : Obj A} (f g : Hom A a b) + → ({a b : Obj A} (f g : Hom A a b) → Equalizer A f g ) → Burroni A f g +lemma-equ1 {a} {b} f g eqa = record { + equ = λ f g → equalizer-c (eqa f g) + ; α = λ f g → equalizer (eqa f g) + ; γ = λ f g h → k (isEqualizer (eqa f g )) ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) + {!!} -- (fe=ge (isEqualizer (eqa (A [ f o h ] ) (A [ g o h ] )))) + ; δ = {!!} + ; b1 = fe=ge (isEqualizer (eqa f g )) + ; b2 = λ {d} {h} → {!!} + ; b3 = {!!} + ; b4 = {!!} + } -------------------------------- -- -- Bourroni equations gives an Equalizer -- -lemma-equ2 : {a b c : Obj A} (f g : Hom A a b) (e : Hom A c a ) - → ( bur : Burroni A {c} {a} {b} f g e ) → IsEqualizer A {c} {a} {b} (α bur f g e) f g -lemma-equ2 {a} {b} {c} f g e bur = record { +lemma-equ2 : {a b : Obj A} (f g : Hom A a b) + → ( bur : Burroni A f g ) → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g +lemma-equ2 {a} {b} f g bur = record { fe=ge = fe=ge1 ; k = k1 ; ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ; uniqueness = λ {d} {h} {eq} {k'} ek=h → uniqueness1 {d} {h} {eq} {k'} ek=h } where + c : Obj A + c = equ bur f g + e : Hom A c a + e = α bur f g k1 : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - k1 {d} h fh=gh = β bur {d} {a} {b} f g h - fe=ge1 : A [ A [ f o (α bur f g e) ] ≈ A [ g o (α bur f g e) ] ] + k1 {d} h fh=gh = β bur {d} {a} {b} f g h fh=gh + fe=ge1 : A [ A [ f o (α bur f g ) ] ≈ A [ g o (α bur f g ) ] ] fe=ge1 = b1 bur - ek=h1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ (α bur f g e) o k1 {d} h eq ] ≈ h ] + ek=h1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ (α bur f g ) o k1 {d} h eq ] ≈ h ] ek=h1 {d} {h} {eq} = let open ≈-Reasoning (A) in begin - α bur f g e o k1 h eq - ≈⟨⟩ - α bur f g e o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h) ) - ≈⟨ assoc ⟩ - ( α bur f g e o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} (id d) (f o h) - ≈⟨ car (b2 bur) ⟩ - ( h o ( α bur ( f o h ) ( g o h ) (id d))) o δ bur {d} {b} {d} (id d) (f o h) - ≈↑⟨ assoc ⟩ - h o ((( α bur ( f o h ) ( g o h ) (id d ))) o δ bur {d} {b} {d} (id d) (f o h) ) + α bur f g o k1 h eq ≈⟨ {!!} ⟩ - h o ((( α bur ( f o h ) ( f o h ) (id d ))) o δ bur {d} {b} {d} (id d) (f o h) ) - ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id d} ) ⟩ h o id d ≈⟨ idR ⟩ h ∎ uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → - A [ A [ (α bur f g e) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] + A [ A [ (α bur f g ) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] uniqueness1 {d} {h} {eq} {k'} ek=h = let open ≈-Reasoning (A) in begin k1 {d} h eq - ≈⟨⟩ - γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h) - ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩ - γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) (f o h) - ≈↑⟨ cdr (cong-δ bur (resp ek=h refl-hom )) ⟩ - γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) ( f o ( α bur f g e o k') ) + ≈⟨ {!!} ⟩ + {!!} ≈⟨ b4 bur ⟩ k' ∎