<p dir="ltr">I think you would be interested in the univalence axiom, see in particular section 2.14 of the recently released HoTT book.</p>
<p dir="ltr">Guillaume</p>
<div class="gmail_quot&lt;blockquote class=" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Fri, 2013-06-21 at 12:08 +0200, Nils Anders Danielsson wrote:<br>
&gt; On 2013-06-20 20:49, Sergei Meshveliani wrote:<br>
&gt; &gt; Is it possible to add some construct foo to the language so that the<br>
&gt; &gt; checker would allow to replace f : PSSmg a with f : PSSmg b, if p :<br>
&gt; &gt; associated a b and foo is set for PSSmg ?<br>
&gt;<br>
&gt; I didn&#39;t read all of your question, but I think you&#39;re looking for<br>
&gt; something like quotients.<br>
&gt;<br>
<br>
The word `quotient&#39; is overloaded with various meanings:<br>
quotient of numbers, quotient of two relations, may be, something from<br>
the Agda library ...<br>
Which one do you mean?<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>