Mercurial > hg > Members > kono > Proof > category

changeset 1065:5a9f5a4cadaa

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 05:10:29 +0900
parents a17348c201e5
children f8b0f1b6fe84
files src/Polynominal.agda src/ToposIL.agda
diffstat 2 files changed, 40 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/src/Polynominal.agda	Mon Apr 26 07:08:12 2021 +0900
+++ b/src/Polynominal.agda	Tue Apr 27 05:10:29 2021 +0900
@@ -74,7 +74,7 @@
   --   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 (variables are the same except its name)
+     -- 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
@@ -207,30 +207,10 @@
   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  > ] 
-     ; isSelect = begin
-        ε ∙ <  ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ ,  ○ a > ) ∙ π')  * ,  Poly.x φ  > ≈↑⟨ cdr (π-cong idR refl-hom ) ⟩
-        ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   id1 A _   ,  Poly.x φ > )  ≈⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩
-        ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   ○ １ ,  Poly.x φ > )  ≈↑⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩
-        ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   (○ a  ∙ Poly.x φ)  ,  Poly.x φ > )  ≈↑⟨ cdr (π-cong (sym assoc) idL ) ⟩
-        ε ∙ (< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   ○ a ) ∙ Poly.x φ  ,  id1 A _ ∙ Poly.x φ > )
-            ≈↑⟨ cdr (IsCCC.distr-π isCCC)  ⟩
-        ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   ○ a ) ,  id1 A _ > )  ∙ Poly.x φ )
-            ≈↑⟨ cdr (car (π-cong (cdr (IsCCC.e3a isCCC) ) refl-hom))  ⟩
-        ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  (π  ∙ <  ○ a , id1 A _ > )) ,  id1 A _ > )  ∙ Poly.x φ )
-            ≈⟨ cdr (car (π-cong assoc (sym (IsCCC.e3b isCCC)) )) ⟩
-        ε ∙ ((< ((((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  π ) ∙ <  ○ a , id1 A _ > ) , (π' ∙  <  ○ a , id1 A _ > ) > )  ∙ Poly.x φ )
-            ≈↑⟨ cdr (car (IsCCC.distr-π isCCC)) ⟩
-        ε ∙ ((< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  π , π' >  ∙ <  ○ a , id1 A _ > )  ∙ Poly.x φ )  ≈⟨ assoc ⟩
-        (ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  π , π' >  ∙ <  ○ a , id1 A _ > ) ) ∙ Poly.x φ   ≈⟨ car assoc ⟩
-        ((ε ∙ < ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  π , π' > ) ∙ <  ○ a , id1 A _ >  ) ∙ Poly.x φ
-            ≈⟨ car (car (IsCCC.e4a isCCC))  ⟩
-        ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) ∙ <  ○ a , id1 A _ >  ) ∙ Poly.x φ   ≈↑⟨ car assoc ⟩
-        (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > ) ∙ (π' ∙ <  ○ a , id1 A _ > ) ) ∙ Poly.x φ   ≈⟨ car (cdr (IsCCC.e3b isCCC)) ⟩
-        (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > ) ∙ id1 A _ ) ∙ Poly.x φ   ≈⟨ car idR ⟩
-        ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > ) ∙ Poly.x φ   ≈⟨ gg  ⟩
-        Poly.f φ ∎
+     ; isSelect = isSelect
      ; isUnique = uniq 
     }  where
+        π-exchg = IsCCC.π-exchg isCCC
         fc0 :  {b c : Obj A} (p : Poly b c １) → A [  k (Poly.x p ) (Poly.phi p) ∙ <  Poly.x p  ∙  ○ １  , id1 A １ >  ≈ Poly.f p ]
         fc0 p =  Functional-completeness.fp (functional-completeness p)
         gg : A [ (  k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > ) ∙ Poly.x φ ≈ Poly.f φ ]
@@ -240,7 +220,29 @@
           k (Poly.x φ ) (Poly.phi φ) ∙ <   Poly.x φ  ,  ○ １ >  ≈⟨ cdr (π-cong (trans-hom (sym idR) (cdr e2) )  (sym e2) ) ⟩
           k (Poly.x φ ) (Poly.phi φ) ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ >  ≈⟨ fc0 φ  ⟩
           Poly.f φ ∎
-        π-exchg = IsCCC.π-exchg isCCC
+        isSelect :  A [ ε ∙ < ( ( k (Poly.x φ ) (  Poly.phi φ) ∙ < id1 A _ , ○ a > ) ∙ π' ) * , Poly.x φ >  ≈ Poly.f φ ]
+        isSelect =      begin
+          ε ∙ <  ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ ,  ○ a > ) ∙ π')  * ,  Poly.x φ  > ≈↑⟨ cdr (π-cong idR refl-hom ) ⟩
+          ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   id1 A _   ,  Poly.x φ > )  ≈⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩
+          ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   ○ １ ,  Poly.x φ > )  ≈↑⟨ cdr (π-cong (cdr e2) refl-hom ) ⟩
+          ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   (○ a  ∙ Poly.x φ)  ,  Poly.x φ > )  ≈↑⟨ cdr (π-cong (sym assoc) idL ) ⟩
+          ε ∙ (< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   ○ a ) ∙ Poly.x φ  ,  id1 A _ ∙ Poly.x φ > )
+              ≈↑⟨ cdr (IsCCC.distr-π isCCC)  ⟩
+          ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙   ○ a ) ,  id1 A _ > )  ∙ Poly.x φ )
+              ≈↑⟨ cdr (car (π-cong (cdr (IsCCC.e3a isCCC) ) refl-hom))  ⟩
+          ε ∙ ((< (((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  (π  ∙ <  ○ a , id1 A _ > )) ,  id1 A _ > )  ∙ Poly.x φ )
+              ≈⟨ cdr (car (π-cong assoc (sym (IsCCC.e3b isCCC)) )) ⟩
+          ε ∙ ((< ((((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  π ) ∙ <  ○ a , id1 A _ > ) , (π' ∙  <  ○ a , id1 A _ > ) > )  ∙ Poly.x φ )
+              ≈↑⟨ cdr (car (IsCCC.distr-π isCCC)) ⟩
+            ε ∙ ((< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  π , π' >  ∙ <  ○ a , id1 A _ > )  ∙ Poly.x φ )  ≈⟨ assoc ⟩
+            (ε ∙ (< ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  π , π' >  ∙ <  ○ a , id1 A _ > ) ) ∙ Poly.x φ   ≈⟨ car assoc ⟩
+          ((ε ∙ < ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) * )  ∙  π , π' > ) ∙ <  ○ a , id1 A _ >  ) ∙ Poly.x φ
+              ≈⟨ car (car (IsCCC.e4a isCCC))  ⟩
+          ((( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  >)  ∙ π' ) ∙ <  ○ a , id1 A _ >  ) ∙ Poly.x φ   ≈↑⟨ car assoc ⟩
+          (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > ) ∙ (π' ∙ <  ○ a , id1 A _ > ) ) ∙ Poly.x φ   ≈⟨ car (cdr (IsCCC.e3b isCCC)) ⟩
+          (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > ) ∙ id1 A _ ) ∙ Poly.x φ   ≈⟨ car idR ⟩
+          ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > ) ∙ Poly.x φ   ≈⟨ gg  ⟩
+          Poly.f φ ∎
         uniq  :  (f : Hom A １ (b <= a)) → A [ A [ ε o < f , Poly.x φ > ] ≈ Poly.f φ ] →
             A [ (( k (Poly.x φ) (Poly.phi φ) ∙  < id1 A _  , ○ a > )∙ π' ) * ≈ f ]
         uniq f eq = begin
--- a/src/ToposIL.agda	Mon Apr 26 07:08:12 2021 +0900
+++ b/src/ToposIL.agda	Tue Apr 27 05:10:29 2021 +0900
@@ -25,15 +25,19 @@
      field
          isSelect : {a : Obj A} → ( φ :  Poly a Ω １ ) → {c : Obj A} (h : Hom A c １ )
             → A [ ( ( Poly.x φ ∈ select φ ) == Poly.f φ )  ∙ h  ≈  ⊤ ∙  ○  c ]
-         uniqueSelect : {a : Obj A} → ( φ :  Poly a Ω １ ) → {c : Obj A} (h : Hom A c １ )
-            → (α : Hom A １ (P a) )
-            → A [ ( ( Poly.x φ ∈ α )  ==  Poly.f φ )  ∙ h  ≈  ⊤ ∙  ○  c ]
+         uniqueSelect : {a : Obj A} → ( φ :  Poly a Ω １ ) → (α : Hom A １ (P a) )
+            → {c : Obj A} (h : Hom A c １ )
+            → A [ ( Poly.f φ == ( Poly.x φ ∈ α ) )  ∙ h  ≈  ⊤ ∙  ○  c ]
             → A [ ( select φ == α )  ∙ h  ≈  ⊤ ∙  ○  c ]
          isApply : {a : Obj A}  (x y : Hom A １ a ) → (q p : Poly a  Ω １ ) 
             → {c : Obj A} (h : Hom A c １ )  → A [ ( x == y )  ∙ h  ≈  ⊤ ∙  ○  c ] 
             → A [ Poly.f q ∙ h  ≈  ⊤ ∙  ○  c ]
             → A [ Poly.f (apply p x ) ∙ h  ≈  ⊤ ∙  ○  c ] 
             → A [ Poly.f (apply p y ) ∙ h  ≈  ⊤ ∙  ○  c ]  
+         applyCong : {a : Obj A}  (x : Hom A １ a ) → (q p : Poly a  Ω １ ) 
+            → {c : Obj A} (h : Hom A c １ )  
+            → ( A [ Poly.f q ∙ h  ≈  ⊤ ∙  ○  c ] → A [ Poly.f p ∙ h  ≈  ⊤ ∙  ○  c ] )
+            → ( A [ Poly.f (apply q x ) ∙ h  ≈  ⊤ ∙  ○  c ] → A [ Poly.f (apply p x ) ∙ h  ≈  ⊤ ∙  ○  c ] )
 
   record InternalLanguage (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A)
           :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
@@ -43,7 +47,7 @@
          -- { x ∈ a | φ x } : P a
          select : {a : Obj A} → ( φ :  Poly a Ω １ ) → Hom A １ (P a)
          apply : {a  : Obj A}  (p : Poly a  Ω １ )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
-         isTL : IsLogic Ω ⊤ P _==_ _∈_  select apply
+         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 [   Poly.f q ∙ h  ≈  ⊤ ∙  ○  c  ] 
@@ -88,10 +92,11 @@
       -- { x ∈ a | φ x } : P a
       ;  select = λ {a} φ →  Fc.g ( fc t φ )
       ;  apply = λ {a}  φ x → record { x = x ; f = Functional-completeness.fun (fc0 t φ ) ∙ < x ∙  ○ _ , id1 A _ >  ; phi = i }
-      ;  isTL = record {
+      ;  isIL = record {
            isSelect = {!!}
          ; uniqueSelect = {!!}
          ; isApply = {!!}
+         ; applyCong = {!!}
         }
     } 
 
@@ -119,18 +124,18 @@
      --- (b : Hom A １ a) → φ y  ⊢ φ' y  → φ b  ⊢ φ' b
      il03 : {a : Obj A}  (b : Hom A １ a ) → (q p : Poly a  Ω １ ) 
         → q ⊢ p → apply q b  ⊢ apply p b
-     il03 {a} = {!!}
+     il03 {a} b q p q<p h = IsLogic.applyCong (InternalLanguage.isIL il ) b q p h (q<p h)
 
      --- a == b → φ a  ⊢ φ b
      il04 : {a : Obj A}  (x y : Hom A １ a ) → (q p : Poly a  Ω １ ) 
         → ⊨ (x == y) 
         → q ⊢ apply p x → q ⊢ apply p y
-     il04 {a} = {!!}
+     il04 {a} x y q p eq q<px h qt = IsLogic.isApply (InternalLanguage.isIL il ) x y q p h (eq h) qt (q<px h qt )
   
      --- ⊨ x ∈ select φ == φ x
      il05 : {a : Obj A}  → (q : Poly a  Ω １ ) 
         → ⊨ ( ( Poly.x q ∈ select q ) == Poly.f q  )
-     il05 {a} = {!!}
+     il05 {a} = IsLogic.isSelect (InternalLanguage.isIL il )
   
      ---    q ⊢  φ x == x ∈ α 
      ---   ----------------------- 
@@ -139,5 +144,5 @@
      il06 : {a : Obj A}  → (q : Poly a  Ω １ )  → (α : Hom A １ (P a) )
         → ⊨ ( Poly.f q  == ( Poly.x q ∈ α ) ) 
         → ⊨ ( select q == α )
-     il06 {a} = {!!}
+     il06 {a} q p eq h = IsLogic.uniqueSelect (InternalLanguage.isIL il ) q p h (eq h)