Mercurial > hg > Members > kono > Proof > category

changeset 1048:28df99fe81de

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 Sun, 18 Apr 2021 11:00:21 +0900
parents cc7103f643b7
children 2871dd5b5e63
files src/Polynominal.agda src/ToposIL.agda
diffstat 2 files changed, 49 insertions(+), 96 deletions(-) [+]
line wrap: on
line diff
--- a/src/Polynominal.agda	Sun Apr 18 09:21:40 2021 +0900
+++ b/src/Polynominal.agda	Sun Apr 18 11:00:21 2021 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 open import Category
 open import CCC
 open import Level
@@ -7,81 +9,7 @@
 module Polynominal { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( C : CCC A )   where
 
   open CCC.CCC C
-  open coMonad 
-  open Functor
-  open NTrans
-  open import Category.Cat
-  
   open ≈-Reasoning A hiding (_∙_)
-  SA : (a : Obj A) → Functor A A
-  SA a = record {
-       FObj = λ x → a ∧ x
-     ; FMap = λ f →  < π ,  A [ f o π' ]   >
-     ; isFunctor = record {
-          identity = sa-id
-        ; ≈-cong = λ eq → IsCCC.π-cong isCCC refl-hom (resp refl-hom eq )
-        ; distr = sa-distr
-       }
-    } where
-        sa-id :  {b : Obj A} →  < π , ( id1 A b o π'  ) > ≈ id1 A (a ∧ b ) 
-        sa-id {b} = begin
-           < π , ( id1 A b o π'  ) > ≈⟨ IsCCC.π-cong isCCC (sym idR) (trans-hom idL (sym idR) ) ⟩
-           < ( π o id1 A _ ) , ( π' o id1 A _ )  > ≈⟨ IsCCC.e3c isCCC  ⟩
-          id1 A (a ∧ b ) ∎
-        sa-distr :  {x b c : Obj A} {f : Hom A x b} {g : Hom A b c} →
-            < π , (( g o f ) o π') > ≈ < π , ( g o π' ) > o < π , (f o π') > 
-        sa-distr {x} {b} {c} {f} {g} = begin
-            < π , (( g o f ) o π') > ≈↑⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) ( begin 
-               ( g o π' ) o < π , (f o π') >  ≈↑⟨ assoc ⟩ 
-                g o ( π'  o < π , (f o π') > )  ≈⟨ cdr (IsCCC.e3b isCCC)  ⟩ 
-                g o ( f o π')   ≈⟨ assoc  ⟩ 
-               ( g o f ) o π'  ∎ ) ⟩
-            < (π o < π , (f o π') >) ,  ( ( g o π' ) o < π , (f o π') >) > ≈↑⟨ IsCCC.distr-π isCCC  ⟩
-            < π , ( g o π' ) > o < π , (f o π') > ∎
-
-  SM : (a : Obj A) → coMonad A (SA a)
-  SM a = record {
-        δ = record { TMap = λ x → < π , id1 A _ > ;  isNTrans = record { commute = δ-comm} }
-      ; ε = record { TMap = λ x → π' ; isNTrans =  record { commute = ε-comm } }
-      ; isCoMonad = record {
-           unity1 = IsCCC.e3b isCCC
-         ; unity2 = unity2
-         ; assoc = assoc2
-        }
-     } where
-        δ-comm :  {a₁ : Obj A} {b : Obj A} {f : Hom A a₁ b} →
-             FMap (_○_ (SA a)  (SA a)) f o < π , id1 A _ > ≈ < π , id1 A _ > o FMap (SA a) f 
-        δ-comm {x} {b} {f} = begin
-           FMap (_○_ (SA a)  (SA a)) f o < π , id1 A _ > ≈⟨  IsCCC.distr-π isCCC ⟩
-           < π o < π , id1 A _ > ,  (FMap (SA a) f o π' ) o < π , id1 A _ > >  ≈⟨ IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩
-           < π ,  FMap (SA a) f o ( π'  o < π , id1 A _ >) >  ≈⟨ IsCCC.π-cong isCCC refl-hom (cdr (IsCCC.e3b isCCC)) ⟩
-           < π ,  FMap (SA a) f o id1 A _  >                  ≈⟨  IsCCC.π-cong isCCC refl-hom idR ⟩
-           < π ,  FMap (SA a) f  >                            ≈↑⟨   IsCCC.π-cong isCCC  (IsCCC.e3a isCCC) idL ⟩
-           < π o  FMap (SA a) f ,  id1 A _ o FMap (SA a) f >  ≈↑⟨  IsCCC.distr-π isCCC   ⟩
-           < π , id1 A _ > o FMap (SA a) f  ∎
-        ε-comm :  {a₁ : Obj A} {b : Obj A} {f : Hom A a₁ b} → 
-             FMap (identityFunctor {_} {_} {_} {A}) f o π'  ≈  π' o FMap (SA a) f 
-        ε-comm {_} {_} {f} = sym  (IsCCC.e3b isCCC)
-        unity2 :  {a₁ : Obj A} →  FMap (SA a) π' o < π , id1 A _ >  ≈ id1 A (a ∧ a₁)
-        unity2 {x} = begin
-           FMap (SA a) π' o < π , id1 A _ >                         ≈⟨  IsCCC.distr-π isCCC   ⟩
-            < π o < π , id1 A _ > , ( π' o π' ) o < π , id1 A _ > > ≈⟨  IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (sym assoc) ⟩
-            < π  ,  π' o ( π'  o < π , id1 A _ > ) >                ≈⟨  IsCCC.π-cong isCCC  refl-hom (cdr (IsCCC.e3b isCCC)) ⟩
-            < π  ,  π' o  id1 A _ >                                 ≈⟨  IsCCC.π-cong isCCC  refl-hom  idR ⟩
-            < π  ,  π' >                                            ≈⟨  IsCCC.π-id isCCC ⟩
-           id1 A (a ∧ x)  ∎
-        assoc2 :   {a₁ : Obj A} →  < π , id1 A _ > o < π , id1  A _ > ≈  FMap (SA a) < π , id1 A (a ∧ a₁) > o < π , id1 A _ > 
-        assoc2 {x} = begin
-            < π , id1 A _ > o < π , id1  A _ >                      ≈⟨  IsCCC.distr-π isCCC ⟩
-            < π o < π , id1  A _ > , id1 A _ o < π , id1  A _ > >   ≈⟨  IsCCC.π-cong isCCC  (IsCCC.e3a isCCC) idL  ⟩
-            < π  , < π , id1 A _ > >                                ≈↑⟨ IsCCC.π-cong isCCC refl-hom idR ⟩
-            < π  , < π , id1 A _ > o  id1 A _ >                     ≈↑⟨ IsCCC.π-cong isCCC refl-hom  (cdr (IsCCC.e3b isCCC)) ⟩
-            < π  , < π , id1 A _ > o  ( π'  o < π , id1 A _ > ) >   ≈↑⟨ IsCCC.π-cong isCCC  (IsCCC.e3a isCCC) (sym assoc) ⟩
-            < π o < π , id1 A _ > , (< π , id1 A _ > o  π' ) o < π , id1 A _ > > ≈↑⟨  IsCCC.distr-π isCCC  ⟩
-           FMap (SA a) < π , id1 A (a ∧ x) > o < π , id1 A _ > ∎
-  --
-  -- coKleisli category of SM should give the fucntional completeness 
-  --
 
   _∙_ = _[_o_] A
 
@@ -126,6 +54,11 @@
   toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
   toφ {a} {⊤} {b} {c} x∈a z = i
 
+  record XHom {a ⊤ : Obj A }  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+    field
+       xhom : Hom A ⊤ a 
+       phi : {b c : Obj A} → {f : Hom A b c} → φ xhom {b} {c} f
+
   record PHom {a ⊤ : Obj A } { x : Hom A ⊤ a } (b c : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
     field
        hom : Hom A b c 
@@ -175,31 +108,34 @@
       uniq : {b c : Obj A} →  (p : PHom b c)  → (f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b   , id1 A b  >  ≈ hom p ] 
          → A [ f  ≈ fun p ]
 
-  record XHom {a ⊤ : Obj A }  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
-    field
-       xhom : Hom A ⊤ a 
-       phi : {b c : Obj A} → {f : Hom A b c} → φ xhom {b} {c} f
-
   -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x  
   record Select  {a b : Obj A} (Ω : Obj A) ( φ : (x :  Hom A １ a ) → Hom A １ b )
          :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
     field
       sl :  Hom A １ (b <= a) 
-      isSelect : (x : Hom A １ a  ) → A [  A [ ε C  o < sl , x > ]  ≈  φ x ]
-      isUnique : (x : Hom A １ a  ) → (f : Hom A １ (b <= a) )  → A [  A [ ε C o < f , x > ]  ≈  φ x ]
+      isSelect : (x : Hom A １ a  ) → A [  A [ ε  o < sl , x > ]  ≈  φ x ]
+      isUnique : (x : Hom A １ a  ) → (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , x > ]  ≈  φ x ]
         →  A [ sl  ≈ f ]
 
-  φ→Phom : {a b : Obj A} (Ω : Obj A) ( φ : (x :  Hom A １ a ) → Hom A １ b ) → Hom A a b
-  φ→Phom = {!!}
-  
+  record Fc {a b : Obj A } ( φ : (x : Hom A １ a  ) → XHom {b} {１} )
+         :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+    field
+      sl :  Hom A a b 
+    g : Hom A １ (b <= a) 
+    g = (A [ A [ A [ sl o π ] o < id1 A _ ,  ○ a > ] o π' ]  ) *
+    field
+      isSelect : (x : Hom A １ a  ) → A [  A [ ε  o < g , x > ]  ≈  XHom.xhom ( φ x ) ]
+      isUnique : (x : Hom A １ a  ) → (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , x > ]  ≈   XHom.xhom ( φ x ) ]
+        →  A [ g  ≈ f ]
 
   -- functional completeness
-  FC : {a b : Obj A}  ( φ : (x :  Hom A １ a ) → Hom A １ b ) → Select b φ
+  FC : {a b : Obj A}  → (φ  : Hom A １ a   → XHom {b} {１} )  → Fc φ 
   FC {a} {b} φ = record {
-       sl = (A [ A [ {!!} o < id1 A _ ,  ○ a > ] o π' ]  ) *
+     sl = {!!}
      ; isSelect = {!!} 
      ; isUnique = {!!} 
-    }
+    } 
+       -- sl = (A [ A [  {!!}  o < id1 A _ ,  ○ a > ] o π' ]  ) *
 
   π-cong = IsCCC.π-cong isCCC
   e2 = IsCCC.e2 isCCC
--- a/src/ToposIL.agda	Sun Apr 18 09:21:40 2021 +0900
+++ b/src/ToposIL.agda	Sun Apr 18 11:00:21 2021 +0900
@@ -15,6 +15,19 @@
   open import Category.Sets hiding (_o_)
   open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
 
+  data  φ  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ⊔ ℓ) where
+     i   : {b c : Obj A} {k : Hom A b c } → φ x k   
+     ii  : φ x {⊤} {a} x
+     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 (A [ f o 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'
+
+  record XHom {a ⊤ : Obj A }  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+    field
+       xhom : Hom A ⊤ a
+       phi : {b c : Obj A} → {f : Hom A b c} → φ xhom {b} {c} f
+
   -- record IsLogic    (c : CCC A) 
   --        (Ω : Obj A)
   --        (⊤ : Hom A １ Ω)
@@ -32,7 +45,7 @@
          _==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω
          _∈_ : {a : Obj A} (x :  Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω
          -- { x ∈ a | φ x } : P a
-         select : {a : Obj A} → ( (x :  Hom A １ a ) →  Hom A １ Ω ) → Hom A １ (P a)
+         select : {a : Obj A} → ( φ : (x : Hom A １ a  ) → XHom {Ω} {１} ) → Hom A １ (P a)
          -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
      _|-_  :  (List (Hom A １ Ω)) → (p : Hom A １ Ω ) → Set ℓ
      [] |-  p = A [ p ≈  ⊤ ] 
@@ -54,24 +67,28 @@
 
   open import ToposEx A c using ( δmono  )
 
-  -- f ≡ λ (x ∈ a) → φ x or  ∃ (f : b <= a) →  f ∙ x ≈  φ x  
-  record Select  {a b : Obj A} (Ω : Obj A) ( φ : (x :  Hom A １ a ) → Hom A １ b )
+  -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x  
+
+  record Fc {a b : Obj A } ( φ : (x : Hom A １ a  ) → XHom {b} {１} )
          :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
     field
-      sl :  Hom A １ (b <= a) 
-      isSelect : (x : Hom A １ a  ) → A [  A [ ε o < sl , x > ]  ≈  φ x ]
-      isUnique : (x : Hom A １ a  ) → (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , x > ]  ≈  φ x ]
-        →  A [ sl  ≈ f ]
+      sl :  Hom A a b
+    g : Hom A １ (b <= a)
+    g = (A [ A [ A [ sl o π ] o < id1 A _ ,  ○ a > ] o π' ]  ) *
+    field
+      isSelect : (x : Hom A １ a  ) → A [  A [ ε  o < g , x > ]  ≈  XHom.xhom ( φ x ) ]
+      isUnique : (x : Hom A １ a  ) → (f : Hom A １ (b <= a) )  → A [  A [ ε  o < f , x > ]  ≈   XHom.xhom ( φ x ) ]
+        →  A [ g  ≈ f ]
 
   -- functional completeness
   FC : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
-  FC = {a b : Obj A}  ( φ : (x :  Hom A １ a ) → Hom A １ b ) → Select b φ
+  FC = {a b : Obj A}  ( φ : (x : Hom A １ a  ) → XHom {b} {１} ) → Fc φ
 
   topos→logic : (t : Topos A c ) → ToposNat A １ → FC  → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a)
   topos→logic t n fc = record {
          _==_ = λ {b} f g →   A [ char t < id1 A b , id1 A b > (δmono t n ) o < f , g > ]
       ;  _∈_ = λ {a} x α →  A [ ε o < α , x > ]
       -- { x ∈ a | φ x } : P a
-      ;  select = λ {a} φ →  Select.sl ( fc φ )
+      ;  select = λ {a} φ →  Fc.g ( fc φ )
       -- ;  isTL = {!!}
     }