(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 on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> 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?