<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<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>
> On 2013-06-20 20:49, Sergei Meshveliani wrote:<br>
> > Is it possible to add some construct foo to the language so that the<br>
> > checker would allow to replace f : PSSmg a with f : PSSmg b, if p :<br>
> > associated a b and foo is set for PSSmg ?<br>
><br>
> I didn't read all of your question, but I think you're looking for<br>
> something like quotients.<br>
><br>
<br>
The word `quotient' 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>