view src/Polynominal.agda @ 1092:e1816090be31

could be. but give up now
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 17 May 2021 09:30:48 +0900
parents 9f967d9312f1
children
line wrap: on
line source

{-# OPTIONS --allow-unsolved-metas #-}

open import Category
open import CCC
open import Level
open import HomReasoning 
open import cat-utility
open import Relation.Nullary
open import Data.Empty
open import Data.Product renaming ( <_,_> to ⟪_,_⟫ )

module Polynominal { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( C : CCC A )   where

  open CCC.CCC C
  open ≈-Reasoning A hiding (_∙_)

  _∙_ = _[_o_] A

  --
  --   Polynominal (p.57) in Introduction to Higher order categorical logic
  --
  --   Given object a₀ and a of a caterisian closed category A, how does one adjoin an interminate arraow x : a₀ → a to A?
  --   A[x] based on the `assumption' x, as was done in Section 2 (data φ). The formulas of A[x] are the objects of A and the
  --   proofs of A[x] are formed from the arrows of A and the new arrow x :  a₀ → a by the appropriate ules of inference.
  --
  -- Here, A is actualy A[x]. It contains x and all the arrow generated from x.
  -- If we can put constraints on rule i (sub : Hom A b c → Set), then A is strictly smaller than A[x],
  -- that is, a subscategory of A[x].
  --
  --   i   : {b c : Obj A} {k : Hom A b c } → sub k  → φ x k
  --         sub k is ¬ ( k ≈ x ), we cannot write this because b≡⊤ c≡a is forced
  --
  -- this makes a few changes, but we don't care.
  -- from page. 51
  --

  open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 

  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 ( f ∙ g )
     v   : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }  (ψ : φ x f )  → φ x {b} {c'' <= c'} ( f * )
  
  α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
  α = < π  ∙ π   , < π'  ∙ π  , π'  > >
  
  -- genetate (a ∧ b) → c proof from  proof b →  c with assumption a
  -- from page. 51
  
  k : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y  : φ {a} x∈a z ) → Hom A (a ∧ b) c
  k x∈a {k} (i _) = k ∙ π'
  k x∈a ii = π
  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 ψ  ∙ α ) *

  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 z

  -- The Polynominal arrow  -- λ term in A
  --
  -- arrow in A[x], equality in A[x] should be a modulo x, that is  k x phi ≈ k x phi'
  -- the smallest equivalence relation
  --
  -- 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 Data.Unit
  xnef :  {a b c : Obj A } → ( x∈a : Hom A 1 a ) → {f : Hom A b c } → ( y  : φ {a} x∈a f ) → Set c₂
  xnef {a} {b} {c} x (i f) = ¬ (x ≅ f)
  xnef {a} {1}  x  ii = Lift _ ⊤
  xnef {a} {b}  x  (iii phi phi₁) = xnef x phi × xnef x phi₁
  xnef {a} {b}  x  (iv phi phi₁) = xnef x phi × xnef x phi₁
  xnef {a} {b}  x  (v phi) = xnef x phi

  nx :  {a b c : Obj A } → ( x : Hom A 1 a ) → {f : Hom A b c } → ( y  : φ {a} x f ) → xnef x y → ¬ (x ≅ f)
  nx = {!!}

  record Poly (a c b : Obj A )  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
    field
       x :  Hom A 1 a                                            -- λ x
       f :  Hom A b c
       phi  : φ x {b} {c} f                                      -- construction of f
       nf : xnef x {f} phi

  -- since we have A[x] now, we can proceed the proof on p.64 in some possible future

  --
  --  Proposition 6.1
  --
  --  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).

  record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set  (c₁ ⊔ c₂ ⊔ ℓ) where
    x = Poly.x p
    field 
      fun  : Hom A (a ∧ b) c
      fp   : A [  fun ∙ <  x ∙ ○ b   , id1 A b  >  ≈ Poly.f p  ]
      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 1 ) 
         :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
    field
      sl :  Hom A a b 
    g :  Hom A 1 (b <= a) 
    g  = ( sl ∙ π'  ) *
    field
      isSelect : A [   ε ∙ < g  , Poly.x φ  >   ≈  Poly.f φ  ]
      isUnique : (f : Hom A 1 (b <= a) )  → A [   ε ∙ < 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
  e2 = IsCCC.e2 isCCC

  -- 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 1 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 ∙ π' .

  ki : {a b c : Obj A} → (x : Hom A 1 a) → (f : Hom A b c ) → (fp  :  φ x {b} {c} f )
     → xnef x fp → ¬ (x ≅ f) →  A [ k x (i f) ≈ k x fp ]
  ki x f (i _) _ _ = refl-hom
  ki {a} x .x ii _ ne  = ⊥-elim ( ne  HE.refl )
  ki x _ (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) xf ne  = begin
               < f₁ ,  f₂  > ∙ π'  ≈⟨ IsCCC.distr-π isCCC ⟩
               < f₁ ∙ π'  ,  f₂   ∙ π' >  ≈⟨ π-cong (ki x f₁ fp₁ (proj₁ xf) {!!}) (ki x f₂ fp₂ (proj₂ xf) {!!})  ⟩
                k x (iii  fp₁ fp₂ )  ∎ 
  ki x _ (iv {_} {_} {_} {f₁} {f₂} fp fp₁) xf ne = begin
               (f₁ ∙ f₂  ) ∙ π'  ≈↑⟨ assoc ⟩
               f₁  ∙ ( f₂ ∙ π')  ≈↑⟨ cdr (IsCCC.e3b isCCC) ⟩
               f₁  ∙ ( π'  ∙ < π , (f₂ ∙ π' )  >)  ≈⟨ assoc ⟩
               (f₁  ∙ π' ) ∙ < π , (f₂ ∙ π' )  >  ≈⟨ resp (π-cong refl-hom (ki x _ fp₁ (proj₂ xf) {!!}) ) (ki x _ fp (proj₁ xf) {!!}) ⟩
               k x fp ∙ < π , k x fp₁ >  ≈⟨⟩
               k x (iv fp fp₁ )  ∎  
  ki x _ (v {_} {_} {_} {f} fp) xf ne = begin
               (f *) ∙ π' ≈⟨ distr-*  ⟩
               ( f ∙ < π' ∙ π , π'  > ) * ≈↑⟨ *-cong (cdr (IsCCC.e3b isCCC)) ⟩
               ( f ∙ ( π'  ∙  < π ∙ π , < π' ∙  π , π' > > ) ) *  ≈⟨ *-cong assoc  ⟩
               ( (f ∙ π')  ∙  < π ∙ π , < π' ∙  π , π' > > ) *  ≈⟨ *-cong ( car ( ki x _ fp xf {!!} )) ⟩
               ( k x fp ∙  < π ∙ π , < π' ∙  π , π' > > ) *  ≈⟨⟩
               k x (v fp )  ∎  
  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=f = begin
          k (Poly.x f) (Poly.phi f) ≈↑⟨ ki  (Poly.x f) (Poly.f f)  (Poly.phi f) (Poly.nf f ) {!!} ⟩
          Poly.f f ∙ π' ≈⟨ car f=f  ⟩
          Poly.f g ∙ π'  ≈⟨ ki  (Poly.x g) (Poly.f g)  (Poly.phi g) (Poly.nf 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)
       ; 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 (Poly.nf p ) {!!} eq 
     } where 
        fc0 : {a b c : Obj A}  → (x :  Hom A 1 a) (f :  Hom A b c) (phi  :  φ x {b} {c} f )
           → A [  k x phi ∙ <  x ∙ ○ b  , id1 A b >  ≈ f ]
        fc0 {a} {b} {c} x f' phi with phi
        ... | i {_} {_} s = begin
             (s ∙ π') ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩
             s ∙ (π' ∙ < ( x ∙ ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩
             s ∙ id1 A b ≈⟨ idR ⟩
             s ∎ 
        ... | ii = begin
             π ∙ < ( x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.e3a isCCC ⟩
             x ∙ ○ b  ≈↑⟨ cdr (e2 ) ⟩
             x ∙ id1 A b  ≈⟨ idR ⟩
             x ∎  
        ... | iii {_} {_} {_} {f} {g} y z  = begin
             < k x y , k x z > ∙ < (x ∙ ○ b ) , id1 A b > ≈⟨ IsCCC.distr-π isCCC  ⟩
             < k x y ∙ < (x ∙ ○ b ) , id1 A b > , k x z ∙ < (x ∙ ○ b ) , id1 A b > >
                 ≈⟨ π-cong (fc0 x  f y ) (fc0 x g z ) ⟩
             < f , g > ≈⟨⟩
             f'  ∎  
        ... | iv {_} {_} {d} {f} {g} y z  = begin
             (k x y ∙ < π , k x z >) ∙ < ( x ∙ ○ b ) , id1 A b > ≈↑⟨ assoc ⟩
             k x y ∙ ( < π , k x z > ∙ < ( x ∙ ○ b ) , id1 A b > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
             k x y ∙ ( < π  ∙ < ( x ∙ ○ b ) , id1 A b > ,  k x z  ∙ < ( x ∙ ○ b ) , id1 A b > > )
                 ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) (fc0 x g z ) ) ⟩
             k x y ∙ ( < x ∙ ○ b  ,  g > ) ≈↑⟨ cdr (π-cong (cdr (e2)) refl-hom ) ⟩
             k x y ∙ ( < x ∙ ( ○ d ∙ g ) ,  g > ) ≈⟨  cdr (π-cong assoc (sym idL)) ⟩
             k x y ∙ ( < (x ∙ ○ d) ∙ g  , id1 A d ∙ g > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩
             k x y ∙ ( < x ∙ ○ d ,  id1 A d > ∙ g ) ≈⟨ assoc ⟩
             (k x y ∙  < x ∙ ○ d ,  id1 A d > ) ∙ g  ≈⟨ car (fc0 x f y ) ⟩
             f ∙ g  ∎   
        ... | v {_} {_} {_} {f} y = begin
            ( (k x y ∙ < π ∙ π , <  π' ∙  π , π' > >) *) ∙ < x ∙ (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩
            ( (k x y ∙ < π ∙ π , <  π' ∙  π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) * ≈⟨  IsCCC.*-cong isCCC ( begin
             ( k x y ∙ < π ∙ π , <  π' ∙  π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' >   ≈↑⟨ assoc ⟩
              k x y ∙ ( < π ∙ π , <  π' ∙  π , π' > > ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > )   ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
              k x y ∙ < (π ∙ π) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' >  , <  π' ∙  π , π' > ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' >  >
                  ≈⟨ cdr (π-cong (sym assoc) (IsCCC.distr-π isCCC )) ⟩
              k x y ∙ < π ∙ (π ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) ,
                <  (π' ∙  π) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > , π'  ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > > >
                    ≈⟨ cdr ( π-cong (cdr (IsCCC.e3a isCCC))( π-cong (sym assoc) (IsCCC.e3b isCCC) )) ⟩
              k x y ∙ < π ∙ ( < x ∙ ○ b , id1 A _ > ∙ π  ) , <  π' ∙  (π ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' >) ,  π'  > >
                ≈⟨  cdr ( π-cong refl-hom (  π-cong (cdr (IsCCC.e3a isCCC)) refl-hom )) ⟩
              k x y ∙ < (π ∙ ( < x ∙ ○ b , id1 A _ > ∙ π ) ) , <  π' ∙  (< x ∙ ○ b , id1 A _ > ∙ π ) , π' > >
                ≈⟨ cdr ( π-cong  assoc (π-cong  assoc refl-hom )) ⟩
              k x y ∙ < (π ∙  < x ∙ ○ b , id1 A _ > ) ∙ π   , <  (π' ∙  < x ∙ ○ b , id1 A _ > ) ∙ π  , π' > >
                  ≈⟨ cdr (π-cong (car (IsCCC.e3a isCCC)) (π-cong (car (IsCCC.e3b isCCC)) refl-hom ))  ⟩
              k x y ∙ < ( (x ∙ ○ b ) ∙ π )  , <   id1 A _  ∙ π  , π' > >    ≈⟨ cdr (π-cong (sym assoc)  (π-cong idL refl-hom ))  ⟩
              k x y ∙ <  x ∙ (○ b  ∙ π )  , <    π  , π' > >    ≈⟨   cdr (π-cong (cdr (e2)) (IsCCC.π-id isCCC) ) ⟩
              k x y ∙  < x ∙ ○ _ , id1 A _  >    ≈⟨ fc0 x f y  ⟩
             f  ∎ )  ⟩
             f * ∎  
        --
        --   f ∙ <  x ∙ ○ b  , id1 A b >  ≈ f →  f ≈ k x (phi p)
        -- 
        uniq : {a b c : Obj A}  → (x :  Hom A 1 a) (f :  Hom A b c) (phi  :  φ x {b} {c} f ) (f' : Hom A (a ∧ b) c)
            → xnef x phi
            → ¬ x ≅ f
            → A [  f' ∙ <  x ∙ ○ b  , id1 A b >  ≈ f ] → A [ f' ≈ k x phi ]
        uniq {a} {b} {c} x f phi f' xf ne fx=p  = sym (begin
               k x phi ≈↑⟨ ki x f phi xf ne ⟩
               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 ∙ π' > ) 
               f' ∙ <  k x (i (x ∙ ○ b)) ,  k x {id1 A b} (i _) >  ≈⟨ cdr (π-cong u2 refl-hom) ⟩ -- ( f' ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ) 
               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 ) ⟩ 
               f' ∙  <  π ∙ < π , (○ b ∙ π' ) >  , π' >   ≈⟨ cdr (π-cong (IsCCC.e3a isCCC)  refl-hom) ⟩
               f' ∙  < π , π' >  ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
               f' ∙  id1 A _ ≈⟨ idR ⟩
               f' ∎  )  where
                   xf1 : {a b : Obj A} → ( x : Hom A 1 a ) →  (f : Hom A b a) → (fp : φ x f) → φ x f ≅ φ x (x ∙ ○ b) → xnef x fp
                   xf1 x f  (i .f) eq = {!!}
                   xf1 x f ii eq = lift tt
                   xf1 x f (iii fp fp₁) eq = {!!}
                   xf1 x f (iv fp fp₁) eq = {!!} -- φ x (f₂ ∙ g) ≅ φ x (x ∙ ○ b₂) → 
                   xf1 x f (v fp) eq = {!!}
                   u2 : k x {x ∙ ○ b} (i _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _) >  --  (x ∙ (○ b)) ∙ π' ≈ π ∙ < π , (○ b) ∙ π' >
                   u2 = ki x (x ∙ ○ b) (iv ii (i _)) (xf1 x (x ∙ ○ b) (iv ii (i _)) HE.refl) {!!}

  -- functional completeness ε form
  --
  --  g : Hom A 1 (b <= a)       fun : Hom A (a ∧ 1) c
  --       fun *                       ε ∙ < g ∙ π , π' >
  --  a -> d <= b  <-> (a ∧ b ) -> d
  --            
  --   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 1 )  → Fc {a} {b} φ 
  FC {a} {b} φ = record {
     sl =  k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > 
     ; isSelect = isSelect
     ; isUnique = uniq 
    }  where
        π-exchg = IsCCC.π-exchg isCCC
        fc0 :  {b c : Obj A} (p : Poly b c 1) → A [  k (Poly.x p ) (Poly.phi p) ∙ <  Poly.x p  ∙  ○ 1  , id1 A 1 >  ≈ 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 φ ]
        gg  = begin
          ( k (Poly.x φ ) (Poly.phi φ) ∙ < id1 A _ ,  ○ a  > ) ∙ Poly.x φ   ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC ) ) ⟩
          k (Poly.x φ ) (Poly.phi φ) ∙ <  id1 A _ ∙  Poly.x φ  ,  ○ a ∙ Poly.x φ >  ≈⟨ cdr (π-cong idL e2 ) ⟩
          k (Poly.x φ ) (Poly.phi φ) ∙ <   Poly.x φ  ,  ○ 1 >  ≈⟨ cdr (π-cong (trans-hom (sym idR) (cdr e2) )  (sym e2) ) ⟩
          k (Poly.x φ ) (Poly.phi φ) ∙ <  Poly.x φ  ∙  ○ 1  , id1 A 1 >  ≈⟨ fc0 φ  ⟩
          Poly.f φ ∎
        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  >)  ∙ π' ) * )  ∙   ○ 1 ,  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 1 (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
              (k (Poly.x φ) (Poly.phi φ) ∙ < id1 A _ , ○ a >) ∙ π' ≈↑⟨ assoc ⟩
              k (Poly.x φ) (Poly.phi φ) ∙ (< id1 A _ , ○ a > ∙ π') ≈⟨ car ( sym (Functional-completeness.uniq (functional-completeness φ) _ ( begin
                ((ε ∙ < f ∙ π , π' >) ∙ < π' , π >) ∙ < Poly.x φ ∙ ○ 1 , id1 A 1 > ≈↑⟨ assoc ⟩
                (ε ∙ < f ∙ π , π' >) ∙ ( < π' , π > ∙ < Poly.x φ ∙ ○ 1 , id1 A 1 > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
                (ε ∙ < f ∙ π , π' >) ∙  < π' ∙ < Poly.x φ ∙ ○ 1 , id1 A 1 > , π ∙  < Poly.x φ ∙ ○ 1 , id1 A 1 > >
                     ≈⟨ cdr (π-cong (IsCCC.e3b isCCC) (IsCCC.e3a isCCC)) ⟩
                (ε ∙ < f ∙ π , π' >) ∙  < id1 A 1  ,  Poly.x φ ∙ ○ 1 > ≈↑⟨ assoc ⟩
                ε ∙ ( < f ∙ π , π' > ∙  < id1 A 1  ,  Poly.x φ ∙ ○ 1 > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
                ε ∙ ( < (f ∙ π ) ∙  < id1 A 1  ,  Poly.x φ ∙ ○ 1 > , π'  ∙  < id1 A 1  ,  Poly.x φ ∙ ○ 1 > > ) ≈⟨ cdr (π-cong (sym assoc) (IsCCC.e3b isCCC)) ⟩
                ε ∙ ( < f ∙ (π  ∙  < id1 A 1  ,  Poly.x φ ∙ ○ 1 > ) ,  Poly.x φ ∙ ○ 1  > ) ≈⟨ cdr (π-cong (cdr (IsCCC.e3a isCCC)) (cdr (trans-hom e2 (sym e2)))) ⟩
                ε ∙ ( < f ∙ id1 A 1 ,  Poly.x φ ∙ id1 A 1  > ) ≈⟨ cdr (π-cong idR idR ) ⟩
                 ε ∙ < f , Poly.x φ > ≈⟨ eq ⟩
                Poly.f φ ∎ ))) ⟩
              ((ε ∙ < f ∙ π , π' > ) ∙ < π' , π > ) ∙  ( < id1 A _ ,  ○ a > ∙ π' ) ≈↑⟨ assoc ⟩
              (ε ∙ < f ∙ π , π' > ) ∙ (< π' , π > ∙ ( < id1 A _ ,  ○ a > ∙ π' ) )  ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
              (ε ∙ < f ∙ π , π' > ) ∙ (< π'  ∙ ( < id1 A _ ,  ○ a > ∙ π' ) , π ∙ ( < id1 A _ ,  ○ a > ∙ π' ) > )  ≈⟨ cdr (π-cong assoc assoc ) ⟩
              (ε ∙ < f ∙ π , π' > ) ∙ (< (π'  ∙  < id1 A _ ,  ○ a > ) ∙ π'  , (π ∙ < id1 A _ ,  ○ a > ) ∙ π'   > )
                 ≈⟨ cdr (π-cong (car (IsCCC.e3b isCCC)) (car (IsCCC.e3a isCCC) ))  ⟩
              (ε ∙ < f ∙ π , π' > ) ∙ < ○ a  ∙ π'  ,  id1 A _ ∙ π'   >   ≈⟨ cdr (π-cong (trans-hom e2 (sym e2) ) idL ) ⟩
              (ε ∙ < f ∙ π , π' > ) ∙ <  π  ,   π'   >   ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
              (ε ∙ < f ∙ π , π' > ) ∙ id1 A  (1 ∧ a) ≈⟨ idR ⟩
              ε ∙ < f ∙ π , π' > ∎ ) ⟩
           ( ε ∙ < A [ f o π ] , π' > ) *   ≈⟨ IsCCC.e4b isCCC  ⟩
           f ∎ 



-- end