The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

The patch is here:
https://sympa.inria.fr/sympa/arc/coq-club/2011-05/msg00204.html

Your work should also be useful for homotopy type theory, so please
keep us informed about your progress.

Best,

Bas

On Wed, Aug 29, 2012 at 10:02 AM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> Thanks!  Is this done mostly in ocaml?  (grepping the source tree suggests
> yes.)  Is it replicable in pure Coq?
> Are there plans to generalize this feature a la [Add Parametric Relation]
> and [Add Parametric Morphism]?
>
> -Jason
>
>
> On Wed, Aug 29, 2012 at 3:24 AM, Bas Spitters 
> <spitters AT cs.ru.nl>
>  wrote:
>>
>> On Wed, Aug 29, 2012 at 7:45 AM, Jason Gross 
>> <jasongross9 AT gmail.com>
>> wrote:
>> > I'm trying to generalize some of the standard library constructs to
>> > permit
>> > the use of [Type] rather than [Prop] (in particular, the structures that
>> > are
>> > behind the scenes of [reflexivity], [transitivity], [symmetry], [Add
>> > Parametric Relation], [Add Parametric Morphism], and
>> > [rewrite]/[setoid_rewrite]).
>>
>> Some of these issues have been resolved when using [identity] instead of
>> [eq].
>>
>> Bas
>
>