The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

A kind of first-order type theory. You need to be careful because many principles like recursors and eliminators rely on functions, e.g. you cannot distribute + over times otherwise.

 

I am not aware whether anybody has worked out the details.

 

I think having coinductive types is quite natural but the equality in a system like coq is designed with only inductive types in mind.

 

T.

From: <coq-club-request AT inria.fr> on behalf of Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, 24 June 2020 at 12:05
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Silly question about decidable equality and inequality

 

Thanks for your answer Thorsten. What would be a type theory w/o functions (and thus Pi types) ?

 

D.

 

---

De: "Thorsten Altenkirch" <Thorsten.Altenkirch AT nottingham.ac.uk>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mercredi 24 Juin 2020 12:58:17
Objet: Re: [Coq-Club] Silly question about decidable equality and inequality

Extensional equality is needed to facilitate abstraction. Otherwise you have to carry around equalities and you end up in setoid hell.

 

It is slightly absurd: you cannot formulate a property in type theory that breaks extensional equality but then you need to prove this again and again?

 

If you have functions you need funext, the function type is a basic coinductive type and this is its coinduction principle. Otherwise you could also argue that you don’t need induction for natural numbers and each time when you say something about natural numbers you relativize this to the inductive ones. Actually we were doing these sort of things when working in the pure calculus of constructions in the 1980ies.

 

Philosophically, you mention Leibniz, i.e. equality of indescernibles. Indeed we should think about mathematical objects as given by their behaviour, ie their extension not the way they are defined, their intension. And indeed in type theory, unlike set theory, you can’t observe the definition. Hence extensionally equal objects are indescernible and hence equal. This is carried further by the univalence principle which applies this idea to types itself.

 

I don’t understand your sentence “to avoid manipulating functions with their  natural identity which is extensional identity”? I mean fun-ext exactly gives you “extensional identity” which is the correct equality of functions.

 

A type theory with functions but without fun-ext is wrong, I don’t know a better word to describe this situation. Yes Coq is currently wrong but this can be fixed. You don’t even have to go all the way to HoTT as I already argued in 1999 (i..e before HoTT).

 

Thorsten

 

From: <coq-club-request AT inria.fr> on behalf of Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, 24 June 2020 at 11:00
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Silly question about decidable equality and inequality

 

Hi Thorsten,

 

Well wanting to prove Leibniz identity of functions is already attributing

them a more specific meaning that what the underlying type theory tells you 

about their properties ;-)

 

I'd be interested with a simple example where funext is actually needed,

ie it is not just a convenience to avoid manipulating functions with their

natural identity which is extensional identity (or recursively for HO functions).

 

Best,

 

D.

 

 

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.

 

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.