Mercurial > hg > Members > kono > Proof > category

changeset 1082:a59d7f0edeae

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 Wed, 12 May 2021 21:14:24 +0900
parents 3f85f57599e0
children caba080b1ded
files src/Polynominal.agda
diffstat 1 files changed, 14 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/src/Polynominal.agda	Wed May 12 12:52:54 2021 +0900
+++ b/src/Polynominal.agda	Wed May 12 21:14:24 2021 +0900
@@ -35,7 +35,6 @@
      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'  -- may be we don't need this
   
   α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
   α = < π  ∙ π   , < π'  ∙ π  , π'  > >
@@ -49,7 +48,6 @@
   k x∈a (iii ψ χ ) = < k x∈a ψ  , k x∈a χ  >
   k x∈a (iv ψ χ ) = k x∈a ψ  ∙ < π , k x∈a χ  >
   k x∈a (v ψ ) = ( k x∈a ψ  ∙ α ) *
-  k x∈a (φ-cong  eq ψ) = k x∈a  ψ
 
   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
@@ -62,8 +60,6 @@
   -- if we use equality on f as in A, Poly is ovioously Hom c b of a Category.
   -- it is better to define A[x] as an extension of A as described before
 
-  open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym  )
-
   record Poly (a c b : Obj A )  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
     field
        x :  Hom A １ a                                            -- λ x
@@ -94,10 +90,10 @@
     field
       sl :  Hom A a b 
     g :  Hom A １ (b <= a) 
-    g  = (A [ sl  o π' ]  ) *
+    g  = ( sl ∙ π'  ) *
     field
-      isSelect : A [  A [ ε  o < g  , Poly.x φ  > ]  ≈  Poly.f φ  ]
-      isUnique : (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , Poly.x φ  > ]  ≈  Poly.f φ  ]
+      isSelect : A [   ε ∙ < g  , Poly.x φ  >   ≈  Poly.f φ  ]
+      isUnique : (f : Hom A １ (b <= a) )  → A [   ε ∙ < f , Poly.x φ  >   ≈  Poly.f φ  ]
         →  A [ g   ≈ f ]
 
   -- we should open IsCCC isCCC
@@ -127,7 +123,7 @@
                x ∙ π'   ≈⟨ cdr e2 ⟩
                x ∙ ○ (a ∧ １) ≈↑⟨ cdr e2 ⟩
                x ∙ (○ a ∙ π )  ≈⟨ assoc ⟩
-               (x ∙ ○ a ) ∙ π   ≈⟨ car (Poly.idx p) ⟩
+               (x ∙ ○ a ) ∙ π   ≈⟨ car (Poly.idx p) ⟩   -- smallest equivalence
                id1 A a ∙ π   ≈⟨ idL ⟩
                k x ii  ∎  
   ki p x _ (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) = begin
@@ -148,21 +144,20 @@
                ( (f ∙ π')  ∙  < π ∙ π , < π' ∙  π , π' > > ) *  ≈⟨ *-cong ( car ( ki p x _ fp)) ⟩
                ( k x fp ∙  < π ∙ π , < π' ∙  π , π' > > ) *  ≈⟨⟩
                k x (v fp )  ∎  
-  ki p x f (φ-cong {_} {_} {f₁} {f} eq fp) = begin
-               f ∙ π' ≈↑⟨ car eq ⟩
-               f₁ ∙ π' ≈⟨ ki p x _ fp ⟩
-               k x fp  ≈⟨⟩
-               k x (φ-cong eq  fp )  ∎  
   k-cong : {a b c : Obj A}  → (f g :  Poly a c b )
-        → Poly.x f ≡ Poly.x g 
         → 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 refl f=f = begin
+  k-cong {a} {b} {c} f g f=f = begin
           k (Poly.x f) (Poly.phi f) ≈↑⟨ ki f (Poly.x f)  _ (Poly.phi f) ⟩
           Poly.f f ∙ π' ≈⟨ car f=f  ⟩
-          Poly.f g ∙ π'  ≈⟨  ki f (Poly.x f)  _ (Poly.phi g) ⟩
+          Poly.f g ∙ π'  ≈⟨  ki f (Poly.x g)  _ (Poly.phi g) ⟩
           k (Poly.x g) (Poly.phi g) ∎   
 
   -- proof in p.59 Lambek
+  --
+  --  (ψ : Poly a c b) is basically λ x.ψ(x). To use x from outside as a ψ(x), apply x ψ will work.
+  --  Instead of replacing x in Poly.phi ψ, we can use simple application with this fuctional completeness
+  --  in the internal language of Topos.
+  --  
   functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p 
   functional-completeness {a} {b} {c} p = record {
          fun = k (Poly.x p) (Poly.phi p)
@@ -220,7 +215,6 @@
               k x y ∙  < x ∙ ○ _ , id1 A _  >    ≈⟨ fc0 x f y  ⟩
              f  ∎ )  ⟩
              f * ∎  
-        ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 x f y ) f=f'
         --
         --   f ∙ <  x ∙ ○ b  , id1 A b >  ≈ f →  f ≈ k x (phi p)
         -- 
@@ -252,7 +246,7 @@
   --      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  > ] 
+     sl =  k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > 
      ; isSelect = isSelect
      ; isUnique = uniq 
     }  where
@@ -289,7 +283,7 @@
           (( 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 φ ] →
+        uniq  :  (f : Hom A １ (b <= a)) → A [  ε ∙ < f , Poly.x φ >  ≈ Poly.f φ ] →
             A [ (( k (Poly.x φ) (Poly.phi φ) ∙  < id1 A _  , ○ a > )∙ π' ) * ≈ f ]
         uniq f eq = begin
            (( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > ) ∙ π' ) *   ≈⟨ IsCCC.*-cong isCCC ( begin
@@ -315,7 +309,7 @@
               (ε ∙ < f ∙ π , π' > ) ∙ <  π  ,   π'   >   ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
               (ε ∙ < f ∙ π , π' > ) ∙ id1 A  (１ ∧ a) ≈⟨ idR ⟩
               ε ∙ < f ∙ π , π' > ∎ ) ⟩
-           ( ε o < A [ f o π ] , π' > ) *   ≈⟨ IsCCC.e4b isCCC  ⟩
+           ( ε ∙ < A [ f o π ] , π' > ) *   ≈⟨ IsCCC.e4b isCCC  ⟩
            f ∎