-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCategory.Applicative.Indexed.html
116 lines (90 loc) · 46 KB
/
Category.Applicative.Indexed.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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Category.Applicative.Indexed</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">-- Indexed applicative functors</a>
<a id="138" class="Comment">------------------------------------------------------------------------</a>
<a id="212" class="Comment">-- Note that currently the applicative functor laws are not included</a>
<a id="281" class="Comment">-- here.</a>
<a id="291" class="Symbol">{-#</a> <a id="295" class="Keyword">OPTIONS</a> <a id="303" class="Pragma">--without-K</a> <a id="315" class="Pragma">--safe</a> <a id="322" class="Symbol">#-}</a>
<a id="327" class="Keyword">module</a> <a id="334" href="Category.Applicative.Indexed.html" class="Module">Category.Applicative.Indexed</a> <a id="363" class="Keyword">where</a>
<a id="370" class="Keyword">open</a> <a id="375" class="Keyword">import</a> <a id="382" href="Category.Functor.html" class="Module">Category.Functor</a> <a id="399" class="Keyword">using</a> <a id="405" class="Symbol">(</a><a id="406" href="Category.Functor.html#499" class="Record">RawFunctor</a><a id="416" class="Symbol">)</a>
<a id="418" class="Keyword">open</a> <a id="423" class="Keyword">import</a> <a id="430" href="Data.Product.html" class="Module">Data.Product</a> <a id="443" class="Keyword">using</a> <a id="449" class="Symbol">(</a><a id="450" href="Data.Product.html#1167" class="Function Operator">_×_</a><a id="453" class="Symbol">;</a> <a id="455" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a><a id="458" class="Symbol">)</a>
<a id="460" class="Keyword">open</a> <a id="465" class="Keyword">import</a> <a id="472" href="Function.html" class="Module">Function</a> <a id="481" class="Keyword">hiding</a> <a id="488" class="Symbol">(</a><a id="489" href="Function.Core.html#646" class="Function">Morphism</a><a id="497" class="Symbol">)</a>
<a id="499" class="Keyword">open</a> <a id="504" class="Keyword">import</a> <a id="511" href="Level.html" class="Module">Level</a>
<a id="517" class="Keyword">open</a> <a id="522" class="Keyword">import</a> <a id="529" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="567" class="Symbol">as</a> <a id="570" class="Module">P</a> <a id="572" class="Keyword">using</a> <a id="578" class="Symbol">(</a><a id="579" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a><a id="582" class="Symbol">)</a>
<a id="585" class="Keyword">private</a>
<a id="595" class="Keyword">variable</a>
<a id="608" href="Category.Applicative.Indexed.html#608" class="Generalizable">a</a> <a id="610" href="Category.Applicative.Indexed.html#610" class="Generalizable">b</a> <a id="612" href="Category.Applicative.Indexed.html#612" class="Generalizable">c</a> <a id="614" href="Category.Applicative.Indexed.html#614" class="Generalizable">i</a> <a id="616" href="Category.Applicative.Indexed.html#616" class="Generalizable">f</a> <a id="618" class="Symbol">:</a> <a id="620" href="Agda.Primitive.html#597" class="Postulate">Level</a>
<a id="630" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="632" class="Symbol">:</a> <a id="634" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="638" href="Category.Applicative.Indexed.html#608" class="Generalizable">a</a>
<a id="644" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a> <a id="646" class="Symbol">:</a> <a id="648" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="652" href="Category.Applicative.Indexed.html#610" class="Generalizable">b</a>
<a id="658" href="Category.Applicative.Indexed.html#658" class="Generalizable">C</a> <a id="660" class="Symbol">:</a> <a id="662" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="666" href="Category.Applicative.Indexed.html#612" class="Generalizable">c</a>
<a id="IFun"></a><a id="669" href="Category.Applicative.Indexed.html#669" class="Function">IFun</a> <a id="674" class="Symbol">:</a> <a id="676" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="680" href="Category.Applicative.Indexed.html#614" class="Generalizable">i</a> <a id="682" class="Symbol">→</a> <a id="684" class="Symbol">(</a><a id="685" href="Category.Applicative.Indexed.html#685" class="Bound">ℓ</a> <a id="687" class="Symbol">:</a> <a id="689" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="694" class="Symbol">)</a> <a id="696" class="Symbol">→</a> <a id="698" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="702" class="Symbol">(</a><a id="703" href="Category.Applicative.Indexed.html#614" class="Generalizable">i</a> <a id="705" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="707" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="711" href="Category.Applicative.Indexed.html#685" class="Bound">ℓ</a><a id="712" class="Symbol">)</a>
<a id="714" href="Category.Applicative.Indexed.html#669" class="Function">IFun</a> <a id="719" href="Category.Applicative.Indexed.html#719" class="Bound">I</a> <a id="721" href="Category.Applicative.Indexed.html#721" class="Bound">ℓ</a> <a id="723" class="Symbol">=</a> <a id="725" href="Category.Applicative.Indexed.html#719" class="Bound">I</a> <a id="727" class="Symbol">→</a> <a id="729" href="Category.Applicative.Indexed.html#719" class="Bound">I</a> <a id="731" class="Symbol">→</a> <a id="733" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="737" href="Category.Applicative.Indexed.html#721" class="Bound">ℓ</a> <a id="739" class="Symbol">→</a> <a id="741" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="745" href="Category.Applicative.Indexed.html#721" class="Bound">ℓ</a>
<a id="748" class="Comment">------------------------------------------------------------------------</a>
<a id="821" class="Comment">-- Type, and usual combinators</a>
<a id="853" class="Keyword">record</a> <a id="RawIApplicative"></a><a id="860" href="Category.Applicative.Indexed.html#860" class="Record">RawIApplicative</a> <a id="876" class="Symbol">{</a><a id="877" href="Category.Applicative.Indexed.html#877" class="Bound">I</a> <a id="879" class="Symbol">:</a> <a id="881" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="885" href="Category.Applicative.Indexed.html#614" class="Generalizable">i</a><a id="886" class="Symbol">}</a> <a id="888" class="Symbol">(</a><a id="889" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="891" class="Symbol">:</a> <a id="893" href="Category.Applicative.Indexed.html#669" class="Function">IFun</a> <a id="898" href="Category.Applicative.Indexed.html#877" class="Bound">I</a> <a id="900" href="Category.Applicative.Indexed.html#616" class="Generalizable">f</a><a id="901" class="Symbol">)</a> <a id="903" class="Symbol">:</a>
<a id="928" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="932" class="Symbol">(</a><a id="933" href="Category.Applicative.Indexed.html#885" class="Bound">i</a> <a id="935" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="937" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="941" href="Category.Applicative.Indexed.html#900" class="Bound">f</a><a id="942" class="Symbol">)</a> <a id="944" class="Keyword">where</a>
<a id="952" class="Keyword">infixl</a> <a id="959" class="Number">4</a> <a id="961" href="Category.Applicative.Indexed.html#1034" class="Function Operator">_⊛_</a> <a id="965" href="Category.Applicative.Indexed.html#1307" class="Function Operator">_<⊛_</a> <a id="970" href="Category.Applicative.Indexed.html#1384" class="Function Operator">_⊛>_</a>
<a id="977" class="Keyword">infix</a> <a id="984" class="Number">4</a> <a id="986" href="Category.Applicative.Indexed.html#1462" class="Function Operator">_⊗_</a>
<a id="993" class="Keyword">field</a>
<a id="RawIApplicative.pure"></a><a id="1003" href="Category.Applicative.Indexed.html#1003" class="Field">pure</a> <a id="1008" class="Symbol">:</a> <a id="1010" class="Symbol">∀</a> <a id="1012" class="Symbol">{</a><a id="1013" href="Category.Applicative.Indexed.html#1013" class="Bound">i</a><a id="1014" class="Symbol">}</a> <a id="1016" class="Symbol">→</a> <a id="1018" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1020" class="Symbol">→</a> <a id="1022" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1024" href="Category.Applicative.Indexed.html#1013" class="Bound">i</a> <a id="1026" href="Category.Applicative.Indexed.html#1013" class="Bound">i</a> <a id="1028" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a>
<a id="RawIApplicative._⊛_"></a><a id="1034" href="Category.Applicative.Indexed.html#1034" class="Field Operator">_⊛_</a> <a id="1039" class="Symbol">:</a> <a id="1041" class="Symbol">∀</a> <a id="1043" class="Symbol">{</a><a id="1044" href="Category.Applicative.Indexed.html#1044" class="Bound">i</a> <a id="1046" href="Category.Applicative.Indexed.html#1046" class="Bound">j</a> <a id="1048" href="Category.Applicative.Indexed.html#1048" class="Bound">k</a><a id="1049" class="Symbol">}</a> <a id="1051" class="Symbol">→</a> <a id="1053" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1055" href="Category.Applicative.Indexed.html#1044" class="Bound">i</a> <a id="1057" href="Category.Applicative.Indexed.html#1046" class="Bound">j</a> <a id="1059" class="Symbol">(</a><a id="1060" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1062" class="Symbol">→</a> <a id="1064" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a><a id="1065" class="Symbol">)</a> <a id="1067" class="Symbol">→</a> <a id="1069" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1071" href="Category.Applicative.Indexed.html#1046" class="Bound">j</a> <a id="1073" href="Category.Applicative.Indexed.html#1048" class="Bound">k</a> <a id="1075" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1077" class="Symbol">→</a> <a id="1079" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1081" href="Category.Applicative.Indexed.html#1044" class="Bound">i</a> <a id="1083" href="Category.Applicative.Indexed.html#1048" class="Bound">k</a> <a id="1085" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a>
<a id="RawIApplicative.rawFunctor"></a><a id="1090" href="Category.Applicative.Indexed.html#1090" class="Function">rawFunctor</a> <a id="1101" class="Symbol">:</a> <a id="1103" class="Symbol">∀</a> <a id="1105" class="Symbol">{</a><a id="1106" href="Category.Applicative.Indexed.html#1106" class="Bound">i</a> <a id="1108" href="Category.Applicative.Indexed.html#1108" class="Bound">j</a><a id="1109" class="Symbol">}</a> <a id="1111" class="Symbol">→</a> <a id="1113" href="Category.Functor.html#499" class="Record">RawFunctor</a> <a id="1124" class="Symbol">(</a><a id="1125" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1127" href="Category.Applicative.Indexed.html#1106" class="Bound">i</a> <a id="1129" href="Category.Applicative.Indexed.html#1108" class="Bound">j</a><a id="1130" class="Symbol">)</a>
<a id="1134" href="Category.Applicative.Indexed.html#1090" class="Function">rawFunctor</a> <a id="1145" class="Symbol">=</a> <a id="1147" class="Keyword">record</a>
<a id="1158" class="Symbol">{</a> <a id="1160" href="Category.Functor.html#608" class="Field Operator">_<$>_</a> <a id="1166" class="Symbol">=</a> <a id="1168" class="Symbol">λ</a> <a id="1170" href="Category.Applicative.Indexed.html#1170" class="Bound">g</a> <a id="1172" href="Category.Applicative.Indexed.html#1172" class="Bound">x</a> <a id="1174" class="Symbol">→</a> <a id="1176" href="Category.Applicative.Indexed.html#1003" class="Field">pure</a> <a id="1181" href="Category.Applicative.Indexed.html#1170" class="Bound">g</a> <a id="1183" href="Category.Applicative.Indexed.html#1034" class="Field Operator">⊛</a> <a id="1185" href="Category.Applicative.Indexed.html#1172" class="Bound">x</a>
<a id="1191" class="Symbol">}</a>
<a id="1196" class="Keyword">private</a>
<a id="1208" class="Keyword">open</a> <a id="1213" class="Keyword">module</a> <a id="RawIApplicative.RF"></a><a id="1220" href="Category.Applicative.Indexed.html#1220" class="Module">RF</a> <a id="1223" class="Symbol">{</a><a id="1224" href="Category.Applicative.Indexed.html#1224" class="Bound">i</a> <a id="1226" href="Category.Applicative.Indexed.html#1226" class="Bound">j</a> <a id="1228" class="Symbol">:</a> <a id="1230" href="Category.Applicative.Indexed.html#877" class="Bound">I</a><a id="1231" class="Symbol">}</a> <a id="1233" class="Symbol">=</a>
<a id="1246" href="Category.Functor.html#499" class="Module">RawFunctor</a> <a id="1257" class="Symbol">(</a><a id="1258" href="Category.Applicative.Indexed.html#1090" class="Function">rawFunctor</a> <a id="1269" class="Symbol">{</a><a id="1270" class="Argument">i</a> <a id="1272" class="Symbol">=</a> <a id="1274" href="Category.Applicative.Indexed.html#1224" class="Bound">i</a><a id="1275" class="Symbol">}</a> <a id="1277" class="Symbol">{</a><a id="1278" class="Argument">j</a> <a id="1280" class="Symbol">=</a> <a id="1282" href="Category.Applicative.Indexed.html#1226" class="Bound">j</a><a id="1283" class="Symbol">})</a>
<a id="1297" class="Keyword">public</a>
<a id="RawIApplicative._<⊛_"></a><a id="1307" href="Category.Applicative.Indexed.html#1307" class="Function Operator">_<⊛_</a> <a id="1312" class="Symbol">:</a> <a id="1314" class="Symbol">∀</a> <a id="1316" class="Symbol">{</a><a id="1317" href="Category.Applicative.Indexed.html#1317" class="Bound">i</a> <a id="1319" href="Category.Applicative.Indexed.html#1319" class="Bound">j</a> <a id="1321" href="Category.Applicative.Indexed.html#1321" class="Bound">k</a><a id="1322" class="Symbol">}</a> <a id="1324" class="Symbol">→</a> <a id="1326" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1328" href="Category.Applicative.Indexed.html#1317" class="Bound">i</a> <a id="1330" href="Category.Applicative.Indexed.html#1319" class="Bound">j</a> <a id="1332" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1334" class="Symbol">→</a> <a id="1336" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1338" href="Category.Applicative.Indexed.html#1319" class="Bound">j</a> <a id="1340" href="Category.Applicative.Indexed.html#1321" class="Bound">k</a> <a id="1342" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a> <a id="1344" class="Symbol">→</a> <a id="1346" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1348" href="Category.Applicative.Indexed.html#1317" class="Bound">i</a> <a id="1350" href="Category.Applicative.Indexed.html#1321" class="Bound">k</a> <a id="1352" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a>
<a id="1356" href="Category.Applicative.Indexed.html#1356" class="Bound">x</a> <a id="1358" href="Category.Applicative.Indexed.html#1307" class="Function Operator"><⊛</a> <a id="1361" href="Category.Applicative.Indexed.html#1361" class="Bound">y</a> <a id="1363" class="Symbol">=</a> <a id="1365" href="Function.Base.html#636" class="Function">const</a> <a id="1371" href="Category.Functor.html#608" class="Function Operator"><$></a> <a id="1375" href="Category.Applicative.Indexed.html#1356" class="Bound">x</a> <a id="1377" href="Category.Applicative.Indexed.html#1034" class="Field Operator">⊛</a> <a id="1379" href="Category.Applicative.Indexed.html#1361" class="Bound">y</a>
<a id="RawIApplicative._⊛>_"></a><a id="1384" href="Category.Applicative.Indexed.html#1384" class="Function Operator">_⊛>_</a> <a id="1389" class="Symbol">:</a> <a id="1391" class="Symbol">∀</a> <a id="1393" class="Symbol">{</a><a id="1394" href="Category.Applicative.Indexed.html#1394" class="Bound">i</a> <a id="1396" href="Category.Applicative.Indexed.html#1396" class="Bound">j</a> <a id="1398" href="Category.Applicative.Indexed.html#1398" class="Bound">k</a><a id="1399" class="Symbol">}</a> <a id="1401" class="Symbol">→</a> <a id="1403" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1405" href="Category.Applicative.Indexed.html#1394" class="Bound">i</a> <a id="1407" href="Category.Applicative.Indexed.html#1396" class="Bound">j</a> <a id="1409" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1411" class="Symbol">→</a> <a id="1413" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1415" href="Category.Applicative.Indexed.html#1396" class="Bound">j</a> <a id="1417" href="Category.Applicative.Indexed.html#1398" class="Bound">k</a> <a id="1419" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a> <a id="1421" class="Symbol">→</a> <a id="1423" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1425" href="Category.Applicative.Indexed.html#1394" class="Bound">i</a> <a id="1427" href="Category.Applicative.Indexed.html#1398" class="Bound">k</a> <a id="1429" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a>
<a id="1433" href="Category.Applicative.Indexed.html#1433" class="Bound">x</a> <a id="1435" href="Category.Applicative.Indexed.html#1384" class="Function Operator">⊛></a> <a id="1438" href="Category.Applicative.Indexed.html#1438" class="Bound">y</a> <a id="1440" class="Symbol">=</a> <a id="1442" href="Function.Base.html#673" class="Function">constᵣ</a> <a id="1449" href="Category.Functor.html#608" class="Function Operator"><$></a> <a id="1453" href="Category.Applicative.Indexed.html#1433" class="Bound">x</a> <a id="1455" href="Category.Applicative.Indexed.html#1034" class="Field Operator">⊛</a> <a id="1457" href="Category.Applicative.Indexed.html#1438" class="Bound">y</a>
<a id="RawIApplicative._⊗_"></a><a id="1462" href="Category.Applicative.Indexed.html#1462" class="Function Operator">_⊗_</a> <a id="1466" class="Symbol">:</a> <a id="1468" class="Symbol">∀</a> <a id="1470" class="Symbol">{</a><a id="1471" href="Category.Applicative.Indexed.html#1471" class="Bound">i</a> <a id="1473" href="Category.Applicative.Indexed.html#1473" class="Bound">j</a> <a id="1475" href="Category.Applicative.Indexed.html#1475" class="Bound">k</a><a id="1476" class="Symbol">}</a> <a id="1478" class="Symbol">→</a> <a id="1480" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1482" href="Category.Applicative.Indexed.html#1471" class="Bound">i</a> <a id="1484" href="Category.Applicative.Indexed.html#1473" class="Bound">j</a> <a id="1486" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1488" class="Symbol">→</a> <a id="1490" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1492" href="Category.Applicative.Indexed.html#1473" class="Bound">j</a> <a id="1494" href="Category.Applicative.Indexed.html#1475" class="Bound">k</a> <a id="1496" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a> <a id="1498" class="Symbol">→</a> <a id="1500" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1502" href="Category.Applicative.Indexed.html#1471" class="Bound">i</a> <a id="1504" href="Category.Applicative.Indexed.html#1475" class="Bound">k</a> <a id="1506" class="Symbol">(</a><a id="1507" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1509" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="1511" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a><a id="1512" class="Symbol">)</a>
<a id="1516" href="Category.Applicative.Indexed.html#1516" class="Bound">x</a> <a id="1518" href="Category.Applicative.Indexed.html#1462" class="Function Operator">⊗</a> <a id="1520" href="Category.Applicative.Indexed.html#1520" class="Bound">y</a> <a id="1522" class="Symbol">=</a> <a id="1524" class="Symbol">(</a><a id="1525" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a><a id="1528" class="Symbol">)</a> <a id="1530" href="Category.Functor.html#608" class="Function Operator"><$></a> <a id="1534" href="Category.Applicative.Indexed.html#1516" class="Bound">x</a> <a id="1536" href="Category.Applicative.Indexed.html#1034" class="Field Operator">⊛</a> <a id="1538" href="Category.Applicative.Indexed.html#1520" class="Bound">y</a>
<a id="RawIApplicative.zipWith"></a><a id="1543" href="Category.Applicative.Indexed.html#1543" class="Function">zipWith</a> <a id="1551" class="Symbol">:</a> <a id="1553" class="Symbol">∀</a> <a id="1555" class="Symbol">{</a><a id="1556" href="Category.Applicative.Indexed.html#1556" class="Bound">i</a> <a id="1558" href="Category.Applicative.Indexed.html#1558" class="Bound">j</a> <a id="1560" href="Category.Applicative.Indexed.html#1560" class="Bound">k</a><a id="1561" class="Symbol">}</a> <a id="1563" class="Symbol">→</a> <a id="1565" class="Symbol">(</a><a id="1566" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1568" class="Symbol">→</a> <a id="1570" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a> <a id="1572" class="Symbol">→</a> <a id="1574" href="Category.Applicative.Indexed.html#658" class="Generalizable">C</a><a id="1575" class="Symbol">)</a> <a id="1577" class="Symbol">→</a> <a id="1579" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1581" href="Category.Applicative.Indexed.html#1556" class="Bound">i</a> <a id="1583" href="Category.Applicative.Indexed.html#1558" class="Bound">j</a> <a id="1585" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1587" class="Symbol">→</a> <a id="1589" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1591" href="Category.Applicative.Indexed.html#1558" class="Bound">j</a> <a id="1593" href="Category.Applicative.Indexed.html#1560" class="Bound">k</a> <a id="1595" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a> <a id="1597" class="Symbol">→</a> <a id="1599" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1601" href="Category.Applicative.Indexed.html#1556" class="Bound">i</a> <a id="1603" href="Category.Applicative.Indexed.html#1560" class="Bound">k</a> <a id="1605" href="Category.Applicative.Indexed.html#658" class="Generalizable">C</a>
<a id="1609" href="Category.Applicative.Indexed.html#1543" class="Function">zipWith</a> <a id="1617" href="Category.Applicative.Indexed.html#1617" class="Bound">f</a> <a id="1619" href="Category.Applicative.Indexed.html#1619" class="Bound">x</a> <a id="1621" href="Category.Applicative.Indexed.html#1621" class="Bound">y</a> <a id="1623" class="Symbol">=</a> <a id="1625" href="Category.Applicative.Indexed.html#1617" class="Bound">f</a> <a id="1627" href="Category.Functor.html#608" class="Function Operator"><$></a> <a id="1631" href="Category.Applicative.Indexed.html#1619" class="Bound">x</a> <a id="1633" href="Category.Applicative.Indexed.html#1034" class="Field Operator">⊛</a> <a id="1635" href="Category.Applicative.Indexed.html#1621" class="Bound">y</a>
<a id="RawIApplicative.zip"></a><a id="1640" href="Category.Applicative.Indexed.html#1640" class="Function">zip</a> <a id="1644" class="Symbol">:</a> <a id="1646" class="Symbol">∀</a> <a id="1648" class="Symbol">{</a><a id="1649" href="Category.Applicative.Indexed.html#1649" class="Bound">i</a> <a id="1651" href="Category.Applicative.Indexed.html#1651" class="Bound">j</a> <a id="1653" href="Category.Applicative.Indexed.html#1653" class="Bound">k</a><a id="1654" class="Symbol">}</a> <a id="1656" class="Symbol">→</a> <a id="1658" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1660" href="Category.Applicative.Indexed.html#1649" class="Bound">i</a> <a id="1662" href="Category.Applicative.Indexed.html#1651" class="Bound">j</a> <a id="1664" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1666" class="Symbol">→</a> <a id="1668" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1670" href="Category.Applicative.Indexed.html#1651" class="Bound">j</a> <a id="1672" href="Category.Applicative.Indexed.html#1653" class="Bound">k</a> <a id="1674" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a> <a id="1676" class="Symbol">→</a> <a id="1678" href="Category.Applicative.Indexed.html#889" class="Bound">F</a> <a id="1680" href="Category.Applicative.Indexed.html#1649" class="Bound">i</a> <a id="1682" href="Category.Applicative.Indexed.html#1653" class="Bound">k</a> <a id="1684" class="Symbol">(</a><a id="1685" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="1687" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="1689" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a><a id="1690" class="Symbol">)</a>
<a id="1694" href="Category.Applicative.Indexed.html#1640" class="Function">zip</a> <a id="1698" class="Symbol">=</a> <a id="1700" href="Category.Applicative.Indexed.html#1543" class="Function">zipWith</a> <a id="1708" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a>
<a id="1713" class="Comment">------------------------------------------------------------------------</a>
<a id="1786" class="Comment">-- Applicative with a zero</a>
<a id="1814" class="Keyword">record</a> <a id="RawIApplicativeZero"></a><a id="1821" href="Category.Applicative.Indexed.html#1821" class="Record">RawIApplicativeZero</a>
<a id="1848" class="Symbol">{</a><a id="1849" href="Category.Applicative.Indexed.html#1849" class="Bound">I</a> <a id="1851" class="Symbol">:</a> <a id="1853" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1857" href="Category.Applicative.Indexed.html#614" class="Generalizable">i</a><a id="1858" class="Symbol">}</a> <a id="1860" class="Symbol">(</a><a id="1861" href="Category.Applicative.Indexed.html#1861" class="Bound">F</a> <a id="1863" class="Symbol">:</a> <a id="1865" href="Category.Applicative.Indexed.html#669" class="Function">IFun</a> <a id="1870" href="Category.Applicative.Indexed.html#1849" class="Bound">I</a> <a id="1872" href="Category.Applicative.Indexed.html#616" class="Generalizable">f</a><a id="1873" class="Symbol">)</a> <a id="1875" class="Symbol">:</a>
<a id="1884" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1888" class="Symbol">(</a><a id="1889" href="Category.Applicative.Indexed.html#1857" class="Bound">i</a> <a id="1891" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1893" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="1897" href="Category.Applicative.Indexed.html#1872" class="Bound">f</a><a id="1898" class="Symbol">)</a> <a id="1900" class="Keyword">where</a>
<a id="1908" class="Keyword">field</a>
<a id="RawIApplicativeZero.applicative"></a><a id="1918" href="Category.Applicative.Indexed.html#1918" class="Field">applicative</a> <a id="1930" class="Symbol">:</a> <a id="1932" href="Category.Applicative.Indexed.html#860" class="Record">RawIApplicative</a> <a id="1948" href="Category.Applicative.Indexed.html#1861" class="Bound">F</a>
<a id="RawIApplicativeZero.∅"></a><a id="1954" href="Category.Applicative.Indexed.html#1954" class="Field">∅</a> <a id="1966" class="Symbol">:</a> <a id="1968" class="Symbol">∀</a> <a id="1970" class="Symbol">{</a><a id="1971" href="Category.Applicative.Indexed.html#1971" class="Bound">i</a> <a id="1973" href="Category.Applicative.Indexed.html#1973" class="Bound">j</a><a id="1974" class="Symbol">}</a> <a id="1976" class="Symbol">→</a> <a id="1978" href="Category.Applicative.Indexed.html#1861" class="Bound">F</a> <a id="1980" href="Category.Applicative.Indexed.html#1971" class="Bound">i</a> <a id="1982" href="Category.Applicative.Indexed.html#1973" class="Bound">j</a> <a id="1984" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a>
<a id="1989" class="Keyword">open</a> <a id="1994" href="Category.Applicative.Indexed.html#860" class="Module">RawIApplicative</a> <a id="2010" href="Category.Applicative.Indexed.html#1918" class="Field">applicative</a> <a id="2022" class="Keyword">public</a>
<a id="2030" class="Comment">------------------------------------------------------------------------</a>
<a id="2103" class="Comment">-- Alternative functors: `F i j A` is a monoid</a>
<a id="2151" class="Keyword">record</a> <a id="RawIAlternative"></a><a id="2158" href="Category.Applicative.Indexed.html#2158" class="Record">RawIAlternative</a>
<a id="2181" class="Symbol">{</a><a id="2182" href="Category.Applicative.Indexed.html#2182" class="Bound">I</a> <a id="2184" class="Symbol">:</a> <a id="2186" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2190" href="Category.Applicative.Indexed.html#614" class="Generalizable">i</a><a id="2191" class="Symbol">}</a> <a id="2193" class="Symbol">(</a><a id="2194" href="Category.Applicative.Indexed.html#2194" class="Bound">F</a> <a id="2196" class="Symbol">:</a> <a id="2198" href="Category.Applicative.Indexed.html#669" class="Function">IFun</a> <a id="2203" href="Category.Applicative.Indexed.html#2182" class="Bound">I</a> <a id="2205" href="Category.Applicative.Indexed.html#616" class="Generalizable">f</a><a id="2206" class="Symbol">)</a> <a id="2208" class="Symbol">:</a>
<a id="2217" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2221" class="Symbol">(</a><a id="2222" href="Category.Applicative.Indexed.html#2190" class="Bound">i</a> <a id="2224" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2226" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="2230" href="Category.Applicative.Indexed.html#2205" class="Bound">f</a><a id="2231" class="Symbol">)</a> <a id="2233" class="Keyword">where</a>
<a id="2241" class="Keyword">infixr</a> <a id="2248" class="Number">3</a> _∣_
<a id="2256" class="Keyword">field</a>
<a id="RawIAlternative.applicativeZero"></a><a id="2266" href="Category.Applicative.Indexed.html#2266" class="Field">applicativeZero</a> <a id="2282" class="Symbol">:</a> <a id="2284" href="Category.Applicative.Indexed.html#1821" class="Record">RawIApplicativeZero</a> <a id="2304" href="Category.Applicative.Indexed.html#2194" class="Bound">F</a>
<a id="RawIAlternative._∣_"></a><a id="2310" href="Category.Applicative.Indexed.html#2310" class="Field Operator">_∣_</a> <a id="2326" class="Symbol">:</a> <a id="2328" class="Symbol">∀</a> <a id="2330" class="Symbol">{</a><a id="2331" href="Category.Applicative.Indexed.html#2331" class="Bound">i</a> <a id="2333" href="Category.Applicative.Indexed.html#2333" class="Bound">j</a><a id="2334" class="Symbol">}</a> <a id="2336" class="Symbol">→</a> <a id="2338" href="Category.Applicative.Indexed.html#2194" class="Bound">F</a> <a id="2340" href="Category.Applicative.Indexed.html#2331" class="Bound">i</a> <a id="2342" href="Category.Applicative.Indexed.html#2333" class="Bound">j</a> <a id="2344" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="2346" class="Symbol">→</a> <a id="2348" href="Category.Applicative.Indexed.html#2194" class="Bound">F</a> <a id="2350" href="Category.Applicative.Indexed.html#2331" class="Bound">i</a> <a id="2352" href="Category.Applicative.Indexed.html#2333" class="Bound">j</a> <a id="2354" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="2356" class="Symbol">→</a> <a id="2358" href="Category.Applicative.Indexed.html#2194" class="Bound">F</a> <a id="2360" href="Category.Applicative.Indexed.html#2331" class="Bound">i</a> <a id="2362" href="Category.Applicative.Indexed.html#2333" class="Bound">j</a> <a id="2364" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a>
<a id="2369" class="Keyword">open</a> <a id="2374" href="Category.Applicative.Indexed.html#1821" class="Module">RawIApplicativeZero</a> <a id="2394" href="Category.Applicative.Indexed.html#2266" class="Field">applicativeZero</a> <a id="2410" class="Keyword">public</a>
<a id="2419" class="Comment">------------------------------------------------------------------------</a>
<a id="2492" class="Comment">-- Applicative functor morphisms, specialised to propositional</a>
<a id="2555" class="Comment">-- equality.</a>
<a id="2569" class="Keyword">record</a> <a id="Morphism"></a><a id="2576" href="Category.Applicative.Indexed.html#2576" class="Record">Morphism</a> <a id="2585" class="Symbol">{</a><a id="2586" href="Category.Applicative.Indexed.html#2586" class="Bound">I</a> <a id="2588" class="Symbol">:</a> <a id="2590" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2594" href="Category.Applicative.Indexed.html#614" class="Generalizable">i</a><a id="2595" class="Symbol">}</a> <a id="2597" class="Symbol">{</a><a id="2598" href="Category.Applicative.Indexed.html#2598" class="Bound">F₁</a> <a id="2601" href="Category.Applicative.Indexed.html#2601" class="Bound">F₂</a> <a id="2604" class="Symbol">:</a> <a id="2606" href="Category.Applicative.Indexed.html#669" class="Function">IFun</a> <a id="2611" href="Category.Applicative.Indexed.html#2586" class="Bound">I</a> <a id="2613" href="Category.Applicative.Indexed.html#616" class="Generalizable">f</a><a id="2614" class="Symbol">}</a>
<a id="2632" class="Symbol">(</a><a id="2633" href="Category.Applicative.Indexed.html#2633" class="Bound">A₁</a> <a id="2636" class="Symbol">:</a> <a id="2638" href="Category.Applicative.Indexed.html#860" class="Record">RawIApplicative</a> <a id="2654" href="Category.Applicative.Indexed.html#2598" class="Bound">F₁</a><a id="2656" class="Symbol">)</a>
<a id="2674" class="Symbol">(</a><a id="2675" href="Category.Applicative.Indexed.html#2675" class="Bound">A₂</a> <a id="2678" class="Symbol">:</a> <a id="2680" href="Category.Applicative.Indexed.html#860" class="Record">RawIApplicative</a> <a id="2696" href="Category.Applicative.Indexed.html#2601" class="Bound">F₂</a><a id="2698" class="Symbol">)</a> <a id="2700" class="Symbol">:</a> <a id="2702" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2706" class="Symbol">(</a><a id="2707" href="Category.Applicative.Indexed.html#2594" class="Bound">i</a> <a id="2709" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2711" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="2715" href="Category.Applicative.Indexed.html#2613" class="Bound">f</a><a id="2716" class="Symbol">)</a> <a id="2718" class="Keyword">where</a>
<a id="2726" class="Keyword">module</a> <a id="Morphism.A₁"></a><a id="2733" href="Category.Applicative.Indexed.html#2733" class="Module">A₁</a> <a id="2736" class="Symbol">=</a> <a id="2738" href="Category.Applicative.Indexed.html#860" class="Module">RawIApplicative</a> <a id="2754" href="Category.Applicative.Indexed.html#2633" class="Bound">A₁</a>
<a id="2759" class="Keyword">module</a> <a id="Morphism.A₂"></a><a id="2766" href="Category.Applicative.Indexed.html#2766" class="Module">A₂</a> <a id="2769" class="Symbol">=</a> <a id="2771" href="Category.Applicative.Indexed.html#860" class="Module">RawIApplicative</a> <a id="2787" href="Category.Applicative.Indexed.html#2675" class="Bound">A₂</a>
<a id="2792" class="Keyword">field</a>
<a id="Morphism.op"></a><a id="2802" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="2810" class="Symbol">:</a> <a id="2812" class="Symbol">∀</a> <a id="2814" class="Symbol">{</a><a id="2815" href="Category.Applicative.Indexed.html#2815" class="Bound">i</a> <a id="2817" href="Category.Applicative.Indexed.html#2817" class="Bound">j</a><a id="2818" class="Symbol">}</a> <a id="2820" class="Symbol">→</a> <a id="2822" href="Category.Applicative.Indexed.html#2598" class="Bound">F₁</a> <a id="2825" href="Category.Applicative.Indexed.html#2815" class="Bound">i</a> <a id="2827" href="Category.Applicative.Indexed.html#2817" class="Bound">j</a> <a id="2829" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="2831" class="Symbol">→</a> <a id="2833" href="Category.Applicative.Indexed.html#2601" class="Bound">F₂</a> <a id="2836" href="Category.Applicative.Indexed.html#2815" class="Bound">i</a> <a id="2838" href="Category.Applicative.Indexed.html#2817" class="Bound">j</a> <a id="2840" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a>
<a id="Morphism.op-pure"></a><a id="2846" href="Category.Applicative.Indexed.html#2846" class="Field">op-pure</a> <a id="2854" class="Symbol">:</a> <a id="2856" class="Symbol">∀</a> <a id="2858" class="Symbol">{</a><a id="2859" href="Category.Applicative.Indexed.html#2859" class="Bound">i</a><a id="2860" class="Symbol">}</a> <a id="2862" class="Symbol">(</a><a id="2863" href="Category.Applicative.Indexed.html#2863" class="Bound">x</a> <a id="2865" class="Symbol">:</a> <a id="2867" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a><a id="2868" class="Symbol">)</a> <a id="2870" class="Symbol">→</a> <a id="2872" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="2875" class="Symbol">(</a><a id="2876" href="Category.Applicative.Indexed.html#1003" class="Function">A₁.pure</a> <a id="2884" class="Symbol">{</a><a id="2885" class="Argument">i</a> <a id="2887" class="Symbol">=</a> <a id="2889" href="Category.Applicative.Indexed.html#2859" class="Bound">i</a><a id="2890" class="Symbol">}</a> <a id="2892" href="Category.Applicative.Indexed.html#2863" class="Bound">x</a><a id="2893" class="Symbol">)</a> <a id="2895" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2897" href="Category.Applicative.Indexed.html#1003" class="Function">A₂.pure</a> <a id="2905" href="Category.Applicative.Indexed.html#2863" class="Bound">x</a>
<a id="Morphism.op-⊛"></a><a id="2911" href="Category.Applicative.Indexed.html#2911" class="Field">op-⊛</a> <a id="2919" class="Symbol">:</a> <a id="2921" class="Symbol">∀</a> <a id="2923" class="Symbol">{</a><a id="2924" href="Category.Applicative.Indexed.html#2924" class="Bound">i</a> <a id="2926" href="Category.Applicative.Indexed.html#2926" class="Bound">j</a> <a id="2928" href="Category.Applicative.Indexed.html#2928" class="Bound">k</a><a id="2929" class="Symbol">}</a> <a id="2931" class="Symbol">(</a><a id="2932" href="Category.Applicative.Indexed.html#2932" class="Bound">f</a> <a id="2934" class="Symbol">:</a> <a id="2936" href="Category.Applicative.Indexed.html#2598" class="Bound">F₁</a> <a id="2939" href="Category.Applicative.Indexed.html#2924" class="Bound">i</a> <a id="2941" href="Category.Applicative.Indexed.html#2926" class="Bound">j</a> <a id="2943" class="Symbol">(</a><a id="2944" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="2946" class="Symbol">→</a> <a id="2948" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a><a id="2949" class="Symbol">))</a> <a id="2952" class="Symbol">(</a><a id="2953" href="Category.Applicative.Indexed.html#2953" class="Bound">x</a> <a id="2955" class="Symbol">:</a> <a id="2957" href="Category.Applicative.Indexed.html#2598" class="Bound">F₁</a> <a id="2960" href="Category.Applicative.Indexed.html#2926" class="Bound">j</a> <a id="2962" href="Category.Applicative.Indexed.html#2928" class="Bound">k</a> <a id="2964" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a><a id="2965" class="Symbol">)</a> <a id="2967" class="Symbol">→</a>
<a id="2983" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="2986" class="Symbol">(</a><a id="2987" href="Category.Applicative.Indexed.html#2932" class="Bound">f</a> <a id="2989" href="Category.Applicative.Indexed.html#1034" class="Function Operator">A₁.⊛</a> <a id="2994" href="Category.Applicative.Indexed.html#2953" class="Bound">x</a><a id="2995" class="Symbol">)</a> <a id="2997" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2999" class="Symbol">(</a><a id="3000" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="3003" href="Category.Applicative.Indexed.html#2932" class="Bound">f</a> <a id="3005" href="Category.Applicative.Indexed.html#1034" class="Function Operator">A₂.⊛</a> <a id="3010" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="3013" href="Category.Applicative.Indexed.html#2953" class="Bound">x</a><a id="3014" class="Symbol">)</a>
<a id="Morphism.op-<$>"></a><a id="3019" href="Category.Applicative.Indexed.html#3019" class="Function">op-<$></a> <a id="3026" class="Symbol">:</a> <a id="3028" class="Symbol">∀</a> <a id="3030" class="Symbol">{</a><a id="3031" href="Category.Applicative.Indexed.html#3031" class="Bound">i</a> <a id="3033" href="Category.Applicative.Indexed.html#3033" class="Bound">j</a><a id="3034" class="Symbol">}</a> <a id="3036" class="Symbol">(</a><a id="3037" href="Category.Applicative.Indexed.html#3037" class="Bound">f</a> <a id="3039" class="Symbol">:</a> <a id="3041" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a> <a id="3043" class="Symbol">→</a> <a id="3045" href="Category.Applicative.Indexed.html#644" class="Generalizable">B</a><a id="3046" class="Symbol">)</a> <a id="3048" class="Symbol">(</a><a id="3049" href="Category.Applicative.Indexed.html#3049" class="Bound">x</a> <a id="3051" class="Symbol">:</a> <a id="3053" href="Category.Applicative.Indexed.html#2598" class="Bound">F₁</a> <a id="3056" href="Category.Applicative.Indexed.html#3031" class="Bound">i</a> <a id="3058" href="Category.Applicative.Indexed.html#3033" class="Bound">j</a> <a id="3060" href="Category.Applicative.Indexed.html#630" class="Generalizable">A</a><a id="3061" class="Symbol">)</a> <a id="3063" class="Symbol">→</a>
<a id="3076" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="3079" class="Symbol">(</a><a id="3080" href="Category.Applicative.Indexed.html#3037" class="Bound">f</a> <a id="3082" href="Category.Functor.html#608" class="Function Operator">A₁.<$></a> <a id="3089" href="Category.Applicative.Indexed.html#3049" class="Bound">x</a><a id="3090" class="Symbol">)</a> <a id="3092" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3094" class="Symbol">(</a><a id="3095" href="Category.Applicative.Indexed.html#3037" class="Bound">f</a> <a id="3097" href="Category.Functor.html#608" class="Function Operator">A₂.<$></a> <a id="3104" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="3107" href="Category.Applicative.Indexed.html#3049" class="Bound">x</a><a id="3108" class="Symbol">)</a>
<a id="3112" href="Category.Applicative.Indexed.html#3019" class="Function">op-<$></a> <a id="3119" href="Category.Applicative.Indexed.html#3119" class="Bound">f</a> <a id="3121" href="Category.Applicative.Indexed.html#3121" class="Bound">x</a> <a id="3123" class="Symbol">=</a> <a id="3125" href="Relation.Binary.PropositionalEquality.Core.html#2806" class="Function Operator">begin</a>
<a id="3135" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="3138" class="Symbol">(</a><a id="3139" href="Category.Applicative.Indexed.html#1034" class="Function Operator">A₁._⊛_</a> <a id="3146" class="Symbol">(</a><a id="3147" href="Category.Applicative.Indexed.html#1003" class="Function">A₁.pure</a> <a id="3155" href="Category.Applicative.Indexed.html#3119" class="Bound">f</a><a id="3156" class="Symbol">)</a> <a id="3158" href="Category.Applicative.Indexed.html#3121" class="Bound">x</a><a id="3159" class="Symbol">)</a> <a id="3167" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3170" href="Category.Applicative.Indexed.html#2911" class="Field">op-⊛</a> <a id="3175" class="Symbol">_</a> <a id="3177" class="Symbol">_</a> <a id="3179" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3185" href="Category.Applicative.Indexed.html#1034" class="Function Operator">A₂._⊛_</a> <a id="3192" class="Symbol">(</a><a id="3193" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="3196" class="Symbol">(</a><a id="3197" href="Category.Applicative.Indexed.html#1003" class="Function">A₁.pure</a> <a id="3205" href="Category.Applicative.Indexed.html#3119" class="Bound">f</a><a id="3206" class="Symbol">))</a> <a id="3209" class="Symbol">(</a><a id="3210" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="3213" href="Category.Applicative.Indexed.html#3121" class="Bound">x</a><a id="3214" class="Symbol">)</a> <a id="3217" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">≡⟨</a> <a id="3220" href="Relation.Binary.PropositionalEquality.Core.html#1367" class="Function">P.cong₂</a> <a id="3228" href="Category.Applicative.Indexed.html#1034" class="Function Operator">A₂._⊛_</a> <a id="3235" class="Symbol">(</a><a id="3236" href="Category.Applicative.Indexed.html#2846" class="Field">op-pure</a> <a id="3244" class="Symbol">_)</a> <a id="3247" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">P.refl</a> <a id="3254" href="Relation.Binary.PropositionalEquality.Core.html#2923" class="Function">⟩</a>
<a id="3260" href="Category.Applicative.Indexed.html#1034" class="Function Operator">A₂._⊛_</a> <a id="3267" class="Symbol">(</a><a id="3268" href="Category.Applicative.Indexed.html#1003" class="Function">A₂.pure</a> <a id="3276" href="Category.Applicative.Indexed.html#3119" class="Bound">f</a><a id="3277" class="Symbol">)</a> <a id="3279" class="Symbol">(</a><a id="3280" href="Category.Applicative.Indexed.html#2802" class="Field">op</a> <a id="3283" href="Category.Applicative.Indexed.html#3121" class="Bound">x</a><a id="3284" class="Symbol">)</a> <a id="3292" href="Relation.Binary.PropositionalEquality.Core.html#3105" class="Function Operator">∎</a>
<a id="3298" class="Keyword">where</a> <a id="3304" class="Keyword">open</a> <a id="3309" href="Relation.Binary.PropositionalEquality.Core.html#2708" class="Module">P.≡-Reasoning</a>
</pre></body></html>