Mercurial > hg > Members > kono > Proof > category

changeset 1066:f8b0f1b6fe84

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 27 Apr 2021 08:52:39 +0900
parents 5a9f5a4cadaa
children be83b28d1dd6
files src/ToposIL.agda
diffstat 1 files changed, 26 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposIL.agda	Tue Apr 27 05:10:29 2021 +0900
+++ b/src/ToposIL.agda	Tue Apr 27 08:52:39 2021 +0900
@@ -98,16 +98,39 @@
          ; isApply = {!!}
          ; applyCong = {!!}
         }
-    } 
+    } 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 [   Poly.f q ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] 
+     tl01 : {a : Obj A}  (p : Poly a  (Topos.Ω t) １ ) (q : Poly a  (Topos.Ω t) １ )
+        → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
+     tl01 {a} 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 p))) (mm p) ∙ {!!} ) ∙ {!!} ≈⟨ car (IsTopos.char-m=⊤ (Topos.isTopos t) (equalizer (Ker t (Poly.f p))) (mm p) ) ⟩
+          (Topos.⊤ t  ∙ {!!} ) ∙ {!!}  ≈⟨   {!!} ⟩
+          Topos.⊤ t ≈⟨  {!!} ⟩
+          {!!}  ≈⟨ tt q ⟩
+          Poly.f q ∎  where
+        pp : Hom A １ (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 = 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)
 
-  module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A) (il : InternalLanguage  Ω ⊤ P) where
+  module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A) (il : InternalLanguage  Ω ⊤ P) (t : Topos A c) where
      open InternalLanguage il
      il00 : {a : Obj A}  (p : Poly a  Ω １ )  → p  ⊢ p
      il00 {a}  p h eq = eq
 
+     ---  Poly.f p ∙  h  ≈  ⊤ ∙  ○  c 
+     ---  Poly.f q ∙  h  ≈  ⊤ ∙  ○  c 
      il01 : {a : Obj A}  (p : Poly a  Ω １ ) (q : Poly a  Ω １ )
         → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
-     il01 {a} p q p<q q<p = {!!}
+     il01 {a} p q p<q q<p = {!!} 
 
      il011 : {a : Obj A}  (p q q1 : Poly a  Ω １ ) 
         → q ⊢ p → q , q1 ⊢ p