-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCategory.Applicative.html
43 lines (32 loc) · 10.5 KB
/
Category.Applicative.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Category.Applicative</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">-- Applicative functors</a>
<a id="130" class="Comment">------------------------------------------------------------------------</a>
<a id="204" class="Comment">-- Note that currently the applicative functor laws are not included</a>
<a id="273" class="Comment">-- here.</a>
<a id="283" class="Symbol">{-#</a> <a id="287" class="Keyword">OPTIONS</a> <a id="295" class="Pragma">--without-K</a> <a id="307" class="Pragma">--safe</a> <a id="314" class="Symbol">#-}</a>
<a id="319" class="Keyword">module</a> <a id="326" href="Category.Applicative.html" class="Module">Category.Applicative</a> <a id="347" class="Keyword">where</a>
<a id="354" class="Keyword">open</a> <a id="359" class="Keyword">import</a> <a id="366" href="Level.html" class="Module">Level</a> <a id="372" class="Keyword">using</a> <a id="378" class="Symbol">(</a><a id="379" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="384" class="Symbol">;</a> <a id="386" href="Agda.Primitive.html#780" class="Primitive">suc</a><a id="389" class="Symbol">;</a> <a id="391" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="394" class="Symbol">)</a>
<a id="396" class="Keyword">open</a> <a id="401" class="Keyword">import</a> <a id="408" href="Data.Unit.html" class="Module">Data.Unit</a>
<a id="418" class="Keyword">open</a> <a id="423" class="Keyword">import</a> <a id="430" href="Category.Applicative.Indexed.html" class="Module">Category.Applicative.Indexed</a>
<a id="460" class="Keyword">private</a>
<a id="470" class="Keyword">variable</a>
<a id="483" href="Category.Applicative.html#483" class="Generalizable">f</a> <a id="485" class="Symbol">:</a> <a id="487" href="Agda.Primitive.html#597" class="Postulate">Level</a>
<a id="RawApplicative"></a><a id="494" href="Category.Applicative.html#494" class="Function">RawApplicative</a> <a id="509" class="Symbol">:</a> <a id="511" class="Symbol">(</a><a id="512" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="516" href="Category.Applicative.html#483" class="Generalizable">f</a> <a id="518" class="Symbol">→</a> <a id="520" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="524" href="Category.Applicative.html#483" class="Generalizable">f</a><a id="525" class="Symbol">)</a> <a id="527" class="Symbol">→</a> <a id="529" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="533" class="Symbol">(</a><a id="534" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="538" href="Category.Applicative.html#483" class="Generalizable">f</a><a id="539" class="Symbol">)</a>
<a id="541" href="Category.Applicative.html#494" class="Function">RawApplicative</a> <a id="556" href="Category.Applicative.html#556" class="Bound">F</a> <a id="558" class="Symbol">=</a> <a id="560" href="Category.Applicative.Indexed.html#860" class="Record">RawIApplicative</a> <a id="576" class="Symbol">{</a><a id="577" class="Argument">I</a> <a id="579" class="Symbol">=</a> <a id="581" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a><a id="582" class="Symbol">}</a> <a id="584" class="Symbol">λ</a> <a id="586" href="Category.Applicative.html#586" class="Bound">_</a> <a id="588" href="Category.Applicative.html#588" class="Bound">_</a> <a id="590" class="Symbol">→</a> <a id="592" href="Category.Applicative.html#556" class="Bound">F</a>
<a id="595" class="Keyword">module</a> <a id="RawApplicative"></a><a id="602" href="Category.Applicative.html#602" class="Module">RawApplicative</a> <a id="617" class="Symbol">{</a><a id="618" href="Category.Applicative.html#618" class="Bound">F</a> <a id="620" class="Symbol">:</a> <a id="622" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="626" href="Category.Applicative.html#483" class="Generalizable">f</a> <a id="628" class="Symbol">→</a> <a id="630" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="634" href="Category.Applicative.html#483" class="Generalizable">f</a><a id="635" class="Symbol">}</a>
<a id="659" class="Symbol">(</a><a id="660" href="Category.Applicative.html#660" class="Bound">app</a> <a id="664" class="Symbol">:</a> <a id="666" href="Category.Applicative.html#494" class="Function">RawApplicative</a> <a id="681" href="Category.Applicative.html#618" class="Bound">F</a><a id="682" class="Symbol">)</a> <a id="684" class="Keyword">where</a>
<a id="692" class="Keyword">open</a> <a id="697" href="Category.Applicative.Indexed.html#860" class="Module">RawIApplicative</a> <a id="713" href="Category.Applicative.html#660" class="Bound">app</a> <a id="717" class="Keyword">public</a>
<a id="RawApplicativeZero"></a><a id="725" href="Category.Applicative.html#725" class="Function">RawApplicativeZero</a> <a id="744" class="Symbol">:</a> <a id="746" class="Symbol">(</a><a id="747" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="751" href="Category.Applicative.html#483" class="Generalizable">f</a> <a id="753" class="Symbol">→</a> <a id="755" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="759" href="Category.Applicative.html#483" class="Generalizable">f</a><a id="760" class="Symbol">)</a> <a id="762" class="Symbol">→</a> <a id="764" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="768" class="Symbol">(</a><a id="769" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="773" href="Category.Applicative.html#483" class="Generalizable">f</a><a id="774" class="Symbol">)</a>
<a id="776" href="Category.Applicative.html#725" class="Function">RawApplicativeZero</a> <a id="795" href="Category.Applicative.html#795" class="Bound">F</a> <a id="797" class="Symbol">=</a> <a id="799" href="Category.Applicative.Indexed.html#1821" class="Record">RawIApplicativeZero</a> <a id="819" class="Symbol">{</a><a id="820" class="Argument">I</a> <a id="822" class="Symbol">=</a> <a id="824" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a><a id="825" class="Symbol">}</a> <a id="827" class="Symbol">(λ</a> <a id="830" href="Category.Applicative.html#830" class="Bound">_</a> <a id="832" href="Category.Applicative.html#832" class="Bound">_</a> <a id="834" class="Symbol">→</a> <a id="836" href="Category.Applicative.html#795" class="Bound">F</a><a id="837" class="Symbol">)</a>
<a id="840" class="Keyword">module</a> <a id="RawApplicativeZero"></a><a id="847" href="Category.Applicative.html#847" class="Module">RawApplicativeZero</a> <a id="866" class="Symbol">{</a><a id="867" href="Category.Applicative.html#867" class="Bound">F</a> <a id="869" class="Symbol">:</a> <a id="871" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="875" href="Category.Applicative.html#483" class="Generalizable">f</a> <a id="877" class="Symbol">→</a> <a id="879" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="883" href="Category.Applicative.html#483" class="Generalizable">f</a><a id="884" class="Symbol">}</a>
<a id="912" class="Symbol">(</a><a id="913" href="Category.Applicative.html#913" class="Bound">app</a> <a id="917" class="Symbol">:</a> <a id="919" href="Category.Applicative.html#725" class="Function">RawApplicativeZero</a> <a id="938" href="Category.Applicative.html#867" class="Bound">F</a><a id="939" class="Symbol">)</a> <a id="941" class="Keyword">where</a>
<a id="949" class="Keyword">open</a> <a id="954" href="Category.Applicative.Indexed.html#1821" class="Module">RawIApplicativeZero</a> <a id="974" href="Category.Applicative.html#913" class="Bound">app</a> <a id="978" class="Keyword">public</a>
<a id="RawAlternative"></a><a id="986" href="Category.Applicative.html#986" class="Function">RawAlternative</a> <a id="1001" class="Symbol">:</a> <a id="1003" class="Symbol">(</a><a id="1004" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1008" href="Category.Applicative.html#483" class="Generalizable">f</a> <a id="1010" class="Symbol">→</a> <a id="1012" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1016" href="Category.Applicative.html#483" class="Generalizable">f</a><a id="1017" class="Symbol">)</a> <a id="1019" class="Symbol">→</a> <a id="1021" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1025" class="Symbol">_</a>
<a id="1027" href="Category.Applicative.html#986" class="Function">RawAlternative</a> <a id="1042" href="Category.Applicative.html#1042" class="Bound">F</a> <a id="1044" class="Symbol">=</a> <a id="1046" href="Category.Applicative.Indexed.html#2158" class="Record">RawIAlternative</a> <a id="1062" class="Symbol">{</a><a id="1063" class="Argument">I</a> <a id="1065" class="Symbol">=</a> <a id="1067" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a><a id="1068" class="Symbol">}</a> <a id="1070" class="Symbol">(λ</a> <a id="1073" href="Category.Applicative.html#1073" class="Bound">_</a> <a id="1075" href="Category.Applicative.html#1075" class="Bound">_</a> <a id="1077" class="Symbol">→</a> <a id="1079" href="Category.Applicative.html#1042" class="Bound">F</a><a id="1080" class="Symbol">)</a>
<a id="1083" class="Keyword">module</a> <a id="RawAlternative"></a><a id="1090" href="Category.Applicative.html#1090" class="Module">RawAlternative</a> <a id="1105" class="Symbol">{</a><a id="1106" href="Category.Applicative.html#1106" class="Bound">F</a> <a id="1108" class="Symbol">:</a> <a id="1110" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1114" href="Category.Applicative.html#483" class="Generalizable">f</a> <a id="1116" class="Symbol">→</a> <a id="1118" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1122" href="Category.Applicative.html#483" class="Generalizable">f</a><a id="1123" class="Symbol">}</a>
<a id="1147" class="Symbol">(</a><a id="1148" href="Category.Applicative.html#1148" class="Bound">app</a> <a id="1152" class="Symbol">:</a> <a id="1154" href="Category.Applicative.html#986" class="Function">RawAlternative</a> <a id="1169" href="Category.Applicative.html#1106" class="Bound">F</a><a id="1170" class="Symbol">)</a> <a id="1172" class="Keyword">where</a>
<a id="1180" class="Keyword">open</a> <a id="1185" href="Category.Applicative.Indexed.html#2158" class="Module">RawIAlternative</a> <a id="1201" href="Category.Applicative.html#1148" class="Bound">app</a> <a id="1205" class="Keyword">public</a>
</pre></body></html>