I'd like to ask what /incompatible types/ Q equates for OTT in

        (λu:1.u[Q> u)(<Q](λu:1.u[Q> u)):1
          |-> (<Q](λu:1.u[Q> u))[Q> (<Q](λu:1.u[Q> u))

I think this program is clear to me only for ITT.

------------------------------------------------------------------------------
     ( Q : S = T ;  s : S !
let  !--------------------!
     !    coe Q s : T     )
                           
     coe Q s <= case Q     
     { coe refl s => s     
     }                     
------------------------------------------------------------------------------
     ( Q : S = T ;  t : T !
let  !--------------------!
     !    eoc Q t : S     )
                           
     eoc Q t <= case Q     
     { eoc refl t => t     
     }                     
------------------------------------------------------------------------------
inspect lam Q : One = (all x : One => One) =>                                
          (lam u : One => coe Q u u) (eoc Q (lam u : One => coe Q u u))      
          =>                                                                 
          (lam Q =>                                                         !
          !  coe Q (eoc Q (lam u => coe Q u u)) (eoc Q (lam u => coe Q u u)))
           : all Q : One = (all x : One => One) => One                       
------------------------------------------------------------------------------

Because coercion ist defined by case analysis ι-reduction gets stuck.

 I recently got myself a text from Robert Constable to get a grip on ETT
(his contribution  to the book  by Buss), where  he gives an  example of
typing general recursion  correct. But this is not an  issue here, since
it would be precluded by strict-positivity conditions.

But concerning your claims on /equality reflection/ for ETT

       Γ |- s01 : s0 = s1
       ------------------
          Γ |- s0 ≡ s1

I'd like ask what's meant by s01 get's thrown away such that terms don't
guarantee type inhabitation.

 To me the extensionality law looks  like some sort of /completion/: add
to the definition what follows from it anyway.

So  I'm wondering  wether  this rule  destroys  normalization for  every
commutative operation.

Like from

          0 + n |-> n
        1+m + n |-> 1+ m + n

it's provable that

        m + n = n + m

and so from

       Γ |- p : m + n = n + m
       -----------------------
          Γ |- m + n ≡ n + m

you could alway proceed

        m + n |-> n + m


Cheers,
Sebastian

-- 
Who then art thou?      
 
                        GENERAL RECURSION

                Part of that power which still
                - computationally -
Produceth good, whilst - logically - ever scheming ill.

Reply via email to