Mercurial > hg > Members > kono > Proof > category
changeset 1068:4e58611b1fb1
fix 1
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Apr 2021 11:16:18 +0900 |
| parents | be83b28d1dd6 |
| children | 849f85e543f1 |
| files | src/CCCSets.agda src/ToposIL.agda |
| diffstat | 2 files changed, 52 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCCSets.agda Tue Apr 27 10:24:04 2021 +0900 +++ b/src/CCCSets.agda Thu Apr 29 11:16:18 2021 +0900 @@ -241,6 +241,31 @@ ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1 ... | t = ⊥-elim (t (isImage x)) + open import Polynominal (Sets {c} ) (sets {c}) + A = Sets {c} + Ω = Bool + １ = One + ⊤ = λ _ → true + ○ = λ _ → λ _ → ! + _⊢_ : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) → Set (suc c ) + _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p o h ≈ ⊤ o ○ c ] + → A [ Poly.f q ∙ h ≈ ⊤ o ○ c ] + tl01 : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) + → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] + tl01 {a} {b} p q p<q q<p = extensionality Sets t1011 where + open ≡-Reasoning + t1011 : (s : b ) → Poly.f p s ≡ Poly.f q s + t1011 x with Poly.f p x | inspect ( Poly.f p) x + ... | true | record { eq = eq1 } = sym tt1 where + tt1 : Poly.f q _ ≡ true + tt1 = cong (λ k → k !) (p<q _ ( extensionality Sets (λ x → eq1) )) + ... | false | record { eq = eq1 } with Poly.f q x | inspect (Poly.f q) x + ... | true | record { eq = eq2 } = ⊥-elim ( ¬x≡t∧x≡f record { fst = eq1 ; snd = tt1 } ) where + tt1 : Poly.f p _ ≡ true + tt1 = cong (λ k → k !) (q<p _ ( extensionality Sets (λ x → eq2) )) + ... | false | eq2 = refl + + open import graph module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where
--- a/src/ToposIL.agda Tue Apr 27 10:24:04 2021 +0900 +++ b/src/ToposIL.agda Thu Apr 29 11:16:18 2021 +0900 @@ -48,11 +48,11 @@ select : {a : Obj A} → ( φ : Poly a Ω １ ) → Hom A １ (P a) apply : {a : Obj A} (p : Poly a Ω １ ) → ( x : Hom A １ a ) → Poly a Ω １ isIL : IsLogic Ω ⊤ P _==_ _∈_ select apply - _⊢_ : {a : Obj A} (p : Poly a Ω １ ) (q : Poly a Ω １ ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) - _⊢_ {a} p q = {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] + _⊢_ : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) + _⊢_ {a} {b} p q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] - _,_⊢_ : {a : Obj A} (p : Poly a Ω １ ) (p1 : Poly a Ω １ ) (q : Poly a Ω １ ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) - _,_⊢_ {a} p p1 q = {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] + _,_⊢_ : {a b : Obj A} (p : Poly a Ω b ) (p1 : Poly a Ω b ) (q : Poly a Ω b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) + _,_⊢_ {a} {b} p p1 q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f p1 ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] expr : {a b c : Obj A} (p : Hom A １ Ω ) → ( x : Hom A １ a ) → Poly a Ω １ @@ -80,10 +80,10 @@ -- functional completeness FC0 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) - FC0 = {a : Obj A} (t : Topos A c) ( φ : Poly a (Ω t)１) → Functional-completeness φ + FC0 = {a b : Obj A} (t : Topos A c) ( φ : Poly a (Ω t) b) → Functional-completeness φ FC1 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) - FC1 = {a : Obj A} (t : Topos A c) ( φ : Poly a (Ω t)１) → Fc φ + FC1 = {a : Obj A} (t : Topos A c) ( φ : Poly a (Ω t) １) → Fc φ topos→logic : (t : Topos A c ) → ToposNat A １ → FC0 → FC1 → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a) topos→logic t n fc0 fc = record { @@ -100,8 +100,8 @@ } } where open ≈-Reasoning A hiding (_∙_) - _⊢_ : {a : Obj A} (p : Poly a (Topos.Ω t) １ ) (q : Poly a (Topos.Ω t) １ ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) - _⊢_ {a} p q = {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] + _⊢_ : {a b : Obj A} (p : Poly a (Topos.Ω t) b ) (q : Poly a (Topos.Ω t) b ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) + _⊢_ {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 @@ -112,27 +112,29 @@ -- + ------→ 1 -----------→ Ω -- ker h fp / fq -- - tl01 : {a : Obj A} (p : Poly a (Topos.Ω t) １ ) (q : Poly a (Topos.Ω t) １ ) + tl01 : {a b : Obj A} (p : Poly a (Topos.Ω t) b ) (q : Poly a (Topos.Ω t) b ) → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] - tl01 {a} p q p<q q<p = begin - Poly.f p ≈⟨ {!!} ⟩ - char t (id1 A _) {!!} ≈⟨ {!!} ⟩ - Topos.⊤ t ≈⟨ {!!} ⟩ - {!!} ≈⟨ tt 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 - pm : {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] → A [ Poly.f q ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] + 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 １ ) → A [ Poly.f q ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] → A [ Poly.f p ∙ h ≈ (Topos.⊤ t) ∙ ○ c ] + 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 - hm : (h : Hom A {!!} １ ) → Mono A h - hm h = record { isMono = {!!} } - pp : Hom A １ (Topos.Ω t) + 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 ) - mm : (q : Poly a (Topos.Ω t) １ ) → Mono A (equalizer (Ker t (Poly.f q))) + 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) １ ) → A [ char t (equalizer (Ker t (Poly.f q))) (mm q) ≈ Poly.f q ] - tt q = IsTopos.char-uniqueness (Topos.isTopos t) {１} (equalizer (Ker t (Poly.f q))) (mm 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) module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P : Obj A → Obj A) (il : InternalLanguage Ω ⊤ P) (t : Topos A c) where open InternalLanguage il @@ -141,15 +143,15 @@ --- Poly.f p ∙ h ≈ ⊤ ∙ ○ c --- Poly.f q ∙ h ≈ ⊤ ∙ ○ c - il01 : {a : Obj A} (p : Poly a Ω １ ) (q : Poly a Ω １ ) + il01 : {a b : Obj A} (p : Poly a Ω b ) (q : Poly a Ω b ) → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] il01 {a} p q p<q q<p = {!!} - il011 : {a : Obj A} (p q q1 : Poly a Ω １ ) + il011 : {a b : Obj A} (p q q1 : Poly a Ω b ) → q ⊢ p → q , q1 ⊢ p il011 {a} p q q1 p<q h tq tq1 = p<q h tq - il012 : {a : Obj A} (p q r : Poly a Ω １ ) + il012 : {a b : Obj A} (p q r : Poly a Ω b ) → q ⊢ p → q , p ⊢ r → q ⊢ r il012 {a} p q r p<q pq<r h qt = pq<r h qt (p<q h qt)