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

[Thorsten Altenkirch]

I tried to explain in common sense term what is a function? And my answer is that it is something you can apply to an element of the domain and you get an element of the codomain. You don’t know how you can inspect the function that is all you know. Hence the function type is explained by what you can do with it. That’s coastal. Compare this with natural numbers. A natural number is 0 or the successor of a natural number. You explain how to produce them. That’s data. What is a stream? A stream is something you can get the head and the tail of. So that is codata as well.

Sent from my iPhone

> On 17 Feb 2019, at 19:36, Thomas Streicher <streicher at mathematik.tu-darmstadt.de> wrote:
> 
> admittedly, by coinductive I understand terminal coalgebra
> 
> in MLTT even function types are inductive though that's a bit of
> cheating in my eyes
> 
> so I must say I don't understand what you mean by codata types
> technically
> 
> I know positive and negative polarity in the sense of linear logic people
> presumably, that'scloser to what you have in mind
> 
> thomas



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.