agda-stdlib-doc 0.14-1 / usr / share / doc / agda-stdlib-doc / html / Algebra.Properties.BooleanAlgebra.Expression.html

This file is indexed.

/usr/share/doc/agda-stdlib-doc/html/Algebra.Properties.BooleanAlgebra.Expression.html is in agda-stdlib-doc 0.14-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Algebra.Properties.BooleanAlgebra.Expression</title><link rel="stylesheet" href="Agda.css"></head><body><pre><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">-- Boolean algebra expressions</a>
<a id="137" class="Comment">------------------------------------------------------------------------</a>

<a id="211" class="Keyword">open</a> <a id="216" class="Keyword">import</a> <a id="223" href="Algebra.html" class="Module">Algebra</a>

<a id="232" class="Keyword">module</a> <a id="239" href="Algebra.Properties.BooleanAlgebra.Expression.html" class="Module">Algebra.Properties.BooleanAlgebra.Expression</a>
  <a id="286" class="Symbol">{</a><a id="287" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a><a id="288" class="Symbol">}</a> <a id="290" class="Symbol">(</a><a id="291" href="Algebra.Properties.BooleanAlgebra.Expression.html#291" class="Bound">B</a> <a id="293" class="Symbol">:</a> <a id="295" href="Algebra.html#BooleanAlgebra" class="Record">BooleanAlgebra</a> <a id="310" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a> <a id="312" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a><a id="313" class="Symbol">)</a>
  <a id="317" class="Keyword">where</a>

<a id="324" class="Keyword">open</a> <a id="329" href="Algebra.html#BooleanAlgebra" class="Module">BooleanAlgebra</a> <a id="344" href="Algebra.Properties.BooleanAlgebra.Expression.html#291" class="Bound">B</a>

