| 123456789101112131415161718192021222324 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Indenting6</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}
- \usepackage{agda}
- \begin{document}
- </a><a id="61" class="Markup">\begin{code}</a>
- <a id="74" class="Keyword">record</a> <a id="Sigma"></a><a id="81" href="Indenting6.html#81" class="Record">Sigma</a> <a id="87" class="Symbol">(</a><a id="88" href="Indenting6.html#88" class="Bound">A</a> <a id="90" class="Symbol">:</a> <a id="92" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="95" class="Symbol">)</a> <a id="97" class="Symbol">(</a><a id="98" href="Indenting6.html#98" class="Bound">B</a> <a id="100" class="Symbol">:</a> <a id="102" href="Indenting6.html#88" class="Bound">A</a> <a id="104" class="Symbol">→</a> <a id="106" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="109" class="Symbol">)</a> <a id="111" class="Symbol">:</a> <a id="113" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="117" class="Keyword">where</a>
- <a id="125" class="Keyword">constructor</a> <a id="_,_"></a><a id="137" href="Indenting6.html#137" class="InductiveConstructor Operator">_,_</a>
- <a id="143" class="Keyword">field</a>
- <a id="Sigma.proj₁"></a><a id="153" href="Indenting6.html#153" class="Field">proj₁</a> <a id="159" class="Symbol">:</a> <a id="161" href="Indenting6.html#88" class="Bound">A</a>
- <a id="Sigma.proj₂"></a><a id="167" href="Indenting6.html#167" class="Field">proj₂</a> <a id="173" class="Symbol">:</a> <a id="175" href="Indenting6.html#98" class="Bound">B</a> <a id="177" href="Indenting6.html#153" class="Field">proj₁</a>
- <a id="184" class="Keyword">open</a> <a id="189" href="Indenting6.html#81" class="Module">Sigma</a> <a id="195" class="Keyword">public</a>
- <a id="202" class="Markup">\end{code}</a><a id="212" class="Background">
- </a><a id="214" class="Markup">\begin{code}</a>
- <a id="227" class="Keyword">record</a> <a id="Equiv"></a><a id="234" href="Indenting6.html#234" class="Record">Equiv</a> <a id="240" class="Symbol">(</a><a id="241" href="Indenting6.html#241" class="Bound">X</a> <a id="243" href="Indenting6.html#243" class="Bound">Y</a> <a id="245" class="Symbol">:</a> <a id="247" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="250" class="Symbol">)</a> <a id="252" class="Symbol">:</a> <a id="254" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="258" class="Keyword">where</a>
- <a id="266" class="Keyword">field</a>
- <a id="Equiv.to"></a><a id="276" href="Indenting6.html#276" class="Field">to</a> <a id="282" class="Symbol">:</a> <a id="284" href="Indenting6.html#241" class="Bound">X</a> <a id="286" class="Symbol">→</a> <a id="288" href="Indenting6.html#243" class="Bound">Y</a>
- <a id="Equiv.from"></a><a id="294" href="Indenting6.html#294" class="Field">from</a> <a id="300" class="Symbol">:</a> <a id="302" href="Indenting6.html#243" class="Bound">Y</a> <a id="304" class="Symbol">→</a> <a id="306" href="Indenting6.html#241" class="Bound">X</a>
- <a id="308" class="Markup">\end{code}</a><a id="318" class="Background">
- \end{document}
- </a></pre></body></html>
|
