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

[Henning Basold]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

I'd like to add my two cents: Thorsten mentioned in a previous email
that function extensionality should hold because of the view on
functions as coinductive type/codata. In fact, this goes down to the
question what coinduction is. The category theoretical view provides
one possible answer, namely that bisimilarity implies equality.
Applying this to functions, bisimilarity says that two functions are
point-wise equal. Thus, point-wise equality would imply equality and
we obtain function extensionality from a general coinduction principle.

Hagino had realised in 87 (DOI: 10.1007/3-540-18508-9_24) that many
type formers can be represented as either inductive or coinductive
type by appealing to their presentation as left/right adjoints. An
exception to this was the function space. However, if we move to a
dependent type theory (or fibred categories), then we can also obtain
the function space in this way. You may find description of the
category theoretical approach to this here
https://arxiv.org/abs/1508.06779v2 and the syntactic side here
http://arxiv.org/abs/1605.02206. (Apologies for the self-advertisement).

Best,
Henning

On 17/02/2019 22:41, Thorsten Altenkirch wrote:
> 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.
> 
> 
> 
> 
> _______________________________________________ Agda mailing list 
> Agda at lists.chalmers.se 
> https://lists.chalmers.se/mailman/listinfo/agda
> 
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlxsjfkACgkQatBsEc2x
Mm4t0g/9FQEf2owWDCJ2d9uYkIv8Sv0lLihqwcxiDuu6FjhtJq256D+ClYoYzKcJ
ajsauJynx2+QZR/Ogb4KORcS8CDisP7SCpnRNclaSE7BZ33Jn5ddXUjGoswjzAEC
yn1272u0rZQDT7IPdJmQCjtyYIzOEqdBZnWqA/OLLv31kOqLV/pLWCC7PcJOLcX5
7LhECFG8xKWeMAU9P5uIKm3okmcvi3tTfh9LQ6UvwOFLg/HUvKpJGZstj260GAXN
OKIHuB2uuvP/NwkeJT/8NyIX3ATaDPlmhBEDrt41mfKcDVtpWhlpRJi1Il84QJBN
6engBqQdJC7AEm6G0tlq+ojPsD0pAyCyHTS3QysFXce+oni0Dvo4NUB8iqHB/EKB
T97x/bn9TN6gRwei6IYAO9sodaswrQBxA9uK5TQ73awIr7ncKsFGa6X6Ftf3IsW/
0WH8cdEvviKsqG1i7OuYS3PFeS5zh9lySoHStw4N+Jt9tZOljMwRNWrESlUHuHPx
ULQ2RYRhQ39UMtS2h48H5BVYyNDe14O6hGD09hzvVsLK6fJajWb6luJAfZ67YrFE
Ar+rNuRHuL0mi2vrEjTyIH/9Efgw266LegHH5lXsB2b1ln6iolrkIMBVvDvtXwUR
v29aVpm5RQJAyRRJl8DFM13zwl2h7CMi12W09XSENnileM9Hd7k=
=+7pF
-----END PGP SIGNATURE-----