Re: [Epigram] Definitional equality in observational type theory

[Robin Green]

Thanks to all who replied.

I have another couple of questions, more fundamental this time.

The paper says "Observational reasoning can be simulated in Intensional
Type Theory by the use of setoids, i.e. types with an explicit
equivalence relation".

I'm not clear on what the differences are between OTT and simulating
observational reasoning with setoids in ITT. Clearly OTT has an
explicit equivalence relation (=) which is "polymorphic" over (certain)
types. So does the paper mean "explicit" in some other sense?

And doesn't OTT have the same problems (equality not automatically
substitutive, complications in formalising category theory, lots of
explicit coercions) that the paper says ITT has? I don't see how OTT
helps with any of those problems, but the way that OTT is contrasted
with ITT suggests that it should. I must be misunderstanding something.

-- 
Robin

ott questions (was: Re: [Epigram] Definitional equality in observational type theory)

[Sebastian Hanowski]

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

(λu:1.u[Q> u)( 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.