coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gabriel Scherer <gabriel.scherer AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Question about Bishop set (setoid) type theory.
- Date: Fri, 25 Sep 2015 18:52:41 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f176.google.com
- Ironport-phdr: 9a23:yi1JzxyLx+2GPKzXCy+O+j09IxM/srCxBDY+r6Qd0e0RIJqq85mqBkHD//Il1AaPBtWHra8cwLKJ+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStKU0pz8j7/60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGx48sgs/M9YUKj8Y79wDfkBVGxnYCgJ45jAsgCLZg+S7DNIWWIP1xFMHgLt7RfgX563vDGs5cRn3yzPEsT8V7E5XXyZ5KdmUhLywHMIPjQj8WzTzNd7jK9BrQiJqBl2woqSa4aQYqktNpjBdM8XEDISFv1aUDZMV8blN9MC
You may be interested in Marc Lasson's paramcoq plugin, which
generates parametricity witnesses from Coq terms. (So it's not trying
to internalize the fact that terms respect equality/parametricity, but
rather make the meta-theorem available in practice as a
meta-programming tool.)
https://github.com/mlasson/paramcoq
On Fri, Sep 25, 2015 at 4:37 PM, Neelakantan Krishnaswami
<n.krishnaswami AT cs.bham.ac.uk>
wrote:
> On 25/09/15 13:35, Ilmārs Cīrulis wrote:
>>
>> I often have to use Equivalence and Proper (while tinkering around),
>> therefore a question appeared:
>>
>> What about Coq (or any other proof assistant / type theory) where
>> setoids and morphisms are first class citizens (built in, replacing
>> standard Type and function that becomes something like lower level of
>> language). In such case there would be no need of special libraries for
>> Equivalence, Setoid and related libraries for, e.g., lists or other data
>> structures that respects equivalence.
>>
>> What are cons of such idea?
>
>
> This is essentially the idea behind Observational Type Theory; you
> should look at:
>
> * Extensional Equality in Intensional Type Theory. T. Altenkirch
> LICS 1999
> * Observational equality, now! T. Altenkirch, C. McBride, W. Swierstra,
> PLPV 2007
>
> The core idea (every type is a setoid and every definable term is a
> equality-respecting morphism) is very simple, but making all the syntax
> line up to make it work is tricky and intricate.
>
> Best,
> Neel
>
- [Coq-Club] Question about Bishop set (setoid) type theory., Ilmārs Cīrulis, 09/25/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Neelakantan Krishnaswami, 09/25/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Gabriel Scherer, 09/25/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Arnaud Spiwack, 09/25/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Abhishek Anand, 09/25/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Ilmārs Cīrulis, 09/28/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Neelakantan Krishnaswami, 09/28/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Bas Spitters, 09/28/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Guillaume Brunerie, 09/29/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Abhishek Anand, 09/29/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Guillaume Brunerie, 09/30/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Abhishek Anand, 09/25/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Arnaud Spiwack, 09/25/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Gabriel Scherer, 09/25/2015
- Re: [Coq-Club] Question about Bishop set (setoid) type theory., Neelakantan Krishnaswami, 09/25/2015
Archive powered by MHonArc 2.6.18.