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

[streicher at 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 at 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