Re: [HoTT] Re: Why do we need judgmental equality?

[streicher@mathematik.tu-darmstadt.de]

> For me the idea of inductive vs coinductive or how I called this a while
> ago data vs codata is an important basic intuition which comes before
> formal model constructions. Types are defined by constructors or by
> destructors, eg coproducts are defined by constructors while functions are
> defined by destructors, namely application. That is a function is
> something you can apply to arguments obtaining a result. Lambda is a
> derived construction, I can construct a function if I have a method to
> compute the result. Similarily natural numbers and lists are given by
> constructors, while streams are defined by destructors, to give a stream
> means to be able to say what its head and its tail are. And that is
> perfectly right Sigma types can be either given by a constructor or by
> destructors so in this sense they are twitters.
>
> There are reductions which just means that certain type formers are
> universal in that we can define all other from them, e.g. function types
> together with some inductive types are sufficient to derive a certain
> class of codata types. That doesn't mean that the dichotomy between data
> and codata isn't an important basic intuition.
>
> On 17/02/2019, 09:19, "Michael Shulman" <shulman@sandiego.edu> wrote:
>
>     Well, I'm not really convinced that coinductive types should be
>     treated as basic type formers, rather than simply constructed out of
>     inductive types and extensional functions.  For one thing, I have no
>     idea how to construct coinductive types as basic type formers in
>     homotopical models.  I think the issue that you raise, Thorsten, could
>     be regarded as another argument against treating them basically, or at
>     least against regarding them as really "negative" in the same way that
>     Pis and (negative) Sigmas are.
>
>     And as for adding random extra strict equalities pertaining certain
>     positive types that happen to hold in some particular model, Matt, I
>     would say similarly that the general perspective gives yet another
>     reason why you shouldn't do that.  (-:
>

But function types are neither inductive nor conductive. Only N-> (-) ist
coinductive.
In presence of function types most coinductive types can be implemented.

Maybe coinductive is a style of programming but nothing really foundational.

Thomas

-- 
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.