<a id="347" class="Keyword">open</a> <a id="352" class="Keyword">import</a> <a id="359" href="Category.Applicative.html" class="Module">Category.Applicative</a>
<a id="380" class="Keyword">import</a> <a id="387" href="Category.Applicative.Indexed.html" class="Module">Category.Applicative.Indexed</a> <a id="416" class="Symbol">as</a> <a id="419" class="Module">Applicative</a>
<a id="431" class="Keyword">open</a> <a id="436" class="Keyword">import</a> <a id="443" href="Category.Monad.html" class="Module">Category.Monad</a>
<a id="458" class="Keyword">open</a> <a id="463" class="Keyword">import</a> <a id="470" href="Category.Monad.Identity.html" class="Module">Category.Monad.Identity</a>
<a id="494" class="Keyword">open</a> <a id="499" class="Keyword">import</a> <a id="506" href="Data.Fin.html" class="Module">Data.Fin</a> <a id="515" class="Keyword">using</a> <a id="521" class="Symbol">(</a><a id="522" href="Data.Fin.html#Fin" class="Datatype">Fin</a><a id="525" class="Symbol">)</a>
<a id="527" class="Keyword">open</a> <a id="532" class="Keyword">import</a> <a id="539" href="Data.Nat.html" class="Module">Data.Nat</a>
<a id="548" class="Keyword">open</a> <a id="553" class="Keyword">import</a> <a id="560" href="Data.Vec.html" class="Module">Data.Vec</a> <a id="569" class="Symbol">as</a> <a id="572" class="Module">Vec</a> <a id="576" class="Keyword">using</a> <a id="582" class="Symbol">(</a><a id="583" href="Data.Vec.html#Vec" class="Datatype">Vec</a><a id="586" class="Symbol">)</a>
<a id="588" class="Keyword">open</a> <a id="593" class="Keyword">import</a> <a id="600" href="Data.Product.html" class="Module">Data.Product</a> <a id="613" class="Keyword">using</a> <a id="619" class="Symbol">(</a><a id="620" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">_,_</a><a id="623" class="Symbol">;</a> <a id="625" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a><a id="630" class="Symbol">;</a> <a id="632" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a><a id="637" class="Symbol">)</a>
<a id="639" class="Keyword">import</a> <a id="646" href="Data.Vec.Properties.html" class="Module">Data.Vec.Properties</a> <a id="666" class="Symbol">as</a> <a id="669" class="Module">VecProp</a>
<a id="677" class="Keyword">open</a> <a id="682" class="Keyword">import</a> <a id="689" href="Function.html" class="Module">Function</a>
<a id="698" class="Keyword">open</a> <a id="703" class="Keyword">import</a> <a id="710" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="748" class="Symbol">as</a> <a id="751" class="Module">P</a> <a id="753" class="Keyword">using</a> <a id="759" class="Symbol">(</a><a id="760" href="Relation.Binary.PropositionalEquality.html#_%E2%89%97_" class="Function Operator">_≗_</a><a id="763" class="Symbol">)</a>
<a id="765" class="Keyword">import</a> <a id="772" href="Relation.Binary.Reflection.html" class="Module">Relation.Binary.Reflection</a> <a id="799" class="Symbol">as</a> <a id="802" class="Module">Reflection</a>
<a id="813" class="Keyword">open</a> <a id="818" class="Keyword">import</a> <a id="825" href="Relation.Binary.Vec.Pointwise.html" class="Module">Relation.Binary.Vec.Pointwise</a> <a id="855" class="Symbol">as</a> <a id="858" class="Module">PW</a>
  <a id="863" class="Keyword">using</a> <a id="869" class="Symbol">(</a><a id="870" href="Relation.Binary.Vec.Pointwise.html#Pointwise" class="Record">Pointwise</a><a id="879" class="Symbol">;</a> <a id="881" class="Keyword">module</a> <a id="888" href="Relation.Binary.Vec.Pointwise.html#Pointwise" class="Module">Pointwise</a><a id="897" class="Symbol">;</a> <a id="899" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a><a id="902" class="Symbol">)</a>

<a id="905" class="Comment">-- Expressions made up of variables and the operations of a boolean</a>
<a id="973" class="Comment">-- algebra.</a>

<a id="986" class="Keyword">infixr</a> <a id="993" class="Number">7</a> <a id="995" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">_and_</a>
<a id="1001" class="Keyword">infixr</a> <a id="1008" class="Number">6</a> <a id="1010" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">_or_</a>

<a id="1016" class="Keyword">data</a> <a id="Expr" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="1026" href="Algebra.Properties.BooleanAlgebra.Expression.html#1026" class="Bound">n</a> <a id="1028" class="Symbol">:</a> <a id="1030" class="PrimitiveType">Set</a> <a id="1034" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a> <a id="1036" class="Keyword">where</a>
  <a id="Expr.var" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.var" class="InductiveConstructor">var</a>        <a id="1055" class="Symbol">:</a> <a id="1057" class="Symbol">(</a><a id="1058" href="Algebra.Properties.BooleanAlgebra.Expression.html#1058" class="Bound">x</a> <a id="1060" class="Symbol">:</a> <a id="1062" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1066" href="Algebra.Properties.BooleanAlgebra.Expression.html#1026" class="Bound">n</a><a id="1067" class="Symbol">)</a> <a id="1069" class="Symbol">→</a> <a id="1071" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="1076" href="Algebra.Properties.BooleanAlgebra.Expression.html#1026" class="Bound">n</a>
  <a id="Expr._or_" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">_or_</a> <a id="Expr._and_" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">_and_</a> <a id="1091" class="Symbol">:</a> <a id="1093" class="Symbol">(</a><a id="1094" href="Algebra.Properties.BooleanAlgebra.Expression.html#1094" class="Bound">e₁</a> <a id="1097" href="Algebra.Properties.BooleanAlgebra.Expression.html#1097" class="Bound">e₂</a> <a id="1100" class="Symbol">:</a> <a id="1102" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="1107" href="Algebra.Properties.BooleanAlgebra.Expression.html#1026" class="Bound">n</a><a id="1108" class="Symbol">)</a> <a id="1110" class="Symbol">→</a> <a id="1112" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="1117" href="Algebra.Properties.BooleanAlgebra.Expression.html#1026" class="Bound">n</a>
  <a id="Expr.not" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.not" class="InductiveConstructor">not</a>        <a id="1132" class="Symbol">:</a> <a id="1134" class="Symbol">(</a><a id="1135" href="Algebra.Properties.BooleanAlgebra.Expression.html#1135" class="Bound">e</a> <a id="1137" class="Symbol">:</a> <a id="1139" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="1144" href="Algebra.Properties.BooleanAlgebra.Expression.html#1026" class="Bound">n</a><a id="1145" class="Symbol">)</a> <a id="1147" class="Symbol">→</a> <a id="1149" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="1154" href="Algebra.Properties.BooleanAlgebra.Expression.html#1026" class="Bound">n</a>
  <a id="Expr.top" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.top" class="InductiveConstructor">top</a> <a id="Expr.bot" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.bot" class="InductiveConstructor">bot</a>    <a id="1169" class="Symbol">:</a> <a id="1171" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="1176" href="Algebra.Properties.BooleanAlgebra.Expression.html#1026" class="Bound">n</a>

<a id="1179" class="Comment">-- The semantics of an expression, parametrised by an applicative</a>
<a id="1245" class="Comment">-- functor.</a>

<a id="1258" class="Keyword">module</a> <a id="Semantics" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics" class="Module">Semantics</a>
  <a id="1277" class="Symbol">{</a><a id="1278" href="Algebra.Properties.BooleanAlgebra.Expression.html#1278" class="Bound">F</a> <a id="1280" class="Symbol">:</a> <a id="1282" class="PrimitiveType">Set</a> <a id="1286" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a> <a id="1288" class="Symbol">→</a> <a id="1290" class="PrimitiveType">Set</a> <a id="1294" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a><a id="1295" class="Symbol">}</a>
  <a id="1299" class="Symbol">(</a><a id="1300" href="Algebra.Properties.BooleanAlgebra.Expression.html#1300" class="Bound">A</a> <a id="1302" class="Symbol">:</a> <a id="1304" href="Category.Applicative.html#RawApplicative" class="Function">RawApplicative</a> <a id="1319" href="Algebra.Properties.BooleanAlgebra.Expression.html#1278" class="Bound">F</a><a id="1320" class="Symbol">)</a>
  <a id="1324" class="Keyword">where</a>

  <a id="1333" class="Keyword">open</a> <a id="1338" href="Category.Applicative.html#RawApplicative" class="Module">RawApplicative</a> <a id="1353" href="Algebra.Properties.BooleanAlgebra.Expression.html#1300" class="Bound">A</a>

  <a id="Semantics.⟦_⟧" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦_⟧</a> <a id="1362" class="Symbol">:</a> <a id="1364" class="Symbol">∀</a> <a id="1366" class="Symbol">{</a><a id="1367" href="Algebra.Properties.BooleanAlgebra.Expression.html#1367" class="Bound">n</a><a id="1368" class="Symbol">}</a> <a id="1370" class="Symbol">→</a> <a id="1372" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="1377" href="Algebra.Properties.BooleanAlgebra.Expression.html#1367" class="Bound">n</a> <a id="1379" class="Symbol">→</a> <a id="1381" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1385" class="Symbol">(</a><a id="1386" href="Algebra.Properties.BooleanAlgebra.Expression.html#1278" class="Bound">F</a> <a id="1388" href="Algebra.html#13345" class="Field">Carrier</a><a id="1395" class="Symbol">)</a> <a id="1397" href="Algebra.Properties.BooleanAlgebra.Expression.html#1367" class="Bound">n</a> <a id="1399" class="Symbol">→</a> <a id="1401" href="Algebra.Properties.BooleanAlgebra.Expression.html#1278" class="Bound">F</a> <a id="1403" href="Algebra.html#13345" class="Field">Carrier</a>
  <a id="1413" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1415" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.var" class="InductiveConstructor">var</a> <a id="1419" href="Algebra.Properties.BooleanAlgebra.Expression.html#1419" class="Bound">x</a>     <a id="1425" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1427" href="Algebra.Properties.BooleanAlgebra.Expression.html#1427" class="Bound">ρ</a> <a id="1429" class="Symbol">=</a> <a id="1431" href="Data.Vec.html#lookup" class="Function">Vec.lookup</a> <a id="1442" href="Algebra.Properties.BooleanAlgebra.Expression.html#1419" class="Bound">x</a> <a id="1444" href="Algebra.Properties.BooleanAlgebra.Expression.html#1427" class="Bound">ρ</a>
  <a id="1448" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1450" href="Algebra.Properties.BooleanAlgebra.Expression.html#1450" class="Bound">e₁</a> <a id="1453" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="1456" href="Algebra.Properties.BooleanAlgebra.Expression.html#1456" class="Bound">e₂</a>  <a id="1460" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1462" href="Algebra.Properties.BooleanAlgebra.Expression.html#1462" class="Bound">ρ</a> <a id="1464" class="Symbol">=</a> <a id="1466" href="Category.Applicative.Indexed.html#747" class="Field">pure</a> <a id="1471" href="Algebra.html#13411" class="Field Operator">_∨_</a> <a id="1475" href="Category.Applicative.Indexed.html#780" class="Field Operator">⊛</a> <a id="1477" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1479" href="Algebra.Properties.BooleanAlgebra.Expression.html#1450" class="Bound">e₁</a> <a id="1482" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1484" href="Algebra.Properties.BooleanAlgebra.Expression.html#1462" class="Bound">ρ</a> <a id="1486" href="Category.Applicative.Indexed.html#780" class="Field Operator">⊛</a> <a id="1488" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1490" href="Algebra.Properties.BooleanAlgebra.Expression.html#1456" class="Bound">e₂</a> <a id="1493" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1495" href="Algebra.Properties.BooleanAlgebra.Expression.html#1462" class="Bound">ρ</a>
  <a id="1499" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1501" href="Algebra.Properties.BooleanAlgebra.Expression.html#1501" class="Bound">e₁</a> <a id="1504" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="1508" href="Algebra.Properties.BooleanAlgebra.Expression.html#1508" class="Bound">e₂</a> <a id="1511" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1513" href="Algebra.Properties.BooleanAlgebra.Expression.html#1513" class="Bound">ρ</a> <a id="1515" class="Symbol">=</a> <a id="1517" href="Category.Applicative.Indexed.html#747" class="Field">pure</a> <a id="1522" href="Algebra.html#13446" class="Field Operator">_∧_</a> <a id="1526" href="Category.Applicative.Indexed.html#780" class="Field Operator">⊛</a> <a id="1528" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1530" href="Algebra.Properties.BooleanAlgebra.Expression.html#1501" class="Bound">e₁</a> <a id="1533" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1535" href="Algebra.Properties.BooleanAlgebra.Expression.html#1513" class="Bound">ρ</a> <a id="1537" href="Category.Applicative.Indexed.html#780" class="Field Operator">⊛</a> <a id="1539" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1541" href="Algebra.Properties.BooleanAlgebra.Expression.html#1508" class="Bound">e₂</a> <a id="1544" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1546" href="Algebra.Properties.BooleanAlgebra.Expression.html#1513" class="Bound">ρ</a>
  <a id="1550" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1552" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.not" class="InductiveConstructor">not</a> <a id="1556" href="Algebra.Properties.BooleanAlgebra.Expression.html#1556" class="Bound">e</a>     <a id="1562" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1564" href="Algebra.Properties.BooleanAlgebra.Expression.html#1564" class="Bound">ρ</a> <a id="1566" class="Symbol">=</a> <a id="1568" href="Category.Applicative.Indexed.html#747" class="Field">pure</a> <a id="1573" href="Algebra.html#13481" class="Field Operator">¬_</a> <a id="1576" href="Category.Applicative.Indexed.html#780" class="Field Operator">⊛</a> <a id="1578" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1580" href="Algebra.Properties.BooleanAlgebra.Expression.html#1556" class="Bound">e</a> <a id="1582" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1584" href="Algebra.Properties.BooleanAlgebra.Expression.html#1564" class="Bound">ρ</a>
  <a id="1588" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1590" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.top" class="InductiveConstructor">top</a>       <a id="1600" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1602" href="Algebra.Properties.BooleanAlgebra.Expression.html#1602" class="Bound">ρ</a> <a id="1604" class="Symbol">=</a> <a id="1606" href="Category.Applicative.Indexed.html#747" class="Field">pure</a> <a id="1611" href="Algebra.html#13516" class="Field">⊤</a>
  <a id="1615" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1617" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.bot" class="InductiveConstructor">bot</a>       <a id="1627" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1629" href="Algebra.Properties.BooleanAlgebra.Expression.html#1629" class="Bound">ρ</a> <a id="1631" class="Symbol">=</a> <a id="1633" href="Category.Applicative.Indexed.html#747" class="Field">pure</a> <a id="1638" href="Algebra.html#13547" class="Field">⊥</a>

<a id="1641" class="Comment">-- flip Semantics.⟦_⟧ e is natural.</a>

<a id="1678" class="Keyword">module</a> <a id="Naturality" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality" class="Module">Naturality</a>
  <a id="1698" class="Symbol">{</a><a id="1699" href="Algebra.Properties.BooleanAlgebra.Expression.html#1699" class="Bound">F₁</a> <a id="1702" href="Algebra.Properties.BooleanAlgebra.Expression.html#1702" class="Bound">F₂</a> <a id="1705" class="Symbol">:</a> <a id="1707" class="PrimitiveType">Set</a> <a id="1711" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a> <a id="1713" class="Symbol">→</a> <a id="1715" class="PrimitiveType">Set</a> <a id="1719" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a><a id="1720" class="Symbol">}</a>
  <a id="1724" class="Symbol">{</a><a id="1725" href="Algebra.Properties.BooleanAlgebra.Expression.html#1725" class="Bound">A₁</a> <a id="1728" class="Symbol">:</a> <a id="1730" href="Category.Applicative.html#RawApplicative" class="Function">RawApplicative</a> <a id="1745" href="Algebra.Properties.BooleanAlgebra.Expression.html#1699" class="Bound">F₁</a><a id="1747" class="Symbol">}</a>
  <a id="1751" class="Symbol">{</a><a id="1752" href="Algebra.Properties.BooleanAlgebra.Expression.html#1752" class="Bound">A₂</a> <a id="1755" class="Symbol">:</a> <a id="1757" href="Category.Applicative.html#RawApplicative" class="Function">RawApplicative</a> <a id="1772" href="Algebra.Properties.BooleanAlgebra.Expression.html#1702" class="Bound">F₂</a><a id="1774" class="Symbol">}</a>
  <a id="1778" class="Symbol">(</a><a id="1779" href="Algebra.Properties.BooleanAlgebra.Expression.html#1779" class="Bound">f</a> <a id="1781" class="Symbol">:</a> <a id="1783" href="Category.Applicative.Indexed.html#Morphism" class="Record">Applicative.Morphism</a> <a id="1804" href="Algebra.Properties.BooleanAlgebra.Expression.html#1725" class="Bound">A₁</a> <a id="1807" href="Algebra.Properties.BooleanAlgebra.Expression.html#1752" class="Bound">A₂</a><a id="1809" class="Symbol">)</a>
  <a id="1813" class="Keyword">where</a>

  <a id="1822" class="Keyword">open</a> <a id="1827" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning" class="Module">P.≡-Reasoning</a>
  <a id="1843" class="Keyword">open</a> <a id="1848" href="Category.Applicative.Indexed.html#Morphism" class="Module">Applicative.Morphism</a> <a id="1869" href="Algebra.Properties.BooleanAlgebra.Expression.html#1779" class="Bound">f</a>
  <a id="1873" class="Keyword">open</a> <a id="1878" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics" class="Module">Semantics</a> <a id="1888" href="Algebra.Properties.BooleanAlgebra.Expression.html#1725" class="Bound">A₁</a> <a id="1891" class="Keyword">renaming</a> <a id="1900" class="Symbol">(</a>⟦_⟧ <a id="1905" class="Symbol">to</a> ⟦_⟧₁<a id="1912" class="Symbol">)</a>
  <a id="1916" class="Keyword">open</a> <a id="1921" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics" class="Module">Semantics</a> <a id="1931" href="Algebra.Properties.BooleanAlgebra.Expression.html#1752" class="Bound">A₂</a> <a id="1934" class="Keyword">renaming</a> <a id="1943" class="Symbol">(</a>⟦_⟧ <a id="1948" class="Symbol">to</a> ⟦_⟧₂<a id="1955" class="Symbol">)</a>
  <a id="1959" class="Keyword">open</a> <a id="1964" href="Category.Applicative.html#RawApplicative" class="Module">RawApplicative</a> <a id="1979" href="Algebra.Properties.BooleanAlgebra.Expression.html#1725" class="Bound">A₁</a> <a id="1982" class="Keyword">renaming</a> <a id="1991" class="Symbol">(</a>pure <a id="1997" class="Symbol">to</a> pure₁<a id="2005" class="Symbol">;</a> _⊛_ <a id="2011" class="Symbol">to</a> _⊛₁_<a id="2018" class="Symbol">)</a>
  <a id="2022" class="Keyword">open</a> <a id="2027" href="Category.Applicative.html#RawApplicative" class="Module">RawApplicative</a> <a id="2042" href="Algebra.Properties.BooleanAlgebra.Expression.html#1752" class="Bound">A₂</a> <a id="2045" class="Keyword">renaming</a> <a id="2054" class="Symbol">(</a>pure <a id="2060" class="Symbol">to</a> pure₂<a id="2068" class="Symbol">;</a> _⊛_ <a id="2074" class="Symbol">to</a> _⊛₂_<a id="2081" class="Symbol">)</a>

  <a id="Naturality.natural" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="2094" class="Symbol">:</a> <a id="2096" class="Symbol">∀</a> <a id="2098" class="Symbol">{</a><a id="2099" href="Algebra.Properties.BooleanAlgebra.Expression.html#2099" class="Bound">n</a><a id="2100" class="Symbol">}</a> <a id="2102" class="Symbol">(</a><a id="2103" href="Algebra.Properties.BooleanAlgebra.Expression.html#2103" class="Bound">e</a> <a id="2105" class="Symbol">:</a> <a id="2107" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="2112" href="Algebra.Properties.BooleanAlgebra.Expression.html#2099" class="Bound">n</a><a id="2113" class="Symbol">)</a> <a id="2115" class="Symbol">→</a> <a id="2117" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2120" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2122" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2124" href="Algebra.Properties.BooleanAlgebra.Expression.html#2103" class="Bound">e</a> <a id="2126" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="2129" href="Relation.Binary.PropositionalEquality.html#_%E2%89%97_" class="Function Operator">≗</a> <a id="2131" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2133" href="Algebra.Properties.BooleanAlgebra.Expression.html#2103" class="Bound">e</a> <a id="2135" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₂</a> <a id="2138" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2140" href="Data.Vec.html#map" class="Function">Vec.map</a> <a id="2148" href="Category.Applicative.Indexed.html#1726" class="Field">op</a>
  <a id="2153" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="2161" class="Symbol">(</a><a id="2162" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.var" class="InductiveConstructor">var</a> <a id="2166" href="Algebra.Properties.BooleanAlgebra.Expression.html#2166" class="Bound">x</a><a id="2167" class="Symbol">)</a> <a id="2169" href="Algebra.Properties.BooleanAlgebra.Expression.html#2169" class="Bound">ρ</a> <a id="2171" class="Symbol">=</a> <a id="2173" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning.begin_" class="Function Operator">begin</a>
    <a id="2183" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2186" class="Symbol">(</a><a id="2187" href="Data.Vec.html#lookup" class="Function">Vec.lookup</a> <a id="2198" href="Algebra.Properties.BooleanAlgebra.Expression.html#2166" class="Bound">x</a> <a id="2200" href="Algebra.Properties.BooleanAlgebra.Expression.html#2169" class="Bound">ρ</a><a id="2201" class="Symbol">)</a>                                            <a id="2246" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="2249" href="Relation.Binary.PropositionalEquality.Core.html#sym" class="Function">P.sym</a> <a id="2255" href="Function.html#_%24_" class="Function Operator">$</a> <a id="2257" href="Data.Vec.Properties.html#lookup-map" class="Function">VecProp.lookup-map</a> <a id="2276" href="Algebra.Properties.BooleanAlgebra.Expression.html#2166" class="Bound">x</a> <a id="2278" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2281" href="Algebra.Properties.BooleanAlgebra.Expression.html#2169" class="Bound">ρ</a> <a id="2283" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="2289" href="Data.Vec.html#lookup" class="Function">Vec.lookup</a> <a id="2300" href="Algebra.Properties.BooleanAlgebra.Expression.html#2166" class="Bound">x</a> <a id="2302" class="Symbol">(</a><a id="2303" href="Data.Vec.html#map" class="Function">Vec.map</a> <a id="2311" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2314" href="Algebra.Properties.BooleanAlgebra.Expression.html#2169" class="Bound">ρ</a><a id="2315" class="Symbol">)</a>                                    <a id="2352" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%88%8E" class="Function Operator">∎</a>
  <a id="2356" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="2364" class="Symbol">(</a><a id="2365" href="Algebra.Properties.BooleanAlgebra.Expression.html#2365" class="Bound">e₁</a> <a id="2368" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="2371" href="Algebra.Properties.BooleanAlgebra.Expression.html#2371" class="Bound">e₂</a><a id="2373" class="Symbol">)</a> <a id="2375" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a> <a id="2377" class="Symbol">=</a> <a id="2379" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning.begin_" class="Function Operator">begin</a>
    <a id="2389" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2392" class="Symbol">(</a><a id="2393" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="2399" href="Algebra.html#13411" class="Field Operator">_∨_</a> <a id="2403" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₁</a> <a id="2406" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2408" href="Algebra.Properties.BooleanAlgebra.Expression.html#2365" class="Bound">e₁</a> <a id="2411" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="2414" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a> <a id="2416" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₁</a> <a id="2419" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2421" href="Algebra.Properties.BooleanAlgebra.Expression.html#2371" class="Bound">e₂</a> <a id="2424" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="2427" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a><a id="2428" class="Symbol">)</a>                       <a id="2452" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="2455" href="Category.Applicative.Indexed.html#1839" class="Field">op-⊛</a> <a id="2460" class="Symbol">_</a> <a id="2462" class="Symbol">_</a> <a id="2464" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="2470" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2473" class="Symbol">(</a><a id="2474" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="2480" href="Algebra.html#13411" class="Field Operator">_∨_</a> <a id="2484" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₁</a> <a id="2487" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2489" href="Algebra.Properties.BooleanAlgebra.Expression.html#2365" class="Bound">e₁</a> <a id="2492" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="2495" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a><a id="2496" class="Symbol">)</a> <a id="2498" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="2501" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2504" class="Symbol">(</a><a id="2505" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2507" href="Algebra.Properties.BooleanAlgebra.Expression.html#2371" class="Bound">e₂</a> <a id="2510" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="2513" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a><a id="2514" class="Symbol">)</a>                  <a id="2533" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="2536" href="Relation.Binary.PropositionalEquality.html#cong%E2%82%82" class="Function">P.cong₂</a> <a id="2544" href="Category.Applicative.Indexed.html#780" class="Function Operator">_⊛₂_</a> <a id="2549" class="Symbol">(</a><a id="2550" href="Category.Applicative.Indexed.html#1839" class="Field">op-⊛</a> <a id="2555" class="Symbol">_</a> <a id="2557" class="Symbol">_)</a> <a id="2560" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a> <a id="2567" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="2573" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2576" class="Symbol">(</a><a id="2577" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="2583" href="Algebra.html#13411" class="Field Operator">_∨_</a><a id="2586" class="Symbol">)</a> <a id="2588" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="2591" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2594" class="Symbol">(</a><a id="2595" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2597" href="Algebra.Properties.BooleanAlgebra.Expression.html#2365" class="Bound">e₁</a> <a id="2600" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="2603" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a><a id="2604" class="Symbol">)</a> <a id="2606" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="2609" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2612" class="Symbol">(</a><a id="2613" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2615" href="Algebra.Properties.BooleanAlgebra.Expression.html#2371" class="Bound">e₂</a> <a id="2618" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="2621" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a><a id="2622" class="Symbol">)</a>             <a id="2636" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="2639" href="Relation.Binary.PropositionalEquality.html#cong%E2%82%82" class="Function">P.cong₂</a> <a id="2647" href="Category.Applicative.Indexed.html#780" class="Function Operator">_⊛₂_</a> <a id="2652" class="Symbol">(</a><a id="2653" href="Relation.Binary.PropositionalEquality.html#cong%E2%82%82" class="Function">P.cong₂</a> <a id="2661" href="Category.Applicative.Indexed.html#780" class="Function Operator">_⊛₂_</a> <a id="2666" class="Symbol">(</a><a id="2667" href="Category.Applicative.Indexed.html#1772" class="Field">op-pure</a> <a id="2675" class="Symbol">_)</a> <a id="2678" class="Symbol">(</a><a id="2679" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="2687" href="Algebra.Properties.BooleanAlgebra.Expression.html#2365" class="Bound">e₁</a> <a id="2690" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a><a id="2691" class="Symbol">))</a>
                                                                                   <a id="2777" class="Symbol">(</a><a id="2778" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="2786" href="Algebra.Properties.BooleanAlgebra.Expression.html#2371" class="Bound">e₂</a> <a id="2789" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a><a id="2790" class="Symbol">)</a> <a id="2792" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="2798" href="Category.Applicative.Indexed.html#747" class="Function">pure₂</a> <a id="2804" href="Algebra.html#13411" class="Field Operator">_∨_</a> <a id="2808" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="2811" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2813" href="Algebra.Properties.BooleanAlgebra.Expression.html#2365" class="Bound">e₁</a> <a id="2816" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₂</a> <a id="2819" class="Symbol">(</a><a id="2820" href="Data.Vec.html#map" class="Function">Vec.map</a> <a id="2828" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2831" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a><a id="2832" class="Symbol">)</a> <a id="2834" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="2837" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2839" href="Algebra.Properties.BooleanAlgebra.Expression.html#2371" class="Bound">e₂</a> <a id="2842" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₂</a> <a id="2845" class="Symbol">(</a><a id="2846" href="Data.Vec.html#map" class="Function">Vec.map</a> <a id="2854" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2857" href="Algebra.Properties.BooleanAlgebra.Expression.html#2375" class="Bound">ρ</a><a id="2858" class="Symbol">)</a>  <a id="2861" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%88%8E" class="Function Operator">∎</a>
  <a id="2865" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="2873" class="Symbol">(</a><a id="2874" href="Algebra.Properties.BooleanAlgebra.Expression.html#2874" class="Bound">e₁</a> <a id="2877" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="2881" href="Algebra.Properties.BooleanAlgebra.Expression.html#2881" class="Bound">e₂</a><a id="2883" class="Symbol">)</a> <a id="2885" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a> <a id="2887" class="Symbol">=</a> <a id="2889" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning.begin_" class="Function Operator">begin</a>
    <a id="2899" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2902" class="Symbol">(</a><a id="2903" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="2909" href="Algebra.html#13446" class="Field Operator">_∧_</a> <a id="2913" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₁</a> <a id="2916" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2918" href="Algebra.Properties.BooleanAlgebra.Expression.html#2874" class="Bound">e₁</a> <a id="2921" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="2924" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a> <a id="2926" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₁</a> <a id="2929" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2931" href="Algebra.Properties.BooleanAlgebra.Expression.html#2881" class="Bound">e₂</a> <a id="2934" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="2937" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a><a id="2938" class="Symbol">)</a>                       <a id="2962" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="2965" href="Category.Applicative.Indexed.html#1839" class="Field">op-⊛</a> <a id="2970" class="Symbol">_</a> <a id="2972" class="Symbol">_</a> <a id="2974" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="2980" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="2983" class="Symbol">(</a><a id="2984" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="2990" href="Algebra.html#13446" class="Field Operator">_∧_</a> <a id="2994" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₁</a> <a id="2997" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="2999" href="Algebra.Properties.BooleanAlgebra.Expression.html#2874" class="Bound">e₁</a> <a id="3002" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="3005" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a><a id="3006" class="Symbol">)</a> <a id="3008" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="3011" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3014" class="Symbol">(</a><a id="3015" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="3017" href="Algebra.Properties.BooleanAlgebra.Expression.html#2881" class="Bound">e₂</a> <a id="3020" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="3023" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a><a id="3024" class="Symbol">)</a>                  <a id="3043" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="3046" href="Relation.Binary.PropositionalEquality.html#cong%E2%82%82" class="Function">P.cong₂</a> <a id="3054" href="Category.Applicative.Indexed.html#780" class="Function Operator">_⊛₂_</a> <a id="3059" class="Symbol">(</a><a id="3060" href="Category.Applicative.Indexed.html#1839" class="Field">op-⊛</a> <a id="3065" class="Symbol">_</a> <a id="3067" class="Symbol">_)</a> <a id="3070" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a> <a id="3077" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="3083" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3086" class="Symbol">(</a><a id="3087" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="3093" href="Algebra.html#13446" class="Field Operator">_∧_</a><a id="3096" class="Symbol">)</a> <a id="3098" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="3101" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3104" class="Symbol">(</a><a id="3105" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="3107" href="Algebra.Properties.BooleanAlgebra.Expression.html#2874" class="Bound">e₁</a> <a id="3110" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="3113" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a><a id="3114" class="Symbol">)</a> <a id="3116" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="3119" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3122" class="Symbol">(</a><a id="3123" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="3125" href="Algebra.Properties.BooleanAlgebra.Expression.html#2881" class="Bound">e₂</a> <a id="3128" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="3131" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a><a id="3132" class="Symbol">)</a>             <a id="3146" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="3149" href="Relation.Binary.PropositionalEquality.html#cong%E2%82%82" class="Function">P.cong₂</a> <a id="3157" href="Category.Applicative.Indexed.html#780" class="Function Operator">_⊛₂_</a> <a id="3162" class="Symbol">(</a><a id="3163" href="Relation.Binary.PropositionalEquality.html#cong%E2%82%82" class="Function">P.cong₂</a> <a id="3171" href="Category.Applicative.Indexed.html#780" class="Function Operator">_⊛₂_</a> <a id="3176" class="Symbol">(</a><a id="3177" href="Category.Applicative.Indexed.html#1772" class="Field">op-pure</a> <a id="3185" class="Symbol">_)</a> <a id="3188" class="Symbol">(</a><a id="3189" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="3197" href="Algebra.Properties.BooleanAlgebra.Expression.html#2874" class="Bound">e₁</a> <a id="3200" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a><a id="3201" class="Symbol">))</a>
                                                                                   <a id="3287" class="Symbol">(</a><a id="3288" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="3296" href="Algebra.Properties.BooleanAlgebra.Expression.html#2881" class="Bound">e₂</a> <a id="3299" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a><a id="3300" class="Symbol">)</a> <a id="3302" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="3308" href="Category.Applicative.Indexed.html#747" class="Function">pure₂</a> <a id="3314" href="Algebra.html#13446" class="Field Operator">_∧_</a> <a id="3318" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="3321" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="3323" href="Algebra.Properties.BooleanAlgebra.Expression.html#2874" class="Bound">e₁</a> <a id="3326" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₂</a> <a id="3329" class="Symbol">(</a><a id="3330" href="Data.Vec.html#map" class="Function">Vec.map</a> <a id="3338" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3341" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a><a id="3342" class="Symbol">)</a> <a id="3344" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="3347" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="3349" href="Algebra.Properties.BooleanAlgebra.Expression.html#2881" class="Bound">e₂</a> <a id="3352" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₂</a> <a id="3355" class="Symbol">(</a><a id="3356" href="Data.Vec.html#map" class="Function">Vec.map</a> <a id="3364" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3367" href="Algebra.Properties.BooleanAlgebra.Expression.html#2885" class="Bound">ρ</a><a id="3368" class="Symbol">)</a>  <a id="3371" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%88%8E" class="Function Operator">∎</a>
  <a id="3375" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="3383" class="Symbol">(</a><a id="3384" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.not" class="InductiveConstructor">not</a> <a id="3388" href="Algebra.Properties.BooleanAlgebra.Expression.html#3388" class="Bound">e</a><a id="3389" class="Symbol">)</a> <a id="3391" href="Algebra.Properties.BooleanAlgebra.Expression.html#3391" class="Bound">ρ</a> <a id="3393" class="Symbol">=</a> <a id="3395" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning.begin_" class="Function Operator">begin</a>
    <a id="3405" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3408" class="Symbol">(</a><a id="3409" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="3415" href="Algebra.html#13481" class="Field Operator">¬_</a> <a id="3418" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₁</a> <a id="3421" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="3423" href="Algebra.Properties.BooleanAlgebra.Expression.html#3388" class="Bound">e</a> <a id="3425" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="3428" href="Algebra.Properties.BooleanAlgebra.Expression.html#3391" class="Bound">ρ</a><a id="3429" class="Symbol">)</a>                                      <a id="3468" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="3471" href="Category.Applicative.Indexed.html#1839" class="Field">op-⊛</a> <a id="3476" class="Symbol">_</a> <a id="3478" class="Symbol">_</a> <a id="3480" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="3486" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3489" class="Symbol">(</a><a id="3490" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="3496" href="Algebra.html#13481" class="Field Operator">¬_</a><a id="3498" class="Symbol">)</a> <a id="3500" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="3503" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3506" class="Symbol">(</a><a id="3507" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="3509" href="Algebra.Properties.BooleanAlgebra.Expression.html#3388" class="Bound">e</a> <a id="3511" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₁</a> <a id="3514" href="Algebra.Properties.BooleanAlgebra.Expression.html#3391" class="Bound">ρ</a><a id="3515" class="Symbol">)</a>                                 <a id="3549" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="3552" href="Relation.Binary.PropositionalEquality.html#cong%E2%82%82" class="Function">P.cong₂</a> <a id="3560" href="Category.Applicative.Indexed.html#780" class="Function Operator">_⊛₂_</a> <a id="3565" class="Symbol">(</a><a id="3566" href="Category.Applicative.Indexed.html#1772" class="Field">op-pure</a> <a id="3574" class="Symbol">_)</a> <a id="3577" class="Symbol">(</a><a id="3578" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="3586" href="Algebra.Properties.BooleanAlgebra.Expression.html#3388" class="Bound">e</a> <a id="3588" href="Algebra.Properties.BooleanAlgebra.Expression.html#3391" class="Bound">ρ</a><a id="3589" class="Symbol">)</a> <a id="3591" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="3597" href="Category.Applicative.Indexed.html#747" class="Function">pure₂</a> <a id="3603" href="Algebra.html#13481" class="Field Operator">¬_</a> <a id="3606" href="Category.Applicative.Indexed.html#780" class="Function Operator">⊛₂</a> <a id="3609" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟦</a> <a id="3611" href="Algebra.Properties.BooleanAlgebra.Expression.html#3388" class="Bound">e</a> <a id="3613" href="Algebra.Properties.BooleanAlgebra.Expression.html#1358" class="Function Operator">⟧₂</a> <a id="3616" class="Symbol">(</a><a id="3617" href="Data.Vec.html#map" class="Function">Vec.map</a> <a id="3625" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3628" href="Algebra.Properties.BooleanAlgebra.Expression.html#3391" class="Bound">ρ</a><a id="3629" class="Symbol">)</a>                              <a id="3660" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%88%8E" class="Function Operator">∎</a>
  <a id="3664" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="3672" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.top" class="InductiveConstructor">top</a> <a id="3676" href="Algebra.Properties.BooleanAlgebra.Expression.html#3676" class="Bound">ρ</a> <a id="3678" class="Symbol">=</a> <a id="3680" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning.begin_" class="Function Operator">begin</a>
    <a id="3690" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3693" class="Symbol">(</a><a id="3694" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="3700" href="Algebra.html#13516" class="Field">⊤</a><a id="3701" class="Symbol">)</a>                                                   <a id="3753" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="3756" href="Category.Applicative.Indexed.html#1772" class="Field">op-pure</a> <a id="3764" class="Symbol">_</a> <a id="3766" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="3772" href="Category.Applicative.Indexed.html#747" class="Function">pure₂</a> <a id="3778" href="Algebra.html#13516" class="Field">⊤</a>                                                        <a id="3835" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%88%8E" class="Function Operator">∎</a>
  <a id="3839" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">natural</a> <a id="3847" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.bot" class="InductiveConstructor">bot</a> <a id="3851" href="Algebra.Properties.BooleanAlgebra.Expression.html#3851" class="Bound">ρ</a> <a id="3853" class="Symbol">=</a> <a id="3855" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning.begin_" class="Function Operator">begin</a>
    <a id="3865" href="Category.Applicative.Indexed.html#1726" class="Field">op</a> <a id="3868" class="Symbol">(</a><a id="3869" href="Category.Applicative.Indexed.html#747" class="Function">pure₁</a> <a id="3875" href="Algebra.html#13547" class="Field">⊥</a><a id="3876" class="Symbol">)</a>                                                   <a id="3928" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="3931" href="Category.Applicative.Indexed.html#1772" class="Field">op-pure</a> <a id="3939" class="Symbol">_</a> <a id="3941" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="3947" href="Category.Applicative.Indexed.html#747" class="Function">pure₂</a> <a id="3953" href="Algebra.html#13547" class="Field">⊥</a>                                                        <a id="4010" href="Relation.Binary.PropositionalEquality.html#%E2%89%A1-Reasoning._%E2%88%8E" class="Function Operator">∎</a>

<a id="4013" class="Comment">-- An example of how naturality can be used: Any boolean algebra can</a>
<a id="4082" class="Comment">-- be lifted, in a pointwise manner, to vectors of carrier elements.</a>

<a id="lift" href="Algebra.Properties.BooleanAlgebra.Expression.html#lift" class="Function">lift</a> <a id="4157" class="Symbol">:</a> <a id="4159" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="4161" class="Symbol">→</a> <a id="4163" href="Algebra.html#BooleanAlgebra" class="Record">BooleanAlgebra</a> <a id="4178" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a> <a id="4180" href="Algebra.Properties.BooleanAlgebra.Expression.html#287" class="Bound">b</a>
<a id="4182" href="Algebra.Properties.BooleanAlgebra.Expression.html#lift" class="Function">lift</a> <a id="4187" href="Algebra.Properties.BooleanAlgebra.Expression.html#4187" class="Bound">n</a> <a id="4189" class="Symbol">=</a> <a id="4191" class="Keyword">record</a>
  <a id="4200" class="Symbol">{</a> <a id="4202" class="Field">Carrier</a>          <a id="4219" class="Symbol">=</a> <a id="4221" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="4225" href="Algebra.html#13345" class="Field">Carrier</a> <a id="4233" href="Algebra.Properties.BooleanAlgebra.Expression.html#4187" class="Bound">n</a>
  <a id="4237" class="Symbol">;</a> <a id="4239" class="Field Operator">_≈_</a>              <a id="4256" class="Symbol">=</a> <a id="4258" href="Relation.Binary.Vec.Pointwise.html#Pointwise" class="Record">Pointwise</a> <a id="4268" href="Algebra.html#13374" class="Field Operator">_≈_</a>
  <a id="4274" class="Symbol">;</a> <a id="4276" class="Field Operator">_∨_</a>              <a id="4293" class="Symbol">=</a> <a id="4295" href="Category.Applicative.Indexed.html#1309" class="Function">zipWith</a> <a id="4303" href="Algebra.html#13411" class="Field Operator">_∨_</a>
  <a id="4309" class="Symbol">;</a> <a id="4311" class="Field Operator">_∧_</a>              <a id="4328" class="Symbol">=</a> <a id="4330" href="Category.Applicative.Indexed.html#1309" class="Function">zipWith</a> <a id="4338" href="Algebra.html#13446" class="Field Operator">_∧_</a>
  <a id="4344" class="Symbol">;</a> <a id="4346" class="Field Operator">¬_</a>               <a id="4363" class="Symbol">=</a> <a id="4365" href="Category.Functor.html#475" class="Function">map</a> <a id="4369" href="Algebra.html#13481" class="Field Operator">¬_</a>
  <a id="4374" class="Symbol">;</a> <a id="4376" class="Field">⊤</a>                <a id="4393" class="Symbol">=</a> <a id="4395" href="Category.Applicative.Indexed.html#747" class="Function">pure</a> <a id="4400" href="Algebra.html#13516" class="Field">⊤</a>
  <a id="4404" class="Symbol">;</a> <a id="4406" class="Field">⊥</a>                <a id="4423" class="Symbol">=</a> <a id="4425" href="Category.Applicative.Indexed.html#747" class="Function">pure</a> <a id="4430" href="Algebra.html#13547" class="Field">⊥</a>
  <a id="4434" class="Symbol">;</a> <a id="4436" class="Field">isBooleanAlgebra</a> <a id="4453" class="Symbol">=</a> <a id="4455" class="Keyword">record</a>
    <a id="4466" class="Symbol">{</a> <a id="4468" class="Field">isDistributiveLattice</a> <a id="4490" class="Symbol">=</a> <a id="4492" class="Keyword">record</a>
      <a id="4505" class="Symbol">{</a> <a id="4507" class="Field">isLattice</a> <a id="4517" class="Symbol">=</a> <a id="4519" class="Keyword">record</a>
        <a id="4534" class="Symbol">{</a> <a id="4536" class="Field">isEquivalence</a> <a id="4550" class="Symbol">=</a> <a id="4552" href="Relation.Binary.Vec.Pointwise.html#isEquivalence" class="Function">PW.isEquivalence</a> <a id="4569" href="Algebra.Structures.html#12979" class="Function">isEquivalence</a>
        <a id="4591" class="Symbol">;</a> <a id="4593" class="Field">∨-comm</a>        <a id="4607" class="Symbol">=</a> <a id="4609" class="Symbol">λ</a> <a id="4611" href="Algebra.Properties.BooleanAlgebra.Expression.html#4611" class="Bound">_</a> <a id="4613" href="Algebra.Properties.BooleanAlgebra.Expression.html#4613" class="Bound">_</a> <a id="4615" class="Symbol">→</a> <a id="4617" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="4621" class="Symbol">λ</a> <a id="4623" href="Algebra.Properties.BooleanAlgebra.Expression.html#4623" class="Bound">i</a> <a id="4625" class="Symbol">→</a>
                            <a id="4655" href="Relation.Binary.Reflection.html#2382" class="Function">solve</a> <a id="4661" href="Algebra.Properties.BooleanAlgebra.Expression.html#4623" class="Bound">i</a> <a id="4663" class="Number">2</a> <a id="4665" class="Symbol">(λ</a> <a id="4668" href="Algebra.Properties.BooleanAlgebra.Expression.html#4668" class="Bound">x</a> <a id="4670" href="Algebra.Properties.BooleanAlgebra.Expression.html#4670" class="Bound">y</a> <a id="4672" class="Symbol">→</a> <a id="4674" href="Algebra.Properties.BooleanAlgebra.Expression.html#4668" class="Bound">x</a> <a id="4676" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="4679" href="Algebra.Properties.BooleanAlgebra.Expression.html#4670" class="Bound">y</a> <a id="4681" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4683" href="Algebra.Properties.BooleanAlgebra.Expression.html#4670" class="Bound">y</a> <a id="4685" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="4688" href="Algebra.Properties.BooleanAlgebra.Expression.html#4668" class="Bound">x</a><a id="4689" class="Symbol">)</a>
                                  <a id="4725" class="Symbol">(</a><a id="4726" href="Algebra.Structures.html#13015" class="Function">∨-comm</a> <a id="4733" class="Symbol">_</a> <a id="4735" class="Symbol">_)</a> <a id="4738" class="Symbol">_</a> <a id="4740" class="Symbol">_</a>
        <a id="4750" class="Symbol">;</a> <a id="4752" class="Field">∨-assoc</a>       <a id="4766" class="Symbol">=</a> <a id="4768" class="Symbol">λ</a> <a id="4770" href="Algebra.Properties.BooleanAlgebra.Expression.html#4770" class="Bound">_</a> <a id="4772" href="Algebra.Properties.BooleanAlgebra.Expression.html#4772" class="Bound">_</a> <a id="4774" href="Algebra.Properties.BooleanAlgebra.Expression.html#4774" class="Bound">_</a> <a id="4776" class="Symbol">→</a> <a id="4778" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="4782" class="Symbol">λ</a> <a id="4784" href="Algebra.Properties.BooleanAlgebra.Expression.html#4784" class="Bound">i</a> <a id="4786" class="Symbol">→</a>
                            <a id="4816" href="Relation.Binary.Reflection.html#2382" class="Function">solve</a> <a id="4822" href="Algebra.Properties.BooleanAlgebra.Expression.html#4784" class="Bound">i</a> <a id="4824" class="Number">3</a>
                              <a id="4856" class="Symbol">(λ</a> <a id="4859" href="Algebra.Properties.BooleanAlgebra.Expression.html#4859" class="Bound">x</a> <a id="4861" href="Algebra.Properties.BooleanAlgebra.Expression.html#4861" class="Bound">y</a> <a id="4863" href="Algebra.Properties.BooleanAlgebra.Expression.html#4863" class="Bound">z</a> <a id="4865" class="Symbol">→</a> <a id="4867" class="Symbol">(</a><a id="4868" href="Algebra.Properties.BooleanAlgebra.Expression.html#4859" class="Bound">x</a> <a id="4870" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="4873" href="Algebra.Properties.BooleanAlgebra.Expression.html#4861" class="Bound">y</a><a id="4874" class="Symbol">)</a> <a id="4876" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="4879" href="Algebra.Properties.BooleanAlgebra.Expression.html#4863" class="Bound">z</a> <a id="4881" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4883" href="Algebra.Properties.BooleanAlgebra.Expression.html#4859" class="Bound">x</a> <a id="4885" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="4888" class="Symbol">(</a><a id="4889" href="Algebra.Properties.BooleanAlgebra.Expression.html#4861" class="Bound">y</a> <a id="4891" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="4894" href="Algebra.Properties.BooleanAlgebra.Expression.html#4863" class="Bound">z</a><a id="4895" class="Symbol">))</a>
                              <a id="4928" class="Symbol">(</a><a id="4929" href="Algebra.Structures.html#13049" class="Function">∨-assoc</a> <a id="4937" class="Symbol">_</a> <a id="4939" class="Symbol">_</a> <a id="4941" class="Symbol">_)</a> <a id="4944" class="Symbol">_</a> <a id="4946" class="Symbol">_</a> <a id="4948" class="Symbol">_</a>
        <a id="4958" class="Symbol">;</a> <a id="4960" class="Field">∨-cong</a>        <a id="4974" class="Symbol">=</a> <a id="4976" class="Symbol">λ</a> <a id="4978" href="Algebra.Properties.BooleanAlgebra.Expression.html#4978" class="Bound">xs≈us</a> <a id="4984" href="Algebra.Properties.BooleanAlgebra.Expression.html#4984" class="Bound">ys≈vs</a> <a id="4990" class="Symbol">→</a> <a id="4992" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="4996" class="Symbol">λ</a> <a id="4998" href="Algebra.Properties.BooleanAlgebra.Expression.html#4998" class="Bound">i</a> <a id="5000" class="Symbol">→</a>
                            <a id="5030" href="Relation.Binary.Reflection.html#2984" class="Function">solve₁</a> <a id="5037" href="Algebra.Properties.BooleanAlgebra.Expression.html#4998" class="Bound">i</a> <a id="5039" class="Number">4</a> <a id="5041" class="Symbol">(λ</a> <a id="5044" href="Algebra.Properties.BooleanAlgebra.Expression.html#5044" class="Bound">x</a> <a id="5046" href="Algebra.Properties.BooleanAlgebra.Expression.html#5046" class="Bound">y</a> <a id="5048" href="Algebra.Properties.BooleanAlgebra.Expression.html#5048" class="Bound">u</a> <a id="5050" href="Algebra.Properties.BooleanAlgebra.Expression.html#5050" class="Bound">v</a> <a id="5052" class="Symbol">→</a> <a id="5054" href="Algebra.Properties.BooleanAlgebra.Expression.html#5044" class="Bound">x</a> <a id="5056" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="5059" href="Algebra.Properties.BooleanAlgebra.Expression.html#5046" class="Bound">y</a> <a id="5061" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5063" href="Algebra.Properties.BooleanAlgebra.Expression.html#5048" class="Bound">u</a> <a id="5065" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="5068" href="Algebra.Properties.BooleanAlgebra.Expression.html#5050" class="Bound">v</a><a id="5069" class="Symbol">)</a>
                                   <a id="5106" class="Symbol">_</a> <a id="5108" class="Symbol">_</a> <a id="5110" class="Symbol">_</a> <a id="5112" class="Symbol">_</a>
                                   <a id="5149" class="Symbol">(</a><a id="5150" href="Algebra.Structures.html#13083" class="Function">∨-cong</a> <a id="5157" class="Symbol">(</a><a id="5158" href="Relation.Binary.Vec.Pointwise.html#Pointwise.app" class="Field">Pointwise.app</a> <a id="5172" href="Algebra.Properties.BooleanAlgebra.Expression.html#4978" class="Bound">xs≈us</a> <a id="5178" href="Algebra.Properties.BooleanAlgebra.Expression.html#4998" class="Bound">i</a><a id="5179" class="Symbol">)</a>
                                           <a id="5224" class="Symbol">(</a><a id="5225" href="Relation.Binary.Vec.Pointwise.html#Pointwise.app" class="Field">Pointwise.app</a> <a id="5239" href="Algebra.Properties.BooleanAlgebra.Expression.html#4984" class="Bound">ys≈vs</a> <a id="5245" href="Algebra.Properties.BooleanAlgebra.Expression.html#4998" class="Bound">i</a><a id="5246" class="Symbol">))</a>
        <a id="5257" class="Symbol">;</a> <a id="5259" class="Field">∧-comm</a>        <a id="5273" class="Symbol">=</a> <a id="5275" class="Symbol">λ</a> <a id="5277" href="Algebra.Properties.BooleanAlgebra.Expression.html#5277" class="Bound">_</a> <a id="5279" href="Algebra.Properties.BooleanAlgebra.Expression.html#5279" class="Bound">_</a> <a id="5281" class="Symbol">→</a> <a id="5283" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="5287" class="Symbol">λ</a> <a id="5289" href="Algebra.Properties.BooleanAlgebra.Expression.html#5289" class="Bound">i</a> <a id="5291" class="Symbol">→</a>
                            <a id="5321" href="Relation.Binary.Reflection.html#2382" class="Function">solve</a> <a id="5327" href="Algebra.Properties.BooleanAlgebra.Expression.html#5289" class="Bound">i</a> <a id="5329" class="Number">2</a> <a id="5331" class="Symbol">(λ</a> <a id="5334" href="Algebra.Properties.BooleanAlgebra.Expression.html#5334" class="Bound">x</a> <a id="5336" href="Algebra.Properties.BooleanAlgebra.Expression.html#5336" class="Bound">y</a> <a id="5338" class="Symbol">→</a> <a id="5340" href="Algebra.Properties.BooleanAlgebra.Expression.html#5334" class="Bound">x</a> <a id="5342" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="5346" href="Algebra.Properties.BooleanAlgebra.Expression.html#5336" class="Bound">y</a> <a id="5348" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5350" href="Algebra.Properties.BooleanAlgebra.Expression.html#5336" class="Bound">y</a> <a id="5352" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="5356" href="Algebra.Properties.BooleanAlgebra.Expression.html#5334" class="Bound">x</a><a id="5357" class="Symbol">)</a>
                                  <a id="5393" class="Symbol">(</a><a id="5394" href="Algebra.Structures.html#13126" class="Function">∧-comm</a> <a id="5401" class="Symbol">_</a> <a id="5403" class="Symbol">_)</a> <a id="5406" class="Symbol">_</a> <a id="5408" class="Symbol">_</a>
        <a id="5418" class="Symbol">;</a> <a id="5420" class="Field">∧-assoc</a>       <a id="5434" class="Symbol">=</a> <a id="5436" class="Symbol">λ</a> <a id="5438" href="Algebra.Properties.BooleanAlgebra.Expression.html#5438" class="Bound">_</a> <a id="5440" href="Algebra.Properties.BooleanAlgebra.Expression.html#5440" class="Bound">_</a> <a id="5442" href="Algebra.Properties.BooleanAlgebra.Expression.html#5442" class="Bound">_</a> <a id="5444" class="Symbol">→</a> <a id="5446" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="5450" class="Symbol">λ</a> <a id="5452" href="Algebra.Properties.BooleanAlgebra.Expression.html#5452" class="Bound">i</a> <a id="5454" class="Symbol">→</a>
                            <a id="5484" href="Relation.Binary.Reflection.html#2382" class="Function">solve</a> <a id="5490" href="Algebra.Properties.BooleanAlgebra.Expression.html#5452" class="Bound">i</a> <a id="5492" class="Number">3</a>
                              <a id="5524" class="Symbol">(λ</a> <a id="5527" href="Algebra.Properties.BooleanAlgebra.Expression.html#5527" class="Bound">x</a> <a id="5529" href="Algebra.Properties.BooleanAlgebra.Expression.html#5529" class="Bound">y</a> <a id="5531" href="Algebra.Properties.BooleanAlgebra.Expression.html#5531" class="Bound">z</a> <a id="5533" class="Symbol">→</a> <a id="5535" class="Symbol">(</a><a id="5536" href="Algebra.Properties.BooleanAlgebra.Expression.html#5527" class="Bound">x</a> <a id="5538" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="5542" href="Algebra.Properties.BooleanAlgebra.Expression.html#5529" class="Bound">y</a><a id="5543" class="Symbol">)</a> <a id="5545" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="5549" href="Algebra.Properties.BooleanAlgebra.Expression.html#5531" class="Bound">z</a> <a id="5551" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a>
                                         <a id="5594" href="Algebra.Properties.BooleanAlgebra.Expression.html#5527" class="Bound">x</a> <a id="5596" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="5600" class="Symbol">(</a><a id="5601" href="Algebra.Properties.BooleanAlgebra.Expression.html#5529" class="Bound">y</a> <a id="5603" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="5607" href="Algebra.Properties.BooleanAlgebra.Expression.html#5531" class="Bound">z</a><a id="5608" class="Symbol">))</a>
                              <a id="5641" class="Symbol">(</a><a id="5642" href="Algebra.Structures.html#13160" class="Function">∧-assoc</a> <a id="5650" class="Symbol">_</a> <a id="5652" class="Symbol">_</a> <a id="5654" class="Symbol">_)</a> <a id="5657" class="Symbol">_</a> <a id="5659" class="Symbol">_</a> <a id="5661" class="Symbol">_</a>
        <a id="5671" class="Symbol">;</a> <a id="5673" class="Field">∧-cong</a>        <a id="5687" class="Symbol">=</a> <a id="5689" class="Symbol">λ</a> <a id="5691" href="Algebra.Properties.BooleanAlgebra.Expression.html#5691" class="Bound">xs≈ys</a> <a id="5697" href="Algebra.Properties.BooleanAlgebra.Expression.html#5697" class="Bound">us≈vs</a> <a id="5703" class="Symbol">→</a> <a id="5705" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="5709" class="Symbol">λ</a> <a id="5711" href="Algebra.Properties.BooleanAlgebra.Expression.html#5711" class="Bound">i</a> <a id="5713" class="Symbol">→</a>
                            <a id="5743" href="Relation.Binary.Reflection.html#2984" class="Function">solve₁</a> <a id="5750" href="Algebra.Properties.BooleanAlgebra.Expression.html#5711" class="Bound">i</a> <a id="5752" class="Number">4</a> <a id="5754" class="Symbol">(λ</a> <a id="5757" href="Algebra.Properties.BooleanAlgebra.Expression.html#5757" class="Bound">x</a> <a id="5759" href="Algebra.Properties.BooleanAlgebra.Expression.html#5759" class="Bound">y</a> <a id="5761" href="Algebra.Properties.BooleanAlgebra.Expression.html#5761" class="Bound">u</a> <a id="5763" href="Algebra.Properties.BooleanAlgebra.Expression.html#5763" class="Bound">v</a> <a id="5765" class="Symbol">→</a> <a id="5767" href="Algebra.Properties.BooleanAlgebra.Expression.html#5757" class="Bound">x</a> <a id="5769" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="5773" href="Algebra.Properties.BooleanAlgebra.Expression.html#5759" class="Bound">y</a> <a id="5775" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="5777" href="Algebra.Properties.BooleanAlgebra.Expression.html#5761" class="Bound">u</a> <a id="5779" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="5783" href="Algebra.Properties.BooleanAlgebra.Expression.html#5763" class="Bound">v</a><a id="5784" class="Symbol">)</a>
                                   <a id="5821" class="Symbol">_</a> <a id="5823" class="Symbol">_</a> <a id="5825" class="Symbol">_</a> <a id="5827" class="Symbol">_</a>
                                   <a id="5864" class="Symbol">(</a><a id="5865" href="Algebra.Structures.html#13194" class="Function">∧-cong</a> <a id="5872" class="Symbol">(</a><a id="5873" href="Relation.Binary.Vec.Pointwise.html#Pointwise.app" class="Field">Pointwise.app</a> <a id="5887" href="Algebra.Properties.BooleanAlgebra.Expression.html#5691" class="Bound">xs≈ys</a> <a id="5893" href="Algebra.Properties.BooleanAlgebra.Expression.html#5711" class="Bound">i</a><a id="5894" class="Symbol">)</a>
                                           <a id="5939" class="Symbol">(</a><a id="5940" href="Relation.Binary.Vec.Pointwise.html#Pointwise.app" class="Field">Pointwise.app</a> <a id="5954" href="Algebra.Properties.BooleanAlgebra.Expression.html#5697" class="Bound">us≈vs</a> <a id="5960" href="Algebra.Properties.BooleanAlgebra.Expression.html#5711" class="Bound">i</a><a id="5961" class="Symbol">))</a>
        <a id="5972" class="Symbol">;</a> <a id="5974" class="Field">absorptive</a>    <a id="5988" class="Symbol">=</a> <a id="5990" class="Symbol">(λ</a> <a id="5993" href="Algebra.Properties.BooleanAlgebra.Expression.html#5993" class="Bound">_</a> <a id="5995" href="Algebra.Properties.BooleanAlgebra.Expression.html#5995" class="Bound">_</a> <a id="5997" class="Symbol">→</a> <a id="5999" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="6003" class="Symbol">λ</a> <a id="6005" href="Algebra.Properties.BooleanAlgebra.Expression.html#6005" class="Bound">i</a> <a id="6007" class="Symbol">→</a>
                             <a id="6038" href="Relation.Binary.Reflection.html#2382" class="Function">solve</a> <a id="6044" href="Algebra.Properties.BooleanAlgebra.Expression.html#6005" class="Bound">i</a> <a id="6046" class="Number">2</a> <a id="6048" class="Symbol">(λ</a> <a id="6051" href="Algebra.Properties.BooleanAlgebra.Expression.html#6051" class="Bound">x</a> <a id="6053" href="Algebra.Properties.BooleanAlgebra.Expression.html#6053" class="Bound">y</a> <a id="6055" class="Symbol">→</a> <a id="6057" href="Algebra.Properties.BooleanAlgebra.Expression.html#6051" class="Bound">x</a> <a id="6059" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="6062" class="Symbol">(</a><a id="6063" href="Algebra.Properties.BooleanAlgebra.Expression.html#6051" class="Bound">x</a> <a id="6065" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="6069" href="Algebra.Properties.BooleanAlgebra.Expression.html#6053" class="Bound">y</a><a id="6070" class="Symbol">)</a> <a id="6072" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6074" href="Algebra.Properties.BooleanAlgebra.Expression.html#6051" class="Bound">x</a><a id="6075" class="Symbol">)</a>
                                   <a id="6112" class="Symbol">(</a><a id="6113" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="6119" href="Algebra.Structures.html#13237" class="Function">absorptive</a> <a id="6130" class="Symbol">_</a> <a id="6132" class="Symbol">_)</a> <a id="6135" class="Symbol">_</a> <a id="6137" class="Symbol">_)</a> <a id="6140" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a>
                          <a id="6168" class="Symbol">(λ</a> <a id="6171" href="Algebra.Properties.BooleanAlgebra.Expression.html#6171" class="Bound">_</a> <a id="6173" href="Algebra.Properties.BooleanAlgebra.Expression.html#6173" class="Bound">_</a> <a id="6175" class="Symbol">→</a> <a id="6177" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="6181" class="Symbol">λ</a> <a id="6183" href="Algebra.Properties.BooleanAlgebra.Expression.html#6183" class="Bound">i</a> <a id="6185" class="Symbol">→</a>
                             <a id="6216" href="Relation.Binary.Reflection.html#2382" class="Function">solve</a> <a id="6222" href="Algebra.Properties.BooleanAlgebra.Expression.html#6183" class="Bound">i</a> <a id="6224" class="Number">2</a> <a id="6226" class="Symbol">(λ</a> <a id="6229" href="Algebra.Properties.BooleanAlgebra.Expression.html#6229" class="Bound">x</a> <a id="6231" href="Algebra.Properties.BooleanAlgebra.Expression.html#6231" class="Bound">y</a> <a id="6233" class="Symbol">→</a> <a id="6235" href="Algebra.Properties.BooleanAlgebra.Expression.html#6229" class="Bound">x</a> <a id="6237" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="6241" class="Symbol">(</a><a id="6242" href="Algebra.Properties.BooleanAlgebra.Expression.html#6229" class="Bound">x</a> <a id="6244" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="6247" href="Algebra.Properties.BooleanAlgebra.Expression.html#6231" class="Bound">y</a><a id="6248" class="Symbol">)</a> <a id="6250" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6252" href="Algebra.Properties.BooleanAlgebra.Expression.html#6229" class="Bound">x</a><a id="6253" class="Symbol">)</a>
                                   <a id="6290" class="Symbol">(</a><a id="6291" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a> <a id="6297" href="Algebra.Structures.html#13237" class="Function">absorptive</a> <a id="6308" class="Symbol">_</a> <a id="6310" class="Symbol">_)</a> <a id="6313" class="Symbol">_</a> <a id="6315" class="Symbol">_)</a>
        <a id="6326" class="Symbol">}</a>
      <a id="6334" class="Symbol">;</a> <a id="6336" class="Field">∨-∧-distribʳ</a> <a id="6349" class="Symbol">=</a> <a id="6351" class="Symbol">λ</a> <a id="6353" href="Algebra.Properties.BooleanAlgebra.Expression.html#6353" class="Bound">_</a> <a id="6355" href="Algebra.Properties.BooleanAlgebra.Expression.html#6355" class="Bound">_</a> <a id="6357" href="Algebra.Properties.BooleanAlgebra.Expression.html#6357" class="Bound">_</a> <a id="6359" class="Symbol">→</a> <a id="6361" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="6365" class="Symbol">λ</a> <a id="6367" href="Algebra.Properties.BooleanAlgebra.Expression.html#6367" class="Bound">i</a> <a id="6369" class="Symbol">→</a>
                         <a id="6396" href="Relation.Binary.Reflection.html#2382" class="Function">solve</a> <a id="6402" href="Algebra.Properties.BooleanAlgebra.Expression.html#6367" class="Bound">i</a> <a id="6404" class="Number">3</a>
                               <a id="6437" class="Symbol">(λ</a> <a id="6440" href="Algebra.Properties.BooleanAlgebra.Expression.html#6440" class="Bound">x</a> <a id="6442" href="Algebra.Properties.BooleanAlgebra.Expression.html#6442" class="Bound">y</a> <a id="6444" href="Algebra.Properties.BooleanAlgebra.Expression.html#6444" class="Bound">z</a> <a id="6446" class="Symbol">→</a> <a id="6448" class="Symbol">(</a><a id="6449" href="Algebra.Properties.BooleanAlgebra.Expression.html#6442" class="Bound">y</a> <a id="6451" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="6455" href="Algebra.Properties.BooleanAlgebra.Expression.html#6444" class="Bound">z</a><a id="6456" class="Symbol">)</a> <a id="6458" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="6461" href="Algebra.Properties.BooleanAlgebra.Expression.html#6440" class="Bound">x</a> <a id="6463" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a>
                                          <a id="6507" class="Symbol">(</a><a id="6508" href="Algebra.Properties.BooleanAlgebra.Expression.html#6442" class="Bound">y</a> <a id="6510" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="6513" href="Algebra.Properties.BooleanAlgebra.Expression.html#6440" class="Bound">x</a><a id="6514" class="Symbol">)</a> <a id="6516" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="6520" class="Symbol">(</a><a id="6521" href="Algebra.Properties.BooleanAlgebra.Expression.html#6444" class="Bound">z</a> <a id="6523" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="6526" href="Algebra.Properties.BooleanAlgebra.Expression.html#6440" class="Bound">x</a><a id="6527" class="Symbol">))</a>
                               <a id="6561" class="Symbol">(</a><a id="6562" href="Algebra.Structures.html#13511" class="Function">∨-∧-distribʳ</a> <a id="6575" class="Symbol">_</a> <a id="6577" class="Symbol">_</a> <a id="6579" class="Symbol">_)</a> <a id="6582" class="Symbol">_</a> <a id="6584" class="Symbol">_</a> <a id="6586" class="Symbol">_</a>
      <a id="6594" class="Symbol">}</a>
    <a id="6600" class="Symbol">;</a> <a id="6602" class="Field">∨-complementʳ</a> <a id="6616" class="Symbol">=</a> <a id="6618" class="Symbol">λ</a> <a id="6620" href="Algebra.Properties.BooleanAlgebra.Expression.html#6620" class="Bound">_</a> <a id="6622" class="Symbol">→</a> <a id="6624" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="6628" class="Symbol">λ</a> <a id="6630" href="Algebra.Properties.BooleanAlgebra.Expression.html#6630" class="Bound">i</a> <a id="6632" class="Symbol">→</a>
                        <a id="6658" href="Relation.Binary.Reflection.html#2382" class="Function">solve</a> <a id="6664" href="Algebra.Properties.BooleanAlgebra.Expression.html#6630" class="Bound">i</a> <a id="6666" class="Number">1</a> <a id="6668" class="Symbol">(λ</a> <a id="6671" href="Algebra.Properties.BooleanAlgebra.Expression.html#6671" class="Bound">x</a> <a id="6673" class="Symbol">→</a> <a id="6675" href="Algebra.Properties.BooleanAlgebra.Expression.html#6671" class="Bound">x</a> <a id="6677" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._or_" class="InductiveConstructor Operator">or</a> <a id="6680" class="Symbol">(</a><a id="6681" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.not" class="InductiveConstructor">not</a> <a id="6685" href="Algebra.Properties.BooleanAlgebra.Expression.html#6671" class="Bound">x</a><a id="6686" class="Symbol">)</a> <a id="6688" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6690" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.top" class="InductiveConstructor">top</a><a id="6693" class="Symbol">)</a>
                              <a id="6725" class="Symbol">(</a><a id="6726" href="Algebra.Structures.html#13809" class="Function">∨-complementʳ</a> <a id="6740" class="Symbol">_)</a> <a id="6743" class="Symbol">_</a>
    <a id="6749" class="Symbol">;</a> <a id="6751" class="Field">∧-complementʳ</a> <a id="6765" class="Symbol">=</a> <a id="6767" class="Symbol">λ</a> <a id="6769" href="Algebra.Properties.BooleanAlgebra.Expression.html#6769" class="Bound">_</a> <a id="6771" class="Symbol">→</a> <a id="6773" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="6777" class="Symbol">λ</a> <a id="6779" href="Algebra.Properties.BooleanAlgebra.Expression.html#6779" class="Bound">i</a> <a id="6781" class="Symbol">→</a>
                        <a id="6807" href="Relation.Binary.Reflection.html#2382" class="Function">solve</a> <a id="6813" href="Algebra.Properties.BooleanAlgebra.Expression.html#6779" class="Bound">i</a> <a id="6815" class="Number">1</a> <a id="6817" class="Symbol">(λ</a> <a id="6820" href="Algebra.Properties.BooleanAlgebra.Expression.html#6820" class="Bound">x</a> <a id="6822" class="Symbol">→</a> <a id="6824" href="Algebra.Properties.BooleanAlgebra.Expression.html#6820" class="Bound">x</a> <a id="6826" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr._and_" class="InductiveConstructor Operator">and</a> <a id="6830" class="Symbol">(</a><a id="6831" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.not" class="InductiveConstructor">not</a> <a id="6835" href="Algebra.Properties.BooleanAlgebra.Expression.html#6820" class="Bound">x</a><a id="6836" class="Symbol">)</a> <a id="6838" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6840" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.bot" class="InductiveConstructor">bot</a><a id="6843" class="Symbol">)</a>
                              <a id="6875" class="Symbol">(</a><a id="6876" href="Algebra.Structures.html#13856" class="Function">∧-complementʳ</a> <a id="6890" class="Symbol">_)</a> <a id="6893" class="Symbol">_</a>
    <a id="6899" class="Symbol">;</a> <a id="6901" class="Field">¬-cong</a>        <a id="6915" class="Symbol">=</a> <a id="6917" class="Symbol">λ</a> <a id="6919" href="Algebra.Properties.BooleanAlgebra.Expression.html#6919" class="Bound">xs≈ys</a> <a id="6925" class="Symbol">→</a> <a id="6927" href="Relation.Binary.Vec.Pointwise.html#Pointwise.ext" class="InductiveConstructor">ext</a> <a id="6931" class="Symbol">λ</a> <a id="6933" href="Algebra.Properties.BooleanAlgebra.Expression.html#6933" class="Bound">i</a> <a id="6935" class="Symbol">→</a>
                        <a id="6961" href="Relation.Binary.Reflection.html#2984" class="Function">solve₁</a> <a id="6968" href="Algebra.Properties.BooleanAlgebra.Expression.html#6933" class="Bound">i</a> <a id="6970" class="Number">2</a> <a id="6972" class="Symbol">(λ</a> <a id="6975" href="Algebra.Properties.BooleanAlgebra.Expression.html#6975" class="Bound">x</a> <a id="6977" href="Algebra.Properties.BooleanAlgebra.Expression.html#6977" class="Bound">y</a> <a id="6979" class="Symbol">→</a> <a id="6981" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.not" class="InductiveConstructor">not</a> <a id="6985" href="Algebra.Properties.BooleanAlgebra.Expression.html#6975" class="Bound">x</a> <a id="6987" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="6989" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.not" class="InductiveConstructor">not</a> <a id="6993" href="Algebra.Properties.BooleanAlgebra.Expression.html#6977" class="Bound">y</a><a id="6994" class="Symbol">)</a> <a id="6996" class="Symbol">_</a> <a id="6998" class="Symbol">_</a>
                               <a id="7031" class="Symbol">(</a><a id="7032" href="Algebra.Structures.html#13903" class="Function">¬-cong</a> <a id="7039" class="Symbol">(</a><a id="7040" href="Relation.Binary.Vec.Pointwise.html#Pointwise.app" class="Field">Pointwise.app</a> <a id="7054" href="Algebra.Properties.BooleanAlgebra.Expression.html#6919" class="Bound">xs≈ys</a> <a id="7060" href="Algebra.Properties.BooleanAlgebra.Expression.html#6933" class="Bound">i</a><a id="7061" class="Symbol">))</a>
    <a id="7068" class="Symbol">}</a>
  <a id="7072" class="Symbol">}</a>
  <a id="7076" class="Keyword">where</a>
  <a id="7084" class="Keyword">open</a> <a id="7089" href="Category.Applicative.html#RawApplicative" class="Module">RawApplicative</a> <a id="7104" href="Data.Vec.html#applicative" class="Function">Vec.applicative</a>
    <a id="7124" class="Keyword">using</a> <a id="7130" class="Symbol">(</a>pure<a id="7135" class="Symbol">;</a> zipWith<a id="7144" class="Symbol">)</a> <a id="7146" class="Keyword">renaming</a> <a id="7155" class="Symbol">(</a>_&lt;$&gt;_ <a id="7162" class="Symbol">to</a> map<a id="7168" class="Symbol">)</a>

  <a id="7173" href="Algebra.Properties.BooleanAlgebra.Expression.html#7173" class="Function Operator">⟦_⟧Id</a> <a id="7179" class="Symbol">:</a> <a id="7181" class="Symbol">∀</a> <a id="7183" class="Symbol">{</a><a id="7184" href="Algebra.Properties.BooleanAlgebra.Expression.html#7184" class="Bound">n</a><a id="7185" class="Symbol">}</a> <a id="7187" class="Symbol">→</a> <a id="7189" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="7194" href="Algebra.Properties.BooleanAlgebra.Expression.html#7184" class="Bound">n</a> <a id="7196" class="Symbol">→</a> <a id="7198" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="7202" href="Algebra.html#13345" class="Field">Carrier</a> <a id="7210" href="Algebra.Properties.BooleanAlgebra.Expression.html#7184" class="Bound">n</a> <a id="7212" class="Symbol">→</a> <a id="7214" href="Algebra.html#13345" class="Field">Carrier</a>
  <a id="7224" href="Algebra.Properties.BooleanAlgebra.Expression.html#7173" class="Function Operator">⟦_⟧Id</a> <a id="7230" class="Symbol">=</a> <a id="7232" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">Semantics.⟦_⟧</a> <a id="7246" class="Symbol">(</a><a id="7247" href="Category.Monad.Indexed.html#1104" class="Function">RawMonad.rawIApplicative</a> <a id="7272" href="Category.Monad.Identity.html#IdentityMonad" class="Function">IdentityMonad</a><a id="7285" class="Symbol">)</a>

  <a id="7290" href="Algebra.Properties.BooleanAlgebra.Expression.html#7290" class="Function Operator">⟦_⟧Vec</a> <a id="7297" class="Symbol">:</a> <a id="7299" class="Symbol">∀</a> <a id="7301" class="Symbol">{</a><a id="7302" href="Algebra.Properties.BooleanAlgebra.Expression.html#7302" class="Bound">m</a> <a id="7304" href="Algebra.Properties.BooleanAlgebra.Expression.html#7304" class="Bound">n</a><a id="7305" class="Symbol">}</a> <a id="7307" class="Symbol">→</a> <a id="7309" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr" class="Datatype">Expr</a> <a id="7314" href="Algebra.Properties.BooleanAlgebra.Expression.html#7304" class="Bound">n</a> <a id="7316" class="Symbol">→</a> <a id="7318" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="7322" class="Symbol">(</a><a id="7323" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="7327" href="Algebra.html#13345" class="Field">Carrier</a> <a id="7335" href="Algebra.Properties.BooleanAlgebra.Expression.html#7302" class="Bound">m</a><a id="7336" class="Symbol">)</a> <a id="7338" href="Algebra.Properties.BooleanAlgebra.Expression.html#7304" class="Bound">n</a> <a id="7340" class="Symbol">→</a> <a id="7342" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="7346" href="Algebra.html#13345" class="Field">Carrier</a> <a id="7354" href="Algebra.Properties.BooleanAlgebra.Expression.html#7302" class="Bound">m</a>
  <a id="7358" href="Algebra.Properties.BooleanAlgebra.Expression.html#7290" class="Function Operator">⟦_⟧Vec</a> <a id="7365" class="Symbol">=</a> <a id="7367" href="Algebra.Properties.BooleanAlgebra.Expression.html#Semantics.%E2%9F%A6_%E2%9F%A7" class="Function Operator">Semantics.⟦_⟧</a> <a id="7381" href="Data.Vec.html#applicative" class="Function">Vec.applicative</a>

  <a id="7400" class="Keyword">open</a> <a id="7405" class="Keyword">module</a> <a id="R" href="Algebra.Properties.BooleanAlgebra.Expression.html#R" class="Module">R</a> <a id="7414" class="Symbol">{</a><a id="7415" href="Algebra.Properties.BooleanAlgebra.Expression.html#7415" class="Bound">n</a><a id="7416" class="Symbol">}</a> <a id="7418" class="Symbol">(</a><a id="7419" href="Algebra.Properties.BooleanAlgebra.Expression.html#7419" class="Bound">i</a> <a id="7421" class="Symbol">:</a> <a id="7423" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="7427" href="Algebra.Properties.BooleanAlgebra.Expression.html#7415" class="Bound">n</a><a id="7428" class="Symbol">)</a> <a id="7430" class="Symbol">=</a>
    <a id="7436" href="Relation.Binary.Reflection.html" class="Module">Reflection</a> <a id="7447" href="Algebra.html#12645" class="Function">setoid</a> <a id="7454" href="Algebra.Properties.BooleanAlgebra.Expression.html#Expr.var" class="InductiveConstructor">var</a>
      <a id="7464" class="Symbol">(λ</a> <a id="7467" href="Algebra.Properties.BooleanAlgebra.Expression.html#7467" class="Bound">e</a> <a id="7469" href="Algebra.Properties.BooleanAlgebra.Expression.html#7469" class="Bound">ρ</a> <a id="7471" class="Symbol">→</a> <a id="7473" href="Data.Vec.html#lookup" class="Function">Vec.lookup</a> <a id="7484" href="Algebra.Properties.BooleanAlgebra.Expression.html#7419" class="Bound">i</a> <a id="7486" class="Symbol">(</a><a id="7487" href="Algebra.Properties.BooleanAlgebra.Expression.html#7290" class="Function Operator">⟦</a> <a id="7489" href="Algebra.Properties.BooleanAlgebra.Expression.html#7467" class="Bound">e</a> <a id="7491" href="Algebra.Properties.BooleanAlgebra.Expression.html#7290" class="Function Operator">⟧Vec</a> <a id="7496" href="Algebra.Properties.BooleanAlgebra.Expression.html#7469" class="Bound">ρ</a><a id="7497" class="Symbol">))</a>
      <a id="7506" class="Symbol">(λ</a> <a id="7509" href="Algebra.Properties.BooleanAlgebra.Expression.html#7509" class="Bound">e</a> <a id="7511" href="Algebra.Properties.BooleanAlgebra.Expression.html#7511" class="Bound">ρ</a> <a id="7513" class="Symbol">→</a> <a id="7515" href="Algebra.Properties.BooleanAlgebra.Expression.html#7173" class="Function Operator">⟦</a> <a id="7517" href="Algebra.Properties.BooleanAlgebra.Expression.html#7509" class="Bound">e</a> <a id="7519" href="Algebra.Properties.BooleanAlgebra.Expression.html#7173" class="Function Operator">⟧Id</a> <a id="7523" class="Symbol">(</a><a id="7524" href="Data.Vec.html#map" class="Function">Vec.map</a> <a id="7532" class="Symbol">(</a><a id="7533" href="Data.Vec.html#lookup" class="Function">Vec.lookup</a> <a id="7544" href="Algebra.Properties.BooleanAlgebra.Expression.html#7419" class="Bound">i</a><a id="7545" class="Symbol">)</a> <a id="7547" href="Algebra.Properties.BooleanAlgebra.Expression.html#7511" class="Bound">ρ</a><a id="7548" class="Symbol">))</a>
      <a id="7557" class="Symbol">(λ</a> <a id="7560" href="Algebra.Properties.BooleanAlgebra.Expression.html#7560" class="Bound">e</a> <a id="7562" href="Algebra.Properties.BooleanAlgebra.Expression.html#7562" class="Bound">ρ</a> <a id="7564" class="Symbol">→</a> <a id="7566" href="Relation.Binary.Core.html#4960" class="Function">sym</a> <a id="7570" href="Function.html#_%24_" class="Function Operator">$</a> <a id="7572" href="Relation.Binary.Core.html#5012" class="Function">reflexive</a> <a id="7582" href="Function.html#_%24_" class="Function Operator">$</a>
                 <a id="7601" href="Algebra.Properties.BooleanAlgebra.Expression.html#Naturality.natural" class="Function">Naturality.natural</a> <a id="7620" class="Symbol">(</a><a id="7621" href="Data.Vec.Properties.html#lookup-morphism" class="Function">VecProp.lookup-morphism</a> <a id="7645" href="Algebra.Properties.BooleanAlgebra.Expression.html#7419" class="Bound">i</a><a id="7646" class="Symbol">)</a> <a id="7648" href="Algebra.Properties.BooleanAlgebra.Expression.html#7560" class="Bound">e</a> <a id="7650" href="Algebra.Properties.BooleanAlgebra.Expression.html#7562" class="Bound">ρ</a><a id="7651" class="Symbol">)</a>
</pre></body></html>

APT Browse - Built by Thomas Orozco.