Positive vs Negative encoded streams

This shows some relations between positively and negatively encoded streams using self types, at the end we conclude that one is definitionally equal to the other if sigma is also encoded as an inductive type with self types.

I would claim that given the relation here, any advantage of one over the other is a matter of ergonomics and the implementation quality.

A nice bit to think later is about extensionalities of those?

So, what did Coq and Agda got wrong?

Positively encoded stream

Stream : (A : Type) -> Type;
cons : (A, x : A, y : Stream(A)) -> Stream(A);

Stream = (A) => (s : Stream(A)) &
  (P, w : (x : A, y : Stream(A)) -> P(cons(x, y))) -> P(s);
cons = (A, x, y) => (P, w) => w(x, y);

Negatively Encoded

Stream : (A : Type) -> Type;
cons : (A, x : A, y : Stream(A)) -> Stream(A);

Stream = (A) => [x : A, y : Stream(A)];
cons = (A, x, y) => [x, y];

But sigma encoding

Remember, Sigma can also be lambda encoded

Sigma : (A : Type, B : (x : A) -> Type) -> Type;
exist : (A, B, x : A, y : B(x)) -> Sigma(A, B);

Sigma = (A, B) => (s : Sigma(A, B)) &
  (P, w : (x : A, y : B(x)) -> P(exist(A, B, x, y))) -> P(s);
exist = (A, B, x, y) => (P, w) => w(x, y);

Sigma encoded stream

This should give you the same properties as the positively encoded stream.

// now, what if we put the negatively encoded with Sigma?
Stream : (A : Type) -> Type;
cons : (A, x : A, y : Stream(A)) -> Stream(A);

Stream = (A) => Sigma(A, Stream(A));
cons = (A, x, y) => exist(A, Stream(A), x, y);

But they're the same

But what if we expand the definitions? Then we can conclude that they're definitionally equal.

Stream = (A) => Sigma(A, Stream(A));
// unfolds
Stream = (A) => (s : Sigma(A, Stream(A, B))) &
  (P, w : (x : A, y : Stream(A)) -> P(exist(A, Stream(A), x, y))) -> P(s);
// which is the same as
Stream = (A) => (s : Stream(A)) &
  (P, w : (x : A, y : Stream(A)) -> P(cons(x, y))) -> P(s);
// and if we look at the constructor
cons = (A, x, y) => exist(A, Stream(A), x, y);
// which expands to
cons = (A, x, y) => (P, w) => w(x, y);

// so by putting them together
Stream : (A : Type) -> Type;
cons : (A, x : A, y : Stream(A)) -> Stream(A);

Stream = (A) => (s : Stream(A)) &
  (P, w : (x : A, y : Stream(A)) -> P(cons(x, y))) -> P(s);
cons = (A, x, y) => (P, w) => w(x, y);