20 lines
3.4 KiB
HTML
20 lines
3.4 KiB
HTML
<!DOCTYPE HTML>
|
|
<html><head><meta charset="utf-8"><title>Agda.Builtin.Sigma</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Pragma">--no-sized-types</a> <a id="49" class="Pragma">--no-guardedness</a>
|
|
<a id="78" class="Pragma">--no-subtyping</a> <a id="93" class="Symbol">#-}</a>
|
|
|
|
<a id="98" class="Keyword">module</a> <a id="105" href="Agda.Builtin.Sigma.html" class="Module">Agda.Builtin.Sigma</a> <a id="124" class="Keyword">where</a>
|
|
|
|
<a id="131" class="Keyword">open</a> <a id="136" class="Keyword">import</a> <a id="143" href="Agda.Primitive.html" class="Module">Agda.Primitive</a>
|
|
|
|
<a id="159" class="Keyword">record</a> <a id="Σ"></a><a id="166" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="168" class="Symbol">{</a><a id="169" href="Agda.Builtin.Sigma.html#169" class="Bound">a</a> <a id="171" href="Agda.Builtin.Sigma.html#171" class="Bound">b</a><a id="172" class="Symbol">}</a> <a id="174" class="Symbol">(</a><a id="175" href="Agda.Builtin.Sigma.html#175" class="Bound">A</a> <a id="177" class="Symbol">:</a> <a id="179" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="183" href="Agda.Builtin.Sigma.html#169" class="Bound">a</a><a id="184" class="Symbol">)</a> <a id="186" class="Symbol">(</a><a id="187" href="Agda.Builtin.Sigma.html#187" class="Bound">B</a> <a id="189" class="Symbol">:</a> <a id="191" href="Agda.Builtin.Sigma.html#175" class="Bound">A</a> <a id="193" class="Symbol">→</a> <a id="195" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="199" href="Agda.Builtin.Sigma.html#171" class="Bound">b</a><a id="200" class="Symbol">)</a> <a id="202" class="Symbol">:</a> <a id="204" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="208" class="Symbol">(</a><a id="209" href="Agda.Builtin.Sigma.html#169" class="Bound">a</a> <a id="211" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="213" href="Agda.Builtin.Sigma.html#171" class="Bound">b</a><a id="214" class="Symbol">)</a> <a id="216" class="Keyword">where</a>
|
|
<a id="224" class="Keyword">constructor</a> <a id="_,_"></a><a id="236" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a>
|
|
<a id="242" class="Keyword">field</a>
|
|
<a id="Σ.fst"></a><a id="252" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="256" class="Symbol">:</a> <a id="258" href="Agda.Builtin.Sigma.html#175" class="Bound">A</a>
|
|
<a id="Σ.snd"></a><a id="264" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="268" class="Symbol">:</a> <a id="270" href="Agda.Builtin.Sigma.html#187" class="Bound">B</a> <a id="272" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a>
|
|
|
|
<a id="277" class="Keyword">open</a> <a id="282" href="Agda.Builtin.Sigma.html#166" class="Module">Σ</a> <a id="284" class="Keyword">public</a>
|
|
|
|
<a id="292" class="Keyword">infixr</a> <a id="299" class="Number">4</a> <a id="301" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a>
|
|
|
|
<a id="306" class="Symbol">{-#</a> <a id="310" class="Keyword">BUILTIN</a> <a id="318" class="Keyword">SIGMA</a> <a id="324" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="326" class="Symbol">#-}</a>
|
|
</pre></body></html> |