-
Notifications
You must be signed in to change notification settings - Fork 0
/
Cubical.HITs.CumulativeHierarchy.Base.html
241 lines (219 loc) · 187 KB
/
Cubical.HITs.CumulativeHierarchy.Base.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
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
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.HITs.CumulativeHierarchy.Base</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Symbol">#-}</a>
<a id="24" class="Comment">{-
This file models "ZF - powerset" in cubical agda, via a cumulative hierarchy, in the sense given
in the HoTT book §10.5 "The cumulative hierarchy".
A great amount of inspiration is taken from the Coq implementations found in
Jérémy Ledent, Modeling set theory in homotopy type theory, code of which can be found online at
https://github.com/jledent/vset
-}</a>
<a id="386" class="Keyword">module</a> <a id="393" href="Cubical.HITs.CumulativeHierarchy.Base.html" class="Module">Cubical.HITs.CumulativeHierarchy.Base</a> <a id="431" class="Keyword">where</a>
<a id="438" class="Keyword">open</a> <a id="443" class="Keyword">import</a> <a id="450" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>
<a id="478" class="Keyword">open</a> <a id="483" class="Keyword">import</a> <a id="490" href="Cubical.Foundations.Path.html" class="Module">Cubical.Foundations.Path</a>
<a id="515" class="Keyword">open</a> <a id="520" class="Keyword">import</a> <a id="527" href="Cubical.Foundations.Function.html" class="Module">Cubical.Foundations.Function</a>
<a id="556" class="Keyword">open</a> <a id="561" class="Keyword">import</a> <a id="568" href="Cubical.Foundations.HLevels.html" class="Module">Cubical.Foundations.HLevels</a>
<a id="596" class="Keyword">open</a> <a id="601" class="Keyword">import</a> <a id="608" href="Cubical.Foundations.Equiv.html" class="Module">Cubical.Foundations.Equiv</a> <a id="634" class="Keyword">using</a> <a id="640" class="Symbol">(</a><a id="641" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a><a id="646" class="Symbol">)</a>
<a id="648" class="Keyword">open</a> <a id="653" class="Keyword">import</a> <a id="660" href="Cubical.Functions.Logic.html" class="Module">Cubical.Functions.Logic</a>
<a id="684" class="Keyword">open</a> <a id="689" class="Keyword">import</a> <a id="696" href="Cubical.Data.Sigma.html" class="Module">Cubical.Data.Sigma</a>
<a id="715" class="Keyword">open</a> <a id="720" class="Keyword">import</a> <a id="727" href="Cubical.HITs.PropositionalTruncation.html" class="Module">Cubical.HITs.PropositionalTruncation</a> <a id="764" class="Symbol">as</a> <a id="767" class="Module">P</a> <a id="769" class="Keyword">hiding</a> <a id="776" class="Symbol">(</a><a id="777" href="Cubical.HITs.PropositionalTruncation.Properties.html#3342" class="Function">elim</a><a id="781" class="Symbol">;</a> <a id="783" href="Cubical.HITs.PropositionalTruncation.Properties.html#3599" class="Function">elim2</a><a id="788" class="Symbol">)</a>
<a id="791" class="Keyword">import</a> <a id="798" href="Cubical.HITs.PropositionalTruncation.Monad.html" class="Module">Cubical.HITs.PropositionalTruncation.Monad</a> <a id="841" class="Symbol">as</a> <a id="844" class="Module">PropMonad</a>
<a id="855" class="Keyword">private</a>
<a id="865" class="Keyword">variable</a>
<a id="878" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a> <a id="880" href="Cubical.HITs.CumulativeHierarchy.Base.html#880" class="Generalizable">ℓ'</a> <a id="883" class="Symbol">:</a> <a id="885" href="Agda.Primitive.html#597" class="Postulate">Level</a>
<a id="892" class="Keyword">infix</a> <a id="898" class="Number">5</a> <a id="900" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">_∈_</a>
<a id="905" class="Comment">-- set up the basic hierarchy definition and _∈_ as recursive, higher inductive types</a>
<a id="991" class="Keyword">data</a> <a id="V"></a><a id="996" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="998" class="Symbol">(</a><a id="999" href="Cubical.HITs.CumulativeHierarchy.Base.html#999" class="Bound">ℓ</a> <a id="1001" class="Symbol">:</a> <a id="1003" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="1008" class="Symbol">)</a> <a id="1010" class="Symbol">:</a> <a id="1012" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1017" class="Symbol">(</a><a id="1018" href="Agda.Primitive.html#780" class="Primitive">ℓ-suc</a> <a id="1024" href="Cubical.HITs.CumulativeHierarchy.Base.html#999" class="Bound">ℓ</a><a id="1025" class="Symbol">)</a>
<a id="_∈_"></a><a id="1027" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">_∈_</a> <a id="1031" class="Symbol">:</a> <a id="1033" class="Symbol">(</a><a id="1034" href="Cubical.HITs.CumulativeHierarchy.Base.html#1034" class="Bound">S</a> <a id="1036" href="Cubical.HITs.CumulativeHierarchy.Base.html#1036" class="Bound">T</a> <a id="1038" class="Symbol">:</a> <a id="1040" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1042" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="1043" class="Symbol">)</a> <a id="1045" class="Symbol">→</a> <a id="1047" href="Cubical.Foundations.HLevels.html#2018" class="Function">hProp</a> <a id="1053" class="Symbol">(</a><a id="1054" href="Agda.Primitive.html#780" class="Primitive">ℓ-suc</a> <a id="1060" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="1061" class="Symbol">)</a>
<a id="eqImage"></a><a id="1064" href="Cubical.HITs.CumulativeHierarchy.Base.html#1064" class="Function">eqImage</a> <a id="1072" class="Symbol">:</a> <a id="1074" class="Symbol">{</a><a id="1075" href="Cubical.HITs.CumulativeHierarchy.Base.html#1075" class="Bound">X</a> <a id="1077" href="Cubical.HITs.CumulativeHierarchy.Base.html#1077" class="Bound">Y</a> <a id="1079" class="Symbol">:</a> <a id="1081" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1086" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="1087" class="Symbol">}</a> <a id="1089" class="Symbol">(</a><a id="1090" href="Cubical.HITs.CumulativeHierarchy.Base.html#1090" class="Bound">ix</a> <a id="1093" class="Symbol">:</a> <a id="1095" href="Cubical.HITs.CumulativeHierarchy.Base.html#1075" class="Bound">X</a> <a id="1097" class="Symbol">→</a> <a id="1099" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1101" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="1102" class="Symbol">)</a> <a id="1104" class="Symbol">(</a><a id="1105" href="Cubical.HITs.CumulativeHierarchy.Base.html#1105" class="Bound">iy</a> <a id="1108" class="Symbol">:</a> <a id="1110" href="Cubical.HITs.CumulativeHierarchy.Base.html#1077" class="Bound">Y</a> <a id="1112" class="Symbol">→</a> <a id="1114" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1116" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="1117" class="Symbol">)</a> <a id="1119" class="Symbol">→</a> <a id="1121" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1126" class="Symbol">(</a><a id="1127" href="Agda.Primitive.html#780" class="Primitive">ℓ-suc</a> <a id="1133" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="1134" class="Symbol">)</a>
<a id="1136" href="Cubical.HITs.CumulativeHierarchy.Base.html#1064" class="Function">eqImage</a> <a id="1144" class="Symbol">{</a><a id="1145" class="Argument">X</a> <a id="1147" class="Symbol">=</a> <a id="1149" href="Cubical.HITs.CumulativeHierarchy.Base.html#1149" class="Bound">X</a><a id="1150" class="Symbol">}</a> <a id="1152" class="Symbol">{</a><a id="1153" class="Argument">Y</a> <a id="1155" class="Symbol">=</a> <a id="1157" href="Cubical.HITs.CumulativeHierarchy.Base.html#1157" class="Bound">Y</a><a id="1158" class="Symbol">}</a> <a id="1160" href="Cubical.HITs.CumulativeHierarchy.Base.html#1160" class="Bound">ix</a> <a id="1163" href="Cubical.HITs.CumulativeHierarchy.Base.html#1163" class="Bound">iy</a> <a id="1166" class="Symbol">=</a> <a id="1168" class="Symbol">(∀</a> <a id="1171" class="Symbol">(</a><a id="1172" href="Cubical.HITs.CumulativeHierarchy.Base.html#1172" class="Bound">a</a> <a id="1174" class="Symbol">:</a> <a id="1176" href="Cubical.HITs.CumulativeHierarchy.Base.html#1149" class="Bound">X</a><a id="1177" class="Symbol">)</a> <a id="1179" class="Symbol">→</a> <a id="1181" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="1183" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="1189" href="Cubical.HITs.CumulativeHierarchy.Base.html#1163" class="Bound">iy</a> <a id="1192" class="Symbol">(</a><a id="1193" href="Cubical.HITs.CumulativeHierarchy.Base.html#1160" class="Bound">ix</a> <a id="1196" href="Cubical.HITs.CumulativeHierarchy.Base.html#1172" class="Bound">a</a><a id="1197" class="Symbol">)</a> <a id="1199" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a><a id="1201" class="Symbol">)</a> <a id="1203" href="Cubical.Functions.Logic.html#3773" class="Function Operator">⊓′</a>
<a id="1238" class="Symbol">(∀</a> <a id="1241" class="Symbol">(</a><a id="1242" href="Cubical.HITs.CumulativeHierarchy.Base.html#1242" class="Bound">b</a> <a id="1244" class="Symbol">:</a> <a id="1246" href="Cubical.HITs.CumulativeHierarchy.Base.html#1157" class="Bound">Y</a><a id="1247" class="Symbol">)</a> <a id="1249" class="Symbol">→</a> <a id="1251" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="1253" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="1259" href="Cubical.HITs.CumulativeHierarchy.Base.html#1160" class="Bound">ix</a> <a id="1262" class="Symbol">(</a><a id="1263" href="Cubical.HITs.CumulativeHierarchy.Base.html#1163" class="Bound">iy</a> <a id="1266" href="Cubical.HITs.CumulativeHierarchy.Base.html#1242" class="Bound">b</a><a id="1267" class="Symbol">)</a> <a id="1269" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a><a id="1271" class="Symbol">)</a>
<a id="1274" class="Keyword">data</a> <a id="1279" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1281" href="Cubical.HITs.CumulativeHierarchy.Base.html#1281" class="Bound">ℓ</a> <a id="1283" class="Keyword">where</a>
<a id="V.sett"></a><a id="1291" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="1296" class="Symbol">:</a> <a id="1298" class="Symbol">(</a><a id="1299" href="Cubical.HITs.CumulativeHierarchy.Base.html#1299" class="Bound">X</a> <a id="1301" class="Symbol">:</a> <a id="1303" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1308" href="Cubical.HITs.CumulativeHierarchy.Base.html#1281" class="Bound">ℓ</a><a id="1309" class="Symbol">)</a> <a id="1311" class="Symbol">→</a> <a id="1313" class="Symbol">(</a><a id="1314" href="Cubical.HITs.CumulativeHierarchy.Base.html#1299" class="Bound">X</a> <a id="1316" class="Symbol">→</a> <a id="1318" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1320" href="Cubical.HITs.CumulativeHierarchy.Base.html#1281" class="Bound">ℓ</a><a id="1321" class="Symbol">)</a> <a id="1323" class="Symbol">→</a> <a id="1325" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1327" href="Cubical.HITs.CumulativeHierarchy.Base.html#1281" class="Bound">ℓ</a>
<a id="V.seteq"></a><a id="1331" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="1337" class="Symbol">:</a> <a id="1339" class="Symbol">(</a><a id="1340" href="Cubical.HITs.CumulativeHierarchy.Base.html#1340" class="Bound">X</a> <a id="1342" href="Cubical.HITs.CumulativeHierarchy.Base.html#1342" class="Bound">Y</a> <a id="1344" class="Symbol">:</a> <a id="1346" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1351" href="Cubical.HITs.CumulativeHierarchy.Base.html#1281" class="Bound">ℓ</a><a id="1352" class="Symbol">)</a> <a id="1354" class="Symbol">(</a><a id="1355" href="Cubical.HITs.CumulativeHierarchy.Base.html#1355" class="Bound">ix</a> <a id="1358" class="Symbol">:</a> <a id="1360" href="Cubical.HITs.CumulativeHierarchy.Base.html#1340" class="Bound">X</a> <a id="1362" class="Symbol">→</a> <a id="1364" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1366" href="Cubical.HITs.CumulativeHierarchy.Base.html#1281" class="Bound">ℓ</a><a id="1367" class="Symbol">)</a> <a id="1369" class="Symbol">(</a><a id="1370" href="Cubical.HITs.CumulativeHierarchy.Base.html#1370" class="Bound">iy</a> <a id="1373" class="Symbol">:</a> <a id="1375" href="Cubical.HITs.CumulativeHierarchy.Base.html#1342" class="Bound">Y</a> <a id="1377" class="Symbol">→</a> <a id="1379" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1381" href="Cubical.HITs.CumulativeHierarchy.Base.html#1281" class="Bound">ℓ</a><a id="1382" class="Symbol">)</a> <a id="1384" class="Symbol">(</a><a id="1385" href="Cubical.HITs.CumulativeHierarchy.Base.html#1385" class="Bound">eq</a> <a id="1388" class="Symbol">:</a> <a id="1390" href="Cubical.HITs.CumulativeHierarchy.Base.html#1064" class="Function">eqImage</a> <a id="1398" href="Cubical.HITs.CumulativeHierarchy.Base.html#1355" class="Bound">ix</a> <a id="1401" href="Cubical.HITs.CumulativeHierarchy.Base.html#1370" class="Bound">iy</a><a id="1403" class="Symbol">)</a> <a id="1405" class="Symbol">→</a> <a id="1407" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="1412" href="Cubical.HITs.CumulativeHierarchy.Base.html#1340" class="Bound">X</a> <a id="1414" href="Cubical.HITs.CumulativeHierarchy.Base.html#1355" class="Bound">ix</a> <a id="1417" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1419" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="1424" href="Cubical.HITs.CumulativeHierarchy.Base.html#1342" class="Bound">Y</a> <a id="1426" href="Cubical.HITs.CumulativeHierarchy.Base.html#1370" class="Bound">iy</a>
<a id="V.setIsSet"></a><a id="1431" href="Cubical.HITs.CumulativeHierarchy.Base.html#1431" class="InductiveConstructor">setIsSet</a> <a id="1440" class="Symbol">:</a> <a id="1442" href="Cubical.Foundations.Prelude.html#14094" class="Function">isSet</a> <a id="1448" class="Symbol">(</a><a id="1449" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1451" href="Cubical.HITs.CumulativeHierarchy.Base.html#1281" class="Bound">ℓ</a><a id="1452" class="Symbol">)</a>
<a id="1455" href="Cubical.HITs.CumulativeHierarchy.Base.html#1455" class="Bound">A</a> <a id="1457" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">∈</a> <a id="1459" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="1464" href="Cubical.HITs.CumulativeHierarchy.Base.html#1464" class="Bound">X</a> <a id="1466" href="Cubical.HITs.CumulativeHierarchy.Base.html#1466" class="Bound">ix</a> <a id="1469" class="Symbol">=</a> <a id="1471" href="Cubical.Functions.Logic.html#1583" class="Function Operator">∥</a> <a id="1473" href="Cubical.Core.Primitives.html#6306" class="Function">Σ[</a> <a id="1476" href="Cubical.HITs.CumulativeHierarchy.Base.html#1476" class="Bound">i</a> <a id="1478" href="Cubical.Core.Primitives.html#6306" class="Function">∈</a> <a id="1480" href="Cubical.HITs.CumulativeHierarchy.Base.html#1464" class="Bound">X</a> <a id="1482" href="Cubical.Core.Primitives.html#6306" class="Function">]</a> <a id="1484" class="Symbol">(</a><a id="1485" href="Cubical.HITs.CumulativeHierarchy.Base.html#1466" class="Bound">ix</a> <a id="1488" href="Cubical.HITs.CumulativeHierarchy.Base.html#1476" class="Bound">i</a> <a id="1490" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1492" href="Cubical.HITs.CumulativeHierarchy.Base.html#1455" class="Bound">A</a><a id="1493" class="Symbol">)</a> <a id="1495" href="Cubical.Functions.Logic.html#1583" class="Function Operator">∥ₚ</a>
<a id="1498" href="Cubical.HITs.CumulativeHierarchy.Base.html#1498" class="Bound">A</a> <a id="1500" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">∈</a> <a id="1502" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="1508" href="Cubical.HITs.CumulativeHierarchy.Base.html#1508" class="Bound">X</a> <a id="1510" href="Cubical.HITs.CumulativeHierarchy.Base.html#1510" class="Bound">Y</a> <a id="1512" href="Cubical.HITs.CumulativeHierarchy.Base.html#1512" class="Bound">ix</a> <a id="1515" href="Cubical.HITs.CumulativeHierarchy.Base.html#1515" class="Bound">iy</a> <a id="1518" class="Symbol">(</a><a id="1519" href="Cubical.HITs.CumulativeHierarchy.Base.html#1519" class="Bound">f</a> <a id="1521" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1523" href="Cubical.HITs.CumulativeHierarchy.Base.html#1523" class="Bound">g</a><a id="1524" class="Symbol">)</a> <a id="1526" href="Cubical.HITs.CumulativeHierarchy.Base.html#1526" class="Bound">i</a> <a id="1528" class="Symbol">=</a>
<a id="1532" href="Cubical.Functions.Logic.html#2028" class="Function">⇔toPath</a> <a id="1540" class="Symbol">{</a><a id="1541" class="Argument">P</a> <a id="1543" class="Symbol">=</a> <a id="1545" href="Cubical.HITs.CumulativeHierarchy.Base.html#1498" class="Bound">A</a> <a id="1547" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">∈</a> <a id="1549" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="1554" href="Cubical.HITs.CumulativeHierarchy.Base.html#1508" class="Bound">X</a> <a id="1556" href="Cubical.HITs.CumulativeHierarchy.Base.html#1512" class="Bound">ix</a><a id="1558" class="Symbol">}</a> <a id="1560" class="Symbol">{</a><a id="1561" class="Argument">Q</a> <a id="1563" class="Symbol">=</a> <a id="1565" href="Cubical.HITs.CumulativeHierarchy.Base.html#1498" class="Bound">A</a> <a id="1567" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">∈</a> <a id="1569" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="1574" href="Cubical.HITs.CumulativeHierarchy.Base.html#1510" class="Bound">Y</a> <a id="1576" href="Cubical.HITs.CumulativeHierarchy.Base.html#1515" class="Bound">iy</a><a id="1578" class="Symbol">}</a>
<a id="1584" class="Symbol">(λ</a> <a id="1587" href="Cubical.HITs.CumulativeHierarchy.Base.html#1587" class="Bound">ax</a> <a id="1590" class="Symbol">→</a> <a id="1592" class="Keyword">do</a> <a id="1595" class="Symbol">(</a><a id="1596" href="Cubical.HITs.CumulativeHierarchy.Base.html#1596" class="Bound">x</a> <a id="1598" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1600" href="Cubical.HITs.CumulativeHierarchy.Base.html#1600" class="Bound">xa</a><a id="1602" class="Symbol">)</a> <a id="1604" href="Cubical.HITs.PropositionalTruncation.Monad.html#624" class="Function Operator">←</a> <a id="1606" href="Cubical.HITs.CumulativeHierarchy.Base.html#1587" class="Bound">ax</a> <a id="1609" class="Symbol">;</a> <a id="1611" class="Symbol">(</a><a id="1612" href="Cubical.HITs.CumulativeHierarchy.Base.html#1612" class="Bound">y</a> <a id="1614" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1616" href="Cubical.HITs.CumulativeHierarchy.Base.html#1616" class="Bound">ya</a><a id="1618" class="Symbol">)</a> <a id="1620" href="Cubical.HITs.PropositionalTruncation.Monad.html#624" class="Function Operator">←</a> <a id="1622" href="Cubical.HITs.CumulativeHierarchy.Base.html#1519" class="Bound">f</a> <a id="1624" href="Cubical.HITs.CumulativeHierarchy.Base.html#1596" class="Bound">x</a> <a id="1626" class="Symbol">;</a> <a id="1628" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="1630" href="Cubical.HITs.CumulativeHierarchy.Base.html#1612" class="Bound">y</a> <a id="1632" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1634" href="Cubical.HITs.CumulativeHierarchy.Base.html#1616" class="Bound">ya</a> <a id="1637" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="1639" href="Cubical.HITs.CumulativeHierarchy.Base.html#1600" class="Bound">xa</a> <a id="1642" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a><a id="1644" class="Symbol">)</a>
<a id="1650" class="Symbol">(λ</a> <a id="1653" href="Cubical.HITs.CumulativeHierarchy.Base.html#1653" class="Bound">ay</a> <a id="1656" class="Symbol">→</a> <a id="1658" class="Keyword">do</a> <a id="1661" class="Symbol">(</a><a id="1662" href="Cubical.HITs.CumulativeHierarchy.Base.html#1662" class="Bound">y</a> <a id="1664" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1666" href="Cubical.HITs.CumulativeHierarchy.Base.html#1666" class="Bound">ya</a><a id="1668" class="Symbol">)</a> <a id="1670" href="Cubical.HITs.PropositionalTruncation.Monad.html#624" class="Function Operator">←</a> <a id="1672" href="Cubical.HITs.CumulativeHierarchy.Base.html#1653" class="Bound">ay</a> <a id="1675" class="Symbol">;</a> <a id="1677" class="Symbol">(</a><a id="1678" href="Cubical.HITs.CumulativeHierarchy.Base.html#1678" class="Bound">x</a> <a id="1680" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1682" href="Cubical.HITs.CumulativeHierarchy.Base.html#1682" class="Bound">xa</a><a id="1684" class="Symbol">)</a> <a id="1686" href="Cubical.HITs.PropositionalTruncation.Monad.html#624" class="Function Operator">←</a> <a id="1688" href="Cubical.HITs.CumulativeHierarchy.Base.html#1523" class="Bound">g</a> <a id="1690" href="Cubical.HITs.CumulativeHierarchy.Base.html#1662" class="Bound">y</a> <a id="1692" class="Symbol">;</a> <a id="1694" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="1696" href="Cubical.HITs.CumulativeHierarchy.Base.html#1678" class="Bound">x</a> <a id="1698" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1700" href="Cubical.HITs.CumulativeHierarchy.Base.html#1682" class="Bound">xa</a> <a id="1703" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="1705" href="Cubical.HITs.CumulativeHierarchy.Base.html#1666" class="Bound">ya</a> <a id="1708" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a><a id="1710" class="Symbol">)</a> <a id="1712" href="Cubical.HITs.CumulativeHierarchy.Base.html#1526" class="Bound">i</a>
<a id="1716" class="Keyword">where</a> <a id="1722" class="Keyword">open</a> <a id="1727" href="Cubical.HITs.PropositionalTruncation.Monad.html" class="Module">PropMonad</a>
<a id="1737" href="Cubical.HITs.CumulativeHierarchy.Base.html#1737" class="Bound">A</a> <a id="1739" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">∈</a> <a id="1741" href="Cubical.HITs.CumulativeHierarchy.Base.html#1431" class="InductiveConstructor">setIsSet</a> <a id="1750" href="Cubical.HITs.CumulativeHierarchy.Base.html#1750" class="Bound">a</a> <a id="1752" href="Cubical.HITs.CumulativeHierarchy.Base.html#1752" class="Bound">b</a> <a id="1754" href="Cubical.HITs.CumulativeHierarchy.Base.html#1754" class="Bound">p</a> <a id="1756" href="Cubical.HITs.CumulativeHierarchy.Base.html#1756" class="Bound">q</a> <a id="1758" href="Cubical.HITs.CumulativeHierarchy.Base.html#1758" class="Bound">i</a> <a id="1760" href="Cubical.HITs.CumulativeHierarchy.Base.html#1760" class="Bound">j</a> <a id="1762" class="Symbol">=</a> <a id="1764" href="Cubical.Foundations.HLevels.html#22223" class="Function">isSetHProp</a> <a id="1775" class="Symbol">(</a><a id="1776" href="Cubical.HITs.CumulativeHierarchy.Base.html#1737" class="Bound">A</a> <a id="1778" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">∈</a> <a id="1780" href="Cubical.HITs.CumulativeHierarchy.Base.html#1750" class="Bound">a</a><a id="1781" class="Symbol">)</a> <a id="1783" class="Symbol">(</a><a id="1784" href="Cubical.HITs.CumulativeHierarchy.Base.html#1737" class="Bound">A</a> <a id="1786" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">∈</a> <a id="1788" href="Cubical.HITs.CumulativeHierarchy.Base.html#1752" class="Bound">b</a><a id="1789" class="Symbol">)</a> <a id="1791" class="Symbol">(λ</a> <a id="1794" href="Cubical.HITs.CumulativeHierarchy.Base.html#1794" class="Bound">j</a> <a id="1796" class="Symbol">→</a> <a id="1798" href="Cubical.HITs.CumulativeHierarchy.Base.html#1737" class="Bound">A</a> <a id="1800" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">∈</a> <a id="1802" href="Cubical.HITs.CumulativeHierarchy.Base.html#1754" class="Bound">p</a> <a id="1804" href="Cubical.HITs.CumulativeHierarchy.Base.html#1794" class="Bound">j</a><a id="1805" class="Symbol">)</a> <a id="1807" class="Symbol">(λ</a> <a id="1810" href="Cubical.HITs.CumulativeHierarchy.Base.html#1810" class="Bound">j</a> <a id="1812" class="Symbol">→</a> <a id="1814" href="Cubical.HITs.CumulativeHierarchy.Base.html#1737" class="Bound">A</a> <a id="1816" href="Cubical.HITs.CumulativeHierarchy.Base.html#1027" class="Function Operator">∈</a> <a id="1818" href="Cubical.HITs.CumulativeHierarchy.Base.html#1756" class="Bound">q</a> <a id="1820" href="Cubical.HITs.CumulativeHierarchy.Base.html#1810" class="Bound">j</a><a id="1821" class="Symbol">)</a> <a id="1823" href="Cubical.HITs.CumulativeHierarchy.Base.html#1758" class="Bound">i</a> <a id="1825" href="Cubical.HITs.CumulativeHierarchy.Base.html#1760" class="Bound">j</a>
<a id="1828" class="Comment">-- setup a general eliminator into h-sets</a>
<a id="1870" class="Keyword">record</a> <a id="ElimSet"></a><a id="1877" href="Cubical.HITs.CumulativeHierarchy.Base.html#1877" class="Record">ElimSet</a> <a id="1885" class="Symbol">{</a><a id="1886" href="Cubical.HITs.CumulativeHierarchy.Base.html#1886" class="Bound">Z</a> <a id="1888" class="Symbol">:</a> <a id="1890" class="Symbol">(</a><a id="1891" href="Cubical.HITs.CumulativeHierarchy.Base.html#1891" class="Bound">s</a> <a id="1893" class="Symbol">:</a> <a id="1895" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="1897" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="1898" class="Symbol">)</a> <a id="1900" class="Symbol">→</a> <a id="1902" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1907" href="Cubical.HITs.CumulativeHierarchy.Base.html#880" class="Generalizable">ℓ'</a><a id="1909" class="Symbol">}</a>
<a id="1926" class="Symbol">(</a><a id="1927" href="Cubical.HITs.CumulativeHierarchy.Base.html#1927" class="Bound">isSetZ</a> <a id="1934" class="Symbol">:</a> <a id="1936" class="Symbol">∀</a> <a id="1938" href="Cubical.HITs.CumulativeHierarchy.Base.html#1938" class="Bound">s</a> <a id="1940" class="Symbol">→</a> <a id="1942" href="Cubical.Foundations.Prelude.html#14094" class="Function">isSet</a> <a id="1948" class="Symbol">(</a><a id="1949" href="Cubical.HITs.CumulativeHierarchy.Base.html#1886" class="Bound">Z</a> <a id="1951" href="Cubical.HITs.CumulativeHierarchy.Base.html#1938" class="Bound">s</a><a id="1952" class="Symbol">))</a> <a id="1955" class="Symbol">:</a> <a id="1957" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1962" class="Symbol">(</a><a id="1963" href="Agda.Primitive.html#810" class="Primitive">ℓ-max</a> <a id="1969" href="Cubical.HITs.CumulativeHierarchy.Base.html#1907" class="Bound">ℓ'</a> <a id="1972" class="Symbol">(</a><a id="1973" href="Agda.Primitive.html#780" class="Primitive">ℓ-suc</a> <a id="1979" href="Cubical.HITs.CumulativeHierarchy.Base.html#1897" class="Bound">ℓ</a><a id="1980" class="Symbol">))</a> <a id="1983" class="Keyword">where</a>
<a id="1991" class="Keyword">field</a>
<a id="ElimSet.ElimSett"></a><a id="2001" href="Cubical.HITs.CumulativeHierarchy.Base.html#2001" class="Field">ElimSett</a> <a id="2010" class="Symbol">:</a>
<a id="2018" class="Symbol">∀</a> <a id="2020" class="Symbol">(</a><a id="2021" href="Cubical.HITs.CumulativeHierarchy.Base.html#2021" class="Bound">X</a> <a id="2023" class="Symbol">:</a> <a id="2025" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2030" href="Cubical.HITs.CumulativeHierarchy.Base.html#1897" class="Bound">ℓ</a><a id="2031" class="Symbol">)</a> <a id="2033" class="Symbol">(</a><a id="2034" href="Cubical.HITs.CumulativeHierarchy.Base.html#2034" class="Bound">ix</a> <a id="2037" class="Symbol">:</a> <a id="2039" href="Cubical.HITs.CumulativeHierarchy.Base.html#2021" class="Bound">X</a> <a id="2041" class="Symbol">→</a> <a id="2043" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="2045" href="Cubical.HITs.CumulativeHierarchy.Base.html#1897" class="Bound">ℓ</a><a id="2046" class="Symbol">)</a>
<a id="2054" class="Comment">-- ^ the structural parts of the set</a>
<a id="2097" class="Symbol">→</a> <a id="2099" class="Symbol">(</a><a id="2100" href="Cubical.HITs.CumulativeHierarchy.Base.html#2100" class="Bound">rec</a> <a id="2104" class="Symbol">:</a> <a id="2106" class="Symbol">∀</a> <a id="2108" href="Cubical.HITs.CumulativeHierarchy.Base.html#2108" class="Bound">x</a> <a id="2110" class="Symbol">→</a> <a id="2112" href="Cubical.HITs.CumulativeHierarchy.Base.html#1886" class="Bound">Z</a> <a id="2114" class="Symbol">(</a><a id="2115" href="Cubical.HITs.CumulativeHierarchy.Base.html#2034" class="Bound">ix</a> <a id="2118" href="Cubical.HITs.CumulativeHierarchy.Base.html#2108" class="Bound">x</a><a id="2119" class="Symbol">))</a>
<a id="2128" class="Comment">-- ^ a recursor into the elements</a>
<a id="2168" class="Symbol">→</a> <a id="2170" href="Cubical.HITs.CumulativeHierarchy.Base.html#1886" class="Bound">Z</a> <a id="2172" class="Symbol">(</a><a id="2173" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="2178" href="Cubical.HITs.CumulativeHierarchy.Base.html#2021" class="Bound">X</a> <a id="2180" href="Cubical.HITs.CumulativeHierarchy.Base.html#2034" class="Bound">ix</a><a id="2182" class="Symbol">)</a>
<a id="ElimSet.ElimEq"></a><a id="2188" href="Cubical.HITs.CumulativeHierarchy.Base.html#2188" class="Field">ElimEq</a> <a id="2195" class="Symbol">:</a>
<a id="2203" class="Symbol">∀</a> <a id="2205" class="Symbol">(</a><a id="2206" href="Cubical.HITs.CumulativeHierarchy.Base.html#2206" class="Bound">X₁</a> <a id="2209" href="Cubical.HITs.CumulativeHierarchy.Base.html#2209" class="Bound">X₂</a> <a id="2212" class="Symbol">:</a> <a id="2214" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2219" href="Cubical.HITs.CumulativeHierarchy.Base.html#1897" class="Bound">ℓ</a><a id="2220" class="Symbol">)</a> <a id="2222" class="Symbol">(</a><a id="2223" href="Cubical.HITs.CumulativeHierarchy.Base.html#2223" class="Bound">ix₁</a> <a id="2227" class="Symbol">:</a> <a id="2229" href="Cubical.HITs.CumulativeHierarchy.Base.html#2206" class="Bound">X₁</a> <a id="2232" class="Symbol">→</a> <a id="2234" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="2236" href="Cubical.HITs.CumulativeHierarchy.Base.html#1897" class="Bound">ℓ</a><a id="2237" class="Symbol">)</a> <a id="2239" class="Symbol">(</a><a id="2240" href="Cubical.HITs.CumulativeHierarchy.Base.html#2240" class="Bound">ix₂</a> <a id="2244" class="Symbol">:</a> <a id="2246" href="Cubical.HITs.CumulativeHierarchy.Base.html#2209" class="Bound">X₂</a> <a id="2249" class="Symbol">→</a> <a id="2251" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="2253" href="Cubical.HITs.CumulativeHierarchy.Base.html#1897" class="Bound">ℓ</a><a id="2254" class="Symbol">)</a> <a id="2256" class="Symbol">(</a><a id="2257" href="Cubical.HITs.CumulativeHierarchy.Base.html#2257" class="Bound">eq</a> <a id="2260" class="Symbol">:</a> <a id="2262" href="Cubical.HITs.CumulativeHierarchy.Base.html#1064" class="Function">eqImage</a> <a id="2270" href="Cubical.HITs.CumulativeHierarchy.Base.html#2223" class="Bound">ix₁</a> <a id="2274" href="Cubical.HITs.CumulativeHierarchy.Base.html#2240" class="Bound">ix₂</a><a id="2277" class="Symbol">)</a>
<a id="2285" class="Comment">-- ^ the structural parts of the seteq path</a>
<a id="2335" class="Symbol">→</a> <a id="2337" class="Symbol">(</a><a id="2338" href="Cubical.HITs.CumulativeHierarchy.Base.html#2338" class="Bound">rc₁</a> <a id="2342" class="Symbol">:</a> <a id="2344" class="Symbol">∀</a> <a id="2346" href="Cubical.HITs.CumulativeHierarchy.Base.html#2346" class="Bound">x₁</a> <a id="2349" class="Symbol">→</a> <a id="2351" href="Cubical.HITs.CumulativeHierarchy.Base.html#1886" class="Bound">Z</a> <a id="2353" class="Symbol">(</a><a id="2354" href="Cubical.HITs.CumulativeHierarchy.Base.html#2223" class="Bound">ix₁</a> <a id="2358" href="Cubical.HITs.CumulativeHierarchy.Base.html#2346" class="Bound">x₁</a><a id="2360" class="Symbol">))</a> <a id="2363" class="Symbol">(</a><a id="2364" href="Cubical.HITs.CumulativeHierarchy.Base.html#2364" class="Bound">rc₂</a> <a id="2368" class="Symbol">:</a> <a id="2370" class="Symbol">∀</a> <a id="2372" href="Cubical.HITs.CumulativeHierarchy.Base.html#2372" class="Bound">x₂</a> <a id="2375" class="Symbol">→</a> <a id="2377" href="Cubical.HITs.CumulativeHierarchy.Base.html#1886" class="Bound">Z</a> <a id="2379" class="Symbol">(</a><a id="2380" href="Cubical.HITs.CumulativeHierarchy.Base.html#2240" class="Bound">ix₂</a> <a id="2384" href="Cubical.HITs.CumulativeHierarchy.Base.html#2372" class="Bound">x₂</a><a id="2386" class="Symbol">))</a>
<a id="2395" class="Comment">-- ^ recursors into the elements</a>
<a id="2434" class="Symbol">→</a> <a id="2436" class="Symbol">((</a><a id="2438" href="Cubical.HITs.CumulativeHierarchy.Base.html#2438" class="Bound">x₁</a> <a id="2441" class="Symbol">:</a> <a id="2443" href="Cubical.HITs.CumulativeHierarchy.Base.html#2206" class="Bound">X₁</a><a id="2445" class="Symbol">)</a> <a id="2447" class="Symbol">→</a> <a id="2449" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="2452" href="Cubical.HITs.CumulativeHierarchy.Base.html#2452" class="Bound">(</a><a id="2453" href="Cubical.HITs.CumulativeHierarchy.Base.html#2453" class="Bound">x₂</a> <a id="2456" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="2458" href="Cubical.HITs.CumulativeHierarchy.Base.html#2458" class="Bound">p</a><a id="2459" href="Cubical.HITs.CumulativeHierarchy.Base.html#2452" class="Bound">)</a> <a id="2461" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="2463" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="2469" href="Cubical.HITs.CumulativeHierarchy.Base.html#2240" class="Bound">ix₂</a> <a id="2473" class="Symbol">(</a><a id="2474" href="Cubical.HITs.CumulativeHierarchy.Base.html#2223" class="Bound">ix₁</a> <a id="2478" href="Cubical.HITs.CumulativeHierarchy.Base.html#2438" class="Bound">x₁</a><a id="2480" class="Symbol">)</a> <a id="2482" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a> <a id="2484" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="2490" class="Symbol">(λ</a> <a id="2493" href="Cubical.HITs.CumulativeHierarchy.Base.html#2493" class="Bound">i</a> <a id="2495" class="Symbol">→</a> <a id="2497" href="Cubical.HITs.CumulativeHierarchy.Base.html#1886" class="Bound">Z</a> <a id="2499" class="Symbol">(</a><a id="2500" href="Cubical.HITs.CumulativeHierarchy.Base.html#2458" class="Bound">p</a> <a id="2502" href="Cubical.HITs.CumulativeHierarchy.Base.html#2493" class="Bound">i</a><a id="2503" class="Symbol">))</a> <a id="2506" class="Symbol">(</a><a id="2507" href="Cubical.HITs.CumulativeHierarchy.Base.html#2364" class="Bound">rc₂</a> <a id="2511" href="Cubical.HITs.CumulativeHierarchy.Base.html#2453" class="Bound">x₂</a><a id="2513" class="Symbol">)</a> <a id="2515" class="Symbol">(</a><a id="2516" href="Cubical.HITs.CumulativeHierarchy.Base.html#2338" class="Bound">rc₁</a> <a id="2520" href="Cubical.HITs.CumulativeHierarchy.Base.html#2438" class="Bound">x₁</a><a id="2522" class="Symbol">))</a>
<a id="2531" class="Symbol">→</a> <a id="2533" class="Symbol">((</a><a id="2535" href="Cubical.HITs.CumulativeHierarchy.Base.html#2535" class="Bound">x₂</a> <a id="2538" class="Symbol">:</a> <a id="2540" href="Cubical.HITs.CumulativeHierarchy.Base.html#2209" class="Bound">X₂</a><a id="2542" class="Symbol">)</a> <a id="2544" class="Symbol">→</a> <a id="2546" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="2549" href="Cubical.HITs.CumulativeHierarchy.Base.html#2549" class="Bound">(</a><a id="2550" href="Cubical.HITs.CumulativeHierarchy.Base.html#2550" class="Bound">x₁</a> <a id="2553" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="2555" href="Cubical.HITs.CumulativeHierarchy.Base.html#2555" class="Bound">p</a><a id="2556" href="Cubical.HITs.CumulativeHierarchy.Base.html#2549" class="Bound">)</a> <a id="2558" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="2560" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="2566" href="Cubical.HITs.CumulativeHierarchy.Base.html#2223" class="Bound">ix₁</a> <a id="2570" class="Symbol">(</a><a id="2571" href="Cubical.HITs.CumulativeHierarchy.Base.html#2240" class="Bound">ix₂</a> <a id="2575" href="Cubical.HITs.CumulativeHierarchy.Base.html#2535" class="Bound">x₂</a><a id="2577" class="Symbol">)</a> <a id="2579" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a> <a id="2581" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="2587" class="Symbol">(λ</a> <a id="2590" href="Cubical.HITs.CumulativeHierarchy.Base.html#2590" class="Bound">i</a> <a id="2592" class="Symbol">→</a> <a id="2594" href="Cubical.HITs.CumulativeHierarchy.Base.html#1886" class="Bound">Z</a> <a id="2596" class="Symbol">(</a><a id="2597" href="Cubical.HITs.CumulativeHierarchy.Base.html#2555" class="Bound">p</a> <a id="2599" href="Cubical.HITs.CumulativeHierarchy.Base.html#2590" class="Bound">i</a><a id="2600" class="Symbol">))</a> <a id="2603" class="Symbol">(</a><a id="2604" href="Cubical.HITs.CumulativeHierarchy.Base.html#2338" class="Bound">rc₁</a> <a id="2608" href="Cubical.HITs.CumulativeHierarchy.Base.html#2550" class="Bound">x₁</a><a id="2610" class="Symbol">)</a> <a id="2612" class="Symbol">(</a><a id="2613" href="Cubical.HITs.CumulativeHierarchy.Base.html#2364" class="Bound">rc₂</a> <a id="2617" href="Cubical.HITs.CumulativeHierarchy.Base.html#2535" class="Bound">x₂</a><a id="2619" class="Symbol">))</a>
<a id="2628" class="Comment">-- ^ proofs that the recursors have equal images</a>
<a id="2683" class="Symbol">→</a> <a id="2685" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="2691" class="Symbol">(λ</a> <a id="2694" href="Cubical.HITs.CumulativeHierarchy.Base.html#2694" class="Bound">i</a> <a id="2696" class="Symbol">→</a> <a id="2698" href="Cubical.HITs.CumulativeHierarchy.Base.html#1886" class="Bound">Z</a> <a id="2700" class="Symbol">(</a><a id="2701" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="2707" href="Cubical.HITs.CumulativeHierarchy.Base.html#2206" class="Bound">X₁</a> <a id="2710" href="Cubical.HITs.CumulativeHierarchy.Base.html#2209" class="Bound">X₂</a> <a id="2713" href="Cubical.HITs.CumulativeHierarchy.Base.html#2223" class="Bound">ix₁</a> <a id="2717" href="Cubical.HITs.CumulativeHierarchy.Base.html#2240" class="Bound">ix₂</a> <a id="2721" href="Cubical.HITs.CumulativeHierarchy.Base.html#2257" class="Bound">eq</a> <a id="2724" href="Cubical.HITs.CumulativeHierarchy.Base.html#2694" class="Bound">i</a><a id="2725" class="Symbol">))</a> <a id="2728" class="Symbol">(</a><a id="2729" href="Cubical.HITs.CumulativeHierarchy.Base.html#2001" class="Field">ElimSett</a> <a id="2738" href="Cubical.HITs.CumulativeHierarchy.Base.html#2206" class="Bound">X₁</a> <a id="2741" href="Cubical.HITs.CumulativeHierarchy.Base.html#2223" class="Bound">ix₁</a> <a id="2745" href="Cubical.HITs.CumulativeHierarchy.Base.html#2338" class="Bound">rc₁</a><a id="2748" class="Symbol">)</a> <a id="2750" class="Symbol">(</a><a id="2751" href="Cubical.HITs.CumulativeHierarchy.Base.html#2001" class="Field">ElimSett</a> <a id="2760" href="Cubical.HITs.CumulativeHierarchy.Base.html#2209" class="Bound">X₂</a> <a id="2763" href="Cubical.HITs.CumulativeHierarchy.Base.html#2240" class="Bound">ix₂</a> <a id="2767" href="Cubical.HITs.CumulativeHierarchy.Base.html#2364" class="Bound">rc₂</a><a id="2770" class="Symbol">)</a>
<a id="2773" class="Keyword">module</a> <a id="2780" href="Cubical.HITs.CumulativeHierarchy.Base.html#2780" class="Module">_</a> <a id="2782" class="Symbol">{</a><a id="2783" href="Cubical.HITs.CumulativeHierarchy.Base.html#2783" class="Bound">Z</a> <a id="2785" class="Symbol">:</a> <a id="2787" class="Symbol">(</a><a id="2788" href="Cubical.HITs.CumulativeHierarchy.Base.html#2788" class="Bound">s</a> <a id="2790" class="Symbol">:</a> <a id="2792" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="2794" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="2795" class="Symbol">)</a> <a id="2797" class="Symbol">→</a> <a id="2799" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2804" href="Cubical.HITs.CumulativeHierarchy.Base.html#880" class="Generalizable">ℓ'</a><a id="2806" class="Symbol">}</a> <a id="2808" class="Symbol">{</a><a id="2809" href="Cubical.HITs.CumulativeHierarchy.Base.html#2809" class="Bound">isSetZ</a> <a id="2816" class="Symbol">:</a> <a id="2818" class="Symbol">∀</a> <a id="2820" href="Cubical.HITs.CumulativeHierarchy.Base.html#2820" class="Bound">s</a> <a id="2822" class="Symbol">→</a> <a id="2824" href="Cubical.Foundations.Prelude.html#14094" class="Function">isSet</a> <a id="2830" class="Symbol">(</a><a id="2831" href="Cubical.HITs.CumulativeHierarchy.Base.html#2783" class="Bound">Z</a> <a id="2833" href="Cubical.HITs.CumulativeHierarchy.Base.html#2820" class="Bound">s</a><a id="2834" class="Symbol">)}</a> <a id="2837" class="Symbol">(</a><a id="2838" href="Cubical.HITs.CumulativeHierarchy.Base.html#2838" class="Bound">E</a> <a id="2840" class="Symbol">:</a> <a id="2842" href="Cubical.HITs.CumulativeHierarchy.Base.html#1877" class="Record">ElimSet</a> <a id="2850" href="Cubical.HITs.CumulativeHierarchy.Base.html#2809" class="Bound">isSetZ</a><a id="2856" class="Symbol">)</a> <a id="2858" class="Keyword">where</a>
<a id="2866" class="Keyword">open</a> <a id="2871" href="Cubical.HITs.CumulativeHierarchy.Base.html#1877" class="Module">ElimSet</a> <a id="2879" href="Cubical.HITs.CumulativeHierarchy.Base.html#2838" class="Bound">E</a>
<a id="2883" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="2888" class="Symbol">:</a> <a id="2890" class="Symbol">(</a><a id="2891" href="Cubical.HITs.CumulativeHierarchy.Base.html#2891" class="Bound">s</a> <a id="2893" class="Symbol">:</a> <a id="2895" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="2897" href="Cubical.HITs.CumulativeHierarchy.Base.html#2794" class="Bound">ℓ</a><a id="2898" class="Symbol">)</a> <a id="2900" class="Symbol">→</a> <a id="2902" href="Cubical.HITs.CumulativeHierarchy.Base.html#2783" class="Bound">Z</a> <a id="2904" href="Cubical.HITs.CumulativeHierarchy.Base.html#2891" class="Bound">s</a>
<a id="2908" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="2913" class="Symbol">(</a><a id="2914" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="2919" href="Cubical.HITs.CumulativeHierarchy.Base.html#2919" class="Bound">X</a> <a id="2921" href="Cubical.HITs.CumulativeHierarchy.Base.html#2921" class="Bound">ix</a><a id="2923" class="Symbol">)</a> <a id="2925" class="Symbol">=</a> <a id="2927" href="Cubical.HITs.CumulativeHierarchy.Base.html#2001" class="Field">ElimSett</a> <a id="2936" href="Cubical.HITs.CumulativeHierarchy.Base.html#2919" class="Bound">X</a> <a id="2938" href="Cubical.HITs.CumulativeHierarchy.Base.html#2921" class="Bound">ix</a> <a id="2941" class="Symbol">(</a><a id="2942" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="2947" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="2949" href="Cubical.HITs.CumulativeHierarchy.Base.html#2921" class="Bound">ix</a><a id="2951" class="Symbol">)</a>
<a id="2955" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="2960" class="Symbol">(</a><a id="2961" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="2967" href="Cubical.HITs.CumulativeHierarchy.Base.html#2967" class="Bound">X₁</a> <a id="2970" href="Cubical.HITs.CumulativeHierarchy.Base.html#2970" class="Bound">X₂</a> <a id="2973" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="2977" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="2981" href="Cubical.HITs.CumulativeHierarchy.Base.html#2981" class="Bound">eq</a> <a id="2984" href="Cubical.HITs.CumulativeHierarchy.Base.html#2984" class="Bound">i</a><a id="2985" class="Symbol">)</a> <a id="2987" class="Symbol">=</a>
<a id="2993" href="Cubical.HITs.CumulativeHierarchy.Base.html#2188" class="Field">ElimEq</a> <a id="3000" href="Cubical.HITs.CumulativeHierarchy.Base.html#2967" class="Bound">X₁</a> <a id="3003" href="Cubical.HITs.CumulativeHierarchy.Base.html#2970" class="Bound">X₂</a> <a id="3006" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3010" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3014" href="Cubical.HITs.CumulativeHierarchy.Base.html#2981" class="Bound">eq</a> <a id="3017" class="Symbol">(</a><a id="3018" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3023" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="3025" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a><a id="3028" class="Symbol">)</a> <a id="3030" class="Symbol">(</a><a id="3031" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3036" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="3038" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a><a id="3041" class="Symbol">)</a> <a id="3043" href="Cubical.HITs.CumulativeHierarchy.Base.html#3073" class="Function">rec₁→₂</a> <a id="3050" href="Cubical.HITs.CumulativeHierarchy.Base.html#3201" class="Function">rec₂→₁</a> <a id="3057" href="Cubical.HITs.CumulativeHierarchy.Base.html#2984" class="Bound">i</a>
<a id="3063" class="Keyword">where</a>
<a id="3073" href="Cubical.HITs.CumulativeHierarchy.Base.html#3073" class="Function">rec₁→₂</a> <a id="3080" class="Symbol">:</a>
<a id="3088" class="Symbol">∀</a> <a id="3090" class="Symbol">(</a><a id="3091" href="Cubical.HITs.CumulativeHierarchy.Base.html#3091" class="Bound">x₁</a> <a id="3094" class="Symbol">:</a> <a id="3096" href="Cubical.HITs.CumulativeHierarchy.Base.html#2967" class="Bound">X₁</a><a id="3098" class="Symbol">)</a>
<a id="3106" class="Symbol">→</a> <a id="3108" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="3111" href="Cubical.HITs.CumulativeHierarchy.Base.html#3111" class="Bound">(</a><a id="3112" href="Cubical.HITs.CumulativeHierarchy.Base.html#3112" class="Bound">x₂</a> <a id="3115" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3117" href="Cubical.HITs.CumulativeHierarchy.Base.html#3117" class="Bound">p</a><a id="3118" href="Cubical.HITs.CumulativeHierarchy.Base.html#3111" class="Bound">)</a> <a id="3120" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="3122" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="3128" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3132" class="Symbol">(</a><a id="3133" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3137" href="Cubical.HITs.CumulativeHierarchy.Base.html#3091" class="Bound">x₁</a><a id="3139" class="Symbol">)</a> <a id="3141" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a> <a id="3143" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="3149" class="Symbol">(λ</a> <a id="3152" href="Cubical.HITs.CumulativeHierarchy.Base.html#3152" class="Bound">i</a> <a id="3154" class="Symbol">→</a> <a id="3156" href="Cubical.HITs.CumulativeHierarchy.Base.html#2783" class="Bound">Z</a> <a id="3158" class="Symbol">(</a><a id="3159" href="Cubical.HITs.CumulativeHierarchy.Base.html#3117" class="Bound">p</a> <a id="3161" href="Cubical.HITs.CumulativeHierarchy.Base.html#3152" class="Bound">i</a><a id="3162" class="Symbol">))</a> <a id="3165" class="Symbol">(</a><a id="3166" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3171" class="Symbol">(</a><a id="3172" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3176" href="Cubical.HITs.CumulativeHierarchy.Base.html#3112" class="Bound">x₂</a><a id="3178" class="Symbol">))</a> <a id="3181" class="Symbol">(</a><a id="3182" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3187" class="Symbol">(</a><a id="3188" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3192" href="Cubical.HITs.CumulativeHierarchy.Base.html#3091" class="Bound">x₁</a><a id="3194" class="Symbol">))</a>
<a id="3201" href="Cubical.HITs.CumulativeHierarchy.Base.html#3201" class="Function">rec₂→₁</a> <a id="3208" class="Symbol">:</a>
<a id="3216" class="Symbol">∀</a> <a id="3218" class="Symbol">(</a><a id="3219" href="Cubical.HITs.CumulativeHierarchy.Base.html#3219" class="Bound">x₂</a> <a id="3222" class="Symbol">:</a> <a id="3224" href="Cubical.HITs.CumulativeHierarchy.Base.html#2970" class="Bound">X₂</a><a id="3226" class="Symbol">)</a>
<a id="3234" class="Symbol">→</a> <a id="3236" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="3239" href="Cubical.HITs.CumulativeHierarchy.Base.html#3239" class="Bound">(</a><a id="3240" href="Cubical.HITs.CumulativeHierarchy.Base.html#3240" class="Bound">x₁</a> <a id="3243" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3245" href="Cubical.HITs.CumulativeHierarchy.Base.html#3245" class="Bound">p</a><a id="3246" href="Cubical.HITs.CumulativeHierarchy.Base.html#3239" class="Bound">)</a> <a id="3248" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="3250" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="3256" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3260" class="Symbol">(</a><a id="3261" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3265" href="Cubical.HITs.CumulativeHierarchy.Base.html#3219" class="Bound">x₂</a><a id="3267" class="Symbol">)</a> <a id="3269" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a> <a id="3271" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="3277" class="Symbol">(λ</a> <a id="3280" href="Cubical.HITs.CumulativeHierarchy.Base.html#3280" class="Bound">i</a> <a id="3282" class="Symbol">→</a> <a id="3284" href="Cubical.HITs.CumulativeHierarchy.Base.html#2783" class="Bound">Z</a> <a id="3286" class="Symbol">(</a><a id="3287" href="Cubical.HITs.CumulativeHierarchy.Base.html#3245" class="Bound">p</a> <a id="3289" href="Cubical.HITs.CumulativeHierarchy.Base.html#3280" class="Bound">i</a><a id="3290" class="Symbol">))</a> <a id="3293" class="Symbol">(</a><a id="3294" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3299" class="Symbol">(</a><a id="3300" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3304" href="Cubical.HITs.CumulativeHierarchy.Base.html#3240" class="Bound">x₁</a><a id="3306" class="Symbol">))</a> <a id="3309" class="Symbol">(</a><a id="3310" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3315" class="Symbol">(</a><a id="3316" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3320" href="Cubical.HITs.CumulativeHierarchy.Base.html#3219" class="Bound">x₂</a><a id="3322" class="Symbol">))</a>
<a id="3329" class="Comment">-- using a local definition of Prop.rec satisfies the termination checker</a>
<a id="3407" href="Cubical.HITs.CumulativeHierarchy.Base.html#3073" class="Function">rec₁→₂</a> <a id="3414" href="Cubical.HITs.CumulativeHierarchy.Base.html#3414" class="Bound">x₁</a> <a id="3417" class="Symbol">=</a> <a id="3419" href="Cubical.HITs.CumulativeHierarchy.Base.html#3454" class="Function">localRec₁</a> <a id="3429" class="Symbol">(</a><a id="3430" href="Cubical.HITs.CumulativeHierarchy.Base.html#2981" class="Bound">eq</a> <a id="3433" class="Symbol">.</a><a id="3434" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="3438" href="Cubical.HITs.CumulativeHierarchy.Base.html#3414" class="Bound">x₁</a><a id="3440" class="Symbol">)</a> <a id="3442" class="Keyword">where</a>
<a id="3454" href="Cubical.HITs.CumulativeHierarchy.Base.html#3454" class="Function">localRec₁</a> <a id="3464" class="Symbol">:</a>
<a id="3476" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="3478" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="3484" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3488" class="Symbol">(</a><a id="3489" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3493" href="Cubical.HITs.CumulativeHierarchy.Base.html#3414" class="Bound">x₁</a><a id="3495" class="Symbol">)</a> <a id="3497" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a>
<a id="3508" class="Symbol">→</a> <a id="3510" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="3513" href="Cubical.HITs.CumulativeHierarchy.Base.html#3513" class="Bound">(</a><a id="3514" href="Cubical.HITs.CumulativeHierarchy.Base.html#3514" class="Bound">x₂</a> <a id="3517" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3519" href="Cubical.HITs.CumulativeHierarchy.Base.html#3519" class="Bound">p</a><a id="3520" href="Cubical.HITs.CumulativeHierarchy.Base.html#3513" class="Bound">)</a> <a id="3522" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="3524" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="3530" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3534" class="Symbol">(</a><a id="3535" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3539" href="Cubical.HITs.CumulativeHierarchy.Base.html#3414" class="Bound">x₁</a><a id="3541" class="Symbol">)</a> <a id="3543" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a> <a id="3545" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="3551" class="Symbol">(λ</a> <a id="3554" href="Cubical.HITs.CumulativeHierarchy.Base.html#3554" class="Bound">i</a> <a id="3556" class="Symbol">→</a> <a id="3558" href="Cubical.HITs.CumulativeHierarchy.Base.html#2783" class="Bound">Z</a> <a id="3560" class="Symbol">(</a><a id="3561" href="Cubical.HITs.CumulativeHierarchy.Base.html#3519" class="Bound">p</a> <a id="3563" href="Cubical.HITs.CumulativeHierarchy.Base.html#3554" class="Bound">i</a><a id="3564" class="Symbol">))</a> <a id="3567" class="Symbol">(</a><a id="3568" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3573" class="Symbol">(</a><a id="3574" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3578" href="Cubical.HITs.CumulativeHierarchy.Base.html#3514" class="Bound">x₂</a><a id="3580" class="Symbol">))</a> <a id="3583" class="Symbol">(</a><a id="3584" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3589" class="Symbol">(</a><a id="3590" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3594" href="Cubical.HITs.CumulativeHierarchy.Base.html#3414" class="Bound">x₁</a><a id="3596" class="Symbol">))</a>
<a id="3605" href="Cubical.HITs.CumulativeHierarchy.Base.html#3454" class="Function">localRec₁</a> <a id="3615" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="3617" href="Cubical.HITs.CumulativeHierarchy.Base.html#3617" class="Bound">x₂</a> <a id="3620" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3622" href="Cubical.HITs.CumulativeHierarchy.Base.html#3622" class="Bound">xx</a> <a id="3625" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a> <a id="3628" class="Symbol">=</a> <a id="3630" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="3632" class="Symbol">(</a><a id="3633" href="Cubical.HITs.CumulativeHierarchy.Base.html#3617" class="Bound">x₂</a> <a id="3636" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3638" href="Cubical.HITs.CumulativeHierarchy.Base.html#3622" class="Bound">xx</a><a id="3640" class="Symbol">)</a> <a id="3642" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3644" class="Symbol">(λ</a> <a id="3647" href="Cubical.HITs.CumulativeHierarchy.Base.html#3647" class="Bound">i</a> <a id="3649" class="Symbol">→</a> <a id="3651" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3656" class="Symbol">(</a><a id="3657" href="Cubical.HITs.CumulativeHierarchy.Base.html#3622" class="Bound">xx</a> <a id="3660" href="Cubical.HITs.CumulativeHierarchy.Base.html#3647" class="Bound">i</a><a id="3661" class="Symbol">))</a> <a id="3664" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a>
<a id="3673" href="Cubical.HITs.CumulativeHierarchy.Base.html#3454" class="Function">localRec₁</a> <a id="3683" class="Symbol">(</a><a id="3684" href="Cubical.HITs.PropositionalTruncation.Base.html#308" class="InductiveConstructor">squash₁</a> <a id="3692" href="Cubical.HITs.CumulativeHierarchy.Base.html#3692" class="Bound">x</a> <a id="3694" href="Cubical.HITs.CumulativeHierarchy.Base.html#3694" class="Bound">y</a> <a id="3696" href="Cubical.HITs.CumulativeHierarchy.Base.html#3696" class="Bound">i</a><a id="3697" class="Symbol">)</a> <a id="3699" class="Symbol">=</a> <a id="3701" href="Cubical.HITs.PropositionalTruncation.Base.html#308" class="InductiveConstructor">squash₁</a> <a id="3709" class="Symbol">(</a><a id="3710" href="Cubical.HITs.CumulativeHierarchy.Base.html#3454" class="Function">localRec₁</a> <a id="3720" href="Cubical.HITs.CumulativeHierarchy.Base.html#3692" class="Bound">x</a><a id="3721" class="Symbol">)</a> <a id="3723" class="Symbol">(</a><a id="3724" href="Cubical.HITs.CumulativeHierarchy.Base.html#3454" class="Function">localRec₁</a> <a id="3734" href="Cubical.HITs.CumulativeHierarchy.Base.html#3694" class="Bound">y</a><a id="3735" class="Symbol">)</a> <a id="3737" href="Cubical.HITs.CumulativeHierarchy.Base.html#3696" class="Bound">i</a>
<a id="3743" href="Cubical.HITs.CumulativeHierarchy.Base.html#3201" class="Function">rec₂→₁</a> <a id="3750" href="Cubical.HITs.CumulativeHierarchy.Base.html#3750" class="Bound">x₂</a> <a id="3753" class="Symbol">=</a> <a id="3755" href="Cubical.HITs.CumulativeHierarchy.Base.html#3790" class="Function">localRec₂</a> <a id="3765" class="Symbol">(</a><a id="3766" href="Cubical.HITs.CumulativeHierarchy.Base.html#2981" class="Bound">eq</a> <a id="3769" class="Symbol">.</a><a id="3770" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="3774" href="Cubical.HITs.CumulativeHierarchy.Base.html#3750" class="Bound">x₂</a><a id="3776" class="Symbol">)</a> <a id="3778" class="Keyword">where</a>
<a id="3790" href="Cubical.HITs.CumulativeHierarchy.Base.html#3790" class="Function">localRec₂</a> <a id="3800" class="Symbol">:</a>
<a id="3812" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="3814" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="3820" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3824" class="Symbol">(</a><a id="3825" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3829" href="Cubical.HITs.CumulativeHierarchy.Base.html#3750" class="Bound">x₂</a><a id="3831" class="Symbol">)</a> <a id="3833" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a>
<a id="3844" class="Symbol">→</a> <a id="3846" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="3849" href="Cubical.HITs.CumulativeHierarchy.Base.html#3849" class="Bound">(</a><a id="3850" href="Cubical.HITs.CumulativeHierarchy.Base.html#3850" class="Bound">x₁</a> <a id="3853" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3855" href="Cubical.HITs.CumulativeHierarchy.Base.html#3855" class="Bound">p</a><a id="3856" href="Cubical.HITs.CumulativeHierarchy.Base.html#3849" class="Bound">)</a> <a id="3858" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="3860" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="3866" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3870" class="Symbol">(</a><a id="3871" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3875" href="Cubical.HITs.CumulativeHierarchy.Base.html#3750" class="Bound">x₂</a><a id="3877" class="Symbol">)</a> <a id="3879" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a> <a id="3881" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="3887" class="Symbol">(λ</a> <a id="3890" href="Cubical.HITs.CumulativeHierarchy.Base.html#3890" class="Bound">i</a> <a id="3892" class="Symbol">→</a> <a id="3894" href="Cubical.HITs.CumulativeHierarchy.Base.html#2783" class="Bound">Z</a> <a id="3896" class="Symbol">(</a><a id="3897" href="Cubical.HITs.CumulativeHierarchy.Base.html#3855" class="Bound">p</a> <a id="3899" href="Cubical.HITs.CumulativeHierarchy.Base.html#3890" class="Bound">i</a><a id="3900" class="Symbol">))</a> <a id="3903" class="Symbol">(</a><a id="3904" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3909" class="Symbol">(</a><a id="3910" href="Cubical.HITs.CumulativeHierarchy.Base.html#2973" class="Bound">ix₁</a> <a id="3914" href="Cubical.HITs.CumulativeHierarchy.Base.html#3850" class="Bound">x₁</a><a id="3916" class="Symbol">))</a> <a id="3919" class="Symbol">(</a><a id="3920" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3925" class="Symbol">(</a><a id="3926" href="Cubical.HITs.CumulativeHierarchy.Base.html#2977" class="Bound">ix₂</a> <a id="3930" href="Cubical.HITs.CumulativeHierarchy.Base.html#3750" class="Bound">x₂</a><a id="3932" class="Symbol">))</a>
<a id="3941" href="Cubical.HITs.CumulativeHierarchy.Base.html#3790" class="Function">localRec₂</a> <a id="3951" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="3953" href="Cubical.HITs.CumulativeHierarchy.Base.html#3953" class="Bound">x₁</a> <a id="3956" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3958" href="Cubical.HITs.CumulativeHierarchy.Base.html#3958" class="Bound">xx</a> <a id="3961" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a> <a id="3964" class="Symbol">=</a> <a id="3966" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="3968" class="Symbol">(</a><a id="3969" href="Cubical.HITs.CumulativeHierarchy.Base.html#3953" class="Bound">x₁</a> <a id="3972" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3974" href="Cubical.HITs.CumulativeHierarchy.Base.html#3958" class="Bound">xx</a><a id="3976" class="Symbol">)</a> <a id="3978" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3980" class="Symbol">(λ</a> <a id="3983" href="Cubical.HITs.CumulativeHierarchy.Base.html#3983" class="Bound">i</a> <a id="3985" class="Symbol">→</a> <a id="3987" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="3992" class="Symbol">(</a><a id="3993" href="Cubical.HITs.CumulativeHierarchy.Base.html#3958" class="Bound">xx</a> <a id="3996" href="Cubical.HITs.CumulativeHierarchy.Base.html#3983" class="Bound">i</a><a id="3997" class="Symbol">))</a> <a id="4000" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a>
<a id="4009" href="Cubical.HITs.CumulativeHierarchy.Base.html#3790" class="Function">localRec₂</a> <a id="4019" class="Symbol">(</a><a id="4020" href="Cubical.HITs.PropositionalTruncation.Base.html#308" class="InductiveConstructor">squash₁</a> <a id="4028" href="Cubical.HITs.CumulativeHierarchy.Base.html#4028" class="Bound">x</a> <a id="4030" href="Cubical.HITs.CumulativeHierarchy.Base.html#4030" class="Bound">y</a> <a id="4032" href="Cubical.HITs.CumulativeHierarchy.Base.html#4032" class="Bound">i</a><a id="4033" class="Symbol">)</a> <a id="4035" class="Symbol">=</a> <a id="4037" href="Cubical.HITs.PropositionalTruncation.Base.html#308" class="InductiveConstructor">squash₁</a> <a id="4045" class="Symbol">(</a><a id="4046" href="Cubical.HITs.CumulativeHierarchy.Base.html#3790" class="Function">localRec₂</a> <a id="4056" href="Cubical.HITs.CumulativeHierarchy.Base.html#4028" class="Bound">x</a><a id="4057" class="Symbol">)</a> <a id="4059" class="Symbol">(</a><a id="4060" href="Cubical.HITs.CumulativeHierarchy.Base.html#3790" class="Function">localRec₂</a> <a id="4070" href="Cubical.HITs.CumulativeHierarchy.Base.html#4030" class="Bound">y</a><a id="4071" class="Symbol">)</a> <a id="4073" href="Cubical.HITs.CumulativeHierarchy.Base.html#4032" class="Bound">i</a>
<a id="4077" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="4082" class="Symbol">(</a><a id="4083" href="Cubical.HITs.CumulativeHierarchy.Base.html#1431" class="InductiveConstructor">setIsSet</a> <a id="4092" href="Cubical.HITs.CumulativeHierarchy.Base.html#4092" class="Bound">S</a> <a id="4094" href="Cubical.HITs.CumulativeHierarchy.Base.html#4094" class="Bound">T</a> <a id="4096" href="Cubical.HITs.CumulativeHierarchy.Base.html#4096" class="Bound">x</a> <a id="4098" href="Cubical.HITs.CumulativeHierarchy.Base.html#4098" class="Bound">y</a> <a id="4100" href="Cubical.HITs.CumulativeHierarchy.Base.html#4100" class="Bound">i</a> <a id="4102" href="Cubical.HITs.CumulativeHierarchy.Base.html#4102" class="Bound">j</a><a id="4103" class="Symbol">)</a> <a id="4105" class="Symbol">=</a> <a id="4107" href="Cubical.Foundations.Prelude.html#17730" class="Function">isProp→PathP</a> <a id="4120" href="Cubical.HITs.CumulativeHierarchy.Base.html#4172" class="Function">propPathP</a> <a id="4130" class="Symbol">(</a><a id="4131" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="4136" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="4141" href="Cubical.HITs.CumulativeHierarchy.Base.html#4096" class="Bound">x</a><a id="4142" class="Symbol">)</a> <a id="4144" class="Symbol">(</a><a id="4145" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="4150" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="4155" href="Cubical.HITs.CumulativeHierarchy.Base.html#4098" class="Bound">y</a><a id="4156" class="Symbol">)</a> <a id="4158" href="Cubical.HITs.CumulativeHierarchy.Base.html#4100" class="Bound">i</a> <a id="4160" href="Cubical.HITs.CumulativeHierarchy.Base.html#4102" class="Bound">j</a> <a id="4162" class="Keyword">where</a>
<a id="4172" href="Cubical.HITs.CumulativeHierarchy.Base.html#4172" class="Function">propPathP</a> <a id="4182" class="Symbol">:</a> <a id="4184" class="Symbol">(</a><a id="4185" href="Cubical.HITs.CumulativeHierarchy.Base.html#4185" class="Bound">i</a> <a id="4187" class="Symbol">:</a> <a id="4189" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="4190" class="Symbol">)</a> <a id="4192" class="Symbol">→</a> <a id="4194" href="Cubical.Foundations.Prelude.html#14039" class="Function">isProp</a> <a id="4201" class="Symbol">(</a><a id="4202" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="4208" class="Symbol">(λ</a> <a id="4211" href="Cubical.HITs.CumulativeHierarchy.Base.html#4211" class="Bound">j</a> <a id="4213" class="Symbol">→</a> <a id="4215" href="Cubical.HITs.CumulativeHierarchy.Base.html#2783" class="Bound">Z</a> <a id="4217" class="Symbol">(</a><a id="4218" href="Cubical.HITs.CumulativeHierarchy.Base.html#1431" class="InductiveConstructor">setIsSet</a> <a id="4227" href="Cubical.HITs.CumulativeHierarchy.Base.html#4092" class="Bound">S</a> <a id="4229" href="Cubical.HITs.CumulativeHierarchy.Base.html#4094" class="Bound">T</a> <a id="4231" href="Cubical.HITs.CumulativeHierarchy.Base.html#4096" class="Bound">x</a> <a id="4233" href="Cubical.HITs.CumulativeHierarchy.Base.html#4098" class="Bound">y</a> <a id="4235" href="Cubical.HITs.CumulativeHierarchy.Base.html#4185" class="Bound">i</a> <a id="4237" href="Cubical.HITs.CumulativeHierarchy.Base.html#4211" class="Bound">j</a><a id="4238" class="Symbol">))</a> <a id="4241" class="Symbol">(</a><a id="4242" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="4247" href="Cubical.HITs.CumulativeHierarchy.Base.html#4092" class="Bound">S</a><a id="4248" class="Symbol">)</a> <a id="4250" class="Symbol">(</a><a id="4251" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="4256" href="Cubical.HITs.CumulativeHierarchy.Base.html#4094" class="Bound">T</a><a id="4257" class="Symbol">))</a>
<a id="4264" href="Cubical.HITs.CumulativeHierarchy.Base.html#4172" class="Function">propPathP</a> <a id="4274" class="Symbol">_</a> <a id="4276" class="Symbol">=</a> <a id="4278" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="4284" href="Cubical.Foundations.Prelude.html#14039" class="Function">isProp</a> <a id="4291" class="Symbol">(</a><a id="4292" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="4296" class="Symbol">(</a><a id="4297" href="Cubical.Foundations.Path.html#917" class="Function">PathP≡Path</a> <a id="4308" class="Symbol">_</a> <a id="4310" class="Symbol">_</a> <a id="4312" class="Symbol">_))</a> <a id="4316" class="Symbol">(</a><a id="4317" href="Cubical.HITs.CumulativeHierarchy.Base.html#2809" class="Bound">isSetZ</a> <a id="4324" class="Symbol">_</a> <a id="4326" class="Symbol">_</a> <a id="4328" class="Symbol">_)</a>
<a id="4332" class="Comment">-- eliminator into propositions</a>
<a id="elimProp"></a><a id="4364" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="4373" class="Symbol">:</a> <a id="4375" class="Symbol">{</a><a id="4376" href="Cubical.HITs.CumulativeHierarchy.Base.html#4376" class="Bound">Z</a> <a id="4378" class="Symbol">:</a> <a id="4380" class="Symbol">(</a><a id="4381" href="Cubical.HITs.CumulativeHierarchy.Base.html#4381" class="Bound">s</a> <a id="4383" class="Symbol">:</a> <a id="4385" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="4387" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="4388" class="Symbol">)</a> <a id="4390" class="Symbol">→</a> <a id="4392" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="4397" href="Cubical.HITs.CumulativeHierarchy.Base.html#880" class="Generalizable">ℓ'</a><a id="4399" class="Symbol">}</a> <a id="4401" class="Symbol">(</a><a id="4402" href="Cubical.HITs.CumulativeHierarchy.Base.html#4402" class="Bound">isPropZ</a> <a id="4410" class="Symbol">:</a> <a id="4412" class="Symbol">∀</a> <a id="4414" href="Cubical.HITs.CumulativeHierarchy.Base.html#4414" class="Bound">s</a> <a id="4416" class="Symbol">→</a> <a id="4418" href="Cubical.Foundations.Prelude.html#14039" class="Function">isProp</a> <a id="4425" class="Symbol">(</a><a id="4426" href="Cubical.HITs.CumulativeHierarchy.Base.html#4376" class="Bound">Z</a> <a id="4428" href="Cubical.HITs.CumulativeHierarchy.Base.html#4414" class="Bound">s</a><a id="4429" class="Symbol">))</a>
<a id="4441" class="Symbol">→</a> <a id="4443" class="Symbol">((</a><a id="4445" href="Cubical.HITs.CumulativeHierarchy.Base.html#4445" class="Bound">X</a> <a id="4447" class="Symbol">:</a> <a id="4449" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="4454" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="4455" class="Symbol">)</a> <a id="4457" class="Symbol">→</a> <a id="4459" class="Symbol">(</a><a id="4460" href="Cubical.HITs.CumulativeHierarchy.Base.html#4460" class="Bound">ix</a> <a id="4463" class="Symbol">:</a> <a id="4465" href="Cubical.HITs.CumulativeHierarchy.Base.html#4445" class="Bound">X</a> <a id="4467" class="Symbol">→</a> <a id="4469" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="4471" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="4472" class="Symbol">)</a> <a id="4474" class="Symbol">→</a> <a id="4476" class="Symbol">(∀</a> <a id="4479" href="Cubical.HITs.CumulativeHierarchy.Base.html#4479" class="Bound">x</a> <a id="4481" class="Symbol">→</a> <a id="4483" href="Cubical.HITs.CumulativeHierarchy.Base.html#4376" class="Bound">Z</a> <a id="4485" class="Symbol">(</a><a id="4486" href="Cubical.HITs.CumulativeHierarchy.Base.html#4460" class="Bound">ix</a> <a id="4489" href="Cubical.HITs.CumulativeHierarchy.Base.html#4479" class="Bound">x</a><a id="4490" class="Symbol">))</a> <a id="4493" class="Symbol">→</a> <a id="4495" href="Cubical.HITs.CumulativeHierarchy.Base.html#4376" class="Bound">Z</a> <a id="4497" class="Symbol">(</a><a id="4498" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="4503" href="Cubical.HITs.CumulativeHierarchy.Base.html#4445" class="Bound">X</a> <a id="4505" href="Cubical.HITs.CumulativeHierarchy.Base.html#4460" class="Bound">ix</a><a id="4507" class="Symbol">))</a>
<a id="4519" class="Symbol">→</a> <a id="4521" class="Symbol">(</a><a id="4522" href="Cubical.HITs.CumulativeHierarchy.Base.html#4522" class="Bound">s</a> <a id="4524" class="Symbol">:</a> <a id="4526" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="4528" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="4529" class="Symbol">)</a> <a id="4531" class="Symbol">→</a> <a id="4533" href="Cubical.HITs.CumulativeHierarchy.Base.html#4376" class="Bound">Z</a> <a id="4535" href="Cubical.HITs.CumulativeHierarchy.Base.html#4522" class="Bound">s</a>
<a id="4537" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="4546" href="Cubical.HITs.CumulativeHierarchy.Base.html#4546" class="Bound">isPropZ</a> <a id="4554" href="Cubical.HITs.CumulativeHierarchy.Base.html#4554" class="Bound">algz</a> <a id="4559" class="Symbol">(</a><a id="4560" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="4565" href="Cubical.HITs.CumulativeHierarchy.Base.html#4565" class="Bound">X</a> <a id="4567" href="Cubical.HITs.CumulativeHierarchy.Base.html#4567" class="Bound">ix</a><a id="4569" class="Symbol">)</a> <a id="4571" class="Symbol">=</a> <a id="4573" href="Cubical.HITs.CumulativeHierarchy.Base.html#4554" class="Bound">algz</a> <a id="4578" href="Cubical.HITs.CumulativeHierarchy.Base.html#4565" class="Bound">X</a> <a id="4580" href="Cubical.HITs.CumulativeHierarchy.Base.html#4567" class="Bound">ix</a> <a id="4583" class="Symbol">(λ</a> <a id="4586" href="Cubical.HITs.CumulativeHierarchy.Base.html#4586" class="Bound">x</a> <a id="4588" class="Symbol">→</a> <a id="4590" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="4599" href="Cubical.HITs.CumulativeHierarchy.Base.html#4546" class="Bound">isPropZ</a> <a id="4607" href="Cubical.HITs.CumulativeHierarchy.Base.html#4554" class="Bound">algz</a> <a id="4612" class="Symbol">(</a><a id="4613" href="Cubical.HITs.CumulativeHierarchy.Base.html#4567" class="Bound">ix</a> <a id="4616" href="Cubical.HITs.CumulativeHierarchy.Base.html#4586" class="Bound">x</a><a id="4617" class="Symbol">))</a>
<a id="4620" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="4629" href="Cubical.HITs.CumulativeHierarchy.Base.html#4629" class="Bound">isPropZ</a> <a id="4637" href="Cubical.HITs.CumulativeHierarchy.Base.html#4637" class="Bound">algz</a> <a id="4642" class="Symbol">(</a><a id="4643" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="4649" href="Cubical.HITs.CumulativeHierarchy.Base.html#4649" class="Bound">X</a> <a id="4651" href="Cubical.HITs.CumulativeHierarchy.Base.html#4651" class="Bound">Y</a> <a id="4653" href="Cubical.HITs.CumulativeHierarchy.Base.html#4653" class="Bound">ix</a> <a id="4656" href="Cubical.HITs.CumulativeHierarchy.Base.html#4656" class="Bound">iy</a> <a id="4659" href="Cubical.HITs.CumulativeHierarchy.Base.html#4659" class="Bound">eq</a> <a id="4662" href="Cubical.HITs.CumulativeHierarchy.Base.html#4662" class="Bound">i</a><a id="4663" class="Symbol">)</a> <a id="4665" class="Symbol">=</a>
<a id="4669" href="Cubical.Foundations.Prelude.html#17730" class="Function">isProp→PathP</a> <a id="4682" class="Symbol">(λ</a> <a id="4685" href="Cubical.HITs.CumulativeHierarchy.Base.html#4685" class="Bound">i</a> <a id="4687" class="Symbol">→</a> <a id="4689" href="Cubical.HITs.CumulativeHierarchy.Base.html#4629" class="Bound">isPropZ</a> <a id="4697" class="Symbol">(</a><a id="4698" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="4704" href="Cubical.HITs.CumulativeHierarchy.Base.html#4649" class="Bound">X</a> <a id="4706" href="Cubical.HITs.CumulativeHierarchy.Base.html#4651" class="Bound">Y</a> <a id="4708" href="Cubical.HITs.CumulativeHierarchy.Base.html#4653" class="Bound">ix</a> <a id="4711" href="Cubical.HITs.CumulativeHierarchy.Base.html#4656" class="Bound">iy</a> <a id="4714" href="Cubical.HITs.CumulativeHierarchy.Base.html#4659" class="Bound">eq</a> <a id="4717" href="Cubical.HITs.CumulativeHierarchy.Base.html#4685" class="Bound">i</a><a id="4718" class="Symbol">))</a>
<a id="4736" class="Symbol">(</a><a id="4737" href="Cubical.HITs.CumulativeHierarchy.Base.html#4637" class="Bound">algz</a> <a id="4742" href="Cubical.HITs.CumulativeHierarchy.Base.html#4649" class="Bound">X</a> <a id="4744" href="Cubical.HITs.CumulativeHierarchy.Base.html#4653" class="Bound">ix</a> <a id="4747" class="Symbol">(</a><a id="4748" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="4757" href="Cubical.HITs.CumulativeHierarchy.Base.html#4629" class="Bound">isPropZ</a> <a id="4765" href="Cubical.HITs.CumulativeHierarchy.Base.html#4637" class="Bound">algz</a> <a id="4770" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="4772" href="Cubical.HITs.CumulativeHierarchy.Base.html#4653" class="Bound">ix</a><a id="4774" class="Symbol">))</a>
<a id="4792" class="Symbol">(</a><a id="4793" href="Cubical.HITs.CumulativeHierarchy.Base.html#4637" class="Bound">algz</a> <a id="4798" href="Cubical.HITs.CumulativeHierarchy.Base.html#4651" class="Bound">Y</a> <a id="4800" href="Cubical.HITs.CumulativeHierarchy.Base.html#4656" class="Bound">iy</a> <a id="4803" class="Symbol">(</a><a id="4804" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="4813" href="Cubical.HITs.CumulativeHierarchy.Base.html#4629" class="Bound">isPropZ</a> <a id="4821" href="Cubical.HITs.CumulativeHierarchy.Base.html#4637" class="Bound">algz</a> <a id="4826" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="4828" href="Cubical.HITs.CumulativeHierarchy.Base.html#4656" class="Bound">iy</a><a id="4830" class="Symbol">))</a> <a id="4833" href="Cubical.HITs.CumulativeHierarchy.Base.html#4662" class="Bound">i</a>
<a id="4835" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="4844" href="Cubical.HITs.CumulativeHierarchy.Base.html#4844" class="Bound">isPropZ</a> <a id="4852" href="Cubical.HITs.CumulativeHierarchy.Base.html#4852" class="Bound">algz</a> <a id="4857" class="Symbol">(</a><a id="4858" href="Cubical.HITs.CumulativeHierarchy.Base.html#1431" class="InductiveConstructor">setIsSet</a> <a id="4867" href="Cubical.HITs.CumulativeHierarchy.Base.html#4867" class="Bound">S</a> <a id="4869" href="Cubical.HITs.CumulativeHierarchy.Base.html#4869" class="Bound">T</a> <a id="4871" href="Cubical.HITs.CumulativeHierarchy.Base.html#4871" class="Bound">x</a> <a id="4873" href="Cubical.HITs.CumulativeHierarchy.Base.html#4873" class="Bound">y</a> <a id="4875" href="Cubical.HITs.CumulativeHierarchy.Base.html#4875" class="Bound">i</a> <a id="4877" href="Cubical.HITs.CumulativeHierarchy.Base.html#4877" class="Bound">j</a><a id="4878" class="Symbol">)</a> <a id="4880" class="Symbol">=</a>
<a id="4884" href="Cubical.Foundations.Path.html#5314" class="Function">isProp→SquareP</a> <a id="4899" class="Symbol">(λ</a> <a id="4902" href="Cubical.HITs.CumulativeHierarchy.Base.html#4902" class="Bound">i</a> <a id="4904" href="Cubical.HITs.CumulativeHierarchy.Base.html#4904" class="Bound">j</a> <a id="4906" class="Symbol">→</a> <a id="4908" href="Cubical.HITs.CumulativeHierarchy.Base.html#4844" class="Bound">isPropZ</a> <a id="4916" class="Symbol">(</a><a id="4917" href="Cubical.HITs.CumulativeHierarchy.Base.html#1431" class="InductiveConstructor">setIsSet</a> <a id="4926" href="Cubical.HITs.CumulativeHierarchy.Base.html#4867" class="Bound">S</a> <a id="4928" href="Cubical.HITs.CumulativeHierarchy.Base.html#4869" class="Bound">T</a> <a id="4930" href="Cubical.HITs.CumulativeHierarchy.Base.html#4871" class="Bound">x</a> <a id="4932" href="Cubical.HITs.CumulativeHierarchy.Base.html#4873" class="Bound">y</a> <a id="4934" href="Cubical.HITs.CumulativeHierarchy.Base.html#4902" class="Bound">i</a> <a id="4936" href="Cubical.HITs.CumulativeHierarchy.Base.html#4904" class="Bound">j</a><a id="4937" class="Symbol">))</a>
<a id="4957" class="Symbol">(λ</a> <a id="4960" href="Cubical.HITs.CumulativeHierarchy.Base.html#4960" class="Bound">_</a> <a id="4962" class="Symbol">→</a> <a id="4964" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="4973" href="Cubical.HITs.CumulativeHierarchy.Base.html#4844" class="Bound">isPropZ</a> <a id="4981" href="Cubical.HITs.CumulativeHierarchy.Base.html#4852" class="Bound">algz</a> <a id="4986" href="Cubical.HITs.CumulativeHierarchy.Base.html#4867" class="Bound">S</a><a id="4987" class="Symbol">)</a>
<a id="5006" class="Symbol">(λ</a> <a id="5009" href="Cubical.HITs.CumulativeHierarchy.Base.html#5009" class="Bound">_</a> <a id="5011" class="Symbol">→</a> <a id="5013" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="5022" href="Cubical.HITs.CumulativeHierarchy.Base.html#4844" class="Bound">isPropZ</a> <a id="5030" href="Cubical.HITs.CumulativeHierarchy.Base.html#4852" class="Bound">algz</a> <a id="5035" href="Cubical.HITs.CumulativeHierarchy.Base.html#4869" class="Bound">T</a><a id="5036" class="Symbol">)</a>
<a id="5055" class="Symbol">(</a><a id="5056" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="5061" class="Symbol">(</a><a id="5062" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="5071" href="Cubical.HITs.CumulativeHierarchy.Base.html#4844" class="Bound">isPropZ</a> <a id="5079" href="Cubical.HITs.CumulativeHierarchy.Base.html#4852" class="Bound">algz</a><a id="5083" class="Symbol">)</a> <a id="5085" href="Cubical.HITs.CumulativeHierarchy.Base.html#4871" class="Bound">x</a><a id="5086" class="Symbol">)</a>
<a id="5105" class="Symbol">(</a><a id="5106" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="5111" class="Symbol">(</a><a id="5112" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="5121" href="Cubical.HITs.CumulativeHierarchy.Base.html#4844" class="Bound">isPropZ</a> <a id="5129" href="Cubical.HITs.CumulativeHierarchy.Base.html#4852" class="Bound">algz</a><a id="5133" class="Symbol">)</a> <a id="5135" href="Cubical.HITs.CumulativeHierarchy.Base.html#4873" class="Bound">y</a><a id="5136" class="Symbol">)</a> <a id="5138" href="Cubical.HITs.CumulativeHierarchy.Base.html#4875" class="Bound">i</a> <a id="5140" href="Cubical.HITs.CumulativeHierarchy.Base.html#4877" class="Bound">j</a>
<a id="5143" class="Comment">-- eliminator for two sets at once</a>
<a id="5178" class="Keyword">record</a> <a id="Elim2Set"></a><a id="5185" href="Cubical.HITs.CumulativeHierarchy.Base.html#5185" class="Record">Elim2Set</a> <a id="5194" class="Symbol">{</a><a id="5195" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="5197" class="Symbol">:</a> <a id="5199" class="Symbol">(</a><a id="5200" href="Cubical.HITs.CumulativeHierarchy.Base.html#5200" class="Bound">s</a> <a id="5202" href="Cubical.HITs.CumulativeHierarchy.Base.html#5202" class="Bound">t</a> <a id="5204" class="Symbol">:</a> <a id="5206" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="5208" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="5209" class="Symbol">)</a> <a id="5211" class="Symbol">→</a> <a id="5213" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5218" href="Cubical.HITs.CumulativeHierarchy.Base.html#880" class="Generalizable">ℓ'</a><a id="5220" class="Symbol">}</a>
<a id="5238" class="Symbol">(</a><a id="5239" href="Cubical.HITs.CumulativeHierarchy.Base.html#5239" class="Bound">isSetZ</a> <a id="5246" class="Symbol">:</a> <a id="5248" class="Symbol">∀</a> <a id="5250" href="Cubical.HITs.CumulativeHierarchy.Base.html#5250" class="Bound">s</a> <a id="5252" href="Cubical.HITs.CumulativeHierarchy.Base.html#5252" class="Bound">t</a> <a id="5254" class="Symbol">→</a> <a id="5256" href="Cubical.Foundations.Prelude.html#14094" class="Function">isSet</a> <a id="5262" class="Symbol">(</a><a id="5263" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="5265" href="Cubical.HITs.CumulativeHierarchy.Base.html#5250" class="Bound">s</a> <a id="5267" href="Cubical.HITs.CumulativeHierarchy.Base.html#5252" class="Bound">t</a><a id="5268" class="Symbol">))</a> <a id="5271" class="Symbol">:</a> <a id="5273" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5278" class="Symbol">(</a><a id="5279" href="Agda.Primitive.html#810" class="Primitive">ℓ-max</a> <a id="5285" href="Cubical.HITs.CumulativeHierarchy.Base.html#5218" class="Bound">ℓ'</a> <a id="5288" class="Symbol">(</a><a id="5289" href="Agda.Primitive.html#780" class="Primitive">ℓ-suc</a> <a id="5295" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5296" class="Symbol">))</a> <a id="5299" class="Keyword">where</a>
<a id="5307" class="Keyword">field</a>
<a id="Elim2Set.ElimSett2"></a><a id="5317" href="Cubical.HITs.CumulativeHierarchy.Base.html#5317" class="Field">ElimSett2</a> <a id="5327" class="Symbol">:</a>
<a id="5335" class="Symbol">∀</a> <a id="5337" class="Symbol">(</a><a id="5338" href="Cubical.HITs.CumulativeHierarchy.Base.html#5338" class="Bound">X</a> <a id="5340" class="Symbol">:</a> <a id="5342" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5347" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5348" class="Symbol">)</a> <a id="5350" class="Symbol">(</a><a id="5351" href="Cubical.HITs.CumulativeHierarchy.Base.html#5351" class="Bound">ix</a> <a id="5354" class="Symbol">:</a> <a id="5356" href="Cubical.HITs.CumulativeHierarchy.Base.html#5338" class="Bound">X</a> <a id="5358" class="Symbol">→</a> <a id="5360" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="5362" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5363" class="Symbol">)</a> <a id="5365" class="Symbol">(</a><a id="5366" href="Cubical.HITs.CumulativeHierarchy.Base.html#5366" class="Bound">Y</a> <a id="5368" class="Symbol">:</a> <a id="5370" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5375" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5376" class="Symbol">)</a> <a id="5378" class="Symbol">(</a><a id="5379" href="Cubical.HITs.CumulativeHierarchy.Base.html#5379" class="Bound">iy</a> <a id="5382" class="Symbol">:</a> <a id="5384" href="Cubical.HITs.CumulativeHierarchy.Base.html#5366" class="Bound">Y</a> <a id="5386" class="Symbol">→</a> <a id="5388" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="5390" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5391" class="Symbol">)</a>
<a id="5399" class="Comment">-- ^ the structural parts of the set</a>
<a id="5442" class="Symbol">→</a> <a id="5444" class="Symbol">(</a><a id="5445" href="Cubical.HITs.CumulativeHierarchy.Base.html#5445" class="Bound">rec</a> <a id="5449" class="Symbol">:</a> <a id="5451" class="Symbol">∀</a> <a id="5453" href="Cubical.HITs.CumulativeHierarchy.Base.html#5453" class="Bound">x</a> <a id="5455" href="Cubical.HITs.CumulativeHierarchy.Base.html#5455" class="Bound">y</a> <a id="5457" class="Symbol">→</a> <a id="5459" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="5461" class="Symbol">(</a><a id="5462" href="Cubical.HITs.CumulativeHierarchy.Base.html#5351" class="Bound">ix</a> <a id="5465" href="Cubical.HITs.CumulativeHierarchy.Base.html#5453" class="Bound">x</a><a id="5466" class="Symbol">)</a> <a id="5468" class="Symbol">(</a><a id="5469" href="Cubical.HITs.CumulativeHierarchy.Base.html#5379" class="Bound">iy</a> <a id="5472" href="Cubical.HITs.CumulativeHierarchy.Base.html#5455" class="Bound">y</a><a id="5473" class="Symbol">))</a>
<a id="5482" class="Comment">-- ^ a recursor into the elements</a>
<a id="5522" class="Symbol">→</a> <a id="5524" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="5526" class="Symbol">(</a><a id="5527" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="5532" href="Cubical.HITs.CumulativeHierarchy.Base.html#5338" class="Bound">X</a> <a id="5534" href="Cubical.HITs.CumulativeHierarchy.Base.html#5351" class="Bound">ix</a><a id="5536" class="Symbol">)</a> <a id="5538" class="Symbol">(</a><a id="5539" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="5544" href="Cubical.HITs.CumulativeHierarchy.Base.html#5366" class="Bound">Y</a> <a id="5546" href="Cubical.HITs.CumulativeHierarchy.Base.html#5379" class="Bound">iy</a><a id="5548" class="Symbol">)</a>
<a id="5554" class="Comment">-- path when the the first argument deforms along seteq and the second argument is held constant</a>
<a id="Elim2Set.ElimEqFst"></a><a id="5655" href="Cubical.HITs.CumulativeHierarchy.Base.html#5655" class="Field">ElimEqFst</a> <a id="5665" class="Symbol">:</a>
<a id="5673" class="Symbol">∀</a> <a id="5675" class="Symbol">(</a><a id="5676" href="Cubical.HITs.CumulativeHierarchy.Base.html#5676" class="Bound">X₁</a> <a id="5679" href="Cubical.HITs.CumulativeHierarchy.Base.html#5679" class="Bound">X₂</a> <a id="5682" class="Symbol">:</a> <a id="5684" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5689" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5690" class="Symbol">)</a> <a id="5692" class="Symbol">(</a><a id="5693" href="Cubical.HITs.CumulativeHierarchy.Base.html#5693" class="Bound">ix₁</a> <a id="5697" class="Symbol">:</a> <a id="5699" href="Cubical.HITs.CumulativeHierarchy.Base.html#5676" class="Bound">X₁</a> <a id="5702" class="Symbol">→</a> <a id="5704" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="5706" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5707" class="Symbol">)</a> <a id="5709" class="Symbol">(</a><a id="5710" href="Cubical.HITs.CumulativeHierarchy.Base.html#5710" class="Bound">ix₂</a> <a id="5714" class="Symbol">:</a> <a id="5716" href="Cubical.HITs.CumulativeHierarchy.Base.html#5679" class="Bound">X₂</a> <a id="5719" class="Symbol">→</a> <a id="5721" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="5723" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5724" class="Symbol">)</a> <a id="5726" class="Symbol">(</a><a id="5727" href="Cubical.HITs.CumulativeHierarchy.Base.html#5727" class="Bound">eq</a> <a id="5730" class="Symbol">:</a> <a id="5732" href="Cubical.HITs.CumulativeHierarchy.Base.html#1064" class="Function">eqImage</a> <a id="5740" href="Cubical.HITs.CumulativeHierarchy.Base.html#5693" class="Bound">ix₁</a> <a id="5744" href="Cubical.HITs.CumulativeHierarchy.Base.html#5710" class="Bound">ix₂</a><a id="5747" class="Symbol">)</a>
<a id="5755" class="Comment">-- ^ the structural parts of the seteq path</a>
<a id="5805" class="Symbol">→</a> <a id="5807" class="Symbol">(</a><a id="5808" href="Cubical.HITs.CumulativeHierarchy.Base.html#5808" class="Bound">Y</a> <a id="5810" class="Symbol">:</a> <a id="5812" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5817" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5818" class="Symbol">)</a> <a id="5820" class="Symbol">(</a><a id="5821" href="Cubical.HITs.CumulativeHierarchy.Base.html#5821" class="Bound">iy</a> <a id="5824" class="Symbol">:</a> <a id="5826" href="Cubical.HITs.CumulativeHierarchy.Base.html#5808" class="Bound">Y</a> <a id="5828" class="Symbol">→</a> <a id="5830" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="5832" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="5833" class="Symbol">)</a>
<a id="5841" class="Comment">-- ^ the second argument held constant</a>
<a id="5886" class="Symbol">→</a> <a id="5888" class="Symbol">(</a><a id="5889" href="Cubical.HITs.CumulativeHierarchy.Base.html#5889" class="Bound">rec₁</a> <a id="5894" class="Symbol">:</a> <a id="5896" class="Symbol">∀</a> <a id="5898" href="Cubical.HITs.CumulativeHierarchy.Base.html#5898" class="Bound">x₁</a> <a id="5901" href="Cubical.HITs.CumulativeHierarchy.Base.html#5901" class="Bound">y</a> <a id="5903" class="Symbol">→</a> <a id="5905" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="5907" class="Symbol">(</a><a id="5908" href="Cubical.HITs.CumulativeHierarchy.Base.html#5693" class="Bound">ix₁</a> <a id="5912" href="Cubical.HITs.CumulativeHierarchy.Base.html#5898" class="Bound">x₁</a><a id="5914" class="Symbol">)</a> <a id="5916" class="Symbol">(</a><a id="5917" href="Cubical.HITs.CumulativeHierarchy.Base.html#5821" class="Bound">iy</a> <a id="5920" href="Cubical.HITs.CumulativeHierarchy.Base.html#5901" class="Bound">y</a><a id="5921" class="Symbol">))</a> <a id="5924" class="Symbol">(</a><a id="5925" href="Cubical.HITs.CumulativeHierarchy.Base.html#5925" class="Bound">rec₂</a> <a id="5930" class="Symbol">:</a> <a id="5932" class="Symbol">∀</a> <a id="5934" href="Cubical.HITs.CumulativeHierarchy.Base.html#5934" class="Bound">x₂</a> <a id="5937" href="Cubical.HITs.CumulativeHierarchy.Base.html#5937" class="Bound">y</a> <a id="5939" class="Symbol">→</a> <a id="5941" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="5943" class="Symbol">(</a><a id="5944" href="Cubical.HITs.CumulativeHierarchy.Base.html#5710" class="Bound">ix₂</a> <a id="5948" href="Cubical.HITs.CumulativeHierarchy.Base.html#5934" class="Bound">x₂</a><a id="5950" class="Symbol">)</a> <a id="5952" class="Symbol">(</a><a id="5953" href="Cubical.HITs.CumulativeHierarchy.Base.html#5821" class="Bound">iy</a> <a id="5956" href="Cubical.HITs.CumulativeHierarchy.Base.html#5937" class="Bound">y</a><a id="5957" class="Symbol">))</a>
<a id="5966" class="Comment">-- ^ recursors into the elements</a>
<a id="6005" class="Symbol">→</a> <a id="6007" class="Symbol">(</a><a id="6008" href="Cubical.HITs.CumulativeHierarchy.Base.html#6008" class="Bound">rec₁→₂</a> <a id="6015" class="Symbol">:</a> <a id="6017" class="Symbol">(</a><a id="6018" href="Cubical.HITs.CumulativeHierarchy.Base.html#6018" class="Bound">x₁</a> <a id="6021" class="Symbol">:</a> <a id="6023" href="Cubical.HITs.CumulativeHierarchy.Base.html#5676" class="Bound">X₁</a><a id="6025" class="Symbol">)</a>
<a id="6043" class="Symbol">→</a> <a id="6045" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="6048" href="Cubical.HITs.CumulativeHierarchy.Base.html#6048" class="Bound">(</a><a id="6049" href="Cubical.HITs.CumulativeHierarchy.Base.html#6049" class="Bound">x₂</a> <a id="6052" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6054" href="Cubical.HITs.CumulativeHierarchy.Base.html#6054" class="Bound">p</a><a id="6055" href="Cubical.HITs.CumulativeHierarchy.Base.html#6048" class="Bound">)</a> <a id="6057" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="6059" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="6065" href="Cubical.HITs.CumulativeHierarchy.Base.html#5710" class="Bound">ix₂</a> <a id="6069" class="Symbol">(</a><a id="6070" href="Cubical.HITs.CumulativeHierarchy.Base.html#5693" class="Bound">ix₁</a> <a id="6074" href="Cubical.HITs.CumulativeHierarchy.Base.html#6018" class="Bound">x₁</a><a id="6076" class="Symbol">)</a> <a id="6078" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="6101" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="6107" class="Symbol">(λ</a> <a id="6110" href="Cubical.HITs.CumulativeHierarchy.Base.html#6110" class="Bound">i</a> <a id="6112" class="Symbol">→</a> <a id="6114" class="Symbol">∀</a> <a id="6116" href="Cubical.HITs.CumulativeHierarchy.Base.html#6116" class="Bound">y</a> <a id="6118" class="Symbol">→</a> <a id="6120" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="6122" class="Symbol">(</a><a id="6123" href="Cubical.HITs.CumulativeHierarchy.Base.html#6054" class="Bound">p</a> <a id="6125" href="Cubical.HITs.CumulativeHierarchy.Base.html#6110" class="Bound">i</a><a id="6126" class="Symbol">)</a> <a id="6128" class="Symbol">(</a><a id="6129" href="Cubical.HITs.CumulativeHierarchy.Base.html#5821" class="Bound">iy</a> <a id="6132" href="Cubical.HITs.CumulativeHierarchy.Base.html#6116" class="Bound">y</a><a id="6133" class="Symbol">))</a> <a id="6136" class="Symbol">(λ</a> <a id="6139" href="Cubical.HITs.CumulativeHierarchy.Base.html#6139" class="Bound">y</a> <a id="6141" class="Symbol">→</a> <a id="6143" href="Cubical.HITs.CumulativeHierarchy.Base.html#5925" class="Bound">rec₂</a> <a id="6148" href="Cubical.HITs.CumulativeHierarchy.Base.html#6049" class="Bound">x₂</a> <a id="6151" href="Cubical.HITs.CumulativeHierarchy.Base.html#6139" class="Bound">y</a><a id="6152" class="Symbol">)</a> <a id="6154" class="Symbol">(λ</a> <a id="6157" href="Cubical.HITs.CumulativeHierarchy.Base.html#6157" class="Bound">y</a> <a id="6159" class="Symbol">→</a> <a id="6161" href="Cubical.HITs.CumulativeHierarchy.Base.html#5889" class="Bound">rec₁</a> <a id="6166" href="Cubical.HITs.CumulativeHierarchy.Base.html#6018" class="Bound">x₁</a> <a id="6169" href="Cubical.HITs.CumulativeHierarchy.Base.html#6157" class="Bound">y</a><a id="6170" class="Symbol">))</a>
<a id="6179" class="Symbol">→</a> <a id="6181" class="Symbol">(</a><a id="6182" href="Cubical.HITs.CumulativeHierarchy.Base.html#6182" class="Bound">rec₂→₁</a> <a id="6189" class="Symbol">:</a> <a id="6191" class="Symbol">(</a><a id="6192" href="Cubical.HITs.CumulativeHierarchy.Base.html#6192" class="Bound">x₂</a> <a id="6195" class="Symbol">:</a> <a id="6197" href="Cubical.HITs.CumulativeHierarchy.Base.html#5679" class="Bound">X₂</a><a id="6199" class="Symbol">)</a>
<a id="6217" class="Symbol">→</a> <a id="6219" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="6222" href="Cubical.HITs.CumulativeHierarchy.Base.html#6222" class="Bound">(</a><a id="6223" href="Cubical.HITs.CumulativeHierarchy.Base.html#6223" class="Bound">x₁</a> <a id="6226" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6228" href="Cubical.HITs.CumulativeHierarchy.Base.html#6228" class="Bound">p</a><a id="6229" href="Cubical.HITs.CumulativeHierarchy.Base.html#6222" class="Bound">)</a> <a id="6231" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="6233" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="6239" href="Cubical.HITs.CumulativeHierarchy.Base.html#5693" class="Bound">ix₁</a> <a id="6243" class="Symbol">(</a><a id="6244" href="Cubical.HITs.CumulativeHierarchy.Base.html#5710" class="Bound">ix₂</a> <a id="6248" href="Cubical.HITs.CumulativeHierarchy.Base.html#6192" class="Bound">x₂</a><a id="6250" class="Symbol">)</a> <a id="6252" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="6275" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="6281" class="Symbol">(λ</a> <a id="6284" href="Cubical.HITs.CumulativeHierarchy.Base.html#6284" class="Bound">i</a> <a id="6286" class="Symbol">→</a> <a id="6288" class="Symbol">∀</a> <a id="6290" href="Cubical.HITs.CumulativeHierarchy.Base.html#6290" class="Bound">y</a> <a id="6292" class="Symbol">→</a> <a id="6294" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="6296" class="Symbol">(</a><a id="6297" href="Cubical.HITs.CumulativeHierarchy.Base.html#6228" class="Bound">p</a> <a id="6299" href="Cubical.HITs.CumulativeHierarchy.Base.html#6284" class="Bound">i</a><a id="6300" class="Symbol">)</a> <a id="6302" class="Symbol">(</a><a id="6303" href="Cubical.HITs.CumulativeHierarchy.Base.html#5821" class="Bound">iy</a> <a id="6306" href="Cubical.HITs.CumulativeHierarchy.Base.html#6290" class="Bound">y</a><a id="6307" class="Symbol">))</a> <a id="6310" class="Symbol">(λ</a> <a id="6313" href="Cubical.HITs.CumulativeHierarchy.Base.html#6313" class="Bound">y</a> <a id="6315" class="Symbol">→</a> <a id="6317" href="Cubical.HITs.CumulativeHierarchy.Base.html#5889" class="Bound">rec₁</a> <a id="6322" href="Cubical.HITs.CumulativeHierarchy.Base.html#6223" class="Bound">x₁</a> <a id="6325" href="Cubical.HITs.CumulativeHierarchy.Base.html#6313" class="Bound">y</a><a id="6326" class="Symbol">)</a> <a id="6328" class="Symbol">(λ</a> <a id="6331" href="Cubical.HITs.CumulativeHierarchy.Base.html#6331" class="Bound">y</a> <a id="6333" class="Symbol">→</a> <a id="6335" href="Cubical.HITs.CumulativeHierarchy.Base.html#5925" class="Bound">rec₂</a> <a id="6340" href="Cubical.HITs.CumulativeHierarchy.Base.html#6192" class="Bound">x₂</a> <a id="6343" href="Cubical.HITs.CumulativeHierarchy.Base.html#6331" class="Bound">y</a><a id="6344" class="Symbol">))</a>
<a id="6353" class="Comment">-- ^ proofs that the recursors have equal images</a>
<a id="6408" class="Symbol">→</a> <a id="6410" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="6416" class="Symbol">(λ</a> <a id="6419" href="Cubical.HITs.CumulativeHierarchy.Base.html#6419" class="Bound">i</a> <a id="6421" class="Symbol">→</a> <a id="6423" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="6425" class="Symbol">(</a><a id="6426" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="6432" href="Cubical.HITs.CumulativeHierarchy.Base.html#5676" class="Bound">X₁</a> <a id="6435" href="Cubical.HITs.CumulativeHierarchy.Base.html#5679" class="Bound">X₂</a> <a id="6438" href="Cubical.HITs.CumulativeHierarchy.Base.html#5693" class="Bound">ix₁</a> <a id="6442" href="Cubical.HITs.CumulativeHierarchy.Base.html#5710" class="Bound">ix₂</a> <a id="6446" href="Cubical.HITs.CumulativeHierarchy.Base.html#5727" class="Bound">eq</a> <a id="6449" href="Cubical.HITs.CumulativeHierarchy.Base.html#6419" class="Bound">i</a><a id="6450" class="Symbol">)</a> <a id="6452" class="Symbol">(</a><a id="6453" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="6458" href="Cubical.HITs.CumulativeHierarchy.Base.html#5808" class="Bound">Y</a> <a id="6460" href="Cubical.HITs.CumulativeHierarchy.Base.html#5821" class="Bound">iy</a><a id="6462" class="Symbol">))</a>
<a id="6479" class="Symbol">(</a><a id="6480" href="Cubical.HITs.CumulativeHierarchy.Base.html#5317" class="Field">ElimSett2</a> <a id="6490" href="Cubical.HITs.CumulativeHierarchy.Base.html#5676" class="Bound">X₁</a> <a id="6493" href="Cubical.HITs.CumulativeHierarchy.Base.html#5693" class="Bound">ix₁</a> <a id="6497" href="Cubical.HITs.CumulativeHierarchy.Base.html#5808" class="Bound">Y</a> <a id="6499" href="Cubical.HITs.CumulativeHierarchy.Base.html#5821" class="Bound">iy</a> <a id="6502" href="Cubical.HITs.CumulativeHierarchy.Base.html#5889" class="Bound">rec₁</a><a id="6506" class="Symbol">)</a>
<a id="6522" class="Symbol">(</a><a id="6523" href="Cubical.HITs.CumulativeHierarchy.Base.html#5317" class="Field">ElimSett2</a> <a id="6533" href="Cubical.HITs.CumulativeHierarchy.Base.html#5679" class="Bound">X₂</a> <a id="6536" href="Cubical.HITs.CumulativeHierarchy.Base.html#5710" class="Bound">ix₂</a> <a id="6540" href="Cubical.HITs.CumulativeHierarchy.Base.html#5808" class="Bound">Y</a> <a id="6542" href="Cubical.HITs.CumulativeHierarchy.Base.html#5821" class="Bound">iy</a> <a id="6545" href="Cubical.HITs.CumulativeHierarchy.Base.html#5925" class="Bound">rec₂</a><a id="6549" class="Symbol">)</a>
<a id="6555" class="Comment">-- path when the the second argument deforms along seteq and the first argument is held constant</a>
<a id="Elim2Set.ElimEqSnd"></a><a id="6656" href="Cubical.HITs.CumulativeHierarchy.Base.html#6656" class="Field">ElimEqSnd</a> <a id="6666" class="Symbol">:</a>
<a id="6674" class="Symbol">∀</a> <a id="6676" class="Symbol">(</a><a id="6677" href="Cubical.HITs.CumulativeHierarchy.Base.html#6677" class="Bound">X</a> <a id="6679" class="Symbol">:</a> <a id="6681" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6686" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="6687" class="Symbol">)</a> <a id="6689" class="Symbol">(</a><a id="6690" href="Cubical.HITs.CumulativeHierarchy.Base.html#6690" class="Bound">ix</a> <a id="6693" class="Symbol">:</a> <a id="6695" href="Cubical.HITs.CumulativeHierarchy.Base.html#6677" class="Bound">X</a> <a id="6697" class="Symbol">→</a> <a id="6699" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="6701" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="6702" class="Symbol">)</a>
<a id="6710" class="Comment">-- ^ the first argument held constant</a>
<a id="6754" class="Symbol">→</a> <a id="6756" class="Symbol">(</a><a id="6757" href="Cubical.HITs.CumulativeHierarchy.Base.html#6757" class="Bound">Y₁</a> <a id="6760" href="Cubical.HITs.CumulativeHierarchy.Base.html#6760" class="Bound">Y₂</a> <a id="6763" class="Symbol">:</a> <a id="6765" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6770" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="6771" class="Symbol">)</a> <a id="6773" class="Symbol">(</a><a id="6774" href="Cubical.HITs.CumulativeHierarchy.Base.html#6774" class="Bound">iy₁</a> <a id="6778" class="Symbol">:</a> <a id="6780" href="Cubical.HITs.CumulativeHierarchy.Base.html#6757" class="Bound">Y₁</a> <a id="6783" class="Symbol">→</a> <a id="6785" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="6787" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="6788" class="Symbol">)</a> <a id="6790" class="Symbol">(</a><a id="6791" href="Cubical.HITs.CumulativeHierarchy.Base.html#6791" class="Bound">iy₂</a> <a id="6795" class="Symbol">:</a> <a id="6797" href="Cubical.HITs.CumulativeHierarchy.Base.html#6760" class="Bound">Y₂</a> <a id="6800" class="Symbol">→</a> <a id="6802" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="6804" href="Cubical.HITs.CumulativeHierarchy.Base.html#5208" class="Bound">ℓ</a><a id="6805" class="Symbol">)</a> <a id="6807" class="Symbol">→</a> <a id="6809" class="Symbol">(</a><a id="6810" href="Cubical.HITs.CumulativeHierarchy.Base.html#6810" class="Bound">eq</a> <a id="6813" class="Symbol">:</a> <a id="6815" href="Cubical.HITs.CumulativeHierarchy.Base.html#1064" class="Function">eqImage</a> <a id="6823" href="Cubical.HITs.CumulativeHierarchy.Base.html#6774" class="Bound">iy₁</a> <a id="6827" href="Cubical.HITs.CumulativeHierarchy.Base.html#6791" class="Bound">iy₂</a><a id="6830" class="Symbol">)</a>
<a id="6838" class="Comment">-- ^ the structural parts of the seteq path</a>
<a id="6888" class="Symbol">→</a> <a id="6890" class="Symbol">(</a><a id="6891" href="Cubical.HITs.CumulativeHierarchy.Base.html#6891" class="Bound">rec₁</a> <a id="6896" class="Symbol">:</a> <a id="6898" class="Symbol">∀</a> <a id="6900" href="Cubical.HITs.CumulativeHierarchy.Base.html#6900" class="Bound">x</a> <a id="6902" href="Cubical.HITs.CumulativeHierarchy.Base.html#6902" class="Bound">y₁</a> <a id="6905" class="Symbol">→</a> <a id="6907" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="6909" class="Symbol">(</a><a id="6910" href="Cubical.HITs.CumulativeHierarchy.Base.html#6690" class="Bound">ix</a> <a id="6913" href="Cubical.HITs.CumulativeHierarchy.Base.html#6900" class="Bound">x</a><a id="6914" class="Symbol">)</a> <a id="6916" class="Symbol">(</a><a id="6917" href="Cubical.HITs.CumulativeHierarchy.Base.html#6774" class="Bound">iy₁</a> <a id="6921" href="Cubical.HITs.CumulativeHierarchy.Base.html#6902" class="Bound">y₁</a><a id="6923" class="Symbol">))</a> <a id="6926" class="Symbol">(</a><a id="6927" href="Cubical.HITs.CumulativeHierarchy.Base.html#6927" class="Bound">rec₂</a> <a id="6932" class="Symbol">:</a> <a id="6934" class="Symbol">∀</a> <a id="6936" href="Cubical.HITs.CumulativeHierarchy.Base.html#6936" class="Bound">x</a> <a id="6938" href="Cubical.HITs.CumulativeHierarchy.Base.html#6938" class="Bound">y₂</a> <a id="6941" class="Symbol">→</a> <a id="6943" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="6945" class="Symbol">(</a><a id="6946" href="Cubical.HITs.CumulativeHierarchy.Base.html#6690" class="Bound">ix</a> <a id="6949" href="Cubical.HITs.CumulativeHierarchy.Base.html#6936" class="Bound">x</a><a id="6950" class="Symbol">)</a> <a id="6952" class="Symbol">(</a><a id="6953" href="Cubical.HITs.CumulativeHierarchy.Base.html#6791" class="Bound">iy₂</a> <a id="6957" href="Cubical.HITs.CumulativeHierarchy.Base.html#6938" class="Bound">y₂</a><a id="6959" class="Symbol">))</a>
<a id="6968" class="Comment">-- ^ recursors into the elements</a>
<a id="7007" class="Symbol">→</a> <a id="7009" class="Symbol">(</a><a id="7010" href="Cubical.HITs.CumulativeHierarchy.Base.html#7010" class="Bound">rec₁→₂</a> <a id="7017" class="Symbol">:</a> <a id="7019" class="Symbol">(</a><a id="7020" href="Cubical.HITs.CumulativeHierarchy.Base.html#7020" class="Bound">y₁</a> <a id="7023" class="Symbol">:</a> <a id="7025" href="Cubical.HITs.CumulativeHierarchy.Base.html#6757" class="Bound">Y₁</a><a id="7027" class="Symbol">)</a>
<a id="7045" class="Symbol">→</a> <a id="7047" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="7050" href="Cubical.HITs.CumulativeHierarchy.Base.html#7050" class="Bound">(</a><a id="7051" href="Cubical.HITs.CumulativeHierarchy.Base.html#7051" class="Bound">y₂</a> <a id="7054" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="7056" href="Cubical.HITs.CumulativeHierarchy.Base.html#7056" class="Bound">p</a><a id="7057" href="Cubical.HITs.CumulativeHierarchy.Base.html#7050" class="Bound">)</a> <a id="7059" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="7061" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="7067" href="Cubical.HITs.CumulativeHierarchy.Base.html#6791" class="Bound">iy₂</a> <a id="7071" class="Symbol">(</a><a id="7072" href="Cubical.HITs.CumulativeHierarchy.Base.html#6774" class="Bound">iy₁</a> <a id="7076" href="Cubical.HITs.CumulativeHierarchy.Base.html#7020" class="Bound">y₁</a><a id="7078" class="Symbol">)</a> <a id="7080" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="7103" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="7109" class="Symbol">(λ</a> <a id="7112" href="Cubical.HITs.CumulativeHierarchy.Base.html#7112" class="Bound">i</a> <a id="7114" class="Symbol">→</a> <a id="7116" class="Symbol">∀</a> <a id="7118" href="Cubical.HITs.CumulativeHierarchy.Base.html#7118" class="Bound">x</a> <a id="7120" class="Symbol">→</a> <a id="7122" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="7124" class="Symbol">(</a><a id="7125" href="Cubical.HITs.CumulativeHierarchy.Base.html#6690" class="Bound">ix</a> <a id="7128" href="Cubical.HITs.CumulativeHierarchy.Base.html#7118" class="Bound">x</a><a id="7129" class="Symbol">)</a> <a id="7131" class="Symbol">(</a><a id="7132" href="Cubical.HITs.CumulativeHierarchy.Base.html#7056" class="Bound">p</a> <a id="7134" href="Cubical.HITs.CumulativeHierarchy.Base.html#7112" class="Bound">i</a><a id="7135" class="Symbol">))</a> <a id="7138" class="Symbol">(λ</a> <a id="7141" href="Cubical.HITs.CumulativeHierarchy.Base.html#7141" class="Bound">x</a> <a id="7143" class="Symbol">→</a> <a id="7145" href="Cubical.HITs.CumulativeHierarchy.Base.html#6927" class="Bound">rec₂</a> <a id="7150" href="Cubical.HITs.CumulativeHierarchy.Base.html#7141" class="Bound">x</a> <a id="7152" href="Cubical.HITs.CumulativeHierarchy.Base.html#7051" class="Bound">y₂</a><a id="7154" class="Symbol">)</a> <a id="7156" class="Symbol">(λ</a> <a id="7159" href="Cubical.HITs.CumulativeHierarchy.Base.html#7159" class="Bound">x</a> <a id="7161" class="Symbol">→</a> <a id="7163" href="Cubical.HITs.CumulativeHierarchy.Base.html#6891" class="Bound">rec₁</a> <a id="7168" href="Cubical.HITs.CumulativeHierarchy.Base.html#7159" class="Bound">x</a> <a id="7170" href="Cubical.HITs.CumulativeHierarchy.Base.html#7020" class="Bound">y₁</a><a id="7172" class="Symbol">))</a>
<a id="7181" class="Symbol">→</a> <a id="7183" class="Symbol">(</a><a id="7184" href="Cubical.HITs.CumulativeHierarchy.Base.html#7184" class="Bound">rec₂→₁</a> <a id="7191" class="Symbol">:</a> <a id="7193" class="Symbol">(</a><a id="7194" href="Cubical.HITs.CumulativeHierarchy.Base.html#7194" class="Bound">y₂</a> <a id="7197" class="Symbol">:</a> <a id="7199" href="Cubical.HITs.CumulativeHierarchy.Base.html#6760" class="Bound">Y₂</a><a id="7201" class="Symbol">)</a>
<a id="7219" class="Symbol">→</a> <a id="7221" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="7224" href="Cubical.HITs.CumulativeHierarchy.Base.html#7224" class="Bound">(</a><a id="7225" href="Cubical.HITs.CumulativeHierarchy.Base.html#7225" class="Bound">y₁</a> <a id="7228" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="7230" href="Cubical.HITs.CumulativeHierarchy.Base.html#7230" class="Bound">p</a><a id="7231" href="Cubical.HITs.CumulativeHierarchy.Base.html#7224" class="Bound">)</a> <a id="7233" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="7235" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="7241" href="Cubical.HITs.CumulativeHierarchy.Base.html#6774" class="Bound">iy₁</a> <a id="7245" class="Symbol">(</a><a id="7246" href="Cubical.HITs.CumulativeHierarchy.Base.html#6791" class="Bound">iy₂</a> <a id="7250" href="Cubical.HITs.CumulativeHierarchy.Base.html#7194" class="Bound">y₂</a><a id="7252" class="Symbol">)</a> <a id="7254" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="7277" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="7283" class="Symbol">(λ</a> <a id="7286" href="Cubical.HITs.CumulativeHierarchy.Base.html#7286" class="Bound">i</a> <a id="7288" class="Symbol">→</a> <a id="7290" class="Symbol">∀</a> <a id="7292" href="Cubical.HITs.CumulativeHierarchy.Base.html#7292" class="Bound">x</a> <a id="7294" class="Symbol">→</a> <a id="7296" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="7298" class="Symbol">(</a><a id="7299" href="Cubical.HITs.CumulativeHierarchy.Base.html#6690" class="Bound">ix</a> <a id="7302" href="Cubical.HITs.CumulativeHierarchy.Base.html#7292" class="Bound">x</a><a id="7303" class="Symbol">)</a> <a id="7305" class="Symbol">(</a><a id="7306" href="Cubical.HITs.CumulativeHierarchy.Base.html#7230" class="Bound">p</a> <a id="7308" href="Cubical.HITs.CumulativeHierarchy.Base.html#7286" class="Bound">i</a><a id="7309" class="Symbol">))</a> <a id="7312" class="Symbol">(λ</a> <a id="7315" href="Cubical.HITs.CumulativeHierarchy.Base.html#7315" class="Bound">x</a> <a id="7317" class="Symbol">→</a> <a id="7319" href="Cubical.HITs.CumulativeHierarchy.Base.html#6891" class="Bound">rec₁</a> <a id="7324" href="Cubical.HITs.CumulativeHierarchy.Base.html#7315" class="Bound">x</a> <a id="7326" href="Cubical.HITs.CumulativeHierarchy.Base.html#7225" class="Bound">y₁</a><a id="7328" class="Symbol">)</a> <a id="7330" class="Symbol">(λ</a> <a id="7333" href="Cubical.HITs.CumulativeHierarchy.Base.html#7333" class="Bound">x</a> <a id="7335" class="Symbol">→</a> <a id="7337" href="Cubical.HITs.CumulativeHierarchy.Base.html#6927" class="Bound">rec₂</a> <a id="7342" href="Cubical.HITs.CumulativeHierarchy.Base.html#7333" class="Bound">x</a> <a id="7344" href="Cubical.HITs.CumulativeHierarchy.Base.html#7194" class="Bound">y₂</a><a id="7346" class="Symbol">))</a>
<a id="7355" class="Comment">-- ^ proofs that the recursors have equal images</a>
<a id="7410" class="Symbol">→</a> <a id="7412" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="7418" class="Symbol">(λ</a> <a id="7421" href="Cubical.HITs.CumulativeHierarchy.Base.html#7421" class="Bound">i</a> <a id="7423" class="Symbol">→</a> <a id="7425" href="Cubical.HITs.CumulativeHierarchy.Base.html#5195" class="Bound">Z</a> <a id="7427" class="Symbol">(</a><a id="7428" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="7433" href="Cubical.HITs.CumulativeHierarchy.Base.html#6677" class="Bound">X</a> <a id="7435" href="Cubical.HITs.CumulativeHierarchy.Base.html#6690" class="Bound">ix</a><a id="7437" class="Symbol">)</a> <a id="7439" class="Symbol">(</a><a id="7440" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="7446" href="Cubical.HITs.CumulativeHierarchy.Base.html#6757" class="Bound">Y₁</a> <a id="7449" href="Cubical.HITs.CumulativeHierarchy.Base.html#6760" class="Bound">Y₂</a> <a id="7452" href="Cubical.HITs.CumulativeHierarchy.Base.html#6774" class="Bound">iy₁</a> <a id="7456" href="Cubical.HITs.CumulativeHierarchy.Base.html#6791" class="Bound">iy₂</a> <a id="7460" href="Cubical.HITs.CumulativeHierarchy.Base.html#6810" class="Bound">eq</a> <a id="7463" href="Cubical.HITs.CumulativeHierarchy.Base.html#7421" class="Bound">i</a><a id="7464" class="Symbol">))</a>
<a id="7481" class="Symbol">(</a><a id="7482" href="Cubical.HITs.CumulativeHierarchy.Base.html#5317" class="Field">ElimSett2</a> <a id="7492" href="Cubical.HITs.CumulativeHierarchy.Base.html#6677" class="Bound">X</a> <a id="7494" href="Cubical.HITs.CumulativeHierarchy.Base.html#6690" class="Bound">ix</a> <a id="7497" href="Cubical.HITs.CumulativeHierarchy.Base.html#6757" class="Bound">Y₁</a> <a id="7500" href="Cubical.HITs.CumulativeHierarchy.Base.html#6774" class="Bound">iy₁</a> <a id="7504" href="Cubical.HITs.CumulativeHierarchy.Base.html#6891" class="Bound">rec₁</a><a id="7508" class="Symbol">)</a>
<a id="7524" class="Symbol">(</a><a id="7525" href="Cubical.HITs.CumulativeHierarchy.Base.html#5317" class="Field">ElimSett2</a> <a id="7535" href="Cubical.HITs.CumulativeHierarchy.Base.html#6677" class="Bound">X</a> <a id="7537" href="Cubical.HITs.CumulativeHierarchy.Base.html#6690" class="Bound">ix</a> <a id="7540" href="Cubical.HITs.CumulativeHierarchy.Base.html#6760" class="Bound">Y₂</a> <a id="7543" href="Cubical.HITs.CumulativeHierarchy.Base.html#6791" class="Bound">iy₂</a> <a id="7547" href="Cubical.HITs.CumulativeHierarchy.Base.html#6927" class="Bound">rec₂</a><a id="7551" class="Symbol">)</a>
<a id="7554" class="Keyword">module</a> <a id="7561" href="Cubical.HITs.CumulativeHierarchy.Base.html#7561" class="Module">_</a> <a id="7563" class="Symbol">{</a><a id="7564" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="7566" class="Symbol">:</a> <a id="7568" class="Symbol">(</a><a id="7569" href="Cubical.HITs.CumulativeHierarchy.Base.html#7569" class="Bound">s</a> <a id="7571" href="Cubical.HITs.CumulativeHierarchy.Base.html#7571" class="Bound">t</a> <a id="7573" class="Symbol">:</a> <a id="7575" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="7577" href="Cubical.HITs.CumulativeHierarchy.Base.html#878" class="Generalizable">ℓ</a><a id="7578" class="Symbol">)</a> <a id="7580" class="Symbol">→</a> <a id="7582" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7587" href="Cubical.HITs.CumulativeHierarchy.Base.html#880" class="Generalizable">ℓ'</a><a id="7589" class="Symbol">}</a> <a id="7591" class="Symbol">{</a><a id="7592" href="Cubical.HITs.CumulativeHierarchy.Base.html#7592" class="Bound">isSetZ</a> <a id="7599" class="Symbol">:</a> <a id="7601" class="Symbol">∀</a> <a id="7603" href="Cubical.HITs.CumulativeHierarchy.Base.html#7603" class="Bound">s</a> <a id="7605" href="Cubical.HITs.CumulativeHierarchy.Base.html#7605" class="Bound">t</a> <a id="7607" class="Symbol">→</a> <a id="7609" href="Cubical.Foundations.Prelude.html#14094" class="Function">isSet</a> <a id="7615" class="Symbol">(</a><a id="7616" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="7618" href="Cubical.HITs.CumulativeHierarchy.Base.html#7603" class="Bound">s</a> <a id="7620" href="Cubical.HITs.CumulativeHierarchy.Base.html#7605" class="Bound">t</a><a id="7621" class="Symbol">)}</a> <a id="7624" class="Symbol">(</a><a id="7625" href="Cubical.HITs.CumulativeHierarchy.Base.html#7625" class="Bound">E</a> <a id="7627" class="Symbol">:</a> <a id="7629" href="Cubical.HITs.CumulativeHierarchy.Base.html#5185" class="Record">Elim2Set</a> <a id="7638" href="Cubical.HITs.CumulativeHierarchy.Base.html#7592" class="Bound">isSetZ</a><a id="7644" class="Symbol">)</a> <a id="7646" class="Keyword">where</a>
<a id="7654" class="Keyword">open</a> <a id="7659" href="Cubical.HITs.CumulativeHierarchy.Base.html#5185" class="Module">Elim2Set</a> <a id="7668" href="Cubical.HITs.CumulativeHierarchy.Base.html#7625" class="Bound">E</a>
<a id="7672" class="Keyword">open</a> <a id="7677" href="Cubical.HITs.CumulativeHierarchy.Base.html#1877" class="Module">ElimSet</a>
<a id="7688" href="Cubical.HITs.CumulativeHierarchy.Base.html#7688" class="Function">elim2</a> <a id="7694" class="Symbol">:</a> <a id="7696" class="Symbol">(</a><a id="7697" href="Cubical.HITs.CumulativeHierarchy.Base.html#7697" class="Bound">s</a> <a id="7699" href="Cubical.HITs.CumulativeHierarchy.Base.html#7699" class="Bound">t</a> <a id="7701" class="Symbol">:</a> <a id="7703" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="7705" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="7706" class="Symbol">)</a> <a id="7708" class="Symbol">→</a> <a id="7710" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="7712" href="Cubical.HITs.CumulativeHierarchy.Base.html#7697" class="Bound">s</a> <a id="7714" href="Cubical.HITs.CumulativeHierarchy.Base.html#7699" class="Bound">t</a>
<a id="7718" href="Cubical.HITs.CumulativeHierarchy.Base.html#7688" class="Function">elim2</a> <a id="7724" class="Symbol">=</a> <a id="7726" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="7731" href="Cubical.HITs.CumulativeHierarchy.Base.html#10824" class="Function">pElim</a> <a id="7737" class="Keyword">where</a>
<a id="7747" class="Keyword">open</a> <a id="7752" href="Cubical.HITs.PropositionalTruncation.Monad.html" class="Module">PropMonad</a>
<a id="7767" href="Cubical.HITs.CumulativeHierarchy.Base.html#7767" class="Function">isSetPElim</a> <a id="7778" class="Symbol">:</a> <a id="7780" class="Symbol">∀</a> <a id="7782" href="Cubical.HITs.CumulativeHierarchy.Base.html#7782" class="Bound">s</a> <a id="7784" class="Symbol">→</a> <a id="7786" href="Cubical.Foundations.Prelude.html#14094" class="Function">isSet</a> <a id="7792" class="Symbol">(∀</a> <a id="7795" href="Cubical.HITs.CumulativeHierarchy.Base.html#7795" class="Bound">t</a> <a id="7797" class="Symbol">→</a> <a id="7799" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="7801" href="Cubical.HITs.CumulativeHierarchy.Base.html#7782" class="Bound">s</a> <a id="7803" href="Cubical.HITs.CumulativeHierarchy.Base.html#7795" class="Bound">t</a><a id="7804" class="Symbol">)</a>
<a id="7810" href="Cubical.HITs.CumulativeHierarchy.Base.html#7767" class="Function">isSetPElim</a> <a id="7821" href="Cubical.HITs.CumulativeHierarchy.Base.html#7821" class="Bound">s</a> <a id="7823" class="Symbol">=</a> <a id="7825" href="Cubical.Foundations.HLevels.html#17906" class="Function">isSetΠ</a> <a id="7832" class="Symbol">(</a><a id="7833" href="Cubical.HITs.CumulativeHierarchy.Base.html#7592" class="Bound">isSetZ</a> <a id="7840" href="Cubical.HITs.CumulativeHierarchy.Base.html#7821" class="Bound">s</a><a id="7841" class="Symbol">)</a>
<a id="7848" href="Cubical.HITs.CumulativeHierarchy.Base.html#7848" class="Function">eliminatorImplX</a> <a id="7864" class="Symbol">:</a> <a id="7866" class="Symbol">(</a><a id="7867" href="Cubical.HITs.CumulativeHierarchy.Base.html#7867" class="Bound">X</a> <a id="7869" class="Symbol">:</a> <a id="7871" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7876" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="7877" class="Symbol">)</a> <a id="7879" class="Symbol">(</a><a id="7880" href="Cubical.HITs.CumulativeHierarchy.Base.html#7880" class="Bound">ix</a> <a id="7883" class="Symbol">:</a> <a id="7885" href="Cubical.HITs.CumulativeHierarchy.Base.html#7867" class="Bound">X</a> <a id="7887" class="Symbol">→</a> <a id="7889" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="7891" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="7892" class="Symbol">)</a>
<a id="7914" class="Symbol">→</a> <a id="7916" class="Symbol">(</a><a id="7917" href="Cubical.HITs.CumulativeHierarchy.Base.html#7917" class="Bound">rec</a> <a id="7921" class="Symbol">:</a> <a id="7923" class="Symbol">∀</a> <a id="7925" href="Cubical.HITs.CumulativeHierarchy.Base.html#7925" class="Bound">x</a> <a id="7927" href="Cubical.HITs.CumulativeHierarchy.Base.html#7927" class="Bound">y</a> <a id="7929" class="Symbol">→</a> <a id="7931" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="7933" class="Symbol">(</a><a id="7934" href="Cubical.HITs.CumulativeHierarchy.Base.html#7880" class="Bound">ix</a> <a id="7937" href="Cubical.HITs.CumulativeHierarchy.Base.html#7925" class="Bound">x</a><a id="7938" class="Symbol">)</a> <a id="7940" href="Cubical.HITs.CumulativeHierarchy.Base.html#7927" class="Bound">y</a><a id="7941" class="Symbol">)</a>
<a id="7963" class="Symbol">→</a> <a id="7965" href="Cubical.HITs.CumulativeHierarchy.Base.html#1877" class="Record">ElimSet</a> <a id="7973" class="Symbol">(λ</a> <a id="7976" href="Cubical.HITs.CumulativeHierarchy.Base.html#7976" class="Bound">t</a> <a id="7978" class="Symbol">→</a> <a id="7980" href="Cubical.HITs.CumulativeHierarchy.Base.html#7592" class="Bound">isSetZ</a> <a id="7987" class="Symbol">(</a><a id="7988" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="7993" href="Cubical.HITs.CumulativeHierarchy.Base.html#7867" class="Bound">X</a> <a id="7995" href="Cubical.HITs.CumulativeHierarchy.Base.html#7880" class="Bound">ix</a><a id="7997" class="Symbol">)</a> <a id="7999" href="Cubical.HITs.CumulativeHierarchy.Base.html#7976" class="Bound">t</a><a id="8000" class="Symbol">)</a>
<a id="8006" href="Cubical.HITs.CumulativeHierarchy.Base.html#2001" class="Field">ElimSett</a> <a id="8015" class="Symbol">(</a><a id="8016" href="Cubical.HITs.CumulativeHierarchy.Base.html#7848" class="Function">eliminatorImplX</a> <a id="8032" href="Cubical.HITs.CumulativeHierarchy.Base.html#8032" class="Bound">X</a> <a id="8034" href="Cubical.HITs.CumulativeHierarchy.Base.html#8034" class="Bound">ix</a> <a id="8037" href="Cubical.HITs.CumulativeHierarchy.Base.html#8037" class="Bound">rec</a><a id="8040" class="Symbol">)</a> <a id="8042" href="Cubical.HITs.CumulativeHierarchy.Base.html#8042" class="Bound">Y</a> <a id="8044" href="Cubical.HITs.CumulativeHierarchy.Base.html#8044" class="Bound">iy</a> <a id="8047" class="Symbol">_</a> <a id="8049" class="Symbol">=</a>
<a id="8057" href="Cubical.HITs.CumulativeHierarchy.Base.html#5317" class="Field">ElimSett2</a> <a id="8067" href="Cubical.HITs.CumulativeHierarchy.Base.html#8032" class="Bound">X</a> <a id="8069" href="Cubical.HITs.CumulativeHierarchy.Base.html#8034" class="Bound">ix</a> <a id="8072" href="Cubical.HITs.CumulativeHierarchy.Base.html#8042" class="Bound">Y</a> <a id="8074" href="Cubical.HITs.CumulativeHierarchy.Base.html#8044" class="Bound">iy</a> <a id="8077" class="Symbol">(λ</a> <a id="8080" href="Cubical.HITs.CumulativeHierarchy.Base.html#8080" class="Bound">x</a> <a id="8082" class="Symbol">→</a> <a id="8084" href="Cubical.HITs.CumulativeHierarchy.Base.html#8037" class="Bound">rec</a> <a id="8088" href="Cubical.HITs.CumulativeHierarchy.Base.html#8080" class="Bound">x</a> <a id="8090" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="8092" href="Cubical.HITs.CumulativeHierarchy.Base.html#8044" class="Bound">iy</a><a id="8094" class="Symbol">)</a>
<a id="8100" href="Cubical.HITs.CumulativeHierarchy.Base.html#2188" class="Field">ElimEq</a> <a id="8107" class="Symbol">(</a><a id="8108" href="Cubical.HITs.CumulativeHierarchy.Base.html#7848" class="Function">eliminatorImplX</a> <a id="8124" href="Cubical.HITs.CumulativeHierarchy.Base.html#8124" class="Bound">X</a> <a id="8126" href="Cubical.HITs.CumulativeHierarchy.Base.html#8126" class="Bound">ix</a> <a id="8129" href="Cubical.HITs.CumulativeHierarchy.Base.html#8129" class="Bound">rec</a><a id="8132" class="Symbol">)</a> <a id="8134" href="Cubical.HITs.CumulativeHierarchy.Base.html#8134" class="Bound">Y₁</a> <a id="8137" href="Cubical.HITs.CumulativeHierarchy.Base.html#8137" class="Bound">Y₂</a> <a id="8140" href="Cubical.HITs.CumulativeHierarchy.Base.html#8140" class="Bound">iy₁</a> <a id="8144" href="Cubical.HITs.CumulativeHierarchy.Base.html#8144" class="Bound">iy₂</a> <a id="8148" href="Cubical.HITs.CumulativeHierarchy.Base.html#8148" class="Bound">eq</a> <a id="8151" class="Symbol">_</a> <a id="8153" class="Symbol">_</a> <a id="8155" class="Symbol">_</a> <a id="8157" class="Symbol">_</a> <a id="8159" class="Symbol">=</a>
<a id="8167" href="Cubical.HITs.CumulativeHierarchy.Base.html#6656" class="Field">ElimEqSnd</a> <a id="8177" href="Cubical.HITs.CumulativeHierarchy.Base.html#8124" class="Bound">X</a> <a id="8179" href="Cubical.HITs.CumulativeHierarchy.Base.html#8126" class="Bound">ix</a> <a id="8182" href="Cubical.HITs.CumulativeHierarchy.Base.html#8134" class="Bound">Y₁</a> <a id="8185" href="Cubical.HITs.CumulativeHierarchy.Base.html#8137" class="Bound">Y₂</a> <a id="8188" href="Cubical.HITs.CumulativeHierarchy.Base.html#8140" class="Bound">iy₁</a> <a id="8192" href="Cubical.HITs.CumulativeHierarchy.Base.html#8144" class="Bound">iy₂</a> <a id="8196" href="Cubical.HITs.CumulativeHierarchy.Base.html#8148" class="Bound">eq</a> <a id="8199" class="Symbol">(λ</a> <a id="8202" href="Cubical.HITs.CumulativeHierarchy.Base.html#8202" class="Bound">x</a> <a id="8204" class="Symbol">→</a> <a id="8206" href="Cubical.HITs.CumulativeHierarchy.Base.html#8129" class="Bound">rec</a> <a id="8210" href="Cubical.HITs.CumulativeHierarchy.Base.html#8202" class="Bound">x</a> <a id="8212" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="8214" href="Cubical.HITs.CumulativeHierarchy.Base.html#8140" class="Bound">iy₁</a><a id="8217" class="Symbol">)</a> <a id="8219" class="Symbol">(λ</a> <a id="8222" href="Cubical.HITs.CumulativeHierarchy.Base.html#8222" class="Bound">x</a> <a id="8224" class="Symbol">→</a> <a id="8226" href="Cubical.HITs.CumulativeHierarchy.Base.html#8129" class="Bound">rec</a> <a id="8230" href="Cubical.HITs.CumulativeHierarchy.Base.html#8222" class="Bound">x</a> <a id="8232" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="8234" href="Cubical.HITs.CumulativeHierarchy.Base.html#8144" class="Bound">iy₂</a><a id="8237" class="Symbol">)</a> <a id="8239" href="Cubical.HITs.CumulativeHierarchy.Base.html#8271" class="Function">rec₁→₂</a> <a id="8246" href="Cubical.HITs.CumulativeHierarchy.Base.html#8445" class="Function">rec₂→₁</a>
<a id="8259" class="Keyword">where</a>
<a id="8271" href="Cubical.HITs.CumulativeHierarchy.Base.html#8271" class="Function">rec₁→₂</a> <a id="8278" class="Symbol">:</a>
<a id="8288" class="Symbol">∀</a> <a id="8290" class="Symbol">(</a><a id="8291" href="Cubical.HITs.CumulativeHierarchy.Base.html#8291" class="Bound">y₁</a> <a id="8294" class="Symbol">:</a> <a id="8296" href="Cubical.HITs.CumulativeHierarchy.Base.html#8134" class="Bound">Y₁</a><a id="8298" class="Symbol">)</a>
<a id="8308" class="Symbol">→</a> <a id="8310" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="8313" href="Cubical.HITs.CumulativeHierarchy.Base.html#8313" class="Bound">(</a><a id="8314" href="Cubical.HITs.CumulativeHierarchy.Base.html#8314" class="Bound">y₂</a> <a id="8317" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="8319" href="Cubical.HITs.CumulativeHierarchy.Base.html#8319" class="Bound">p</a><a id="8320" href="Cubical.HITs.CumulativeHierarchy.Base.html#8313" class="Bound">)</a> <a id="8322" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="8324" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="8330" href="Cubical.HITs.CumulativeHierarchy.Base.html#8144" class="Bound">iy₂</a> <a id="8334" class="Symbol">(</a><a id="8335" href="Cubical.HITs.CumulativeHierarchy.Base.html#8140" class="Bound">iy₁</a> <a id="8339" href="Cubical.HITs.CumulativeHierarchy.Base.html#8291" class="Bound">y₁</a><a id="8341" class="Symbol">)</a> <a id="8343" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="8358" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="8364" class="Symbol">(λ</a> <a id="8367" href="Cubical.HITs.CumulativeHierarchy.Base.html#8367" class="Bound">i</a> <a id="8369" class="Symbol">→</a> <a id="8371" class="Symbol">∀</a> <a id="8373" href="Cubical.HITs.CumulativeHierarchy.Base.html#8373" class="Bound">x</a> <a id="8375" class="Symbol">→</a> <a id="8377" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="8379" class="Symbol">(</a><a id="8380" href="Cubical.HITs.CumulativeHierarchy.Base.html#8126" class="Bound">ix</a> <a id="8383" href="Cubical.HITs.CumulativeHierarchy.Base.html#8373" class="Bound">x</a><a id="8384" class="Symbol">)</a> <a id="8386" class="Symbol">(</a><a id="8387" href="Cubical.HITs.CumulativeHierarchy.Base.html#8319" class="Bound">p</a> <a id="8389" href="Cubical.HITs.CumulativeHierarchy.Base.html#8367" class="Bound">i</a><a id="8390" class="Symbol">))</a> <a id="8393" class="Symbol">(λ</a> <a id="8396" href="Cubical.HITs.CumulativeHierarchy.Base.html#8396" class="Bound">x</a> <a id="8398" class="Symbol">→</a> <a id="8400" href="Cubical.HITs.CumulativeHierarchy.Base.html#8129" class="Bound">rec</a> <a id="8404" href="Cubical.HITs.CumulativeHierarchy.Base.html#8396" class="Bound">x</a> <a id="8406" class="Symbol">(</a><a id="8407" href="Cubical.HITs.CumulativeHierarchy.Base.html#8144" class="Bound">iy₂</a> <a id="8411" href="Cubical.HITs.CumulativeHierarchy.Base.html#8314" class="Bound">y₂</a><a id="8413" class="Symbol">))</a> <a id="8416" class="Symbol">(λ</a> <a id="8419" href="Cubical.HITs.CumulativeHierarchy.Base.html#8419" class="Bound">x</a> <a id="8421" class="Symbol">→</a> <a id="8423" href="Cubical.HITs.CumulativeHierarchy.Base.html#8129" class="Bound">rec</a> <a id="8427" href="Cubical.HITs.CumulativeHierarchy.Base.html#8419" class="Bound">x</a> <a id="8429" class="Symbol">(</a><a id="8430" href="Cubical.HITs.CumulativeHierarchy.Base.html#8140" class="Bound">iy₁</a> <a id="8434" href="Cubical.HITs.CumulativeHierarchy.Base.html#8291" class="Bound">y₁</a><a id="8436" class="Symbol">))</a>
<a id="8445" href="Cubical.HITs.CumulativeHierarchy.Base.html#8445" class="Function">rec₂→₁</a> <a id="8452" class="Symbol">:</a>
<a id="8462" class="Symbol">∀</a> <a id="8464" class="Symbol">(</a><a id="8465" href="Cubical.HITs.CumulativeHierarchy.Base.html#8465" class="Bound">y₂</a> <a id="8468" class="Symbol">:</a> <a id="8470" href="Cubical.HITs.CumulativeHierarchy.Base.html#8137" class="Bound">Y₂</a><a id="8472" class="Symbol">)</a>
<a id="8482" class="Symbol">→</a> <a id="8484" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="8487" href="Cubical.HITs.CumulativeHierarchy.Base.html#8487" class="Bound">(</a><a id="8488" href="Cubical.HITs.CumulativeHierarchy.Base.html#8488" class="Bound">y₁</a> <a id="8491" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="8493" href="Cubical.HITs.CumulativeHierarchy.Base.html#8493" class="Bound">p</a><a id="8494" href="Cubical.HITs.CumulativeHierarchy.Base.html#8487" class="Bound">)</a> <a id="8496" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="8498" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="8504" href="Cubical.HITs.CumulativeHierarchy.Base.html#8140" class="Bound">iy₁</a> <a id="8508" class="Symbol">(</a><a id="8509" href="Cubical.HITs.CumulativeHierarchy.Base.html#8144" class="Bound">iy₂</a> <a id="8513" href="Cubical.HITs.CumulativeHierarchy.Base.html#8465" class="Bound">y₂</a><a id="8515" class="Symbol">)</a> <a id="8517" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="8532" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="8538" class="Symbol">(λ</a> <a id="8541" href="Cubical.HITs.CumulativeHierarchy.Base.html#8541" class="Bound">i</a> <a id="8543" class="Symbol">→</a> <a id="8545" class="Symbol">∀</a> <a id="8547" href="Cubical.HITs.CumulativeHierarchy.Base.html#8547" class="Bound">x</a> <a id="8549" class="Symbol">→</a> <a id="8551" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="8553" class="Symbol">(</a><a id="8554" href="Cubical.HITs.CumulativeHierarchy.Base.html#8126" class="Bound">ix</a> <a id="8557" href="Cubical.HITs.CumulativeHierarchy.Base.html#8547" class="Bound">x</a><a id="8558" class="Symbol">)</a> <a id="8560" class="Symbol">(</a><a id="8561" href="Cubical.HITs.CumulativeHierarchy.Base.html#8493" class="Bound">p</a> <a id="8563" href="Cubical.HITs.CumulativeHierarchy.Base.html#8541" class="Bound">i</a><a id="8564" class="Symbol">))</a> <a id="8567" class="Symbol">(λ</a> <a id="8570" href="Cubical.HITs.CumulativeHierarchy.Base.html#8570" class="Bound">x</a> <a id="8572" class="Symbol">→</a> <a id="8574" href="Cubical.HITs.CumulativeHierarchy.Base.html#8129" class="Bound">rec</a> <a id="8578" href="Cubical.HITs.CumulativeHierarchy.Base.html#8570" class="Bound">x</a> <a id="8580" class="Symbol">(</a><a id="8581" href="Cubical.HITs.CumulativeHierarchy.Base.html#8140" class="Bound">iy₁</a> <a id="8585" href="Cubical.HITs.CumulativeHierarchy.Base.html#8488" class="Bound">y₁</a><a id="8587" class="Symbol">))</a> <a id="8590" class="Symbol">(λ</a> <a id="8593" href="Cubical.HITs.CumulativeHierarchy.Base.html#8593" class="Bound">x</a> <a id="8595" class="Symbol">→</a> <a id="8597" href="Cubical.HITs.CumulativeHierarchy.Base.html#8129" class="Bound">rec</a> <a id="8601" href="Cubical.HITs.CumulativeHierarchy.Base.html#8593" class="Bound">x</a> <a id="8603" class="Symbol">(</a><a id="8604" href="Cubical.HITs.CumulativeHierarchy.Base.html#8144" class="Bound">iy₂</a> <a id="8608" href="Cubical.HITs.CumulativeHierarchy.Base.html#8465" class="Bound">y₂</a><a id="8610" class="Symbol">))</a>
<a id="8619" href="Cubical.HITs.CumulativeHierarchy.Base.html#8271" class="Function">rec₁→₂</a> <a id="8626" href="Cubical.HITs.CumulativeHierarchy.Base.html#8626" class="Bound">y₁</a> <a id="8629" class="Symbol">=</a> <a id="8631" class="Keyword">do</a> <a id="8634" class="Symbol">(</a><a id="8635" href="Cubical.HITs.CumulativeHierarchy.Base.html#8635" class="Bound">y₂</a> <a id="8638" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="8640" href="Cubical.HITs.CumulativeHierarchy.Base.html#8640" class="Bound">yy</a><a id="8642" class="Symbol">)</a> <a id="8644" href="Cubical.HITs.PropositionalTruncation.Monad.html#624" class="Function Operator">←</a> <a id="8646" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="8650" href="Cubical.HITs.CumulativeHierarchy.Base.html#8148" class="Bound">eq</a> <a id="8653" href="Cubical.HITs.CumulativeHierarchy.Base.html#8626" class="Bound">y₁</a> <a id="8656" class="Symbol">;</a> <a id="8658" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="8660" class="Symbol">(</a><a id="8661" href="Cubical.HITs.CumulativeHierarchy.Base.html#8635" class="Bound">y₂</a> <a id="8664" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="8666" href="Cubical.HITs.CumulativeHierarchy.Base.html#8640" class="Bound">yy</a><a id="8668" class="Symbol">)</a> <a id="8670" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="8672" class="Symbol">(λ</a> <a id="8675" href="Cubical.HITs.CumulativeHierarchy.Base.html#8675" class="Bound">i</a> <a id="8677" href="Cubical.HITs.CumulativeHierarchy.Base.html#8677" class="Bound">x</a> <a id="8679" class="Symbol">→</a> <a id="8681" href="Cubical.HITs.CumulativeHierarchy.Base.html#8129" class="Bound">rec</a> <a id="8685" href="Cubical.HITs.CumulativeHierarchy.Base.html#8677" class="Bound">x</a> <a id="8687" class="Symbol">(</a><a id="8688" href="Cubical.HITs.CumulativeHierarchy.Base.html#8640" class="Bound">yy</a> <a id="8691" href="Cubical.HITs.CumulativeHierarchy.Base.html#8675" class="Bound">i</a><a id="8692" class="Symbol">))</a> <a id="8695" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a>
<a id="8704" href="Cubical.HITs.CumulativeHierarchy.Base.html#8445" class="Function">rec₂→₁</a> <a id="8711" href="Cubical.HITs.CumulativeHierarchy.Base.html#8711" class="Bound">y₂</a> <a id="8714" class="Symbol">=</a> <a id="8716" class="Keyword">do</a> <a id="8719" class="Symbol">(</a><a id="8720" href="Cubical.HITs.CumulativeHierarchy.Base.html#8720" class="Bound">y₁</a> <a id="8723" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="8725" href="Cubical.HITs.CumulativeHierarchy.Base.html#8725" class="Bound">yy</a><a id="8727" class="Symbol">)</a> <a id="8729" href="Cubical.HITs.PropositionalTruncation.Monad.html#624" class="Function Operator">←</a> <a id="8731" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="8735" href="Cubical.HITs.CumulativeHierarchy.Base.html#8148" class="Bound">eq</a> <a id="8738" href="Cubical.HITs.CumulativeHierarchy.Base.html#8711" class="Bound">y₂</a> <a id="8741" class="Symbol">;</a> <a id="8743" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="8745" class="Symbol">(</a><a id="8746" href="Cubical.HITs.CumulativeHierarchy.Base.html#8720" class="Bound">y₁</a> <a id="8749" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="8751" href="Cubical.HITs.CumulativeHierarchy.Base.html#8725" class="Bound">yy</a><a id="8753" class="Symbol">)</a> <a id="8755" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="8757" class="Symbol">(λ</a> <a id="8760" href="Cubical.HITs.CumulativeHierarchy.Base.html#8760" class="Bound">i</a> <a id="8762" href="Cubical.HITs.CumulativeHierarchy.Base.html#8762" class="Bound">x</a> <a id="8764" class="Symbol">→</a> <a id="8766" href="Cubical.HITs.CumulativeHierarchy.Base.html#8129" class="Bound">rec</a> <a id="8770" href="Cubical.HITs.CumulativeHierarchy.Base.html#8762" class="Bound">x</a> <a id="8772" class="Symbol">(</a><a id="8773" href="Cubical.HITs.CumulativeHierarchy.Base.html#8725" class="Bound">yy</a> <a id="8776" href="Cubical.HITs.CumulativeHierarchy.Base.html#8760" class="Bound">i</a><a id="8777" class="Symbol">))</a> <a id="8780" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a>
<a id="8788" href="Cubical.HITs.CumulativeHierarchy.Base.html#8788" class="Function">elimImplS</a> <a id="8798" class="Symbol">:</a>
<a id="8806" class="Symbol">∀</a> <a id="8808" class="Symbol">(</a><a id="8809" href="Cubical.HITs.CumulativeHierarchy.Base.html#8809" class="Bound">X</a> <a id="8811" class="Symbol">:</a> <a id="8813" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8818" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="8819" class="Symbol">)</a> <a id="8821" class="Symbol">(</a><a id="8822" href="Cubical.HITs.CumulativeHierarchy.Base.html#8822" class="Bound">ix</a> <a id="8825" class="Symbol">:</a> <a id="8827" href="Cubical.HITs.CumulativeHierarchy.Base.html#8809" class="Bound">X</a> <a id="8829" class="Symbol">→</a> <a id="8831" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="8833" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="8834" class="Symbol">)</a>
<a id="8842" class="Symbol">→</a> <a id="8844" class="Symbol">(∀</a> <a id="8847" href="Cubical.HITs.CumulativeHierarchy.Base.html#8847" class="Bound">x</a> <a id="8849" href="Cubical.HITs.CumulativeHierarchy.Base.html#8849" class="Bound">t₂</a> <a id="8852" class="Symbol">→</a> <a id="8854" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="8856" class="Symbol">(</a><a id="8857" href="Cubical.HITs.CumulativeHierarchy.Base.html#8822" class="Bound">ix</a> <a id="8860" href="Cubical.HITs.CumulativeHierarchy.Base.html#8847" class="Bound">x</a><a id="8861" class="Symbol">)</a> <a id="8863" href="Cubical.HITs.CumulativeHierarchy.Base.html#8849" class="Bound">t₂</a><a id="8865" class="Symbol">)</a>
<a id="8873" class="Symbol">→</a> <a id="8875" class="Symbol">(</a><a id="8876" href="Cubical.HITs.CumulativeHierarchy.Base.html#8876" class="Bound">t</a> <a id="8878" class="Symbol">:</a> <a id="8880" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="8882" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="8883" class="Symbol">)</a> <a id="8885" class="Symbol">→</a> <a id="8887" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="8889" class="Symbol">(</a><a id="8890" href="Cubical.HITs.CumulativeHierarchy.Base.html#1291" class="InductiveConstructor">sett</a> <a id="8895" href="Cubical.HITs.CumulativeHierarchy.Base.html#8809" class="Bound">X</a> <a id="8897" href="Cubical.HITs.CumulativeHierarchy.Base.html#8822" class="Bound">ix</a><a id="8899" class="Symbol">)</a> <a id="8901" href="Cubical.HITs.CumulativeHierarchy.Base.html#8876" class="Bound">t</a>
<a id="8907" href="Cubical.HITs.CumulativeHierarchy.Base.html#8788" class="Function">elimImplS</a> <a id="8917" href="Cubical.HITs.CumulativeHierarchy.Base.html#8917" class="Bound">X</a> <a id="8919" href="Cubical.HITs.CumulativeHierarchy.Base.html#8919" class="Bound">ix</a> <a id="8922" href="Cubical.HITs.CumulativeHierarchy.Base.html#8922" class="Bound">rec</a> <a id="8926" class="Symbol">=</a> <a id="8928" href="Cubical.HITs.CumulativeHierarchy.Base.html#2883" class="Function">elim</a> <a id="8933" class="Symbol">(</a><a id="8934" href="Cubical.HITs.CumulativeHierarchy.Base.html#7848" class="Function">eliminatorImplX</a> <a id="8950" href="Cubical.HITs.CumulativeHierarchy.Base.html#8917" class="Bound">X</a> <a id="8952" href="Cubical.HITs.CumulativeHierarchy.Base.html#8919" class="Bound">ix</a> <a id="8955" href="Cubical.HITs.CumulativeHierarchy.Base.html#8922" class="Bound">rec</a><a id="8958" class="Symbol">)</a>
<a id="8965" href="Cubical.HITs.CumulativeHierarchy.Base.html#8965" class="Function">elimImplSExt</a> <a id="8978" class="Symbol">:</a>
<a id="8986" class="Symbol">∀</a> <a id="8988" class="Symbol">(</a><a id="8989" href="Cubical.HITs.CumulativeHierarchy.Base.html#8989" class="Bound">X₁</a> <a id="8992" href="Cubical.HITs.CumulativeHierarchy.Base.html#8992" class="Bound">X₂</a> <a id="8995" class="Symbol">:</a> <a id="8997" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="9002" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="9003" class="Symbol">)</a> <a id="9005" class="Symbol">(</a><a id="9006" href="Cubical.HITs.CumulativeHierarchy.Base.html#9006" class="Bound">ix₁</a> <a id="9010" class="Symbol">:</a> <a id="9012" href="Cubical.HITs.CumulativeHierarchy.Base.html#8989" class="Bound">X₁</a> <a id="9015" class="Symbol">→</a> <a id="9017" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="9019" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="9020" class="Symbol">)</a> <a id="9022" class="Symbol">(</a><a id="9023" href="Cubical.HITs.CumulativeHierarchy.Base.html#9023" class="Bound">ix₂</a> <a id="9027" class="Symbol">:</a> <a id="9029" href="Cubical.HITs.CumulativeHierarchy.Base.html#8992" class="Bound">X₂</a> <a id="9032" class="Symbol">→</a> <a id="9034" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="9036" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="9037" class="Symbol">)</a> <a id="9039" class="Symbol">→</a> <a id="9041" class="Symbol">(</a><a id="9042" href="Cubical.HITs.CumulativeHierarchy.Base.html#9042" class="Bound">eq</a> <a id="9045" class="Symbol">:</a> <a id="9047" href="Cubical.HITs.CumulativeHierarchy.Base.html#1064" class="Function">eqImage</a> <a id="9055" href="Cubical.HITs.CumulativeHierarchy.Base.html#9006" class="Bound">ix₁</a> <a id="9059" href="Cubical.HITs.CumulativeHierarchy.Base.html#9023" class="Bound">ix₂</a><a id="9062" class="Symbol">)</a>
<a id="9070" class="Symbol">→</a> <a id="9072" class="Symbol">(</a><a id="9073" href="Cubical.HITs.CumulativeHierarchy.Base.html#9073" class="Bound">rec₁</a> <a id="9078" class="Symbol">:</a> <a id="9080" class="Symbol">∀</a> <a id="9082" href="Cubical.HITs.CumulativeHierarchy.Base.html#9082" class="Bound">x₁</a> <a id="9085" href="Cubical.HITs.CumulativeHierarchy.Base.html#9085" class="Bound">t₂</a> <a id="9088" class="Symbol">→</a> <a id="9090" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="9092" class="Symbol">(</a><a id="9093" href="Cubical.HITs.CumulativeHierarchy.Base.html#9006" class="Bound">ix₁</a> <a id="9097" href="Cubical.HITs.CumulativeHierarchy.Base.html#9082" class="Bound">x₁</a><a id="9099" class="Symbol">)</a> <a id="9101" href="Cubical.HITs.CumulativeHierarchy.Base.html#9085" class="Bound">t₂</a><a id="9103" class="Symbol">)</a> <a id="9105" class="Symbol">(</a><a id="9106" href="Cubical.HITs.CumulativeHierarchy.Base.html#9106" class="Bound">rec₂</a> <a id="9111" class="Symbol">:</a> <a id="9113" class="Symbol">∀</a> <a id="9115" href="Cubical.HITs.CumulativeHierarchy.Base.html#9115" class="Bound">x₂</a> <a id="9118" href="Cubical.HITs.CumulativeHierarchy.Base.html#9118" class="Bound">t₂</a> <a id="9121" class="Symbol">→</a> <a id="9123" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="9125" class="Symbol">(</a><a id="9126" href="Cubical.HITs.CumulativeHierarchy.Base.html#9023" class="Bound">ix₂</a> <a id="9130" href="Cubical.HITs.CumulativeHierarchy.Base.html#9115" class="Bound">x₂</a><a id="9132" class="Symbol">)</a> <a id="9134" href="Cubical.HITs.CumulativeHierarchy.Base.html#9118" class="Bound">t₂</a><a id="9136" class="Symbol">)</a>
<a id="9144" class="Symbol">→</a> <a id="9146" class="Symbol">((</a><a id="9148" href="Cubical.HITs.CumulativeHierarchy.Base.html#9148" class="Bound">x₁</a> <a id="9151" class="Symbol">:</a> <a id="9153" href="Cubical.HITs.CumulativeHierarchy.Base.html#8989" class="Bound">X₁</a><a id="9155" class="Symbol">)</a> <a id="9157" class="Symbol">→</a> <a id="9159" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="9162" href="Cubical.HITs.CumulativeHierarchy.Base.html#9162" class="Bound">(</a><a id="9163" href="Cubical.HITs.CumulativeHierarchy.Base.html#9163" class="Bound">x₂</a> <a id="9166" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="9168" href="Cubical.HITs.CumulativeHierarchy.Base.html#9168" class="Bound">p</a><a id="9169" href="Cubical.HITs.CumulativeHierarchy.Base.html#9162" class="Bound">)</a> <a id="9171" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="9173" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="9179" href="Cubical.HITs.CumulativeHierarchy.Base.html#9023" class="Bound">ix₂</a> <a id="9183" class="Symbol">(</a><a id="9184" href="Cubical.HITs.CumulativeHierarchy.Base.html#9006" class="Bound">ix₁</a> <a id="9188" href="Cubical.HITs.CumulativeHierarchy.Base.html#9148" class="Bound">x₁</a><a id="9190" class="Symbol">)</a> <a id="9192" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="9218" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="9224" class="Symbol">(λ</a> <a id="9227" href="Cubical.HITs.CumulativeHierarchy.Base.html#9227" class="Bound">i</a> <a id="9229" class="Symbol">→</a> <a id="9231" class="Symbol">∀</a> <a id="9233" href="Cubical.HITs.CumulativeHierarchy.Base.html#9233" class="Bound">t</a> <a id="9235" class="Symbol">→</a> <a id="9237" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="9239" class="Symbol">(</a><a id="9240" href="Cubical.HITs.CumulativeHierarchy.Base.html#9168" class="Bound">p</a> <a id="9242" href="Cubical.HITs.CumulativeHierarchy.Base.html#9227" class="Bound">i</a><a id="9243" class="Symbol">)</a> <a id="9245" href="Cubical.HITs.CumulativeHierarchy.Base.html#9233" class="Bound">t</a><a id="9246" class="Symbol">)</a> <a id="9248" class="Symbol">(</a><a id="9249" href="Cubical.HITs.CumulativeHierarchy.Base.html#9106" class="Bound">rec₂</a> <a id="9254" href="Cubical.HITs.CumulativeHierarchy.Base.html#9163" class="Bound">x₂</a><a id="9256" class="Symbol">)</a> <a id="9258" class="Symbol">(</a><a id="9259" href="Cubical.HITs.CumulativeHierarchy.Base.html#9073" class="Bound">rec₁</a> <a id="9264" href="Cubical.HITs.CumulativeHierarchy.Base.html#9148" class="Bound">x₁</a><a id="9266" class="Symbol">))</a>
<a id="9275" class="Symbol">→</a> <a id="9277" class="Symbol">((</a><a id="9279" href="Cubical.HITs.CumulativeHierarchy.Base.html#9279" class="Bound">x₂</a> <a id="9282" class="Symbol">:</a> <a id="9284" href="Cubical.HITs.CumulativeHierarchy.Base.html#8992" class="Bound">X₂</a><a id="9286" class="Symbol">)</a> <a id="9288" class="Symbol">→</a> <a id="9290" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="9293" href="Cubical.HITs.CumulativeHierarchy.Base.html#9293" class="Bound">(</a><a id="9294" href="Cubical.HITs.CumulativeHierarchy.Base.html#9294" class="Bound">x₁</a> <a id="9297" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="9299" href="Cubical.HITs.CumulativeHierarchy.Base.html#9299" class="Bound">p</a><a id="9300" href="Cubical.HITs.CumulativeHierarchy.Base.html#9293" class="Bound">)</a> <a id="9302" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="9304" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="9310" href="Cubical.HITs.CumulativeHierarchy.Base.html#9006" class="Bound">ix₁</a> <a id="9314" class="Symbol">(</a><a id="9315" href="Cubical.HITs.CumulativeHierarchy.Base.html#9023" class="Bound">ix₂</a> <a id="9319" href="Cubical.HITs.CumulativeHierarchy.Base.html#9279" class="Bound">x₂</a><a id="9321" class="Symbol">)</a> <a id="9323" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="9349" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="9355" class="Symbol">(λ</a> <a id="9358" href="Cubical.HITs.CumulativeHierarchy.Base.html#9358" class="Bound">i</a> <a id="9360" class="Symbol">→</a> <a id="9362" class="Symbol">∀</a> <a id="9364" href="Cubical.HITs.CumulativeHierarchy.Base.html#9364" class="Bound">t</a> <a id="9366" class="Symbol">→</a> <a id="9368" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="9370" class="Symbol">(</a><a id="9371" href="Cubical.HITs.CumulativeHierarchy.Base.html#9299" class="Bound">p</a> <a id="9373" href="Cubical.HITs.CumulativeHierarchy.Base.html#9358" class="Bound">i</a><a id="9374" class="Symbol">)</a> <a id="9376" href="Cubical.HITs.CumulativeHierarchy.Base.html#9364" class="Bound">t</a><a id="9377" class="Symbol">)</a> <a id="9379" class="Symbol">(</a><a id="9380" href="Cubical.HITs.CumulativeHierarchy.Base.html#9073" class="Bound">rec₁</a> <a id="9385" href="Cubical.HITs.CumulativeHierarchy.Base.html#9294" class="Bound">x₁</a><a id="9387" class="Symbol">)</a> <a id="9389" class="Symbol">(</a><a id="9390" href="Cubical.HITs.CumulativeHierarchy.Base.html#9106" class="Bound">rec₂</a> <a id="9395" href="Cubical.HITs.CumulativeHierarchy.Base.html#9279" class="Bound">x₂</a><a id="9397" class="Symbol">))</a>
<a id="9406" class="Symbol">→</a> <a id="9408" class="Symbol">(</a><a id="9409" href="Cubical.HITs.CumulativeHierarchy.Base.html#9409" class="Bound">t</a> <a id="9411" class="Symbol">:</a> <a id="9413" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="9415" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="9416" class="Symbol">)</a>
<a id="9424" class="Symbol">→</a> <a id="9426" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="9432" class="Symbol">(λ</a> <a id="9435" href="Cubical.HITs.CumulativeHierarchy.Base.html#9435" class="Bound">i</a> <a id="9437" class="Symbol">→</a> <a id="9439" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="9441" class="Symbol">(</a><a id="9442" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="9448" href="Cubical.HITs.CumulativeHierarchy.Base.html#8989" class="Bound">X₁</a> <a id="9451" href="Cubical.HITs.CumulativeHierarchy.Base.html#8992" class="Bound">X₂</a> <a id="9454" href="Cubical.HITs.CumulativeHierarchy.Base.html#9006" class="Bound">ix₁</a> <a id="9458" href="Cubical.HITs.CumulativeHierarchy.Base.html#9023" class="Bound">ix₂</a> <a id="9462" href="Cubical.HITs.CumulativeHierarchy.Base.html#9042" class="Bound">eq</a> <a id="9465" href="Cubical.HITs.CumulativeHierarchy.Base.html#9435" class="Bound">i</a><a id="9466" class="Symbol">)</a> <a id="9468" href="Cubical.HITs.CumulativeHierarchy.Base.html#9409" class="Bound">t</a><a id="9469" class="Symbol">)</a>
<a id="9485" class="Symbol">(</a><a id="9486" href="Cubical.HITs.CumulativeHierarchy.Base.html#8788" class="Function">elimImplS</a> <a id="9496" href="Cubical.HITs.CumulativeHierarchy.Base.html#8989" class="Bound">X₁</a> <a id="9499" href="Cubical.HITs.CumulativeHierarchy.Base.html#9006" class="Bound">ix₁</a> <a id="9503" href="Cubical.HITs.CumulativeHierarchy.Base.html#9073" class="Bound">rec₁</a> <a id="9508" href="Cubical.HITs.CumulativeHierarchy.Base.html#9409" class="Bound">t</a><a id="9509" class="Symbol">)</a>
<a id="9525" class="Symbol">(</a><a id="9526" href="Cubical.HITs.CumulativeHierarchy.Base.html#8788" class="Function">elimImplS</a> <a id="9536" href="Cubical.HITs.CumulativeHierarchy.Base.html#8992" class="Bound">X₂</a> <a id="9539" href="Cubical.HITs.CumulativeHierarchy.Base.html#9023" class="Bound">ix₂</a> <a id="9543" href="Cubical.HITs.CumulativeHierarchy.Base.html#9106" class="Bound">rec₂</a> <a id="9548" href="Cubical.HITs.CumulativeHierarchy.Base.html#9409" class="Bound">t</a><a id="9549" class="Symbol">)</a>
<a id="9555" href="Cubical.HITs.CumulativeHierarchy.Base.html#8965" class="Function">elimImplSExt</a> <a id="9568" href="Cubical.HITs.CumulativeHierarchy.Base.html#9568" class="Bound">X₁</a> <a id="9571" href="Cubical.HITs.CumulativeHierarchy.Base.html#9571" class="Bound">X₂</a> <a id="9574" href="Cubical.HITs.CumulativeHierarchy.Base.html#9574" class="Bound">ix₁</a> <a id="9578" href="Cubical.HITs.CumulativeHierarchy.Base.html#9578" class="Bound">ix₂</a> <a id="9582" href="Cubical.HITs.CumulativeHierarchy.Base.html#9582" class="Bound">eq</a> <a id="9585" href="Cubical.HITs.CumulativeHierarchy.Base.html#9585" class="Bound">rec₁</a> <a id="9590" href="Cubical.HITs.CumulativeHierarchy.Base.html#9590" class="Bound">rec₂</a> <a id="9595" href="Cubical.HITs.CumulativeHierarchy.Base.html#9595" class="Bound">rec₁→₂</a> <a id="9602" href="Cubical.HITs.CumulativeHierarchy.Base.html#9602" class="Bound">rec₂→₁</a> <a id="9609" class="Symbol">=</a>
<a id="9617" href="Cubical.HITs.CumulativeHierarchy.Base.html#4364" class="Function">elimProp</a> <a id="9626" href="Cubical.HITs.CumulativeHierarchy.Base.html#9686" class="Function">propPathP</a> <a id="9636" class="Symbol">(λ</a> <a id="9639" href="Cubical.HITs.CumulativeHierarchy.Base.html#9639" class="Bound">Y</a> <a id="9641" href="Cubical.HITs.CumulativeHierarchy.Base.html#9641" class="Bound">iy</a> <a id="9644" href="Cubical.HITs.CumulativeHierarchy.Base.html#9644" class="Bound">_</a> <a id="9646" class="Symbol">→</a> <a id="9648" href="Cubical.HITs.CumulativeHierarchy.Base.html#9978" class="Function">elimImplSExtT</a> <a id="9662" href="Cubical.HITs.CumulativeHierarchy.Base.html#9639" class="Bound">Y</a> <a id="9664" href="Cubical.HITs.CumulativeHierarchy.Base.html#9641" class="Bound">iy</a><a id="9666" class="Symbol">)</a>
<a id="9674" class="Keyword">where</a>
<a id="9686" href="Cubical.HITs.CumulativeHierarchy.Base.html#9686" class="Function">propPathP</a> <a id="9696" class="Symbol">:</a> <a id="9698" class="Symbol">(</a><a id="9699" href="Cubical.HITs.CumulativeHierarchy.Base.html#9699" class="Bound">t</a> <a id="9701" class="Symbol">:</a> <a id="9703" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="9705" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="9706" class="Symbol">)</a>
<a id="9724" class="Symbol">→</a> <a id="9726" href="Cubical.Foundations.Prelude.html#14039" class="Function">isProp</a> <a id="9733" class="Symbol">(</a><a id="9734" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="9740" class="Symbol">(λ</a> <a id="9743" href="Cubical.HITs.CumulativeHierarchy.Base.html#9743" class="Bound">i</a> <a id="9745" class="Symbol">→</a> <a id="9747" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="9749" class="Symbol">(</a><a id="9750" href="Cubical.HITs.CumulativeHierarchy.Base.html#1331" class="InductiveConstructor">seteq</a> <a id="9756" href="Cubical.HITs.CumulativeHierarchy.Base.html#9568" class="Bound">X₁</a> <a id="9759" href="Cubical.HITs.CumulativeHierarchy.Base.html#9571" class="Bound">X₂</a> <a id="9762" href="Cubical.HITs.CumulativeHierarchy.Base.html#9574" class="Bound">ix₁</a> <a id="9766" href="Cubical.HITs.CumulativeHierarchy.Base.html#9578" class="Bound">ix₂</a> <a id="9770" href="Cubical.HITs.CumulativeHierarchy.Base.html#9582" class="Bound">eq</a> <a id="9773" href="Cubical.HITs.CumulativeHierarchy.Base.html#9743" class="Bound">i</a><a id="9774" class="Symbol">)</a> <a id="9776" href="Cubical.HITs.CumulativeHierarchy.Base.html#9699" class="Bound">t</a><a id="9777" class="Symbol">)</a>
<a id="9811" class="Symbol">(</a><a id="9812" href="Cubical.HITs.CumulativeHierarchy.Base.html#8788" class="Function">elimImplS</a> <a id="9822" href="Cubical.HITs.CumulativeHierarchy.Base.html#9568" class="Bound">X₁</a> <a id="9825" href="Cubical.HITs.CumulativeHierarchy.Base.html#9574" class="Bound">ix₁</a> <a id="9829" href="Cubical.HITs.CumulativeHierarchy.Base.html#9585" class="Bound">rec₁</a> <a id="9834" href="Cubical.HITs.CumulativeHierarchy.Base.html#9699" class="Bound">t</a><a id="9835" class="Symbol">)</a>
<a id="9869" class="Symbol">(</a><a id="9870" href="Cubical.HITs.CumulativeHierarchy.Base.html#8788" class="Function">elimImplS</a> <a id="9880" href="Cubical.HITs.CumulativeHierarchy.Base.html#9571" class="Bound">X₂</a> <a id="9883" href="Cubical.HITs.CumulativeHierarchy.Base.html#9578" class="Bound">ix₂</a> <a id="9887" href="Cubical.HITs.CumulativeHierarchy.Base.html#9590" class="Bound">rec₂</a> <a id="9892" href="Cubical.HITs.CumulativeHierarchy.Base.html#9699" class="Bound">t</a><a id="9893" class="Symbol">))</a>
<a id="9902" href="Cubical.HITs.CumulativeHierarchy.Base.html#9686" class="Function">propPathP</a> <a id="9912" class="Symbol">_</a> <a id="9914" class="Symbol">=</a> <a id="9916" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="9922" href="Cubical.Foundations.Prelude.html#14039" class="Function">isProp</a> <a id="9929" class="Symbol">(</a><a id="9930" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="9934" class="Symbol">(</a><a id="9935" href="Cubical.Foundations.Path.html#917" class="Function">PathP≡Path</a> <a id="9946" class="Symbol">_</a> <a id="9948" class="Symbol">_</a> <a id="9950" class="Symbol">_))</a> <a id="9954" class="Symbol">(</a><a id="9955" href="Cubical.HITs.CumulativeHierarchy.Base.html#7592" class="Bound">isSetZ</a> <a id="9962" class="Symbol">_</a> <a id="9964" class="Symbol">_</a> <a id="9966" class="Symbol">_</a> <a id="9968" class="Symbol">_)</a>
<a id="9978" href="Cubical.HITs.CumulativeHierarchy.Base.html#9978" class="Function">elimImplSExtT</a> <a id="9992" class="Symbol">:</a> <a id="9994" class="Symbol">(</a><a id="9995" href="Cubical.HITs.CumulativeHierarchy.Base.html#9995" class="Bound">Y</a> <a id="9997" class="Symbol">:</a> <a id="9999" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="10004" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="10005" class="Symbol">)</a> <a id="10007" class="Symbol">(</a><a id="10008" href="Cubical.HITs.CumulativeHierarchy.Base.html#10008" class="Bound">iy</a> <a id="10011" class="Symbol">:</a> <a id="10013" href="Cubical.HITs.CumulativeHierarchy.Base.html#9995" class="Bound">Y</a> <a id="10015" class="Symbol">→</a> <a id="10017" href="Cubical.HITs.CumulativeHierarchy.Base.html#996" class="Datatype">V</a> <a id="10019" href="Cubical.HITs.CumulativeHierarchy.Base.html#7577" class="Bound">ℓ</a><a id="10020" class="Symbol">)</a> <a id="10022" class="Symbol">→</a> <a id="10024" class="Symbol">_</a> <a id="10026" class="Comment">{- the appropriate path type -}</a>
<a id="10064" href="Cubical.HITs.CumulativeHierarchy.Base.html#9978" class="Function">elimImplSExtT</a> <a id="10078" href="Cubical.HITs.CumulativeHierarchy.Base.html#10078" class="Bound">Y</a> <a id="10080" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10083" class="Symbol">=</a>
<a id="10093" href="Cubical.HITs.CumulativeHierarchy.Base.html#5655" class="Field">ElimEqFst</a> <a id="10103" href="Cubical.HITs.CumulativeHierarchy.Base.html#9568" class="Bound">X₁</a> <a id="10106" href="Cubical.HITs.CumulativeHierarchy.Base.html#9571" class="Bound">X₂</a> <a id="10109" href="Cubical.HITs.CumulativeHierarchy.Base.html#9574" class="Bound">ix₁</a> <a id="10113" href="Cubical.HITs.CumulativeHierarchy.Base.html#9578" class="Bound">ix₂</a> <a id="10117" href="Cubical.HITs.CumulativeHierarchy.Base.html#9582" class="Bound">eq</a> <a id="10120" href="Cubical.HITs.CumulativeHierarchy.Base.html#10078" class="Bound">Y</a> <a id="10122" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10125" class="Symbol">(λ</a> <a id="10128" href="Cubical.HITs.CumulativeHierarchy.Base.html#10128" class="Bound">x₁</a> <a id="10131" href="Cubical.HITs.CumulativeHierarchy.Base.html#10131" class="Bound">y</a> <a id="10133" class="Symbol">→</a> <a id="10135" href="Cubical.HITs.CumulativeHierarchy.Base.html#9585" class="Bound">rec₁</a> <a id="10140" href="Cubical.HITs.CumulativeHierarchy.Base.html#10128" class="Bound">x₁</a> <a id="10143" class="Symbol">(</a><a id="10144" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10147" href="Cubical.HITs.CumulativeHierarchy.Base.html#10131" class="Bound">y</a><a id="10148" class="Symbol">))</a>
<a id="10191" class="Symbol">(λ</a> <a id="10194" href="Cubical.HITs.CumulativeHierarchy.Base.html#10194" class="Bound">x₂</a> <a id="10197" href="Cubical.HITs.CumulativeHierarchy.Base.html#10197" class="Bound">y</a> <a id="10199" class="Symbol">→</a> <a id="10201" href="Cubical.HITs.CumulativeHierarchy.Base.html#9590" class="Bound">rec₂</a> <a id="10206" href="Cubical.HITs.CumulativeHierarchy.Base.html#10194" class="Bound">x₂</a> <a id="10209" class="Symbol">(</a><a id="10210" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10213" href="Cubical.HITs.CumulativeHierarchy.Base.html#10197" class="Bound">y</a><a id="10214" class="Symbol">))</a> <a id="10217" href="Cubical.HITs.CumulativeHierarchy.Base.html#10261" class="Function">rec₁→₂Impl</a> <a id="10228" href="Cubical.HITs.CumulativeHierarchy.Base.html#10447" class="Function">rec₂→₁Impl</a>
<a id="10247" class="Keyword">where</a>
<a id="10261" href="Cubical.HITs.CumulativeHierarchy.Base.html#10261" class="Function">rec₁→₂Impl</a> <a id="10272" class="Symbol">:</a>
<a id="10284" class="Symbol">∀</a> <a id="10286" class="Symbol">(</a><a id="10287" href="Cubical.HITs.CumulativeHierarchy.Base.html#10287" class="Bound">x₁</a> <a id="10290" class="Symbol">:</a> <a id="10292" href="Cubical.HITs.CumulativeHierarchy.Base.html#9568" class="Bound">X₁</a><a id="10294" class="Symbol">)</a>
<a id="10306" class="Symbol">→</a> <a id="10308" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="10311" href="Cubical.HITs.CumulativeHierarchy.Base.html#10311" class="Bound">(</a><a id="10312" href="Cubical.HITs.CumulativeHierarchy.Base.html#10312" class="Bound">x₂</a> <a id="10315" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10317" href="Cubical.HITs.CumulativeHierarchy.Base.html#10317" class="Bound">p</a><a id="10318" href="Cubical.HITs.CumulativeHierarchy.Base.html#10311" class="Bound">)</a> <a id="10320" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="10322" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="10328" href="Cubical.HITs.CumulativeHierarchy.Base.html#9578" class="Bound">ix₂</a> <a id="10332" class="Symbol">(</a><a id="10333" href="Cubical.HITs.CumulativeHierarchy.Base.html#9574" class="Bound">ix₁</a> <a id="10337" href="Cubical.HITs.CumulativeHierarchy.Base.html#10287" class="Bound">x₁</a><a id="10339" class="Symbol">)</a> <a id="10341" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="10358" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="10364" class="Symbol">(λ</a> <a id="10367" href="Cubical.HITs.CumulativeHierarchy.Base.html#10367" class="Bound">i</a> <a id="10369" class="Symbol">→</a> <a id="10371" class="Symbol">∀</a> <a id="10373" href="Cubical.HITs.CumulativeHierarchy.Base.html#10373" class="Bound">y</a> <a id="10375" class="Symbol">→</a> <a id="10377" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="10379" class="Symbol">(</a><a id="10380" href="Cubical.HITs.CumulativeHierarchy.Base.html#10317" class="Bound">p</a> <a id="10382" href="Cubical.HITs.CumulativeHierarchy.Base.html#10367" class="Bound">i</a><a id="10383" class="Symbol">)</a> <a id="10385" class="Symbol">(</a><a id="10386" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10389" href="Cubical.HITs.CumulativeHierarchy.Base.html#10373" class="Bound">y</a><a id="10390" class="Symbol">))</a> <a id="10393" class="Symbol">(λ</a> <a id="10396" href="Cubical.HITs.CumulativeHierarchy.Base.html#10396" class="Bound">y</a> <a id="10398" class="Symbol">→</a> <a id="10400" href="Cubical.HITs.CumulativeHierarchy.Base.html#9590" class="Bound">rec₂</a> <a id="10405" href="Cubical.HITs.CumulativeHierarchy.Base.html#10312" class="Bound">x₂</a> <a id="10408" class="Symbol">(</a><a id="10409" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10412" href="Cubical.HITs.CumulativeHierarchy.Base.html#10396" class="Bound">y</a><a id="10413" class="Symbol">))</a> <a id="10416" class="Symbol">(λ</a> <a id="10419" href="Cubical.HITs.CumulativeHierarchy.Base.html#10419" class="Bound">y</a> <a id="10421" class="Symbol">→</a> <a id="10423" href="Cubical.HITs.CumulativeHierarchy.Base.html#9585" class="Bound">rec₁</a> <a id="10428" href="Cubical.HITs.CumulativeHierarchy.Base.html#10287" class="Bound">x₁</a> <a id="10431" class="Symbol">(</a><a id="10432" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10435" href="Cubical.HITs.CumulativeHierarchy.Base.html#10419" class="Bound">y</a><a id="10436" class="Symbol">))</a>
<a id="10447" href="Cubical.HITs.CumulativeHierarchy.Base.html#10447" class="Function">rec₂→₁Impl</a> <a id="10458" class="Symbol">:</a>
<a id="10470" class="Symbol">∀</a> <a id="10472" class="Symbol">(</a><a id="10473" href="Cubical.HITs.CumulativeHierarchy.Base.html#10473" class="Bound">x₂</a> <a id="10476" class="Symbol">:</a> <a id="10478" href="Cubical.HITs.CumulativeHierarchy.Base.html#9571" class="Bound">X₂</a><a id="10480" class="Symbol">)</a>
<a id="10492" class="Symbol">→</a> <a id="10494" href="Cubical.Data.Sigma.Base.html#682" class="Function">∃[</a> <a id="10497" href="Cubical.HITs.CumulativeHierarchy.Base.html#10497" class="Bound">(</a><a id="10498" href="Cubical.HITs.CumulativeHierarchy.Base.html#10498" class="Bound">x₁</a> <a id="10501" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10503" href="Cubical.HITs.CumulativeHierarchy.Base.html#10503" class="Bound">p</a><a id="10504" href="Cubical.HITs.CumulativeHierarchy.Base.html#10497" class="Bound">)</a> <a id="10506" href="Cubical.Data.Sigma.Base.html#682" class="Function">∈</a> <a id="10508" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="10514" href="Cubical.HITs.CumulativeHierarchy.Base.html#9574" class="Bound">ix₁</a> <a id="10518" class="Symbol">(</a><a id="10519" href="Cubical.HITs.CumulativeHierarchy.Base.html#9578" class="Bound">ix₂</a> <a id="10523" href="Cubical.HITs.CumulativeHierarchy.Base.html#10473" class="Bound">x₂</a><a id="10525" class="Symbol">)</a> <a id="10527" href="Cubical.Data.Sigma.Base.html#682" class="Function">]</a>
<a id="10544" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="10550" class="Symbol">(λ</a> <a id="10553" href="Cubical.HITs.CumulativeHierarchy.Base.html#10553" class="Bound">i</a> <a id="10555" class="Symbol">→</a> <a id="10557" class="Symbol">∀</a> <a id="10559" href="Cubical.HITs.CumulativeHierarchy.Base.html#10559" class="Bound">y</a> <a id="10561" class="Symbol">→</a> <a id="10563" href="Cubical.HITs.CumulativeHierarchy.Base.html#7564" class="Bound">Z</a> <a id="10565" class="Symbol">(</a><a id="10566" href="Cubical.HITs.CumulativeHierarchy.Base.html#10503" class="Bound">p</a> <a id="10568" href="Cubical.HITs.CumulativeHierarchy.Base.html#10553" class="Bound">i</a><a id="10569" class="Symbol">)</a> <a id="10571" class="Symbol">(</a><a id="10572" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10575" href="Cubical.HITs.CumulativeHierarchy.Base.html#10559" class="Bound">y</a><a id="10576" class="Symbol">))</a> <a id="10579" class="Symbol">(λ</a> <a id="10582" href="Cubical.HITs.CumulativeHierarchy.Base.html#10582" class="Bound">y</a> <a id="10584" class="Symbol">→</a> <a id="10586" href="Cubical.HITs.CumulativeHierarchy.Base.html#9585" class="Bound">rec₁</a> <a id="10591" href="Cubical.HITs.CumulativeHierarchy.Base.html#10498" class="Bound">x₁</a> <a id="10594" class="Symbol">(</a><a id="10595" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10598" href="Cubical.HITs.CumulativeHierarchy.Base.html#10582" class="Bound">y</a><a id="10599" class="Symbol">))</a> <a id="10602" class="Symbol">(λ</a> <a id="10605" href="Cubical.HITs.CumulativeHierarchy.Base.html#10605" class="Bound">y</a> <a id="10607" class="Symbol">→</a> <a id="10609" href="Cubical.HITs.CumulativeHierarchy.Base.html#9590" class="Bound">rec₂</a> <a id="10614" href="Cubical.HITs.CumulativeHierarchy.Base.html#10473" class="Bound">x₂</a> <a id="10617" class="Symbol">(</a><a id="10618" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10621" href="Cubical.HITs.CumulativeHierarchy.Base.html#10605" class="Bound">y</a><a id="10622" class="Symbol">))</a>
<a id="10633" href="Cubical.HITs.CumulativeHierarchy.Base.html#10261" class="Function">rec₁→₂Impl</a> <a id="10644" href="Cubical.HITs.CumulativeHierarchy.Base.html#10644" class="Bound">x₁</a> <a id="10647" class="Symbol">=</a> <a id="10649" class="Keyword">do</a> <a id="10652" class="Symbol">((</a><a id="10654" href="Cubical.HITs.CumulativeHierarchy.Base.html#10654" class="Bound">x₂</a> <a id="10657" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10659" href="Cubical.HITs.CumulativeHierarchy.Base.html#10659" class="Bound">xx</a><a id="10661" class="Symbol">)</a> <a id="10663" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10665" href="Cubical.HITs.CumulativeHierarchy.Base.html#10665" class="Bound">rx</a><a id="10667" class="Symbol">)</a> <a id="10669" href="Cubical.HITs.PropositionalTruncation.Monad.html#624" class="Function Operator">←</a> <a id="10671" href="Cubical.HITs.CumulativeHierarchy.Base.html#9595" class="Bound">rec₁→₂</a> <a id="10678" href="Cubical.HITs.CumulativeHierarchy.Base.html#10644" class="Bound">x₁</a> <a id="10681" class="Symbol">;</a> <a id="10683" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="10685" class="Symbol">(</a><a id="10686" href="Cubical.HITs.CumulativeHierarchy.Base.html#10654" class="Bound">x₂</a> <a id="10689" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10691" href="Cubical.HITs.CumulativeHierarchy.Base.html#10659" class="Bound">xx</a><a id="10693" class="Symbol">)</a> <a id="10695" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10697" class="Symbol">(λ</a> <a id="10700" href="Cubical.HITs.CumulativeHierarchy.Base.html#10700" class="Bound">i</a> <a id="10702" href="Cubical.HITs.CumulativeHierarchy.Base.html#10702" class="Bound">y</a> <a id="10704" class="Symbol">→</a> <a id="10706" href="Cubical.HITs.CumulativeHierarchy.Base.html#10665" class="Bound">rx</a> <a id="10709" href="Cubical.HITs.CumulativeHierarchy.Base.html#10700" class="Bound">i</a> <a id="10711" class="Symbol">(</a><a id="10712" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10715" href="Cubical.HITs.CumulativeHierarchy.Base.html#10702" class="Bound">y</a><a id="10716" class="Symbol">))</a> <a id="10719" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a>
<a id="10730" href="Cubical.HITs.CumulativeHierarchy.Base.html#10447" class="Function">rec₂→₁Impl</a> <a id="10741" href="Cubical.HITs.CumulativeHierarchy.Base.html#10741" class="Bound">x₂</a> <a id="10744" class="Symbol">=</a> <a id="10746" class="Keyword">do</a> <a id="10749" class="Symbol">((</a><a id="10751" href="Cubical.HITs.CumulativeHierarchy.Base.html#10751" class="Bound">x₁</a> <a id="10754" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10756" href="Cubical.HITs.CumulativeHierarchy.Base.html#10756" class="Bound">xx</a><a id="10758" class="Symbol">)</a> <a id="10760" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10762" href="Cubical.HITs.CumulativeHierarchy.Base.html#10762" class="Bound">rx</a><a id="10764" class="Symbol">)</a> <a id="10766" href="Cubical.HITs.PropositionalTruncation.Monad.html#624" class="Function Operator">←</a> <a id="10768" href="Cubical.HITs.CumulativeHierarchy.Base.html#9602" class="Bound">rec₂→₁</a> <a id="10775" href="Cubical.HITs.CumulativeHierarchy.Base.html#10741" class="Bound">x₂</a> <a id="10778" class="Symbol">;</a> <a id="10780" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣</a> <a id="10782" class="Symbol">(</a><a id="10783" href="Cubical.HITs.CumulativeHierarchy.Base.html#10751" class="Bound">x₁</a> <a id="10786" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10788" href="Cubical.HITs.CumulativeHierarchy.Base.html#10756" class="Bound">xx</a><a id="10790" class="Symbol">)</a> <a id="10792" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="10794" class="Symbol">(λ</a> <a id="10797" href="Cubical.HITs.CumulativeHierarchy.Base.html#10797" class="Bound">i</a> <a id="10799" href="Cubical.HITs.CumulativeHierarchy.Base.html#10799" class="Bound">y</a> <a id="10801" class="Symbol">→</a> <a id="10803" href="Cubical.HITs.CumulativeHierarchy.Base.html#10762" class="Bound">rx</a> <a id="10806" href="Cubical.HITs.CumulativeHierarchy.Base.html#10797" class="Bound">i</a> <a id="10808" class="Symbol">(</a><a id="10809" href="Cubical.HITs.CumulativeHierarchy.Base.html#10080" class="Bound">iy</a> <a id="10812" href="Cubical.HITs.CumulativeHierarchy.Base.html#10799" class="Bound">y</a><a id="10813" class="Symbol">))</a> <a id="10816" href="Cubical.HITs.PropositionalTruncation.Base.html#288" class="InductiveConstructor Operator">∣₁</a>
<a id="10824" href="Cubical.HITs.CumulativeHierarchy.Base.html#10824" class="Function">pElim</a> <a id="10830" class="Symbol">:</a> <a id="10832" href="Cubical.HITs.CumulativeHierarchy.Base.html#1877" class="Record">ElimSet</a> <a id="10840" href="Cubical.HITs.CumulativeHierarchy.Base.html#7767" class="Function">isSetPElim</a>
<a id="10855" href="Cubical.HITs.CumulativeHierarchy.Base.html#2001" class="Field">ElimSett</a> <a id="10864" href="Cubical.HITs.CumulativeHierarchy.Base.html#10824" class="Function">pElim</a> <a id="10870" class="Symbol">=</a> <a id="10872" href="Cubical.HITs.CumulativeHierarchy.Base.html#8788" class="Function">elimImplS</a>
<a id="10886" href="Cubical.HITs.CumulativeHierarchy.Base.html#2188" class="Field">ElimEq</a> <a id="10893" href="Cubical.HITs.CumulativeHierarchy.Base.html#10824" class="Function">pElim</a> <a id="10899" href="Cubical.HITs.CumulativeHierarchy.Base.html#10899" class="Bound">X₁</a> <a id="10902" href="Cubical.HITs.CumulativeHierarchy.Base.html#10902" class="Bound">X₂</a> <a id="10905" href="Cubical.HITs.CumulativeHierarchy.Base.html#10905" class="Bound">ix₁</a> <a id="10909" href="Cubical.HITs.CumulativeHierarchy.Base.html#10909" class="Bound">ix₂</a> <a id="10913" href="Cubical.HITs.CumulativeHierarchy.Base.html#10913" class="Bound">eq</a> <a id="10916" href="Cubical.HITs.CumulativeHierarchy.Base.html#10916" class="Bound">rec₁</a> <a id="10921" href="Cubical.HITs.CumulativeHierarchy.Base.html#10921" class="Bound">rec₂</a> <a id="10926" href="Cubical.HITs.CumulativeHierarchy.Base.html#10926" class="Bound">rec₁→₂</a> <a id="10933" href="Cubical.HITs.CumulativeHierarchy.Base.html#10933" class="Bound">rec₂→₁</a> <a id="10940" href="Cubical.HITs.CumulativeHierarchy.Base.html#10940" class="Bound">i</a> <a id="10942" href="Cubical.HITs.CumulativeHierarchy.Base.html#10942" class="Bound">t</a> <a id="10944" class="Symbol">=</a>
<a id="10952" href="Cubical.HITs.CumulativeHierarchy.Base.html#8965" class="Function">elimImplSExt</a> <a id="10965" href="Cubical.HITs.CumulativeHierarchy.Base.html#10899" class="Bound">X₁</a> <a id="10968" href="Cubical.HITs.CumulativeHierarchy.Base.html#10902" class="Bound">X₂</a> <a id="10971" href="Cubical.HITs.CumulativeHierarchy.Base.html#10905" class="Bound">ix₁</a> <a id="10975" href="Cubical.HITs.CumulativeHierarchy.Base.html#10909" class="Bound">ix₂</a> <a id="10979" href="Cubical.HITs.CumulativeHierarchy.Base.html#10913" class="Bound">eq</a> <a id="10982" href="Cubical.HITs.CumulativeHierarchy.Base.html#10916" class="Bound">rec₁</a> <a id="10987" href="Cubical.HITs.CumulativeHierarchy.Base.html#10921" class="Bound">rec₂</a> <a id="10992" href="Cubical.HITs.CumulativeHierarchy.Base.html#10926" class="Bound">rec₁→₂</a> <a id="10999" href="Cubical.HITs.CumulativeHierarchy.Base.html#10933" class="Bound">rec₂→₁</a> <a id="11006" href="Cubical.HITs.CumulativeHierarchy.Base.html#10942" class="Bound">t</a> <a id="11008" href="Cubical.HITs.CumulativeHierarchy.Base.html#10940" class="Bound">i</a>
</pre></body></html>