The Coq mailing list

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

The danger of overgeneralisation in your statement.

 

I am referring to the use of setoids. When you are using setoids you don’t know that your definitions are congruences wrt setoid equality. Hence you need to prove for every definition that it is a congruence, that is you get a lot of theorems which need to be proven. Ok, you can write a tactic for this but this misses the point – it makes more sense to build it into the type theory.

 

Also it isn’t the case that “fun-ext” is just “any consistent theorem”, it is a fundamental principle which reflects our understanding what functions are. As I said you may as well give up induction for natural numbers.

 

We don’t have “axioms” in type theory. Fun-ext is a coinduction principle and yes it does compute, if you set up things the right way. I referred to my ’99 LICS paper where I described this but we have been working on setoid type theory recently, continutng the thread. However, another alternative is cubical type theory which also enables a nice symmetry between induction and coindution (including fun-ext).

 

I don’t think adding extensionality changes the set of computable function but neither does induction, if you have primitive recursion. I don’t have a proof for this. Btw, neither does univalence.

 

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 12:39
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Silly question about decidable equality and inequality

 

AK: thank you very much for the reference

 

TA:

 

This below is quite a poor argument:

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?

It applies to ANY consistent axiom. Are you telling me that you are willing to accept

any consistent axiom just because you do not want to prove some of its direct

consequences over and over again ?

 

Btw, axioms cannot be judged solely by their consistency but also on how they impact

meta-theoretical results such as eg, the computability of the functions definable in the

theory ...

 

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.