33 lines
6.5 KiB
HTML
33 lines
6.5 KiB
HTML
|
<!DOCTYPE HTML>
|
|||
|
|
<html><head><meta charset="utf-8"><title>Algebra.Core</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="74" class="Comment">-- The Agda standard library</a>
|
|||
|
|
<a id="103" class="Comment">--</a>
|
|||
|
|
<a id="106" class="Comment">-- Core algebraic definitions</a>
|
|||
|
|
<a id="136" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
|
|||
|
|
<a id="210" class="Comment">-- The contents of this module should be accessed via `Algebra`.</a>
|
|||
|
|
|
|||
|
|
<a id="276" class="Symbol">{-#</a> <a id="280" class="Keyword">OPTIONS</a> <a id="288" class="Pragma">--without-K</a> <a id="300" class="Pragma">--safe</a> <a id="307" class="Symbol">#-}</a>
|
|||
|
|
|
|||
|
|
<a id="312" class="Keyword">module</a> <a id="319" href="Algebra.Core.html" class="Module">Algebra.Core</a> <a id="332" class="Keyword">where</a>
|
|||
|
|
|
|||
|
|
<a id="339" class="Keyword">open</a> <a id="344" class="Keyword">import</a> <a id="351" href="Level.html" class="Module">Level</a> <a id="357" class="Keyword">using</a> <a id="363" class="Symbol">(</a><a id="364" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="367" class="Symbol">)</a>
|
|||
|
|
|
|||
|
|
<a id="370" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="443" class="Comment">-- Unary and binary operations</a>
|
|||
|
|
|
|||
|
|
<a id="Op₁"></a><a id="475" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="479" class="Symbol">:</a> <a id="481" class="Symbol">∀</a> <a id="483" class="Symbol">{</a><a id="484" href="Algebra.Core.html#484" class="Bound">ℓ</a><a id="485" class="Symbol">}</a> <a id="487" class="Symbol">→</a> <a id="489" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="493" href="Algebra.Core.html#484" class="Bound">ℓ</a> <a id="495" class="Symbol">→</a> <a id="497" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="501" href="Algebra.Core.html#484" class="Bound">ℓ</a>
|
|||
|
|
<a id="503" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="507" href="Algebra.Core.html#507" class="Bound">A</a> <a id="509" class="Symbol">=</a> <a id="511" href="Algebra.Core.html#507" class="Bound">A</a> <a id="513" class="Symbol">→</a> <a id="515" href="Algebra.Core.html#507" class="Bound">A</a>
|
|||
|
|
|
|||
|
|
<a id="Op₂"></a><a id="518" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="522" class="Symbol">:</a> <a id="524" class="Symbol">∀</a> <a id="526" class="Symbol">{</a><a id="527" href="Algebra.Core.html#527" class="Bound">ℓ</a><a id="528" class="Symbol">}</a> <a id="530" class="Symbol">→</a> <a id="532" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="536" href="Algebra.Core.html#527" class="Bound">ℓ</a> <a id="538" class="Symbol">→</a> <a id="540" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="544" href="Algebra.Core.html#527" class="Bound">ℓ</a>
|
|||
|
|
<a id="546" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="550" href="Algebra.Core.html#550" class="Bound">A</a> <a id="552" class="Symbol">=</a> <a id="554" href="Algebra.Core.html#550" class="Bound">A</a> <a id="556" class="Symbol">→</a> <a id="558" href="Algebra.Core.html#550" class="Bound">A</a> <a id="560" class="Symbol">→</a> <a id="562" href="Algebra.Core.html#550" class="Bound">A</a>
|
|||
|
|
|
|||
|
|
<a id="565" class="Comment">------------------------------------------------------------------------</a>
|
|||
|
|
<a id="638" class="Comment">-- Left and right actions</a>
|
|||
|
|
|
|||
|
|
<a id="Opₗ"></a><a id="665" href="Algebra.Core.html#665" class="Function">Opₗ</a> <a id="669" class="Symbol">:</a> <a id="671" class="Symbol">∀</a> <a id="673" class="Symbol">{</a><a id="674" href="Algebra.Core.html#674" class="Bound">a</a> <a id="676" href="Algebra.Core.html#676" class="Bound">b</a><a id="677" class="Symbol">}</a> <a id="679" class="Symbol">→</a> <a id="681" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="685" href="Algebra.Core.html#674" class="Bound">a</a> <a id="687" class="Symbol">→</a> <a id="689" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="693" href="Algebra.Core.html#676" class="Bound">b</a> <a id="695" class="Symbol">→</a> <a id="697" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="701" class="Symbol">(</a><a id="702" href="Algebra.Core.html#674" class="Bound">a</a> <a id="704" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="706" href="Algebra.Core.html#676" class="Bound">b</a><a id="707" class="Symbol">)</a>
|
|||
|
|
<a id="709" href="Algebra.Core.html#665" class="Function">Opₗ</a> <a id="713" href="Algebra.Core.html#713" class="Bound">A</a> <a id="715" href="Algebra.Core.html#715" class="Bound">B</a> <a id="717" class="Symbol">=</a> <a id="719" href="Algebra.Core.html#713" class="Bound">A</a> <a id="721" class="Symbol">→</a> <a id="723" href="Algebra.Core.html#715" class="Bound">B</a> <a id="725" class="Symbol">→</a> <a id="727" href="Algebra.Core.html#715" class="Bound">B</a>
|
|||
|
|
|
|||
|
|
<a id="Opᵣ"></a><a id="730" href="Algebra.Core.html#730" class="Function">Opᵣ</a> <a id="734" class="Symbol">:</a> <a id="736" class="Symbol">∀</a> <a id="738" class="Symbol">{</a><a id="739" href="Algebra.Core.html#739" class="Bound">a</a> <a id="741" href="Algebra.Core.html#741" class="Bound">b</a><a id="742" class="Symbol">}</a> <a id="744" class="Symbol">→</a> <a id="746" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="750" href="Algebra.Core.html#739" class="Bound">a</a> <a id="752" class="Symbol">→</a> <a id="754" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="758" href="Algebra.Core.html#741" class="Bound">b</a> <a id="760" class="Symbol">→</a> <a id="762" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="766" class="Symbol">(</a><a id="767" href="Algebra.Core.html#739" class="Bound">a</a> <a id="769" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="771" href="Algebra.Core.html#741" class="Bound">b</a><a id="772" class="Symbol">)</a>
|
|||
|
|
<a id="774" href="Algebra.Core.html#730" class="Function">Opᵣ</a> <a id="778" href="Algebra.Core.html#778" class="Bound">A</a> <a id="780" href="Algebra.Core.html#780" class="Bound">B</a> <a id="782" class="Symbol">=</a> <a id="784" href="Algebra.Core.html#780" class="Bound">B</a> <a id="786" class="Symbol">→</a> <a id="788" href="Algebra.Core.html#778" class="Bound">A</a> <a id="790" class="Symbol">→</a> <a id="792" href="Algebra.Core.html#780" class="Bound">B</a>
|
|||
|
|
</pre></body></html>
|