The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Thanks.  That doesn't seem to be the complete story, though, because rewriting and [reflexivity]/[symmetry]/[transitivity] all just work for something like

  Set Implicit Arguments.

  Inductive identity_dep (A : Type) (a : A) : forall B : Type, B -> Type :=

    identity_dep_refl : identity_dep a a.

Anyway, I'll keep you updated.  So far, I've managed to implement versions of [reflexivity], [symmetry], and [transitivity] that allow relations in [Type] rather than [Prop] without much trouble.  I'm currently exploring rewriting (which I don't yet understand well enough to implement), mostly by trying to replace [Prop] with [Type] in Coq.Relations.Relation_Definitions, Coq.Classes.RelationClasses, and Coq.Classes.Morphisms.  I've ~finished the first two (though I haven't quite finished the versions that permit relations to be both [A -> A -> Type] and [A -> A -> Prop], depending on whether [A : Type] or [A : Prop]), and I'm about 2/3 of the way though Coq.Classes.Morphisms (universe inconsistency errors keep giving me trouble.  So far, I've bypassed all of them by some combination of replacing [Definition]s with [Notation]s, expanding out definitions manually, and duplicating a [Fixpoint].)

-Jason

On Wed, Aug 29, 2012 at 4:09 AM, Bas Spitters <spitters AT cs.ru.nl> wrote:

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
>
>