Mercurial > hg > Members > kono > Proof > category

changeset 1062:d35b395370ff

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 Sat, 24 Apr 2021 15:15:17 +0900
parents 805a4113ad74
children f1f625c3866c
files src/Polynominal.agda src/ToposIL.agda
diffstat 2 files changed, 24 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/Polynominal.agda	Wed Apr 21 10:22:37 2021 +0900
+++ b/src/Polynominal.agda	Sat Apr 24 15:15:17 2021 +0900
@@ -35,7 +35,7 @@
      iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c'  ∧ c''} < f , g > 
      iv  : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ∙ g )
      v   : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }  (ψ : φ x f )  → φ x {b} {c'' <= c'} ( f * )
-     φ-cong   : {b c : Obj A} {k k' : Hom A b c } → A [ k ≈ k' ] → φ x k  → φ x k'
+     φ-cong   : {b c : Obj A} {k k' : Hom A b c } → A [ k ≈ k' ] → φ x k  → φ x k'  -- may be we don't need this
   
   α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
   α = < π  ∙ π   , < π'  ∙ π  , π'  > >
@@ -74,12 +74,15 @@
   --   we have (x y :  Hom A １ a) → x ≡ y (minimul equivalende assumption). this makes all k x ii case valid
   --   all other cases, arguments are reduced to f ∙ π' .
   postulate
-     x-singleon : {a b c : Obj A}  → (f :  Poly a c b ) → (x y : Hom A b a) → x ≡ y  -- minimul equivalende assumption
+     x-singleon : {a b c : Obj A}  → (f :  Poly a c b ) → (x y : Hom A b a) → x ≡ y  -- minimul equivalende assumption (variables are the same except its name)
      k-cong : {a b c : Obj A}  → (f g :  Poly a c b ) → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f)   ≈ k (Poly.x g) (Poly.phi g) ]
 
+  -- we may prove k-cong from x-singleon
   -- k-cong' : {a b c : Obj A}  → (f g :  Poly a c b ) → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f)   ≈ k (Poly.x g) (Poly.phi g) ]
   -- k-cong' {a} {b} {c} f g f=g with Poly.phi f | Poly.phi g
 
+  -- since we have A[x] now, we can proceed the proof on p.64 in some possible future
+
   --
   --  Proposition 6.1
   --
@@ -96,6 +99,7 @@
       uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b   , id1 A b  >  ≈ Poly.f p ] 
          → A [ f  ≈ fun  ]
 
+  -- ε form
   -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x  
   record Fc {a b : Obj A } ( φ :  Poly a b １ ) 
          :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
@@ -108,6 +112,7 @@
       isUnique : (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , Poly.x φ  > ]  ≈  Poly.f φ  ]
         →  A [ g   ≈ f ]
 
+  -- we should open IsCCC isCCC
   π-cong = IsCCC.π-cong isCCC
   *-cong = IsCCC.*-cong isCCC
   distr-* = IsCCC.distr-* isCCC
@@ -198,7 +203,7 @@
   --            
   --   fun ∙ <  x ∙ ○ b   , id1 A b  >  ≈ Poly.f p
   --   (ε ∙ < g ∙ π , π' >) ∙ <  x ∙ ○ b   , id1 A b  >  ≈ Poly.f p
-  --
+  --      could be simpler
   FC : {a b : Obj A}  → (φ  : Poly a b １ )  → Fc {a} {b} φ 
   FC {a} {b} φ = record {
      sl = A [ k (Poly.x φ ) (Poly.phi φ) o < id1 A _ ,  ○ a  > ] 
--- a/src/ToposIL.agda	Wed Apr 21 10:22:37 2021 +0900
+++ b/src/ToposIL.agda	Sat Apr 24 15:15:17 2021 +0900
@@ -8,7 +8,7 @@
 
   open Topos
   open Equalizer
-  open ≈-Reasoning A
+  -- open ≈-Reasoning A hiding (_∙_)
   open CCC.CCC c
 
   open Functor
@@ -27,6 +27,7 @@
   --    field
   --        a : {!!}
 
+
   record InternalLanguage (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A)
           :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
@@ -35,10 +36,10 @@
          -- { x ∈ a | φ x } : P a
          select : {a : Obj A} → ( φ :  Poly a Ω １ ) → Hom A １ (P a)
          -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
-     -- _|-_  :  (List (Hom A １ Ω)) → (p : Hom A １ Ω ) → Set ℓ
-     -- [] |-  p = A [ p ≈  ⊤ ] 
-     -- (h ∷ t) |-  p = {!!}
-  
+     _⊢_  : {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 [   Poly.f q ∙ h  ≈  ⊤ ∙  ○  c  ] 
+
 --             ○ b
 --       b -----------→ 1
 --       |              |
@@ -69,3 +70,13 @@
       ;  select = λ {a} φ →  Fc.g ( fc t φ )
       -- ;  isTL = {!!}
     } 
+
+  module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A) (il : InternalLanguage  Ω ⊤ P) where
+     open InternalLanguage il
+     il00 : {a : Obj A}  (p : Poly a  Ω １ )  → p  ⊢ p
+     il00 {a}  p h eq = eq
+
+     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 = {!!}
+