# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1620786641 -32400
# Node ID c61639f34e7b55902553cc0d82f65c6add56454a
# Parent  d07cfce032369c45fc5c96aa44d0fd78fe547811
fix Poly minimum equality

diff -r d07cfce03236 -r c61639f34e7b src/Polynominal.agda
--- a/src/Polynominal.agda	Wed May 12 00:42:14 2021 +0900
+++ b/src/Polynominal.agda	Wed May 12 11:30:41 2021 +0900
@@ -67,17 +67,7 @@
        x :  Hom A １ a
        f :  Hom A b c
        phi  :  φ x {b} {c} f 
-
-  -- f  ≈ g → k x {f} _ ≡  k x {g} _   Lambek p.60
-  --   if A is locally small, it is ≡-cong.
-  --   case i i is π ∙ f ≈ π ∙ g
-  --   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)
-  -- 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
+       idx : {a : Obj A} → {x : Hom A １ a} → x ∙ ○ a  ≈ id1 A a
 
   -- since we have A[x] now, we can proceed the proof on p.64 in some possible future
 
@@ -86,8 +76,6 @@
   --
   --  For every polynominal ψ(x) : b → c in an indeterminate x : 1 → a over a cartesian or cartesian closed
   --  category A there is a unique arrow f : a ∧ b → c in A such that f ∙ < x ∙ ○ b , id1 A b > ≈ ψ(x).
-  --
-  --  equality assumption in uniq should be modulo-x, k x phi ≈ k x phi'
 
   record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set  (c₁ ⊔ c₂ ⊔ ℓ) where
     x = Poly.x p
@@ -115,17 +103,78 @@
   *-cong = IsCCC.*-cong isCCC
   distr-* = IsCCC.distr-* isCCC
   e2 = IsCCC.e2 isCCC
