[Agda] PreorderReasoning not Polymorphic Enough?

[Nils Anders Danielsson]

On Dec 21, 2007 9:46 AM, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:
>
> [...] The problem seems to have been noticed before, as seen in the
> comments in PropositionalEquality.agda:
>
>    -- Relation.Binary.EqReasoning is more convenient to use with _≡_ if
>    -- the combinators take the type argument (a) as a hidden argument,
>    -- instead of being locked to a fixed type at module instantiation
>    -- time.
>
> That is, rather than being tied to a fixed carrier, we may
> need a module that somehow accepts, for example, these information:
>
>       (_∼_ : {A : Set} -> A -> A -> Set)
>       (refl : {A : Set}{x : A} -> x ∼ x)
>       (trans : {A : Set}{x y z : A} -> x ∼ y -> y ∼ z -> x ∼ z)

This is (more or less) what we have today. I think what you want is to
be able to open the module once, but use the combinators with
different carriers. This would require changing the interface, since
there is no way (in general) to derive a preorder from the underlying
carrier. In PropositionalEquality.agda the preorder is always
instantiated to _≡_, but this does not work in general.

If you want this then I suggest that you add a preorder as an argument
to the begin_ function, with suitable changes to the other functions.

> However, even this may not be enough. [...] And therefore, I may
> need a module offering combinators having types:
>
>    _∼⟨_⟩_ :  {A B : Set} (x : F A B) {y z : F A B} -> x ∼ y ->
>                y IsRelatedTo z -> x IsRelatedTo z
>
> where (F : Set -> Set -> Set) is also a parameter to
> the module.

Can't you just let the carrier be F A B, with a suitable preorder?
Maybe I haven't quite understood what you want.

--
/NAD