Mercurial > hg > Members > kono > Proof > category
changeset 1069:849f85e543f1
char-cong
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 08 May 2021 10:04:34 +0900 |
| parents | 4e58611b1fb1 |
| children | ff1d4188f94d |
| files | src/CCC.agda src/CCCSets.agda src/ToposIL.agda src/cat-utility.agda src/equalizer.agda |
| diffstat | 5 files changed, 68 insertions(+), 73 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCC.agda Thu Apr 29 11:16:18 2021 +0900 +++ b/src/CCC.agda Sat May 08 10:04:34 2021 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} open import Level open import Category module CCC where @@ -206,15 +207,40 @@ open Mono +iso-mono : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {m : Hom A a b} ( mono : Mono A m ) (i : Iso A a c ) → Mono A (A [ m o Iso.≅← i ] ) +iso-mono A {a} {b} {c} {m} mono i = record { isMono = λ {d} f g → im f g } where + im : {d : Obj A} (f g : Hom A d c ) → A [ A [ A [ m o Iso.≅← i ] o f ] ≈ A [ A [ m o Iso.≅← i ] o g ] ] → A [ f ≈ g ] + im {d} f g mf=mg = begin + f ≈↑⟨ idL ⟩ + id1 A _ o f ≈↑⟨ car (Iso.iso← i) ⟩ + ( Iso.≅→ i o Iso.≅← i) o f ≈↑⟨ assoc ⟩ + Iso.≅→ i o (Iso.≅← i o f) ≈⟨ cdr ( Mono.isMono mono _ _ (if=ig mf=mg) ) ⟩ + Iso.≅→ i o (Iso.≅← i o g) ≈⟨ assoc ⟩ + ( Iso.≅→ i o Iso.≅← i) o g ≈⟨ car (Iso.iso← i) ⟩ + id1 A _ o g ≈⟨ idL ⟩ + g ∎ where + open ≈-Reasoning A + if=ig : ( m o Iso.≅← i ) o f ≈ ( m o Iso.≅← i ) o g → m o (Iso.≅← i o f ) ≈ m o ( Iso.≅← i o g ) + if=ig eq = trans-hom assoc (trans-hom eq (sym-hom assoc ) ) + + record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) ( Ω : Obj A ) ( ⊤ : Hom A (CCC.１ c) Ω ) (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ])) (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-uniqueness : {a b : Obj A } {h : Hom A a Ω} (m : Hom A b a) → (mono : Mono A m) + char-uniqueness : {a b : Obj A } {h : Hom A a Ω} → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ] + char-cong : {a b : Obj A } { m m' : Hom A b a } { mono : Mono A m } { mono' : Mono A m' } + → A [ m ≈ m' ] → A [ char m mono ≈ char m' mono' ] ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ]) + char-iso : {a b c : Obj A } {m : Hom A a b} {h : Hom A b Ω}( mono : Mono A m ) → ( i : Iso A a (equalizer-c (Ker h)) ) + → A [ char (A [ m o Iso.≅← i ]) (iso-mono A mono i) ≈ h ] + char-iso {a} {b} {c} {m} {h} mono i = begin + char ( m o Iso.≅← i ) (iso-mono A mono i) ≈⟨ char-cong {!!} ⟩ + char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h) }) ≈⟨ char-uniqueness {b} {a} {h} ⟩ + h ∎ where open ≈-Reasoning A ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a ker h = equalizer (Ker h) char-m=⊤ : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → A [ A [ char m mono o m ] ≈ A [ ⊤ o CCC.○ c b ] ]
--- a/src/CCCSets.agda Thu Apr 29 11:16:18 2021 +0900 +++ b/src/CCCSets.agda Sat May 08 10:04:34 2021 +0900 @@ -136,7 +136,7 @@ ; Ker = tker ; char = λ m mono → tchar m mono ; isTopos = record { - char-uniqueness = λ {a} {b} {h} m mono → extensionality Sets ( λ x → uniq h m mono x ) + char-uniqueness = λ {a} {b} {h} → extensionality Sets ( λ x → uniq h x ) ; ker-m = λ m mono → equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) } } where @@ -165,9 +165,9 @@ ... | case2 f = false -- imequ : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true ) o CCC.○ sets a ]) -- imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) - uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) → + uniq : {a : Obj (Sets {c})} (h : Hom Sets a Bool) (y : a) → tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y - uniq {a} {b} h m mono y with h y | inspect h y | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y + uniq {a} h y with h y | inspect h y | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y ... | true | record { eq = eqhy } | case1 x | record { eq = eq1 } = eq1 ... | true | record { eq = eqhy } | case2 x | record { eq = eq1 } = ⊥-elim (x (isImage (elem y eqhy))) ... | false | record { eq = eqhy } | case1 (isImage (elem x eq)) | record { eq = eq1 } = ⊥-elim ( ¬x≡t∧x≡f record {fst = eqhy ; snd = eq })
--- a/src/ToposIL.agda Thu Apr 29 11:16:18 2021 +0900 +++ b/src/ToposIL.agda Sat May 08 10:04:34 2021 +0900 @@ -104,37 +104,34 @@ _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] → A [ Poly.f q ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] -- --- iso ○ b --- e ⇐====⇒ b -----------→ 1 +-- iso ○ c +-- e ⇐====⇒ c -----------→ 1 -- | | | -- | h | | ⊤ -- | ↓ char h ↓ --- + ------→ 1 -----------→ Ω +-- + ------→ b -----------→ Ω -- ker h fp / fq -- - tl01 : {a b : Obj A} (p : Poly a (Topos.Ω t) b ) (q : Poly a (Topos.Ω t) b ) + tl01 : {a b : Obj A} (p q : Poly a (Topos.Ω t) b ) → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] tl01 {a} {b} p q p<q q<p = begin Poly.f p ≈↑⟨ tt p ⟩ char t (equalizer (Ker t (Poly.f p))) (mm p) ≈⟨ {!!} ⟩ char t (equalizer (Ker t (Poly.f q))) (mm q) ≈⟨ tt q ⟩ Poly.f q ∎ where - ek : (h : Hom A (equalizer-c (Ker t (Poly.f p))) (equalizer-c (Ker t (Poly.f q))) ) - → A [ IsEqualizer.k (Equalizer.isEqualizer (Ker t (Poly.f p))) (equalizer (Ker t (Poly.f q)) ∙ h) {!!} ≈ id1 A _ ] - ek = {!!} pm : {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] → A [ Poly.f q ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] pm h = p<q h qm : {c : Obj A} (h : Hom A c b ) → A [ Poly.f q ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] qm h = q<p h - idmono : {a : Obj A } → Mono A (id1 A a) - idmono = record { isMono = λ f g eq → trans-hom ( trans-hom (sym idL) eq ) idL } pp : Hom A b (Topos.Ω t) pp = Poly.f q open import equalizer using ( monic ) + ee : A [ equalizer (Ker t (Poly.f p)) ∙ {!!} ≈ equalizer (Ker t (Poly.f q )) ] + ee = IsEqualizer.ek=h (Equalizer.isEqualizer (Ker t (Poly.f p))) {{!!}} {{!!}} {{!!}} mm : (q : Poly a (Topos.Ω t) b ) → Mono A (equalizer (Ker t (Poly.f q))) mm q = record { isMono = λ f g → monic (Ker t (Poly.f q)) } tt : (q : Poly a (Topos.Ω t) b ) → A [ char t (equalizer (Ker t (Poly.f q))) (mm q) ≈ Poly.f q ] - tt q = IsTopos.char-uniqueness (Topos.isTopos t) {b} (equalizer (Ker t (Poly.f q))) (mm q) + tt q = IsTopos.char-uniqueness (Topos.isTopos t) {b} {a} module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P : Obj A → Obj A) (il : InternalLanguage Ω ⊤ P) (t : Topos A c) where open InternalLanguage il
--- a/src/cat-utility.agda Thu Apr 29 11:16:18 2021 +0900 +++ b/src/cat-utility.agda Sat May 08 10:04:34 2021 +0900 @@ -22,36 +22,8 @@ iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ] iso← : C [ C [ ≅→ o ≅← ] ≈ id1 C y ] - record IsoR {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) - {a b c : Obj C } - ( f : Hom C a b ) - ( g : Hom C a c ) - : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where - field - iso-R : Iso C b c - iso≈R : C [ C [ Iso.≅→ iso-R o f ] ≈ g ] - R≈iso : C [ C [ Iso.≅← iso-R o g ] ≈ f ] - R≈iso = begin Iso.≅← iso-R o g ≈↑⟨ cdr iso≈R ⟩ - Iso.≅← iso-R o (Iso.≅→ iso-R o f) ≈⟨ assoc ⟩ - (Iso.≅← iso-R o Iso.≅→ iso-R ) o f ≈⟨ car (Iso.iso→ iso-R ) ⟩ - id1 C _ o f ≈⟨ idL ⟩ - f ∎ where open ≈-Reasoning C - - record IsoL {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) - {a b c : Obj C } - ( f : Hom C b a ) - ( g : Hom C c a ) - : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where - field - iso-L : Iso C b c - iso≈L : C [ C [ f o Iso.≅← iso-L ] ≈ g ] - L≈iso : C [ C [ g o Iso.≅→ iso-L ] ≈ f ] - L≈iso = begin g o Iso.≅→ iso-L ≈↑⟨ car iso≈L ⟩ - (f o Iso.≅← iso-L ) o Iso.≅→ iso-L ≈↑⟨ assoc ⟩ - f o (Iso.≅← iso-L o Iso.≅→ iso-L ) ≈⟨ cdr (Iso.iso→ iso-L ) ⟩ - f o id1 C _ ≈⟨ idR ⟩ - f ∎ where open ≈-Reasoning C - + ≡-iso : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (x : Obj C ) → Iso C x x + ≡-iso C x = record { ≅→ = id1 C _ ; ≅← = id1 C _ ; iso→ = ≈-Reasoning.idL C ; iso← = ≈-Reasoning.idL C } record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A )
--- a/src/equalizer.agda Thu Apr 29 11:16:18 2021 +0900 +++ b/src/equalizer.agda Sat May 08 10:04:34 2021 +0900 @@ -115,16 +115,18 @@ -- c' equalizer+iso : {a b c' : Obj A } {f g : Hom A a b } → - ( eqa : Equalizer A f g ) → - (h-1 : Hom A c' (equalizer-c eqa) ) → (h : Hom A (equalizer-c eqa) c' ) → - A [ A [ h o h-1 ] ≈ id1 A c' ] → A [ A [ h-1 o h ] ≈ id1 A (equalizer-c eqa) ] - → IsEqualizer A (A [ equalizer eqa o h-1 ] ) f g -equalizer+iso {a} {b} {c'} {f} {g} eqa h-1 h hh-1=1 h-1h=1 = record { + ( eqa : Equalizer A f g ) → (iso : Iso A c' (equalizer-c eqa) ) + → IsEqualizer A (A [ equalizer eqa o Iso.≅→ iso ] ) f g -- h-1 +equalizer+iso {a} {b} {c'} {f} {g} eqa iso = record { fe=ge = fe=ge1 ; k = λ j eq → A [ h o k (isEqualizer eqa) j eq ] ; ek=h = ek=h1 ; uniqueness = uniqueness1 } where + h-1 : Hom A c' (equalizer-c eqa) + h-1 = Iso.≅→ iso + h : Hom A (equalizer-c eqa) c' + h = Iso.≅← iso e = equalizer eqa fe=ge1 : A [ A [ f o A [ e o h-1 ] ] ≈ A [ g o A [ e o h-1 ] ] ] fe=ge1 = f1=gh ( fe=ge (isEqualizer eqa) ) @@ -137,7 +139,7 @@ e o ( h-1 o ( h o k (isEqualizer eqa) j eq ) ) ≈⟨ cdr assoc ⟩ e o (( h-1 o h) o k (isEqualizer eqa) j eq ) - ≈⟨ cdr (car h-1h=1 ) ⟩ + ≈⟨ cdr (car ( Iso.iso← iso) ) ⟩ e o (id1 A (equalizer-c eqa) o k (isEqualizer eqa) j eq ) ≈⟨ cdr idL ⟩ e o k (isEqualizer eqa) j eq @@ -160,7 +162,7 @@ h o ( h-1 o j ) ≈⟨ assoc ⟩ (h o h-1 ) o j - ≈⟨ car hh-1=1 ⟩ + ≈⟨ car (Iso.iso→ iso) ⟩ id c' o j ≈⟨ idL ⟩ j @@ -168,55 +170,53 @@ equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g ) - → (m : Hom A c a) - → ( ker-iso : IsoL A m (equalizer equ) ) + → (m : Hom A c a) → ( iso : Iso A c (equalizer-c equ)) + → ( mm : A [ A [ equalizer equ o Iso.≅→ iso ] ≈ m ] ) → IsEqualizer A m f g -equalizerIso {a} {b} {c} f g equ m ker-iso = record { +equalizerIso {a} {b} {c} f g equ m iso mm = record { fe=ge = fe-ge - ; k = λ {d} h eq → A [ Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ] + ; k = λ {d} h eq → A [ Iso.≅← iso o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ] ; ek=h = ek=h1 ; uniqueness = uniqueness1 } where ker : Hom A ( equalizer-c equ ) a ker = equalizer equ - mm : A [ A [ equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso ) ] ≈ m ] - mm = IsoL.L≈iso ker-iso fe-ge : A [ A [ f o m ] ≈ A [ g o m ] ] fe-ge = begin f o m ≈↑⟨ cdr mm ⟩ - f o (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) ≈⟨ assoc ⟩ - (f o equalizer equ) o Iso.≅→ (IsoL.iso-L ker-iso) ≈⟨ car ( IsEqualizer.fe=ge (Equalizer.isEqualizer equ) ) ⟩ - (g o equalizer equ ) o Iso.≅→ (IsoL.iso-L ker-iso) ≈↑⟨ assoc ⟩ - g o (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) ≈⟨ cdr mm ⟩ + f o (equalizer equ o Iso.≅→ iso) ≈⟨ assoc ⟩ + (f o equalizer equ) o Iso.≅→ iso ≈⟨ car ( IsEqualizer.fe=ge (Equalizer.isEqualizer equ) ) ⟩ + (g o equalizer equ ) o Iso.≅→ iso ≈↑⟨ assoc ⟩ + g o (equalizer equ o Iso.≅→ iso) ≈⟨ cdr mm ⟩ g o m ∎ where open ≈-Reasoning A ek=h1 : {d : Obj A} {h : Hom A d a} {eq : A [ A [ f o h ] ≈ A [ g o h ] ]} → - A [ A [ m o (A Category.o Iso.≅← (IsoL.iso-L ker-iso)) (IsEqualizer.k (isEqualizer equ) h eq) ] ≈ h ] + A [ A [ m o (A Category.o Iso.≅← iso) (IsEqualizer.k (isEqualizer equ) h eq) ] ≈ h ] ek=h1 {d} {h} {eq} = begin - m o ( Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ car mm ⟩ - (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) o ( Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ assoc ⟩ - _ o (Iso.≅→ (IsoL.iso-L ker-iso) o ( Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq )) ≈⟨ cdr assoc ⟩ - equalizer equ o ((Iso.≅→ (IsoL.iso-L ker-iso) o Iso.≅← (IsoL.iso-L ker-iso)) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈⟨ cdr (car (Iso.iso← (IsoL.iso-L ker-iso))) ⟩ + m o ( Iso.≅← iso o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ car mm ⟩ + (equalizer equ o Iso.≅→ iso) o ( Iso.≅← iso o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ assoc ⟩ + _ o (Iso.≅→ iso o ( Iso.≅← iso o IsEqualizer.k (Equalizer.isEqualizer equ) h eq )) ≈⟨ cdr assoc ⟩ + equalizer equ o ((Iso.≅→ iso o Iso.≅← iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈⟨ cdr (car (Iso.iso← iso)) ⟩ equalizer equ o (id1 A _ o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈⟨ cdr idL ⟩ equalizer equ o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ≈⟨ IsEqualizer.ek=h (isEqualizer equ) ⟩ h ∎ where open ≈-Reasoning A 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 [ m o k' ] ≈ h ] - → A [ (A Category.o Iso.≅← (IsoL.iso-L ker-iso)) (IsEqualizer.k (isEqualizer equ) h eq) ≈ k' ] + → A [ (A Category.o Iso.≅← iso) (IsEqualizer.k (isEqualizer equ) h eq) ≈ k' ] uniqueness1 {d} {h} {eq} {k'} eqk = begin - Iso.≅← (IsoL.iso-L ker-iso) o (IsEqualizer.k (isEqualizer equ) h eq) ≈⟨ cdr ( IsEqualizer.uniqueness (Equalizer.isEqualizer equ) ( begin - equalizer equ o ((Iso.≅→ (IsoL.iso-L ker-iso)) o k' ) ≈⟨ assoc ⟩ - (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) o k' ≈⟨ car mm ⟩ + Iso.≅← iso o (IsEqualizer.k (isEqualizer equ) h eq) ≈⟨ cdr ( IsEqualizer.uniqueness (Equalizer.isEqualizer equ) ( begin + equalizer equ o ((Iso.≅→ iso) o k' ) ≈⟨ assoc ⟩ + (equalizer equ o Iso.≅→ iso) o k' ≈⟨ car mm ⟩ m o k' ≈⟨ eqk ⟩ h ∎ )) ⟩ - Iso.≅← (IsoL.iso-L ker-iso) o ( Iso.≅→ (IsoL.iso-L ker-iso) o k' ) ≈⟨ assoc ⟩ - (Iso.≅← (IsoL.iso-L ker-iso) o Iso.≅→ (IsoL.iso-L ker-iso) ) o k' ≈⟨ car (Iso.iso→ (IsoL.iso-L ker-iso) )⟩ + Iso.≅← iso o ( Iso.≅→ iso o k' ) ≈⟨ assoc ⟩ + (Iso.≅← iso o Iso.≅→ iso ) o k' ≈⟨ car (Iso.iso→ iso )⟩ id1 A _ o k' ≈⟨ idL ⟩ k' ∎ where open ≈-Reasoning A mequ : Equalizer A f g mequ = record { equalizer-c = c ; equalizer = m ; isEqualizer = record { fe=ge = fe-ge - ; k = λ {d} h fh=gh → A [ Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h fh=gh ] + ; k = λ {d} h fh=gh → A [ Iso.≅← iso o IsEqualizer.k (Equalizer.isEqualizer equ) h fh=gh ] ; ek=h = ek=h1 ; uniqueness = uniqueness1 } }