The Coq mailing list

[Benedikt Ahrens <benedikt.ahrens AT gmx.net>]

Dear Eddy,

maybe this article

http://drops.dagstuhl.de/opus/volltexte/2015/5152/

answers some of your questions.

Best,
Benedikt

On 12/11/2015 05:39 PM, Eddy Westbrook wrote:
> Thorsten,
> 
> The theoretical reason I don’t like co-inductive types is that they
> require some notion of an infinite term in the meta-language. This
> leads to all sorts of issues in formalizing the meta-theory of a
> system. But maybe you know how to get around these issues? A
> translation like you suggest, that defines co-inductive types in
> terms of constructs already in the system, would be a great help in
> this direction.
> 
> I will admit that I don’t quite understand everything you said in
> complete detail, but it sounds at a high level like you are basically
> saying that positive functors have greatest fixed-points, for the
> usual reason of being continuous. I buy this. But I at least would be
> interested to see more of the details of how to actually do this in
> type theory.
> 
> For instance, I imagine that directly formalizing the terminal
> coalgebra of a positive functor would lead to some trickiness with
> universes, and same thing with taking the omega-limit of a type
> functor. I could be wrong, but if not, you would probably have to do
> this part on paper, defining a translation from a given positive
> functor to the type of its terminal coalgebra. It would be especially
> neat if this somehow yielded the results you gave in the examples you
> mentioned; i.e., if you could run it on the stream type and get nat
> functions, and if you could run it on the colist type and get the nat
> -> maybe A type you described.
> 
> As for W-types, I thought they were well-founded? I.e., inductive,
> and not co-inductive?
> 
> -Eddy