The Coq mailing list

[Ambrus Kaposi <kaposi.ambrus AT gmail.com>]

Hi,

"Type Theory based on Dependent Inductive and Coinductive Types" by
Basold and Geuvers (LICS 2016) presents a type theory without a
function space and then extends it in a symmetric way with inductive
and coinductive types. Function space is given by a coinductive type.

Cheers,
Ambrus

On Wed, Jun 24, 2020 at 1:10 PM Thorsten Altenkirch
<Thorsten.Altenkirch AT nottingham.ac.uk> wrote:
>
> 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.
>
>
>