(Since I've already made such a fuss about Nuprl anyway...)

Nuprl has a type of streams (of whatever) up to bisimilarity. That is, 
bisimilar streams are judgmentally equal. Bisimilarity of bit streams is 
already undecidable. This is essentially the same problem as extensional 
equality of functions (nat->bool). I think eta *reduction* of streams would 
be OK to throw in, but it won't get you strict extensionality.

On Sunday, February 17, 2019 at 2:56:40 AM UTC-5, Thorsten Altenkirch wrote:
>
> On 17/02/2019, 01:25, "homotopyt...@googlegroups.com <javascript:> on 
> behalf of Michael Shulman" <homotopyt...@googlegroups.com <javascript:> 
> on behalf of shu...@sandiego.edu <javascript:>> wrote: 
>
>     However, I don't find it 
>     arbitrary at all: *negative* types have strict eta, while positive 
>     types don't. 
>
> This is a very good point. However Streams are negative types but for 
> example agda doesn't use eta conversion on them, I think for a good reason. 
> Actually I am not completely sure whether this is undecidable. 
>
> E.g. the following equation cannot be proven using refl (it can be proven 
> in cubical agda btw). The corresponding equation for Sigma types holds 
> definitionally. 
>
> infix 5 _∷_ 
>
> record Stream (A : Set) : Set where 
>   constructor _∷_ 
>   coinductive 
>   field 
>     hd : A 
>     tl : Stream A 
>
> open Stream 
> etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s 
> etaStream = {!refl!} 
>
> CCed to the agda list. Maybe somebody can comment on the decidabilty 
> status? 
>
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.