- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Issue2756</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">module</a> <a id="8" href="Issue2756.html" class="Module">Issue2756</a> <a id="18" class="Keyword">where</a>
- <a id="25" class="Keyword">module</a> <a id="M"></a><a id="32" href="Issue2756.html#32" class="Module">M</a> <a id="34" class="Keyword">where</a>
- <a id="43" class="Keyword">postulate</a> <a id="M.A"></a><a id="53" href="Issue2756.html#53" class="Postulate">A</a> <a id="55" class="Symbol">:</a> <a id="57" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="62" class="Keyword">module</a> <a id="M′"></a><a id="69" href="Issue2756.html#69" class="Module">M′</a> <a id="72" class="Symbol">=</a> <a id="74" href="Issue2756.html#32" class="Module">M</a>
- <a id="B"></a><a id="77" href="Issue2756.html#77" class="Function">B</a> <a id="79" class="Symbol">:</a> <a id="81" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="85" href="Issue2756.html#77" class="Function">B</a> <a id="87" class="Symbol">=</a> <a id="89" href="Issue2756.html#53" class="Function">M′.A</a>
- </pre></body></html>
|