-  idx : {a : Obj A} → {x : Hom A １ a} → x ∙ ○ a  ≈ id1 A a
-  idx {a} {x} = begin
-      x ∙ ○ a ≈⟨ {!!} ⟩
-      id1 A a ∎
+
+  -- f  ≈ g → k x {f} _ ≡  k x {g} _   Lambek p.60
+  --   if A is locally small, it is ≡-cong.
+  --   case i i is π ∙ f ≈ π ∙ g
+  --   we have (x y :  Hom A １ a) → x ≈ y (minimul equivalende assumption) in record Poly. this makes all k x ii case valid
+  --   all other cases, arguments are reduced to f ∙ π' .
+
+  mineq : {a b c : Obj A } → Poly a b c → (x y :  Hom A １ a) → x ≈ y 
+  mineq {a} p x y = begin
+      x  ≈↑⟨ idR ⟩
+      x  ∙ id1 A １ ≈⟨ cdr e2 ⟩
+      x  ∙  ○ _ ≈↑⟨ cdr e2 ⟩
+      x  ∙ (○ a  ∙ y )  ≈⟨ assoc ⟩
+      (x  ∙ ○ a ) ∙ y   ≈⟨ car (Poly.idx p) ⟩
+      id1 A _ ∙ y   ≈⟨ idL ⟩
+      y ∎
+  ki : {a b b' c c' : Obj A} → Poly a c' b'  → (x : Hom A １ a) → (f : Hom A b c ) → (fp  :  φ x {b} {c} f ) → A [ f ∙  π' ≈ k x fp ]
+  ki p x f i = refl-hom
+  ki {a} p x .x ii  = begin
+               x ∙ π'   ≈⟨ cdr e2 ⟩
+               x ∙ ○ (a ∧ １) ≈↑⟨ cdr e2 ⟩
+               x ∙ (○ a ∙ π )  ≈⟨ assoc ⟩
+               (x ∙ ○ a ) ∙ π   ≈⟨ car (Poly.idx p) ⟩
+               id1 A a ∙ π   ≈⟨ idL ⟩
+               k x ii  ∎  
+  ki p x .(< f₁  , f₂ > ) (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) = begin
+               < f₁ ,  f₂  > ∙ π'  ≈⟨ IsCCC.distr-π isCCC ⟩
+               < f₁ ∙ π'  ,  f₂   ∙ π' >  ≈⟨ π-cong (ki p x f₁ fp₁) (ki p x f₂ fp₂) ⟩
+                k x (iii  fp₁ fp₂ )  ∎  
+  ki p x .((A Category.o _) _) (iv {_} {_} {_} {f₁} {f₂} fp fp₁) = begin
+               (f₁ ∙ f₂  ) ∙ π'  ≈↑⟨ assoc ⟩
+               f₁  ∙ ( f₂ ∙ π')  ≈↑⟨ cdr (IsCCC.e3b isCCC) ⟩
+               f₁  ∙ ( π'  ∙ < π , (f₂ ∙ π' )  >)  ≈⟨ assoc ⟩
+               (f₁  ∙ π' ) ∙ < π , (f₂ ∙ π' )  >  ≈⟨ resp (π-cong refl-hom (ki p x _ fp₁) ) (ki p x _ fp) ⟩
+               k x fp ∙ < π , k x fp₁ >  ≈⟨⟩
+               k x (iv fp fp₁ )  ∎  
+  ki p x .((C CCC.*) _) (v fp) = {!!}
+  ki p x f (φ-cong x₁ 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 = kcong f (Poly.x f ) (Poly.f f) (Poly.f g) f=f ( Poly.phi f ) ( Poly.phi g) where
+     kcong : {a b b' c c' : Obj A} → Poly a c' b'
+        → (x : Hom A １ a) → (f g : Hom A b c ) → (f=g : f ≈ g ) → (fp  :  φ x {b} {c} f )( gp :  φ x {b} {c} g ) → A [ k x fp  ≈ k x gp ]
+     kcong {a} {b} {c} p x f g f=g i i = resp refl-hom f=g
+     kcong {a} {.(CCC.１ C)} {_} {.a} p x f .x f=g i ii = begin
+          k x {f} i ≈⟨⟩
+          f ∙ π' ≈⟨ car f=g ⟩
+          x ∙ π' ≈⟨ ki p x x ii ⟩
+          k x ii ∎   
+     kcong {a} {b} {_} {.((C CCC.∧ _) _)} p x f .(< g₁ , g₂ >)  f=g i (iii {_} {_} {_} {g₁} {g₂} gp₁ gp₂) = begin
+          k x i ≈⟨ car f=g ⟩
+          < g₁ , g₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩
+          < g₁ ∙ π' , g₂ ∙ π' >  ≈⟨ IsCCC.π-cong isCCC (ki p x _ gp₁ ) (ki p x _ gp₂) ⟩
+          < k x gp₁  , k x gp₂  >  ≈⟨⟩
+          k x (iii gp₁ gp₂) ∎   
+     kcong {a} {b} {_} {c} p x f .((A Category.o _) _) f=g i (iv gp gp₁) = {!!}
+     kcong {a} {b} {_} {.((C CCC.<= _) _)} p x f .((C CCC.*) _) f=g i (v gp) = {!!}
+     kcong {a} {b} {_} {c} p x f g f=g i (φ-cong x₁ gp) = {!!}
+     kcong {a} {.(CCC.１ C)} {_} {.a} p x .x g f=g ii gp = {!!}
+     kcong {a} {b} {_} {.((C CCC.∧ _) _)} p x .(CCC.< C , _ > _) g f=g (iii fp fp₁) gp = {!!}
+     kcong {a} {b} {_} {c} p x .((A Category.o _) _) g f=g (iv fp fp₁) gp = {!!}
+     kcong {a} {b} {_} {.((C CCC.<= _) _)} p x .((C CCC.*) _) g f=g (v fp) gp = {!!}
+     kcong {a} {b} {_} {c} p x f g f=g (φ-cong x₁ fp) gp = {!!}
+
 
   -- proof in p.59 Lambek
   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)
        ; fp = fc0 (Poly.x p) (Poly.f p) (Poly.phi p)
-       ; uniq = λ f eq  → uniq (Poly.x p) (Poly.f p) (Poly.phi p) f eq
+       ; uniq = λ f eq  → uniq p (Poly.x p) (Poly.f p) (Poly.phi p) f eq
      } where 
         fc0 : {a b c : Obj A}  → (x :  Hom A １ a) (f :  Hom A b c) (phi  :  φ x {b} {c} f )
            → A [  k x phi ∙ <  x ∙ ○ b  , id1 A b >  ≈ f ]
@@ -182,36 +231,14 @@
         --
         --   f ∙ <  x ∙ ○ b  , id1 A b >  ≈ f →  f ≈ k x (phi p)
         -- 
