I use these defs:<br><br><span style="font-family: courier new,monospace;">-- | Lift proof through a unary type constructor</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">liftEq :: a :=: a&#39; -&gt; f a :=: f a&#39;</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">liftEq Refl = Refl</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- | Lift proof through a binary type constructor (including &#39;(,)&#39;)</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">liftEq2 :: a :=: a&#39; -&gt; b :=: b&#39; -&gt; f a b :=: f a&#39; b&#39;</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">liftEq2 Refl Refl = Refl</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- | Lift proof through a ternary type constructor (including &#39;(,,)&#39;)</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">liftEq3 :: a :=: a&#39; -&gt; b :=: b&#39; -&gt; c :=: c&#39; -&gt; f a b c :=: f a&#39; b&#39; c&#39;</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">liftEq3 Refl Refl Refl = Refl</span><br>
<br>etc.<br><br><br><br><div class="gmail_quote">On Tue, Mar 17, 2009 at 3:39 AM, Martijn van Steenbergen <span dir="ltr">&lt;<a href="mailto:martijn@van.steenbergen.nl">martijn@van.steenbergen.nl</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Olá café,<br>
<br>
With the recent generic programming work and influences from type-dependent languages such as Agda, the following data type seems to come up often:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
data (a :=: a&#39;) where<br>
  Refl :: a :=: a<br>
</blockquote>
<br>
Everyone who needs it writes their own version; I&#39;d like to compile a package with this data type and related utilities, if such a package doesn&#39;t exist already (I couldn&#39;t find one). Below is what I have so far; I&#39;d much appreciate it if you added your ideas of what else the package should contain.<br>

<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
{-# LANGUAGE GADTs #-}<br>
{-# LANGUAGE TypeOperators #-}<br>
<br>
module Eq where<br>
<br>
data (a :=: a&#39;) where<br>
  Refl :: a :=: a<br>
<br>
class Eq1 f where<br>
  eq1 :: f a -&gt; f a&#39; -&gt; Maybe (a :=: a&#39;)<br>
<br>
class Eq2 f where<br>
  eq2 :: f a b -&gt; f a&#39; b&#39; -&gt; Maybe (a :=: a&#39;, b :=: b&#39;)<br>
<br>
class Eq3 f where<br>
  eq3 :: f a b c -&gt; f a&#39; b&#39; c&#39; -&gt; Maybe (a :=: a&#39;, b :=: b&#39;, c :=: c&#39;)<br>
</blockquote>
<br>
Thank you,<br>
<br>
Martijn.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br>