Mercurial > hg > Members > kono > Proof > category
changeset 953:eb62812b5885
Topos written
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 19 Feb 2021 12:09:48 +0900 |
| parents | 61bc4fcba050 |
| children | 6aa6cbf630a0 |
| files | src/CCC.agda src/equalizer.agda |
| diffstat | 2 files changed, 33 insertions(+), 42 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCC.agda Fri Feb 19 11:29:03 2021 +0900 +++ b/src/CCC.agda Fri Feb 19 12:09:48 2021 +0900 @@ -144,7 +144,7 @@ (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field char-ker-id : {a b : Obj A } {h : Hom A a Ω} → (m : Hom A b a) → (mono : Mono A m) - → A [ char (equalizer (Ker h)) record { isMono = {!!} } ≈ h ] + → A [ char (equalizer (Ker h)) record { isMono = monic (Ker h) } ≈ h ] ker-char-iso : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → Iso A b ( equalizer-c (Ker ( char m mono ))) record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
--- a/src/equalizer.agda Fri Feb 19 11:29:03 2021 +0900 +++ b/src/equalizer.agda Fri Feb 19 12:09:48 2021 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} --- -- -- Equalizer @@ -97,10 +98,10 @@ -- || -- d -monoic : { c a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g) - → { i j : Hom A d (equalizer-c eqa) } +monic : { a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g) + → ( i j : Hom A d (equalizer-c eqa) ) → A [ A [ equalizer eqa o i ] ≈ A [ equalizer eqa o j ] ] → A [ i ≈ j ] -monoic {c} {a} {b} {d} {f} {g} eqa {i} {j} ei=ej = let open ≈-Reasoning (A) in begin +monic {a} {b} {d} {f} {g} eqa i j ei=ej = let open ≈-Reasoning (A) in begin i ≈↑⟨ uniqueness (isEqualizer eqa) ( begin equalizer eqa o i @@ -247,24 +248,24 @@ ---- lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) → - ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → IsEqualizer A e f g ) + ( 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 e -lemma-equ1 {a} {b} {c} f g e eqa = record { - α = λ {a} {b} {c} f g e → equalizer1 (eqa {a} {b} {c} f g {e} ) ; -- 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-equ1 {a} {b} {c} f g e eqa-e eqa = record { + α = λ {a} {b} {c} f g e → equalizer1 (eqa {a} {b} {c} f g ) ; -- Hom A c a -- eqa-e f g + γ = λ {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 {e} ) {a} (id1 A a) (f1=f1 f); -- Hom A a c + δ = λ {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} {e} {f} {f'} f=f' ; - b1 = fe=ge (eqa {a} {b} {c} f g {e}) ; + 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 + -- e eqa f g f -- c ---------→ a ------→b -- ^ g -- | -- |k₁ = e eqa (f o (e (eqa f g))) (g o (e (eqa f g)))) @@ -294,33 +295,23 @@ 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 {e} )≈ equalizer1 (eqa {a} {b} {c} f g' {e} ) ] - cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = let open ≈-Reasoning (A) in refl-hom - cong-γ1 : {a c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] → { e : Hom A c a} → - A [ k (eqa f g {e} ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) - ≈ k (eqa f g {e} ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ] - cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' {e} = let open ≈-Reasoning (A) in begin + → {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 = {!!} -- let open ≈-Reasoning (A) in refl-hom + 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 ) - ≈⟨ uniqueness (eqa f g) ( begin - e 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' ] ))) - ∎ )⟩ + ≈⟨ uniqueness (eqa f g) {!!} ⟩ 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} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a) (f1=f1 f) ≈ - k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') ] + cong-δ1 : {a b c : Obj A} {e : Hom A c 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} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in begin - k (eqa {a} {b} {c} f f {e} ) (id a) (f1=f1 f) - ≈⟨ uniqueness (eqa f f) ( begin - e o k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f') - ≈⟨ ek=h (eqa {a} {b} {c} f' f' {e} ) ⟩ - id a - ∎ )⟩ - k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f') + k (eqa {a} {b} {c} f f ) (id a) (f1=f1 f) + ≈⟨ uniqueness (eqa f f) {!!} ⟩ + k (eqa {a} {b} {c} f' f' ) (id a) (f1=f1 f') ∎ lemma-b2 : {d : Obj A} {h : Hom A d a} → A [ @@ -335,30 +326,30 @@ 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 {e}) o j ] ]) (A [ g o A [ equalizer1 (eqa f g {e} ) o j ] ])) ]) + 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 {e}) o j ) )) (( g o ( equalizer1 (eqa f g {e}) o j ) ))) )) + ( 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 {e}) o j) (g o equalizer1 (eqa f g {e}) o j))) + ≈⟨ {!!} ⟩ -- here we decide e (fej) (gej)' is id d + {!!} ∎ ))) ⟩ 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 {e} ) o j) (f o equalizer1 (eqa f g {e}) o j)) o id d + 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 {e}) o j) (f o equalizer1 (eqa f g {e}) o j)) - ≈⟨⟩ -- here we decide e (fej) (fej)' is id d - id d + 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 + {!!} ∎ ))) ⟩ j o id d ≈⟨ idR ⟩