-        ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp  :  φ x {b} {c} f ) → A [ f ∙  π' ≈ k x fp ]
-        ki x f i = refl-hom
-        ki {a} x .x ii  = begin
-               x ∙ π'   ≈⟨ {!!} ⟩
-               x ∙ ○ (a ∧ １) ≈⟨ {!!} ⟩
-               x ∙ (○ a ∙ π )  ≈⟨ {!!} ⟩
-               (x ∙ ○ a ) ∙ π   ≈⟨ {!!} ⟩
-               id1 A a ∙ π   ≈⟨ {!!} ⟩
-               k x ii  ∎  
-        ki x .(< f₁  , f₂ > ) (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) = begin
-               < f₁ ,  f₂  > ∙ π'  ≈⟨ IsCCC.distr-π isCCC ⟩
-               < f₁ ∙ π'  ,  f₂   ∙ π' >  ≈⟨ π-cong (ki x f₁ fp₁) (ki x f₂ fp₂) ⟩
-                k x (iii  fp₁ fp₂ )  ∎  
-        ki x .((A Category.o _) _) (iv {_} {_} {_} {f₁} {f₂} fp fp₁) = begin
-               (f₁ ∙ f₂  ) ∙ π'  ≈⟨ {!!}  ⟩
-               f₁  ∙ ( f₂ ∙ π')  ≈⟨ {!!} ⟩
-               f₁  ∙ ( π'  ∙ < π , (f₂ ∙ π' )  >)  ≈⟨ {!!} ⟩
-               (f₁  ∙ π' ) ∙ < π , (f₂ ∙ π' )  >  ≈⟨ {!!} ⟩
-               k x fp ∙ < π , k x fp₁ >  ≈⟨⟩
-               k x (iv fp fp₁ )  ∎  
-        ki x .((C CCC.*) _) (v fp) = {!!}
-        ki x f (φ-cong x₁ fp) = {!!}
-        uniq : {a b c : Obj A}  → (x :  Hom A １ a) (f :  Hom A b c) (phi  :  φ x {b} {c} f ) (f' : Hom A (a ∧ b) c) →
+        uniq : {a b c : Obj A}  → (p : Poly a c b) → (x :  Hom A １ a) (f :  Hom A b c) (phi  :  φ x {b} {c} f ) (f' : Hom A (a ∧ b) c) →
             A [  f' ∙ <  x ∙ ○ b  , id1 A b >  ≈ f ] → A [ f' ≈ k x phi ]
-        uniq {a} {b} {c} x f phi  f' fx=p  = sym (begin
-               k x phi ≈↑⟨ ki x f phi ⟩
+        uniq {a} {b} {c} p x f phi  f' fx=p  = sym (begin
+               k x phi ≈↑⟨ ki p x f phi ⟩
                k x {f} i ≈↑⟨ car fx=p ⟩
                k x {f' ∙ < x ∙ ○ b , id1 A b >} i ≈⟨ trans-hom (sym assoc)  (cdr (IsCCC.distr-π isCCC) ) ⟩ -- ( f' ∙ < x ∙ ○ b , id1 A b> ) ∙ π'
                f' ∙ k x {< x ∙ ○ b , id1 A b >} (iii i i ) -- ( f' ∙ < (x ∙ ○ b) ∙ π'              , id1 A b ∙ π' > ) 
-                  ≈⟨ cdr (π-cong (ki x ( x ∙ ○ b) (iv ii i) ) refl-hom)  ⟩
+                  ≈⟨ cdr (π-cong (ki p x ( x ∙ ○ b) (iv ii i) ) refl-hom)  ⟩
                f' ∙ < k x {x ∙ ○ b} (iv ii i ) , k x {id1 A b} i >   ≈⟨ refl-hom ⟩
                f' ∙ < k x {x} ii ∙ < π , k x {○ b} i >  , k x {id1 A b} i >   -- ( f' ∙ < π ∙ < π , (x ∙ ○ b) ∙ π' >  , id1 A b ∙ π' > ) 
                    ≈⟨ cdr (π-cong (cdr (π-cong refl-hom (car e2))) idL ) ⟩ 
@@ -220,34 +247,6 @@
                f' ∙  id1 A _ ≈⟨ idR ⟩
                f' ∎  ) 
 
-  ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp  :  φ x {b} {c} f ) → A [ f ∙  π' ≈ k x fp ]
-  ki = {!!}
-  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 = kcong (Poly.x f ) (Poly.f f) (Poly.f g) f=f ( Poly.phi f ) ( Poly.phi g) where
-     kcong : {a b c : Obj A} → (x : Hom A １ a) → (f g : Hom A b c ) → (f=g : f ≈ g ) → (fp  :  φ x {b} {c} f )( gp :  φ x {b} {c} g ) → A [ k x fp  ≈ k x gp ]
-     kcong {a} {b} {c} x f g f=g i i = resp refl-hom f=g
-     kcong {a} {.(CCC.１ C)} {.a} x f .x f=g i ii = begin
-          k x {f} i ≈⟨⟩
-          f ∙ π' ≈⟨ car f=g ⟩
-          x ∙ π' ≈⟨ ki x x ii ⟩
-          k x ii ∎   
-     kcong {a} {b} {.((C CCC.∧ _) _)} x f .(< g₁ , g₂ >)  f=g i (iii {_} {_} {_} {g₁} {g₂} gp₁ gp₂) = begin
-          k x i ≈⟨ car f=g ⟩
-          < g₁ , g₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩
-          < g₁ ∙ π' , g₂ ∙ π' >  ≈⟨ IsCCC.π-cong isCCC (ki x _ gp₁ ) (ki x _ gp₂) ⟩
-          < k x gp₁  , k x gp₂  >  ≈⟨⟩
-          k x (iii gp₁ gp₂) ∎   
-     kcong {a} {b} {c} x f .((A Category.o _) _) f=g i (iv gp gp₁) = {!!}
-     kcong {a} {b} {.((C CCC.<= _) _)} x f .((C CCC.*) _) f=g i (v gp) = {!!}
-     kcong {a} {b} {c} x f g f=g i (φ-cong x₁ gp) = {!!}
-     kcong {a} {.(CCC.１ C)} {.a} x .x g f=g ii gp = {!!}
-     kcong {a} {b} {.((C CCC.∧ _) _)} x .(CCC.< C , _ > _) g f=g (iii fp fp₁) gp = {!!}
-     kcong {a} {b} {c} x .((A Category.o _) _) g f=g (iv fp fp₁) gp = {!!}
-     kcong {a} {b} {.((C CCC.<= _) _)} x .((C CCC.*) _) g f=g (v fp) gp = {!!}
-     kcong {a} {b} {c} x f g f=g (φ-cong x₁ fp) gp = {!!}
-
 
   -- functional completeness ε form
   --
diff -r d07cfce03236 -r c61639f34e7b src/ToposIL.agda
--- a/src/ToposIL.agda	Wed May 12 00:42:14 2021 +0900
+++ b/src/ToposIL.agda	Wed May 12 11:30:41 2021 +0900
@@ -55,8 +55,8 @@
      _,_⊢_  {a} {b} p p1 q = {c : Obj A} (h : Hom A c b ) → A [ Poly.f p ∙  h  ≈  ⊤ ∙  ○  c  ]
          → A [   Poly.f p1 ∙ h  ≈  ⊤ ∙  ○  c  ] 
          → A [   Poly.f q  ∙ h  ≈  ⊤ ∙  ○  c  ] 
-     expr : {a b c  : Obj A}  (p : Hom A １ Ω  )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
-     expr p x = record { x = x ;  f = p ; phi = i }
+     -- expr : {a b c  : Obj A}  (p : Hom A １ Ω  )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
+     -- expr p x = record { x = x ;  f = p ; phi = i ; idx = {!!} }
      ⊨_ :   (p : Hom A １ Ω  ) →  Set  ( c₁  ⊔  c₂ ⊔ ℓ )
      ⊨  p = {c : Obj A} (h : Hom A c １ )  → A [ p  ∙ h  ≈  ⊤ ∙  ○  c ] 
 
@@ -91,7 +91,7 @@
       ;  _∈_ = λ {a} x α →  A [ ε o < α , x > ]
       -- { 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 }
+      ;  apply = λ {a}  φ x → record { x = x ; f = Functional-completeness.fun (fc0 t φ ) ∙ < x ∙  ○ _ , id1 A _ >  ; phi = i ; idx = Poly.idx φ }
       ;  isIL = record {
            isSelect = {!!}
          ; uniqueSelect = {!!}