-
Notifications
You must be signed in to change notification settings - Fork 0
/
Cubical.Foundations.Univalence.html
324 lines (257 loc) · 215 KB
/
Cubical.Foundations.Univalence.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
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Foundations.Univalence</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">{-
Proof of the standard formulation of the univalence theorem and
various consequences of univalence
- Re-exports Glue types from Cubical.Core.Glue
- The ua constant and its computation rule (up to a path)
- Proof of univalence using that unglue is an equivalence ([EquivContr])
- Equivalence induction ([EquivJ], [elimEquiv])
- Univalence theorem ([univalence])
- The computation rule for ua ([uaβ])
- Isomorphism induction ([elimIso])
-}</a>
<a id="445" class="Symbol">{-#</a> <a id="449" class="Keyword">OPTIONS</a> <a id="457" class="Pragma">--safe</a> <a id="464" class="Symbol">#-}</a>
<a id="468" class="Keyword">module</a> <a id="475" href="Cubical.Foundations.Univalence.html" class="Module">Cubical.Foundations.Univalence</a> <a id="506" class="Keyword">where</a>
<a id="513" class="Keyword">open</a> <a id="518" class="Keyword">import</a> <a id="525" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>
<a id="553" class="Keyword">open</a> <a id="558" class="Keyword">import</a> <a id="565" href="Cubical.Foundations.Function.html" class="Module">Cubical.Foundations.Function</a>
<a id="594" class="Keyword">open</a> <a id="599" class="Keyword">import</a> <a id="606" href="Cubical.Foundations.Isomorphism.html" class="Module">Cubical.Foundations.Isomorphism</a>
<a id="638" class="Keyword">open</a> <a id="643" class="Keyword">import</a> <a id="650" href="Cubical.Foundations.Equiv.html" class="Module">Cubical.Foundations.Equiv</a>
<a id="676" class="Keyword">open</a> <a id="681" class="Keyword">import</a> <a id="688" href="Cubical.Foundations.GroupoidLaws.html" class="Module">Cubical.Foundations.GroupoidLaws</a>
<a id="722" class="Keyword">open</a> <a id="727" class="Keyword">import</a> <a id="734" href="Cubical.Data.Sigma.Base.html" class="Module">Cubical.Data.Sigma.Base</a>
<a id="759" class="Keyword">open</a> <a id="764" class="Keyword">import</a> <a id="771" href="Cubical.Core.Glue.html" class="Module">Cubical.Core.Glue</a> <a id="789" class="Keyword">public</a>
<a id="798" class="Keyword">using</a> <a id="804" class="Symbol">(</a><a id="805" href="Cubical.Core.Glue.html#1521" class="Function">Glue</a> <a id="810" class="Symbol">;</a> <a id="812" href="Agda.Builtin.Cubical.Glue.html#2169" class="Primitive">glue</a> <a id="817" class="Symbol">;</a> <a id="819" href="Cubical.Core.Glue.html#1724" class="Function">unglue</a><a id="825" class="Symbol">)</a>
<a id="828" class="Keyword">open</a> <a id="833" class="Keyword">import</a> <a id="840" href="Cubical.Reflection.StrictEquiv.html" class="Module">Cubical.Reflection.StrictEquiv</a>
<a id="872" class="Keyword">private</a>
<a id="882" class="Keyword">variable</a>
<a id="895" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a> <a id="897" href="Cubical.Foundations.Univalence.html#897" class="Generalizable">ℓ'</a> <a id="900" class="Symbol">:</a> <a id="902" href="Agda.Primitive.html#597" class="Postulate">Level</a>
<a id="909" class="Comment">-- The ua constant</a>
<a id="ua"></a><a id="928" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="931" class="Symbol">:</a> <a id="933" class="Symbol">∀</a> <a id="935" class="Symbol">{</a><a id="936" href="Cubical.Foundations.Univalence.html#936" class="Bound">A</a> <a id="938" href="Cubical.Foundations.Univalence.html#938" class="Bound">B</a> <a id="940" class="Symbol">:</a> <a id="942" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="947" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="948" class="Symbol">}</a> <a id="950" class="Symbol">→</a> <a id="952" href="Cubical.Foundations.Univalence.html#936" class="Bound">A</a> <a id="954" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="956" href="Cubical.Foundations.Univalence.html#938" class="Bound">B</a> <a id="958" class="Symbol">→</a> <a id="960" href="Cubical.Foundations.Univalence.html#936" class="Bound">A</a> <a id="962" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="964" href="Cubical.Foundations.Univalence.html#938" class="Bound">B</a>
<a id="966" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="969" class="Symbol">{</a><a id="970" class="Argument">A</a> <a id="972" class="Symbol">=</a> <a id="974" href="Cubical.Foundations.Univalence.html#974" class="Bound">A</a><a id="975" class="Symbol">}</a> <a id="977" class="Symbol">{</a><a id="978" class="Argument">B</a> <a id="980" class="Symbol">=</a> <a id="982" href="Cubical.Foundations.Univalence.html#982" class="Bound">B</a><a id="983" class="Symbol">}</a> <a id="985" href="Cubical.Foundations.Univalence.html#985" class="Bound">e</a> <a id="987" href="Cubical.Foundations.Univalence.html#987" class="Bound">i</a> <a id="989" class="Symbol">=</a> <a id="991" href="Cubical.Core.Glue.html#1521" class="Function">Glue</a> <a id="996" href="Cubical.Foundations.Univalence.html#982" class="Bound">B</a> <a id="998" class="Symbol">(λ</a> <a id="1001" class="Symbol">{</a> <a id="1003" class="Symbol">(</a><a id="1004" href="Cubical.Foundations.Univalence.html#987" class="Bound">i</a> <a id="1006" class="Symbol">=</a> <a id="1008" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="1010" class="Symbol">)</a> <a id="1012" class="Symbol">→</a> <a id="1014" class="Symbol">(</a><a id="1015" href="Cubical.Foundations.Univalence.html#974" class="Bound">A</a> <a id="1017" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1019" href="Cubical.Foundations.Univalence.html#985" class="Bound">e</a><a id="1020" class="Symbol">)</a>
<a id="1057" class="Symbol">;</a> <a id="1059" class="Symbol">(</a><a id="1060" href="Cubical.Foundations.Univalence.html#987" class="Bound">i</a> <a id="1062" class="Symbol">=</a> <a id="1064" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="1066" class="Symbol">)</a> <a id="1068" class="Symbol">→</a> <a id="1070" class="Symbol">(</a><a id="1071" href="Cubical.Foundations.Univalence.html#982" class="Bound">B</a> <a id="1073" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1075" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="1083" href="Cubical.Foundations.Univalence.html#982" class="Bound">B</a><a id="1084" class="Symbol">)</a> <a id="1086" class="Symbol">})</a>
<a id="uaIdEquiv"></a><a id="1090" href="Cubical.Foundations.Univalence.html#1090" class="Function">uaIdEquiv</a> <a id="1100" class="Symbol">:</a> <a id="1102" class="Symbol">{</a><a id="1103" href="Cubical.Foundations.Univalence.html#1103" class="Bound">A</a> <a id="1105" class="Symbol">:</a> <a id="1107" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1112" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="1113" class="Symbol">}</a> <a id="1115" class="Symbol">→</a> <a id="1117" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="1120" class="Symbol">(</a><a id="1121" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="1129" href="Cubical.Foundations.Univalence.html#1103" class="Bound">A</a><a id="1130" class="Symbol">)</a> <a id="1132" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1134" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="1139" href="Cubical.Foundations.Univalence.html#1090" class="Function">uaIdEquiv</a> <a id="1149" class="Symbol">{</a><a id="1150" class="Argument">A</a> <a id="1152" class="Symbol">=</a> <a id="1154" href="Cubical.Foundations.Univalence.html#1154" class="Bound">A</a><a id="1155" class="Symbol">}</a> <a id="1157" href="Cubical.Foundations.Univalence.html#1157" class="Bound">i</a> <a id="1159" href="Cubical.Foundations.Univalence.html#1159" class="Bound">j</a> <a id="1161" class="Symbol">=</a> <a id="1163" href="Cubical.Core.Glue.html#1521" class="Function">Glue</a> <a id="1168" href="Cubical.Foundations.Univalence.html#1154" class="Bound">A</a> <a id="1170" class="Symbol">{</a><a id="1171" class="Argument">φ</a> <a id="1173" class="Symbol">=</a> <a id="1175" href="Cubical.Foundations.Univalence.html#1157" class="Bound">i</a> <a id="1177" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="1179" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="1181" href="Cubical.Foundations.Univalence.html#1159" class="Bound">j</a> <a id="1183" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="1185" href="Cubical.Foundations.Univalence.html#1159" class="Bound">j</a><a id="1186" class="Symbol">}</a> <a id="1188" class="Symbol">(λ</a> <a id="1191" href="Cubical.Foundations.Univalence.html#1191" class="Bound">_</a> <a id="1193" class="Symbol">→</a> <a id="1195" href="Cubical.Foundations.Univalence.html#1154" class="Bound">A</a> <a id="1197" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1199" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="1207" href="Cubical.Foundations.Univalence.html#1154" class="Bound">A</a><a id="1208" class="Symbol">)</a>
<a id="1211" class="Comment">-- Propositional extensionality</a>
<a id="hPropExt"></a><a id="1243" href="Cubical.Foundations.Univalence.html#1243" class="Function">hPropExt</a> <a id="1252" class="Symbol">:</a> <a id="1254" class="Symbol">{</a><a id="1255" href="Cubical.Foundations.Univalence.html#1255" class="Bound">A</a> <a id="1257" href="Cubical.Foundations.Univalence.html#1257" class="Bound">B</a> <a id="1259" class="Symbol">:</a> <a id="1261" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1266" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="1267" class="Symbol">}</a> <a id="1269" class="Symbol">→</a> <a id="1271" href="Cubical.Foundations.Prelude.html#14039" class="Function">isProp</a> <a id="1278" href="Cubical.Foundations.Univalence.html#1255" class="Bound">A</a> <a id="1280" class="Symbol">→</a> <a id="1282" href="Cubical.Foundations.Prelude.html#14039" class="Function">isProp</a> <a id="1289" href="Cubical.Foundations.Univalence.html#1257" class="Bound">B</a> <a id="1291" class="Symbol">→</a> <a id="1293" class="Symbol">(</a><a id="1294" href="Cubical.Foundations.Univalence.html#1255" class="Bound">A</a> <a id="1296" class="Symbol">→</a> <a id="1298" href="Cubical.Foundations.Univalence.html#1257" class="Bound">B</a><a id="1299" class="Symbol">)</a> <a id="1301" class="Symbol">→</a> <a id="1303" class="Symbol">(</a><a id="1304" href="Cubical.Foundations.Univalence.html#1257" class="Bound">B</a> <a id="1306" class="Symbol">→</a> <a id="1308" href="Cubical.Foundations.Univalence.html#1255" class="Bound">A</a><a id="1309" class="Symbol">)</a> <a id="1311" class="Symbol">→</a> <a id="1313" href="Cubical.Foundations.Univalence.html#1255" class="Bound">A</a> <a id="1315" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1317" href="Cubical.Foundations.Univalence.html#1257" class="Bound">B</a>
<a id="1319" href="Cubical.Foundations.Univalence.html#1243" class="Function">hPropExt</a> <a id="1328" href="Cubical.Foundations.Univalence.html#1328" class="Bound">Aprop</a> <a id="1334" href="Cubical.Foundations.Univalence.html#1334" class="Bound">Bprop</a> <a id="1340" href="Cubical.Foundations.Univalence.html#1340" class="Bound">f</a> <a id="1342" href="Cubical.Foundations.Univalence.html#1342" class="Bound">g</a> <a id="1344" class="Symbol">=</a> <a id="1346" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="1349" class="Symbol">(</a><a id="1350" href="Cubical.Foundations.Equiv.html#6072" class="Function">propBiimpl→Equiv</a> <a id="1367" href="Cubical.Foundations.Univalence.html#1328" class="Bound">Aprop</a> <a id="1373" href="Cubical.Foundations.Univalence.html#1334" class="Bound">Bprop</a> <a id="1379" href="Cubical.Foundations.Univalence.html#1340" class="Bound">f</a> <a id="1381" href="Cubical.Foundations.Univalence.html#1342" class="Bound">g</a><a id="1382" class="Symbol">)</a>
<a id="1385" class="Comment">-- the unglue and glue primitives specialized to the case of ua</a>
<a id="ua-unglue"></a><a id="1450" href="Cubical.Foundations.Univalence.html#1450" class="Function">ua-unglue</a> <a id="1460" class="Symbol">:</a> <a id="1462" class="Symbol">∀</a> <a id="1464" class="Symbol">{</a><a id="1465" href="Cubical.Foundations.Univalence.html#1465" class="Bound">A</a> <a id="1467" href="Cubical.Foundations.Univalence.html#1467" class="Bound">B</a> <a id="1469" class="Symbol">:</a> <a id="1471" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1476" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="1477" class="Symbol">}</a> <a id="1479" class="Symbol">(</a><a id="1480" href="Cubical.Foundations.Univalence.html#1480" class="Bound">e</a> <a id="1482" class="Symbol">:</a> <a id="1484" href="Cubical.Foundations.Univalence.html#1465" class="Bound">A</a> <a id="1486" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="1488" href="Cubical.Foundations.Univalence.html#1467" class="Bound">B</a><a id="1489" class="Symbol">)</a> <a id="1491" class="Symbol">(</a><a id="1492" href="Cubical.Foundations.Univalence.html#1492" class="Bound">i</a> <a id="1494" class="Symbol">:</a> <a id="1496" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="1497" class="Symbol">)</a> <a id="1499" class="Symbol">(</a><a id="1500" href="Cubical.Foundations.Univalence.html#1500" class="Bound">x</a> <a id="1502" class="Symbol">:</a> <a id="1504" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="1507" href="Cubical.Foundations.Univalence.html#1480" class="Bound">e</a> <a id="1509" href="Cubical.Foundations.Univalence.html#1492" class="Bound">i</a><a id="1510" class="Symbol">)</a>
<a id="1524" class="Symbol">→</a> <a id="1526" href="Cubical.Foundations.Univalence.html#1467" class="Bound">B</a> <a id="1528" class="Comment">{- [ _ ↦ (λ { (i = i0) → e .fst x ; (i = i1) → x }) ] -}</a>
<a id="1585" href="Cubical.Foundations.Univalence.html#1450" class="Function">ua-unglue</a> <a id="1595" href="Cubical.Foundations.Univalence.html#1595" class="Bound">e</a> <a id="1597" href="Cubical.Foundations.Univalence.html#1597" class="Bound">i</a> <a id="1599" href="Cubical.Foundations.Univalence.html#1599" class="Bound">x</a> <a id="1601" class="Symbol">=</a> <a id="1603" href="Cubical.Core.Glue.html#1724" class="Function">unglue</a> <a id="1610" class="Symbol">(</a><a id="1611" href="Cubical.Foundations.Univalence.html#1597" class="Bound">i</a> <a id="1613" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="1615" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="1617" href="Cubical.Foundations.Univalence.html#1597" class="Bound">i</a><a id="1618" class="Symbol">)</a> <a id="1620" href="Cubical.Foundations.Univalence.html#1599" class="Bound">x</a>
<a id="ua-glue"></a><a id="1623" href="Cubical.Foundations.Univalence.html#1623" class="Function">ua-glue</a> <a id="1631" class="Symbol">:</a> <a id="1633" class="Symbol">∀</a> <a id="1635" class="Symbol">{</a><a id="1636" href="Cubical.Foundations.Univalence.html#1636" class="Bound">A</a> <a id="1638" href="Cubical.Foundations.Univalence.html#1638" class="Bound">B</a> <a id="1640" class="Symbol">:</a> <a id="1642" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1647" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="1648" class="Symbol">}</a> <a id="1650" class="Symbol">(</a><a id="1651" href="Cubical.Foundations.Univalence.html#1651" class="Bound">e</a> <a id="1653" class="Symbol">:</a> <a id="1655" href="Cubical.Foundations.Univalence.html#1636" class="Bound">A</a> <a id="1657" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="1659" href="Cubical.Foundations.Univalence.html#1638" class="Bound">B</a><a id="1660" class="Symbol">)</a> <a id="1662" class="Symbol">(</a><a id="1663" href="Cubical.Foundations.Univalence.html#1663" class="Bound">i</a> <a id="1665" class="Symbol">:</a> <a id="1667" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="1668" class="Symbol">)</a> <a id="1670" class="Symbol">(</a><a id="1671" href="Cubical.Foundations.Univalence.html#1671" class="Bound">x</a> <a id="1673" class="Symbol">:</a> <a id="1675" href="Agda.Primitive.Cubical.html#1072" class="Primitive">Partial</a> <a id="1683" class="Symbol">(</a><a id="1684" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="1686" href="Cubical.Foundations.Univalence.html#1663" class="Bound">i</a><a id="1687" class="Symbol">)</a> <a id="1689" href="Cubical.Foundations.Univalence.html#1636" class="Bound">A</a><a id="1690" class="Symbol">)</a>
<a id="1704" class="Symbol">(</a><a id="1705" href="Cubical.Foundations.Univalence.html#1705" class="Bound">y</a> <a id="1707" class="Symbol">:</a> <a id="1709" href="Cubical.Foundations.Univalence.html#1638" class="Bound">B</a> <a id="1711" href="Cubical.Core.Primitives.html#3508" class="Function Operator">[</a> <a id="1713" class="Symbol">_</a> <a id="1715" href="Cubical.Core.Primitives.html#3508" class="Function Operator">↦</a> <a id="1717" class="Symbol">(λ</a> <a id="1720" class="Symbol">{</a> <a id="1722" class="Symbol">(</a><a id="1723" href="Cubical.Foundations.Univalence.html#1663" class="Bound">i</a> <a id="1725" class="Symbol">=</a> <a id="1727" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="1729" class="Symbol">)</a> <a id="1731" class="Symbol">→</a> <a id="1733" href="Cubical.Foundations.Univalence.html#1651" class="Bound">e</a> <a id="1735" class="Symbol">.</a><a id="1736" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="1740" class="Symbol">(</a><a id="1741" href="Cubical.Foundations.Univalence.html#1671" class="Bound">x</a> <a id="1743" href="Cubical.Core.Primitives.html#732" class="Postulate">1=1</a><a id="1746" class="Symbol">)</a> <a id="1748" class="Symbol">})</a> <a id="1751" href="Cubical.Core.Primitives.html#3508" class="Function Operator">]</a><a id="1752" class="Symbol">)</a>
<a id="1764" class="Symbol">→</a> <a id="1766" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="1769" href="Cubical.Foundations.Univalence.html#1651" class="Bound">e</a> <a id="1771" href="Cubical.Foundations.Univalence.html#1663" class="Bound">i</a> <a id="1773" class="Comment">{- [ _ ↦ (λ { (i = i0) → x 1=1 ; (i = i1) → outS y }) ] -}</a>
<a id="1832" href="Cubical.Foundations.Univalence.html#1623" class="Function">ua-glue</a> <a id="1840" href="Cubical.Foundations.Univalence.html#1840" class="Bound">e</a> <a id="1842" href="Cubical.Foundations.Univalence.html#1842" class="Bound">i</a> <a id="1844" href="Cubical.Foundations.Univalence.html#1844" class="Bound">x</a> <a id="1846" href="Cubical.Foundations.Univalence.html#1846" class="Bound">y</a> <a id="1848" class="Symbol">=</a> <a id="1850" href="Agda.Builtin.Cubical.Glue.html#2169" class="Primitive">glue</a> <a id="1855" class="Symbol">{</a><a id="1856" class="Argument">φ</a> <a id="1858" class="Symbol">=</a> <a id="1860" href="Cubical.Foundations.Univalence.html#1842" class="Bound">i</a> <a id="1862" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="1864" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="1866" href="Cubical.Foundations.Univalence.html#1842" class="Bound">i</a><a id="1867" class="Symbol">}</a> <a id="1869" class="Symbol">(λ</a> <a id="1872" class="Symbol">{</a> <a id="1874" class="Symbol">(</a><a id="1875" href="Cubical.Foundations.Univalence.html#1842" class="Bound">i</a> <a id="1877" class="Symbol">=</a> <a id="1879" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="1881" class="Symbol">)</a> <a id="1883" class="Symbol">→</a> <a id="1885" href="Cubical.Foundations.Univalence.html#1844" class="Bound">x</a> <a id="1887" href="Cubical.Core.Primitives.html#732" class="Postulate">1=1</a> <a id="1891" class="Symbol">;</a> <a id="1893" class="Symbol">(</a><a id="1894" href="Cubical.Foundations.Univalence.html#1842" class="Bound">i</a> <a id="1896" class="Symbol">=</a> <a id="1898" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="1900" class="Symbol">)</a> <a id="1902" class="Symbol">→</a> <a id="1904" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="1909" href="Cubical.Foundations.Univalence.html#1846" class="Bound">y</a> <a id="1911" class="Symbol">})</a> <a id="1914" class="Symbol">(</a><a id="1915" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="1920" href="Cubical.Foundations.Univalence.html#1846" class="Bound">y</a><a id="1921" class="Symbol">)</a>
<a id="1924" class="Keyword">module</a> <a id="1931" href="Cubical.Foundations.Univalence.html#1931" class="Module">_</a> <a id="1933" class="Symbol">{</a><a id="1934" href="Cubical.Foundations.Univalence.html#1934" class="Bound">A</a> <a id="1936" href="Cubical.Foundations.Univalence.html#1936" class="Bound">B</a> <a id="1938" class="Symbol">:</a> <a id="1940" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1945" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="1946" class="Symbol">}</a> <a id="1948" class="Symbol">(</a><a id="1949" href="Cubical.Foundations.Univalence.html#1949" class="Bound">e</a> <a id="1951" class="Symbol">:</a> <a id="1953" href="Cubical.Foundations.Univalence.html#1934" class="Bound">A</a> <a id="1955" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="1957" href="Cubical.Foundations.Univalence.html#1936" class="Bound">B</a><a id="1958" class="Symbol">)</a> <a id="1960" class="Symbol">{</a><a id="1961" href="Cubical.Foundations.Univalence.html#1961" class="Bound">x</a> <a id="1963" class="Symbol">:</a> <a id="1965" href="Cubical.Foundations.Univalence.html#1934" class="Bound">A</a><a id="1966" class="Symbol">}</a> <a id="1968" class="Symbol">{</a><a id="1969" href="Cubical.Foundations.Univalence.html#1969" class="Bound">y</a> <a id="1971" class="Symbol">:</a> <a id="1973" href="Cubical.Foundations.Univalence.html#1936" class="Bound">B</a><a id="1974" class="Symbol">}</a> <a id="1976" class="Keyword">where</a>
<a id="1984" class="Comment">-- sometimes more useful are versions of these functions with the (i : I) factored in</a>
<a id="2073" href="Cubical.Foundations.Univalence.html#2073" class="Function">ua-ungluePath</a> <a id="2087" class="Symbol">:</a> <a id="2089" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="2095" class="Symbol">(λ</a> <a id="2098" href="Cubical.Foundations.Univalence.html#2098" class="Bound">i</a> <a id="2100" class="Symbol">→</a> <a id="2102" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="2105" href="Cubical.Foundations.Univalence.html#1949" class="Bound">e</a> <a id="2107" href="Cubical.Foundations.Univalence.html#2098" class="Bound">i</a><a id="2108" class="Symbol">)</a> <a id="2110" href="Cubical.Foundations.Univalence.html#1961" class="Bound">x</a> <a id="2112" href="Cubical.Foundations.Univalence.html#1969" class="Bound">y</a> <a id="2114" class="Symbol">→</a> <a id="2116" href="Cubical.Foundations.Univalence.html#1949" class="Bound">e</a> <a id="2118" class="Symbol">.</a><a id="2119" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="2123" href="Cubical.Foundations.Univalence.html#1961" class="Bound">x</a> <a id="2125" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2127" href="Cubical.Foundations.Univalence.html#1969" class="Bound">y</a>
<a id="2131" href="Cubical.Foundations.Univalence.html#2073" class="Function">ua-ungluePath</a> <a id="2145" href="Cubical.Foundations.Univalence.html#2145" class="Bound">p</a> <a id="2147" href="Cubical.Foundations.Univalence.html#2147" class="Bound">i</a> <a id="2149" class="Symbol">=</a> <a id="2151" href="Cubical.Foundations.Univalence.html#1450" class="Function">ua-unglue</a> <a id="2161" href="Cubical.Foundations.Univalence.html#1949" class="Bound">e</a> <a id="2163" href="Cubical.Foundations.Univalence.html#2147" class="Bound">i</a> <a id="2165" class="Symbol">(</a><a id="2166" href="Cubical.Foundations.Univalence.html#2145" class="Bound">p</a> <a id="2168" href="Cubical.Foundations.Univalence.html#2147" class="Bound">i</a><a id="2169" class="Symbol">)</a>
<a id="2174" href="Cubical.Foundations.Univalence.html#2174" class="Function">ua-gluePath</a> <a id="2186" class="Symbol">:</a> <a id="2188" href="Cubical.Foundations.Univalence.html#1949" class="Bound">e</a> <a id="2190" class="Symbol">.</a><a id="2191" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="2195" href="Cubical.Foundations.Univalence.html#1961" class="Bound">x</a> <a id="2197" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2199" href="Cubical.Foundations.Univalence.html#1969" class="Bound">y</a> <a id="2201" class="Symbol">→</a> <a id="2203" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="2209" class="Symbol">(λ</a> <a id="2212" href="Cubical.Foundations.Univalence.html#2212" class="Bound">i</a> <a id="2214" class="Symbol">→</a> <a id="2216" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="2219" href="Cubical.Foundations.Univalence.html#1949" class="Bound">e</a> <a id="2221" href="Cubical.Foundations.Univalence.html#2212" class="Bound">i</a><a id="2222" class="Symbol">)</a> <a id="2224" href="Cubical.Foundations.Univalence.html#1961" class="Bound">x</a> <a id="2226" href="Cubical.Foundations.Univalence.html#1969" class="Bound">y</a>
<a id="2230" href="Cubical.Foundations.Univalence.html#2174" class="Function">ua-gluePath</a> <a id="2242" href="Cubical.Foundations.Univalence.html#2242" class="Bound">p</a> <a id="2244" href="Cubical.Foundations.Univalence.html#2244" class="Bound">i</a> <a id="2246" class="Symbol">=</a> <a id="2248" href="Cubical.Foundations.Univalence.html#1623" class="Function">ua-glue</a> <a id="2256" href="Cubical.Foundations.Univalence.html#1949" class="Bound">e</a> <a id="2258" href="Cubical.Foundations.Univalence.html#2244" class="Bound">i</a> <a id="2260" class="Symbol">(λ</a> <a id="2263" class="Symbol">{</a> <a id="2265" class="Symbol">(</a><a id="2266" href="Cubical.Foundations.Univalence.html#2244" class="Bound">i</a> <a id="2268" class="Symbol">=</a> <a id="2270" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="2272" class="Symbol">)</a> <a id="2274" class="Symbol">→</a> <a id="2276" href="Cubical.Foundations.Univalence.html#1961" class="Bound">x</a> <a id="2278" class="Symbol">})</a> <a id="2281" class="Symbol">(</a><a id="2282" href="Agda.Builtin.Cubical.Sub.html#223" class="Postulate">inS</a> <a id="2286" class="Symbol">(</a><a id="2287" href="Cubical.Foundations.Univalence.html#2242" class="Bound">p</a> <a id="2289" href="Cubical.Foundations.Univalence.html#2244" class="Bound">i</a><a id="2290" class="Symbol">))</a>
<a id="2296" class="Comment">-- ua-ungluePath and ua-gluePath are definitional inverses</a>
<a id="2357" href="Cubical.Foundations.Univalence.html#2357" class="Function">ua-ungluePath-Equiv</a> <a id="2377" class="Symbol">:</a> <a id="2379" class="Symbol">(</a><a id="2380" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="2386" class="Symbol">(λ</a> <a id="2389" href="Cubical.Foundations.Univalence.html#2389" class="Bound">i</a> <a id="2391" class="Symbol">→</a> <a id="2393" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="2396" href="Cubical.Foundations.Univalence.html#1949" class="Bound">e</a> <a id="2398" href="Cubical.Foundations.Univalence.html#2389" class="Bound">i</a><a id="2399" class="Symbol">)</a> <a id="2401" href="Cubical.Foundations.Univalence.html#1961" class="Bound">x</a> <a id="2403" href="Cubical.Foundations.Univalence.html#1969" class="Bound">y</a><a id="2404" class="Symbol">)</a> <a id="2406" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="2408" class="Symbol">(</a><a id="2409" href="Cubical.Foundations.Univalence.html#1949" class="Bound">e</a> <a id="2411" class="Symbol">.</a><a id="2412" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="2416" href="Cubical.Foundations.Univalence.html#1961" class="Bound">x</a> <a id="2418" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2420" href="Cubical.Foundations.Univalence.html#1969" class="Bound">y</a><a id="2421" class="Symbol">)</a>
<a id="2425" class="Keyword">unquoteDef</a> <a id="2436" href="Cubical.Foundations.Univalence.html#2357" class="Function">ua-ungluePath-Equiv</a> <a id="2456" class="Symbol">=</a>
<a id="2462" href="Cubical.Reflection.StrictEquiv.html#1246" class="Function">defStrictEquiv</a> <a id="2477" href="Cubical.Foundations.Univalence.html#2357" class="Function">ua-ungluePath-Equiv</a> <a id="2497" href="Cubical.Foundations.Univalence.html#2073" class="Function">ua-ungluePath</a> <a id="2511" href="Cubical.Foundations.Univalence.html#2174" class="Function">ua-gluePath</a>
<a id="2524" class="Comment">-- ua-unglue and ua-glue are also definitional inverses, in a way</a>
<a id="2590" class="Comment">-- strengthening the types of ua-unglue and ua-glue gives a nicer formulation of this, see below</a>
<a id="ua-unglue-glue"></a><a id="2688" href="Cubical.Foundations.Univalence.html#2688" class="Function">ua-unglue-glue</a> <a id="2703" class="Symbol">:</a> <a id="2705" class="Symbol">∀</a> <a id="2707" class="Symbol">{</a><a id="2708" href="Cubical.Foundations.Univalence.html#2708" class="Bound">A</a> <a id="2710" href="Cubical.Foundations.Univalence.html#2710" class="Bound">B</a> <a id="2712" class="Symbol">:</a> <a id="2714" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2719" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="2720" class="Symbol">}</a> <a id="2722" class="Symbol">(</a><a id="2723" href="Cubical.Foundations.Univalence.html#2723" class="Bound">e</a> <a id="2725" class="Symbol">:</a> <a id="2727" href="Cubical.Foundations.Univalence.html#2708" class="Bound">A</a> <a id="2729" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="2731" href="Cubical.Foundations.Univalence.html#2710" class="Bound">B</a><a id="2732" class="Symbol">)</a> <a id="2734" class="Symbol">(</a><a id="2735" href="Cubical.Foundations.Univalence.html#2735" class="Bound">i</a> <a id="2737" class="Symbol">:</a> <a id="2739" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="2740" class="Symbol">)</a> <a id="2742" class="Symbol">(</a><a id="2743" href="Cubical.Foundations.Univalence.html#2743" class="Bound">x</a> <a id="2745" class="Symbol">:</a> <a id="2747" href="Agda.Primitive.Cubical.html#1072" class="Primitive">Partial</a> <a id="2755" class="Symbol">(</a><a id="2756" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="2758" href="Cubical.Foundations.Univalence.html#2735" class="Bound">i</a><a id="2759" class="Symbol">)</a> <a id="2761" href="Cubical.Foundations.Univalence.html#2708" class="Bound">A</a><a id="2762" class="Symbol">)</a> <a id="2764" class="Symbol">(</a><a id="2765" href="Cubical.Foundations.Univalence.html#2765" class="Bound">y</a> <a id="2767" class="Symbol">:</a> <a id="2769" href="Cubical.Foundations.Univalence.html#2710" class="Bound">B</a> <a id="2771" href="Cubical.Core.Primitives.html#3508" class="Function Operator">[</a> <a id="2773" class="Symbol">_</a> <a id="2775" href="Cubical.Core.Primitives.html#3508" class="Function Operator">↦</a> <a id="2777" class="Symbol">_</a> <a id="2779" href="Cubical.Core.Primitives.html#3508" class="Function Operator">]</a><a id="2780" class="Symbol">)</a>
<a id="2799" class="Symbol">→</a> <a id="2801" href="Cubical.Foundations.Univalence.html#1450" class="Function">ua-unglue</a> <a id="2811" href="Cubical.Foundations.Univalence.html#2723" class="Bound">e</a> <a id="2813" href="Cubical.Foundations.Univalence.html#2735" class="Bound">i</a> <a id="2815" class="Symbol">(</a><a id="2816" href="Cubical.Foundations.Univalence.html#1623" class="Function">ua-glue</a> <a id="2824" href="Cubical.Foundations.Univalence.html#2723" class="Bound">e</a> <a id="2826" href="Cubical.Foundations.Univalence.html#2735" class="Bound">i</a> <a id="2828" href="Cubical.Foundations.Univalence.html#2743" class="Bound">x</a> <a id="2830" href="Cubical.Foundations.Univalence.html#2765" class="Bound">y</a><a id="2831" class="Symbol">)</a> <a id="2833" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2835" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="2840" href="Cubical.Foundations.Univalence.html#2765" class="Bound">y</a>
<a id="2842" href="Cubical.Foundations.Univalence.html#2688" class="Function">ua-unglue-glue</a> <a id="2857" class="Symbol">_</a> <a id="2859" class="Symbol">_</a> <a id="2861" class="Symbol">_</a> <a id="2863" class="Symbol">_</a> <a id="2865" class="Symbol">=</a> <a id="2867" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="ua-glue-unglue"></a><a id="2873" href="Cubical.Foundations.Univalence.html#2873" class="Function">ua-glue-unglue</a> <a id="2888" class="Symbol">:</a> <a id="2890" class="Symbol">∀</a> <a id="2892" class="Symbol">{</a><a id="2893" href="Cubical.Foundations.Univalence.html#2893" class="Bound">A</a> <a id="2895" href="Cubical.Foundations.Univalence.html#2895" class="Bound">B</a> <a id="2897" class="Symbol">:</a> <a id="2899" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2904" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="2905" class="Symbol">}</a> <a id="2907" class="Symbol">(</a><a id="2908" href="Cubical.Foundations.Univalence.html#2908" class="Bound">e</a> <a id="2910" class="Symbol">:</a> <a id="2912" href="Cubical.Foundations.Univalence.html#2893" class="Bound">A</a> <a id="2914" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="2916" href="Cubical.Foundations.Univalence.html#2895" class="Bound">B</a><a id="2917" class="Symbol">)</a> <a id="2919" class="Symbol">(</a><a id="2920" href="Cubical.Foundations.Univalence.html#2920" class="Bound">i</a> <a id="2922" class="Symbol">:</a> <a id="2924" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="2925" class="Symbol">)</a> <a id="2927" class="Symbol">(</a><a id="2928" href="Cubical.Foundations.Univalence.html#2928" class="Bound">x</a> <a id="2930" class="Symbol">:</a> <a id="2932" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="2935" href="Cubical.Foundations.Univalence.html#2908" class="Bound">e</a> <a id="2937" href="Cubical.Foundations.Univalence.html#2920" class="Bound">i</a><a id="2938" class="Symbol">)</a>
<a id="2957" class="Symbol">→</a> <a id="2959" href="Cubical.Foundations.Univalence.html#1623" class="Function">ua-glue</a> <a id="2967" href="Cubical.Foundations.Univalence.html#2908" class="Bound">e</a> <a id="2969" href="Cubical.Foundations.Univalence.html#2920" class="Bound">i</a> <a id="2971" class="Symbol">(λ</a> <a id="2974" class="Symbol">{</a> <a id="2976" class="Symbol">(</a><a id="2977" href="Cubical.Foundations.Univalence.html#2920" class="Bound">i</a> <a id="2979" class="Symbol">=</a> <a id="2981" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="2983" class="Symbol">)</a> <a id="2985" class="Symbol">→</a> <a id="2987" href="Cubical.Foundations.Univalence.html#2928" class="Bound">x</a> <a id="2989" class="Symbol">})</a> <a id="2992" class="Symbol">(</a><a id="2993" href="Agda.Builtin.Cubical.Sub.html#223" class="Postulate">inS</a> <a id="2997" class="Symbol">(</a><a id="2998" href="Cubical.Foundations.Univalence.html#1450" class="Function">ua-unglue</a> <a id="3008" href="Cubical.Foundations.Univalence.html#2908" class="Bound">e</a> <a id="3010" href="Cubical.Foundations.Univalence.html#2920" class="Bound">i</a> <a id="3012" href="Cubical.Foundations.Univalence.html#2928" class="Bound">x</a><a id="3013" class="Symbol">))</a> <a id="3016" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="3018" href="Cubical.Foundations.Univalence.html#2928" class="Bound">x</a>
<a id="3020" href="Cubical.Foundations.Univalence.html#2873" class="Function">ua-glue-unglue</a> <a id="3035" class="Symbol">_</a> <a id="3037" class="Symbol">_</a> <a id="3039" class="Symbol">_</a> <a id="3041" class="Symbol">=</a> <a id="3043" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="3049" class="Comment">-- mainly for documentation purposes, ua-unglue and ua-glue wrapped in cubical subtypes</a>
<a id="ua-unglueS"></a><a id="3138" href="Cubical.Foundations.Univalence.html#3138" class="Function">ua-unglueS</a> <a id="3149" class="Symbol">:</a> <a id="3151" class="Symbol">∀</a> <a id="3153" class="Symbol">{</a><a id="3154" href="Cubical.Foundations.Univalence.html#3154" class="Bound">A</a> <a id="3156" href="Cubical.Foundations.Univalence.html#3156" class="Bound">B</a> <a id="3158" class="Symbol">:</a> <a id="3160" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3165" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="3166" class="Symbol">}</a> <a id="3168" class="Symbol">(</a><a id="3169" href="Cubical.Foundations.Univalence.html#3169" class="Bound">e</a> <a id="3171" class="Symbol">:</a> <a id="3173" href="Cubical.Foundations.Univalence.html#3154" class="Bound">A</a> <a id="3175" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="3177" href="Cubical.Foundations.Univalence.html#3156" class="Bound">B</a><a id="3178" class="Symbol">)</a> <a id="3180" class="Symbol">(</a><a id="3181" href="Cubical.Foundations.Univalence.html#3181" class="Bound">i</a> <a id="3183" class="Symbol">:</a> <a id="3185" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="3186" class="Symbol">)</a> <a id="3188" class="Symbol">(</a><a id="3189" href="Cubical.Foundations.Univalence.html#3189" class="Bound">x</a> <a id="3191" class="Symbol">:</a> <a id="3193" href="Cubical.Foundations.Univalence.html#3154" class="Bound">A</a><a id="3194" class="Symbol">)</a> <a id="3196" class="Symbol">(</a><a id="3197" href="Cubical.Foundations.Univalence.html#3197" class="Bound">y</a> <a id="3199" class="Symbol">:</a> <a id="3201" href="Cubical.Foundations.Univalence.html#3156" class="Bound">B</a><a id="3202" class="Symbol">)</a>
<a id="3217" class="Symbol">→</a> <a id="3219" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="3222" href="Cubical.Foundations.Univalence.html#3169" class="Bound">e</a> <a id="3224" href="Cubical.Foundations.Univalence.html#3181" class="Bound">i</a> <a id="3226" href="Cubical.Core.Primitives.html#3508" class="Function Operator">[</a> <a id="3228" class="Symbol">_</a> <a id="3230" href="Cubical.Core.Primitives.html#3508" class="Function Operator">↦</a> <a id="3232" class="Symbol">(λ</a> <a id="3235" class="Symbol">{</a> <a id="3237" class="Symbol">(</a><a id="3238" href="Cubical.Foundations.Univalence.html#3181" class="Bound">i</a> <a id="3240" class="Symbol">=</a> <a id="3242" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="3244" class="Symbol">)</a> <a id="3246" class="Symbol">→</a> <a id="3248" href="Cubical.Foundations.Univalence.html#3189" class="Bound">x</a> <a id="3257" class="Symbol">;</a> <a id="3259" class="Symbol">(</a><a id="3260" href="Cubical.Foundations.Univalence.html#3181" class="Bound">i</a> <a id="3262" class="Symbol">=</a> <a id="3264" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="3266" class="Symbol">)</a> <a id="3268" class="Symbol">→</a> <a id="3270" href="Cubical.Foundations.Univalence.html#3197" class="Bound">y</a> <a id="3272" class="Symbol">})</a> <a id="3275" href="Cubical.Core.Primitives.html#3508" class="Function Operator">]</a>
<a id="3290" class="Symbol">→</a> <a id="3292" href="Cubical.Foundations.Univalence.html#3156" class="Bound">B</a> <a id="3299" href="Cubical.Core.Primitives.html#3508" class="Function Operator">[</a> <a id="3301" class="Symbol">_</a> <a id="3303" href="Cubical.Core.Primitives.html#3508" class="Function Operator">↦</a> <a id="3305" class="Symbol">(λ</a> <a id="3308" class="Symbol">{</a> <a id="3310" class="Symbol">(</a><a id="3311" href="Cubical.Foundations.Univalence.html#3181" class="Bound">i</a> <a id="3313" class="Symbol">=</a> <a id="3315" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="3317" class="Symbol">)</a> <a id="3319" class="Symbol">→</a> <a id="3321" href="Cubical.Foundations.Univalence.html#3169" class="Bound">e</a> <a id="3323" class="Symbol">.</a><a id="3324" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="3328" href="Cubical.Foundations.Univalence.html#3189" class="Bound">x</a> <a id="3330" class="Symbol">;</a> <a id="3332" class="Symbol">(</a><a id="3333" href="Cubical.Foundations.Univalence.html#3181" class="Bound">i</a> <a id="3335" class="Symbol">=</a> <a id="3337" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="3339" class="Symbol">)</a> <a id="3341" class="Symbol">→</a> <a id="3343" href="Cubical.Foundations.Univalence.html#3197" class="Bound">y</a> <a id="3345" class="Symbol">})</a> <a id="3348" href="Cubical.Core.Primitives.html#3508" class="Function Operator">]</a>
<a id="3350" href="Cubical.Foundations.Univalence.html#3138" class="Function">ua-unglueS</a> <a id="3361" href="Cubical.Foundations.Univalence.html#3361" class="Bound">e</a> <a id="3363" href="Cubical.Foundations.Univalence.html#3363" class="Bound">i</a> <a id="3365" href="Cubical.Foundations.Univalence.html#3365" class="Bound">x</a> <a id="3367" href="Cubical.Foundations.Univalence.html#3367" class="Bound">y</a> <a id="3369" href="Cubical.Foundations.Univalence.html#3369" class="Bound">s</a> <a id="3371" class="Symbol">=</a> <a id="3373" href="Agda.Builtin.Cubical.Sub.html#223" class="Postulate">inS</a> <a id="3377" class="Symbol">(</a><a id="3378" href="Cubical.Foundations.Univalence.html#1450" class="Function">ua-unglue</a> <a id="3388" href="Cubical.Foundations.Univalence.html#3361" class="Bound">e</a> <a id="3390" href="Cubical.Foundations.Univalence.html#3363" class="Bound">i</a> <a id="3392" class="Symbol">(</a><a id="3393" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="3398" href="Cubical.Foundations.Univalence.html#3369" class="Bound">s</a><a id="3399" class="Symbol">))</a>
<a id="ua-glueS"></a><a id="3403" href="Cubical.Foundations.Univalence.html#3403" class="Function">ua-glueS</a> <a id="3412" class="Symbol">:</a> <a id="3414" class="Symbol">∀</a> <a id="3416" class="Symbol">{</a><a id="3417" href="Cubical.Foundations.Univalence.html#3417" class="Bound">A</a> <a id="3419" href="Cubical.Foundations.Univalence.html#3419" class="Bound">B</a> <a id="3421" class="Symbol">:</a> <a id="3423" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3428" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="3429" class="Symbol">}</a> <a id="3431" class="Symbol">(</a><a id="3432" href="Cubical.Foundations.Univalence.html#3432" class="Bound">e</a> <a id="3434" class="Symbol">:</a> <a id="3436" href="Cubical.Foundations.Univalence.html#3417" class="Bound">A</a> <a id="3438" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="3440" href="Cubical.Foundations.Univalence.html#3419" class="Bound">B</a><a id="3441" class="Symbol">)</a> <a id="3443" class="Symbol">(</a><a id="3444" href="Cubical.Foundations.Univalence.html#3444" class="Bound">i</a> <a id="3446" class="Symbol">:</a> <a id="3448" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="3449" class="Symbol">)</a> <a id="3451" class="Symbol">(</a><a id="3452" href="Cubical.Foundations.Univalence.html#3452" class="Bound">x</a> <a id="3454" class="Symbol">:</a> <a id="3456" href="Cubical.Foundations.Univalence.html#3417" class="Bound">A</a><a id="3457" class="Symbol">)</a> <a id="3459" class="Symbol">(</a><a id="3460" href="Cubical.Foundations.Univalence.html#3460" class="Bound">y</a> <a id="3462" class="Symbol">:</a> <a id="3464" href="Cubical.Foundations.Univalence.html#3419" class="Bound">B</a><a id="3465" class="Symbol">)</a>
<a id="3478" class="Symbol">→</a> <a id="3480" href="Cubical.Foundations.Univalence.html#3419" class="Bound">B</a> <a id="3487" href="Cubical.Core.Primitives.html#3508" class="Function Operator">[</a> <a id="3489" class="Symbol">_</a> <a id="3491" href="Cubical.Core.Primitives.html#3508" class="Function Operator">↦</a> <a id="3493" class="Symbol">(λ</a> <a id="3496" class="Symbol">{</a> <a id="3498" class="Symbol">(</a><a id="3499" href="Cubical.Foundations.Univalence.html#3444" class="Bound">i</a> <a id="3501" class="Symbol">=</a> <a id="3503" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="3505" class="Symbol">)</a> <a id="3507" class="Symbol">→</a> <a id="3509" href="Cubical.Foundations.Univalence.html#3432" class="Bound">e</a> <a id="3511" class="Symbol">.</a><a id="3512" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="3516" href="Cubical.Foundations.Univalence.html#3452" class="Bound">x</a> <a id="3518" class="Symbol">;</a> <a id="3520" class="Symbol">(</a><a id="3521" href="Cubical.Foundations.Univalence.html#3444" class="Bound">i</a> <a id="3523" class="Symbol">=</a> <a id="3525" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="3527" class="Symbol">)</a> <a id="3529" class="Symbol">→</a> <a id="3531" href="Cubical.Foundations.Univalence.html#3460" class="Bound">y</a> <a id="3533" class="Symbol">})</a> <a id="3536" href="Cubical.Core.Primitives.html#3508" class="Function Operator">]</a>
<a id="3549" class="Symbol">→</a> <a id="3551" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="3554" href="Cubical.Foundations.Univalence.html#3432" class="Bound">e</a> <a id="3556" href="Cubical.Foundations.Univalence.html#3444" class="Bound">i</a> <a id="3558" href="Cubical.Core.Primitives.html#3508" class="Function Operator">[</a> <a id="3560" class="Symbol">_</a> <a id="3562" href="Cubical.Core.Primitives.html#3508" class="Function Operator">↦</a> <a id="3564" class="Symbol">(λ</a> <a id="3567" class="Symbol">{</a> <a id="3569" class="Symbol">(</a><a id="3570" href="Cubical.Foundations.Univalence.html#3444" class="Bound">i</a> <a id="3572" class="Symbol">=</a> <a id="3574" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="3576" class="Symbol">)</a> <a id="3578" class="Symbol">→</a> <a id="3580" href="Cubical.Foundations.Univalence.html#3452" class="Bound">x</a> <a id="3589" class="Symbol">;</a> <a id="3591" class="Symbol">(</a><a id="3592" href="Cubical.Foundations.Univalence.html#3444" class="Bound">i</a> <a id="3594" class="Symbol">=</a> <a id="3596" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="3598" class="Symbol">)</a> <a id="3600" class="Symbol">→</a> <a id="3602" href="Cubical.Foundations.Univalence.html#3460" class="Bound">y</a> <a id="3604" class="Symbol">})</a> <a id="3607" href="Cubical.Core.Primitives.html#3508" class="Function Operator">]</a>
<a id="3609" href="Cubical.Foundations.Univalence.html#3403" class="Function">ua-glueS</a> <a id="3618" href="Cubical.Foundations.Univalence.html#3618" class="Bound">e</a> <a id="3620" href="Cubical.Foundations.Univalence.html#3620" class="Bound">i</a> <a id="3622" href="Cubical.Foundations.Univalence.html#3622" class="Bound">x</a> <a id="3624" href="Cubical.Foundations.Univalence.html#3624" class="Bound">y</a> <a id="3626" href="Cubical.Foundations.Univalence.html#3626" class="Bound">s</a> <a id="3628" class="Symbol">=</a> <a id="3630" href="Agda.Builtin.Cubical.Sub.html#223" class="Postulate">inS</a> <a id="3634" class="Symbol">(</a><a id="3635" href="Cubical.Foundations.Univalence.html#1623" class="Function">ua-glue</a> <a id="3643" href="Cubical.Foundations.Univalence.html#3618" class="Bound">e</a> <a id="3645" href="Cubical.Foundations.Univalence.html#3620" class="Bound">i</a> <a id="3647" class="Symbol">(λ</a> <a id="3650" class="Symbol">{</a> <a id="3652" class="Symbol">(</a><a id="3653" href="Cubical.Foundations.Univalence.html#3620" class="Bound">i</a> <a id="3655" class="Symbol">=</a> <a id="3657" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="3659" class="Symbol">)</a> <a id="3661" class="Symbol">→</a> <a id="3663" href="Cubical.Foundations.Univalence.html#3622" class="Bound">x</a> <a id="3665" class="Symbol">})</a> <a id="3668" class="Symbol">(</a><a id="3669" href="Agda.Builtin.Cubical.Sub.html#223" class="Postulate">inS</a> <a id="3673" class="Symbol">(</a><a id="3674" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="3679" href="Cubical.Foundations.Univalence.html#3626" class="Bound">s</a><a id="3680" class="Symbol">)))</a>
<a id="ua-unglueS-glueS"></a><a id="3685" href="Cubical.Foundations.Univalence.html#3685" class="Function">ua-unglueS-glueS</a> <a id="3702" class="Symbol">:</a> <a id="3704" class="Symbol">∀</a> <a id="3706" class="Symbol">{</a><a id="3707" href="Cubical.Foundations.Univalence.html#3707" class="Bound">A</a> <a id="3709" href="Cubical.Foundations.Univalence.html#3709" class="Bound">B</a> <a id="3711" class="Symbol">:</a> <a id="3713" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3718" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="3719" class="Symbol">}</a> <a id="3721" class="Symbol">(</a><a id="3722" href="Cubical.Foundations.Univalence.html#3722" class="Bound">e</a> <a id="3724" class="Symbol">:</a> <a id="3726" href="Cubical.Foundations.Univalence.html#3707" class="Bound">A</a> <a id="3728" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="3730" href="Cubical.Foundations.Univalence.html#3709" class="Bound">B</a><a id="3731" class="Symbol">)</a> <a id="3733" class="Symbol">(</a><a id="3734" href="Cubical.Foundations.Univalence.html#3734" class="Bound">i</a> <a id="3736" class="Symbol">:</a> <a id="3738" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="3739" class="Symbol">)</a> <a id="3741" class="Symbol">(</a><a id="3742" href="Cubical.Foundations.Univalence.html#3742" class="Bound">x</a> <a id="3744" class="Symbol">:</a> <a id="3746" href="Cubical.Foundations.Univalence.html#3707" class="Bound">A</a><a id="3747" class="Symbol">)</a> <a id="3749" class="Symbol">(</a><a id="3750" href="Cubical.Foundations.Univalence.html#3750" class="Bound">y</a> <a id="3752" class="Symbol">:</a> <a id="3754" href="Cubical.Foundations.Univalence.html#3709" class="Bound">B</a><a id="3755" class="Symbol">)</a>
<a id="3778" class="Symbol">(</a><a id="3779" href="Cubical.Foundations.Univalence.html#3779" class="Bound">s</a> <a id="3781" class="Symbol">:</a> <a id="3783" href="Cubical.Foundations.Univalence.html#3709" class="Bound">B</a> <a id="3785" href="Cubical.Core.Primitives.html#3508" class="Function Operator">[</a> <a id="3787" class="Symbol">_</a> <a id="3789" href="Cubical.Core.Primitives.html#3508" class="Function Operator">↦</a> <a id="3791" class="Symbol">(λ</a> <a id="3794" class="Symbol">{</a> <a id="3796" class="Symbol">(</a><a id="3797" href="Cubical.Foundations.Univalence.html#3734" class="Bound">i</a> <a id="3799" class="Symbol">=</a> <a id="3801" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="3803" class="Symbol">)</a> <a id="3805" class="Symbol">→</a> <a id="3807" href="Cubical.Foundations.Univalence.html#3722" class="Bound">e</a> <a id="3809" class="Symbol">.</a><a id="3810" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="3814" href="Cubical.Foundations.Univalence.html#3742" class="Bound">x</a> <a id="3816" class="Symbol">;</a> <a id="3818" class="Symbol">(</a><a id="3819" href="Cubical.Foundations.Univalence.html#3734" class="Bound">i</a> <a id="3821" class="Symbol">=</a> <a id="3823" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="3825" class="Symbol">)</a> <a id="3827" class="Symbol">→</a> <a id="3829" href="Cubical.Foundations.Univalence.html#3750" class="Bound">y</a> <a id="3831" class="Symbol">})</a> <a id="3834" href="Cubical.Core.Primitives.html#3508" class="Function Operator">]</a><a id="3835" class="Symbol">)</a>
<a id="3856" class="Symbol">→</a> <a id="3858" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="3863" class="Symbol">(</a><a id="3864" href="Cubical.Foundations.Univalence.html#3138" class="Function">ua-unglueS</a> <a id="3875" href="Cubical.Foundations.Univalence.html#3722" class="Bound">e</a> <a id="3877" href="Cubical.Foundations.Univalence.html#3734" class="Bound">i</a> <a id="3879" href="Cubical.Foundations.Univalence.html#3742" class="Bound">x</a> <a id="3881" href="Cubical.Foundations.Univalence.html#3750" class="Bound">y</a> <a id="3883" class="Symbol">(</a><a id="3884" href="Cubical.Foundations.Univalence.html#3403" class="Function">ua-glueS</a> <a id="3893" href="Cubical.Foundations.Univalence.html#3722" class="Bound">e</a> <a id="3895" href="Cubical.Foundations.Univalence.html#3734" class="Bound">i</a> <a id="3897" href="Cubical.Foundations.Univalence.html#3742" class="Bound">x</a> <a id="3899" href="Cubical.Foundations.Univalence.html#3750" class="Bound">y</a> <a id="3901" href="Cubical.Foundations.Univalence.html#3779" class="Bound">s</a><a id="3902" class="Symbol">))</a> <a id="3905" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="3907" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="3912" href="Cubical.Foundations.Univalence.html#3779" class="Bound">s</a>
<a id="3914" href="Cubical.Foundations.Univalence.html#3685" class="Function">ua-unglueS-glueS</a> <a id="3931" class="Symbol">_</a> <a id="3933" class="Symbol">_</a> <a id="3935" class="Symbol">_</a> <a id="3937" class="Symbol">_</a> <a id="3939" class="Symbol">_</a> <a id="3941" class="Symbol">=</a> <a id="3943" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="ua-glueS-unglueS"></a><a id="3949" href="Cubical.Foundations.Univalence.html#3949" class="Function">ua-glueS-unglueS</a> <a id="3966" class="Symbol">:</a> <a id="3968" class="Symbol">∀</a> <a id="3970" class="Symbol">{</a><a id="3971" href="Cubical.Foundations.Univalence.html#3971" class="Bound">A</a> <a id="3973" href="Cubical.Foundations.Univalence.html#3973" class="Bound">B</a> <a id="3975" class="Symbol">:</a> <a id="3977" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3982" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="3983" class="Symbol">}</a> <a id="3985" class="Symbol">(</a><a id="3986" href="Cubical.Foundations.Univalence.html#3986" class="Bound">e</a> <a id="3988" class="Symbol">:</a> <a id="3990" href="Cubical.Foundations.Univalence.html#3971" class="Bound">A</a> <a id="3992" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="3994" href="Cubical.Foundations.Univalence.html#3973" class="Bound">B</a><a id="3995" class="Symbol">)</a> <a id="3997" class="Symbol">(</a><a id="3998" href="Cubical.Foundations.Univalence.html#3998" class="Bound">i</a> <a id="4000" class="Symbol">:</a> <a id="4002" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="4003" class="Symbol">)</a> <a id="4005" class="Symbol">(</a><a id="4006" href="Cubical.Foundations.Univalence.html#4006" class="Bound">x</a> <a id="4008" class="Symbol">:</a> <a id="4010" href="Cubical.Foundations.Univalence.html#3971" class="Bound">A</a><a id="4011" class="Symbol">)</a> <a id="4013" class="Symbol">(</a><a id="4014" href="Cubical.Foundations.Univalence.html#4014" class="Bound">y</a> <a id="4016" class="Symbol">:</a> <a id="4018" href="Cubical.Foundations.Univalence.html#3973" class="Bound">B</a><a id="4019" class="Symbol">)</a>
<a id="4042" class="Symbol">(</a><a id="4043" href="Cubical.Foundations.Univalence.html#4043" class="Bound">s</a> <a id="4045" class="Symbol">:</a> <a id="4047" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="4050" href="Cubical.Foundations.Univalence.html#3986" class="Bound">e</a> <a id="4052" href="Cubical.Foundations.Univalence.html#3998" class="Bound">i</a> <a id="4054" href="Cubical.Core.Primitives.html#3508" class="Function Operator">[</a> <a id="4056" class="Symbol">_</a> <a id="4058" href="Cubical.Core.Primitives.html#3508" class="Function Operator">↦</a> <a id="4060" class="Symbol">(λ</a> <a id="4063" class="Symbol">{</a> <a id="4065" class="Symbol">(</a><a id="4066" href="Cubical.Foundations.Univalence.html#3998" class="Bound">i</a> <a id="4068" class="Symbol">=</a> <a id="4070" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="4072" class="Symbol">)</a> <a id="4074" class="Symbol">→</a> <a id="4076" href="Cubical.Foundations.Univalence.html#4006" class="Bound">x</a> <a id="4078" class="Symbol">;</a> <a id="4080" class="Symbol">(</a><a id="4081" href="Cubical.Foundations.Univalence.html#3998" class="Bound">i</a> <a id="4083" class="Symbol">=</a> <a id="4085" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="4087" class="Symbol">)</a> <a id="4089" class="Symbol">→</a> <a id="4091" href="Cubical.Foundations.Univalence.html#4014" class="Bound">y</a> <a id="4093" class="Symbol">})</a> <a id="4096" href="Cubical.Core.Primitives.html#3508" class="Function Operator">]</a><a id="4097" class="Symbol">)</a>
<a id="4118" class="Symbol">→</a> <a id="4120" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="4125" class="Symbol">(</a><a id="4126" href="Cubical.Foundations.Univalence.html#3403" class="Function">ua-glueS</a> <a id="4135" href="Cubical.Foundations.Univalence.html#3986" class="Bound">e</a> <a id="4137" href="Cubical.Foundations.Univalence.html#3998" class="Bound">i</a> <a id="4139" href="Cubical.Foundations.Univalence.html#4006" class="Bound">x</a> <a id="4141" href="Cubical.Foundations.Univalence.html#4014" class="Bound">y</a> <a id="4143" class="Symbol">(</a><a id="4144" href="Cubical.Foundations.Univalence.html#3138" class="Function">ua-unglueS</a> <a id="4155" href="Cubical.Foundations.Univalence.html#3986" class="Bound">e</a> <a id="4157" href="Cubical.Foundations.Univalence.html#3998" class="Bound">i</a> <a id="4159" href="Cubical.Foundations.Univalence.html#4006" class="Bound">x</a> <a id="4161" href="Cubical.Foundations.Univalence.html#4014" class="Bound">y</a> <a id="4163" href="Cubical.Foundations.Univalence.html#4043" class="Bound">s</a><a id="4164" class="Symbol">))</a> <a id="4167" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="4169" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="4174" href="Cubical.Foundations.Univalence.html#4043" class="Bound">s</a>
<a id="4176" href="Cubical.Foundations.Univalence.html#3949" class="Function">ua-glueS-unglueS</a> <a id="4193" class="Symbol">_</a> <a id="4195" class="Symbol">_</a> <a id="4197" class="Symbol">_</a> <a id="4199" class="Symbol">_</a> <a id="4201" class="Symbol">_</a> <a id="4203" class="Symbol">=</a> <a id="4205" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="4212" class="Comment">-- a version of ua-glue with a single endpoint, identical to `ua-gluePath e {x} refl i`</a>
<a id="ua-gluePt"></a><a id="4300" href="Cubical.Foundations.Univalence.html#4300" class="Function">ua-gluePt</a> <a id="4310" class="Symbol">:</a> <a id="4312" class="Symbol">∀</a> <a id="4314" class="Symbol">{</a><a id="4315" href="Cubical.Foundations.Univalence.html#4315" class="Bound">A</a> <a id="4317" href="Cubical.Foundations.Univalence.html#4317" class="Bound">B</a> <a id="4319" class="Symbol">:</a> <a id="4321" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="4326" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="4327" class="Symbol">}</a> <a id="4329" class="Symbol">(</a><a id="4330" href="Cubical.Foundations.Univalence.html#4330" class="Bound">e</a> <a id="4332" class="Symbol">:</a> <a id="4334" href="Cubical.Foundations.Univalence.html#4315" class="Bound">A</a> <a id="4336" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="4338" href="Cubical.Foundations.Univalence.html#4317" class="Bound">B</a><a id="4339" class="Symbol">)</a> <a id="4341" class="Symbol">(</a><a id="4342" href="Cubical.Foundations.Univalence.html#4342" class="Bound">i</a> <a id="4344" class="Symbol">:</a> <a id="4346" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="4347" class="Symbol">)</a> <a id="4349" class="Symbol">(</a><a id="4350" href="Cubical.Foundations.Univalence.html#4350" class="Bound">x</a> <a id="4352" class="Symbol">:</a> <a id="4354" href="Cubical.Foundations.Univalence.html#4315" class="Bound">A</a><a id="4355" class="Symbol">)</a>
<a id="4369" class="Symbol">→</a> <a id="4371" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="4374" href="Cubical.Foundations.Univalence.html#4330" class="Bound">e</a> <a id="4376" href="Cubical.Foundations.Univalence.html#4342" class="Bound">i</a> <a id="4378" class="Comment">{- [ _ ↦ (λ { (i = i0) → x ; (i = i1) → e .fst x }) ] -}</a>
<a id="4435" href="Cubical.Foundations.Univalence.html#4300" class="Function">ua-gluePt</a> <a id="4445" href="Cubical.Foundations.Univalence.html#4445" class="Bound">e</a> <a id="4447" href="Cubical.Foundations.Univalence.html#4447" class="Bound">i</a> <a id="4449" href="Cubical.Foundations.Univalence.html#4449" class="Bound">x</a> <a id="4451" class="Symbol">=</a> <a id="4453" href="Cubical.Foundations.Univalence.html#1623" class="Function">ua-glue</a> <a id="4461" href="Cubical.Foundations.Univalence.html#4445" class="Bound">e</a> <a id="4463" href="Cubical.Foundations.Univalence.html#4447" class="Bound">i</a> <a id="4465" class="Symbol">(λ</a> <a id="4468" class="Symbol">{</a> <a id="4470" class="Symbol">(</a><a id="4471" href="Cubical.Foundations.Univalence.html#4447" class="Bound">i</a> <a id="4473" class="Symbol">=</a> <a id="4475" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="4477" class="Symbol">)</a> <a id="4479" class="Symbol">→</a> <a id="4481" href="Cubical.Foundations.Univalence.html#4449" class="Bound">x</a> <a id="4483" class="Symbol">})</a> <a id="4486" class="Symbol">(</a><a id="4487" href="Agda.Builtin.Cubical.Sub.html#223" class="Postulate">inS</a> <a id="4491" class="Symbol">(</a><a id="4492" href="Cubical.Foundations.Univalence.html#4445" class="Bound">e</a> <a id="4494" class="Symbol">.</a><a id="4495" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="4499" href="Cubical.Foundations.Univalence.html#4449" class="Bound">x</a><a id="4500" class="Symbol">))</a>
<a id="4505" class="Comment">-- Proof of univalence using that unglue is an equivalence:</a>
<a id="4566" class="Comment">-- unglue is an equivalence</a>
<a id="unglueIsEquiv"></a><a id="4594" href="Cubical.Foundations.Univalence.html#4594" class="Function">unglueIsEquiv</a> <a id="4608" class="Symbol">:</a> <a id="4610" class="Symbol">∀</a> <a id="4612" class="Symbol">(</a><a id="4613" href="Cubical.Foundations.Univalence.html#4613" class="Bound">A</a> <a id="4615" class="Symbol">:</a> <a id="4617" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="4622" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="4623" class="Symbol">)</a> <a id="4625" class="Symbol">(</a><a id="4626" href="Cubical.Foundations.Univalence.html#4626" class="Bound">φ</a> <a id="4628" class="Symbol">:</a> <a id="4630" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="4631" class="Symbol">)</a>
<a id="4649" class="Symbol">(</a><a id="4650" href="Cubical.Foundations.Univalence.html#4650" class="Bound">f</a> <a id="4652" class="Symbol">:</a> <a id="4654" href="Agda.Primitive.Cubical.html#1106" class="Primitive">PartialP</a> <a id="4663" href="Cubical.Foundations.Univalence.html#4626" class="Bound">φ</a> <a id="4665" class="Symbol">(λ</a> <a id="4668" href="Cubical.Foundations.Univalence.html#4668" class="Bound">o</a> <a id="4670" class="Symbol">→</a> <a id="4672" href="Cubical.Core.Primitives.html#6306" class="Function">Σ[</a> <a id="4675" href="Cubical.Foundations.Univalence.html#4675" class="Bound">T</a> <a id="4677" href="Cubical.Core.Primitives.html#6306" class="Function">∈</a> <a id="4679" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="4684" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a> <a id="4686" href="Cubical.Core.Primitives.html#6306" class="Function">]</a> <a id="4688" href="Cubical.Foundations.Univalence.html#4675" class="Bound">T</a> <a id="4690" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="4692" href="Cubical.Foundations.Univalence.html#4613" class="Bound">A</a><a id="4693" class="Symbol">))</a> <a id="4696" class="Symbol">→</a>
<a id="4714" href="Agda.Builtin.Cubical.Glue.html#868" class="Record">isEquiv</a> <a id="4722" class="Symbol">{</a><a id="4723" class="Argument">A</a> <a id="4725" class="Symbol">=</a> <a id="4727" href="Cubical.Core.Glue.html#1521" class="Function">Glue</a> <a id="4732" href="Cubical.Foundations.Univalence.html#4613" class="Bound">A</a> <a id="4734" href="Cubical.Foundations.Univalence.html#4650" class="Bound">f</a><a id="4735" class="Symbol">}</a> <a id="4737" class="Symbol">(</a><a id="4738" href="Cubical.Core.Glue.html#1724" class="Function">unglue</a> <a id="4745" href="Cubical.Foundations.Univalence.html#4626" class="Bound">φ</a><a id="4746" class="Symbol">)</a>
<a id="4748" href="Agda.Builtin.Cubical.Glue.html#971" class="Field">equiv-proof</a> <a id="4760" class="Symbol">(</a><a id="4761" href="Cubical.Foundations.Univalence.html#4594" class="Function">unglueIsEquiv</a> <a id="4775" href="Cubical.Foundations.Univalence.html#4775" class="Bound">A</a> <a id="4777" href="Cubical.Foundations.Univalence.html#4777" class="Bound">φ</a> <a id="4779" href="Cubical.Foundations.Univalence.html#4779" class="Bound">f</a><a id="4780" class="Symbol">)</a> <a id="4782" class="Symbol">=</a> <a id="4784" class="Symbol">λ</a> <a id="4786" class="Symbol">(</a><a id="4787" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a> <a id="4789" class="Symbol">:</a> <a id="4791" href="Cubical.Foundations.Univalence.html#4775" class="Bound">A</a><a id="4792" class="Symbol">)</a> <a id="4794" class="Symbol">→</a>
<a id="4798" class="Keyword">let</a> <a id="4802" href="Cubical.Foundations.Univalence.html#4802" class="Bound">u</a> <a id="4804" class="Symbol">:</a> <a id="4806" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a> <a id="4808" class="Symbol">→</a> <a id="4810" href="Agda.Primitive.Cubical.html#1072" class="Primitive">Partial</a> <a id="4818" href="Cubical.Foundations.Univalence.html#4777" class="Bound">φ</a> <a id="4820" href="Cubical.Foundations.Univalence.html#4775" class="Bound">A</a>
<a id="4828" href="Cubical.Foundations.Univalence.html#4802" class="Bound">u</a> <a id="4830" href="Cubical.Foundations.Univalence.html#4830" class="Bound">i</a> <a id="4832" class="Symbol">=</a> <a id="4834" class="Symbol">λ{</a> <a id="4837" class="Symbol">(</a><a id="4838" href="Cubical.Foundations.Univalence.html#4777" class="Bound">φ</a> <a id="4840" class="Symbol">=</a> <a id="4842" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="4844" class="Symbol">)</a> <a id="4846" class="Symbol">→</a> <a id="4848" href="Cubical.Foundations.Equiv.html#898" class="Function">equivCtr</a> <a id="4857" class="Symbol">(</a><a id="4858" href="Cubical.Foundations.Univalence.html#4779" class="Bound">f</a> <a id="4860" href="Cubical.Core.Primitives.html#732" class="Postulate">1=1</a> <a id="4864" class="Symbol">.</a><a id="4865" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a><a id="4868" class="Symbol">)</a> <a id="4870" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a> <a id="4872" class="Symbol">.</a><a id="4873" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="4877" class="Symbol">(</a><a id="4878" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="4880" href="Cubical.Foundations.Univalence.html#4830" class="Bound">i</a><a id="4881" class="Symbol">)</a> <a id="4883" class="Symbol">}</a>
<a id="4891" href="Cubical.Foundations.Univalence.html#4891" class="Bound">ctr</a> <a id="4895" class="Symbol">:</a> <a id="4897" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="4903" class="Symbol">(</a><a id="4904" href="Cubical.Core.Glue.html#1724" class="Function">unglue</a> <a id="4911" href="Cubical.Foundations.Univalence.html#4777" class="Bound">φ</a><a id="4912" class="Symbol">)</a> <a id="4914" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a>
<a id="4922" href="Cubical.Foundations.Univalence.html#4891" class="Bound">ctr</a> <a id="4926" class="Symbol">=</a> <a id="4928" class="Symbol">(</a> <a id="4930" href="Agda.Builtin.Cubical.Glue.html#2169" class="Primitive">glue</a> <a id="4935" class="Symbol">(λ</a> <a id="4938" class="Symbol">{</a> <a id="4940" class="Symbol">(</a><a id="4941" href="Cubical.Foundations.Univalence.html#4777" class="Bound">φ</a> <a id="4943" class="Symbol">=</a> <a id="4945" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="4947" class="Symbol">)</a> <a id="4949" class="Symbol">→</a> <a id="4951" href="Cubical.Foundations.Equiv.html#898" class="Function">equivCtr</a> <a id="4960" class="Symbol">(</a><a id="4961" href="Cubical.Foundations.Univalence.html#4779" class="Bound">f</a> <a id="4963" href="Cubical.Core.Primitives.html#732" class="Postulate">1=1</a> <a id="4967" class="Symbol">.</a><a id="4968" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a><a id="4971" class="Symbol">)</a> <a id="4973" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a> <a id="4975" class="Symbol">.</a><a id="4976" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="4980" class="Symbol">})</a> <a id="4983" class="Symbol">(</a><a id="4984" href="Cubical.Core.Primitives.html#657" class="Primitive">hcomp</a> <a id="4990" href="Cubical.Foundations.Univalence.html#4802" class="Bound">u</a> <a id="4992" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a><a id="4993" class="Symbol">)</a>
<a id="5007" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5009" class="Symbol">λ</a> <a id="5011" href="Cubical.Foundations.Univalence.html#5011" class="Bound">j</a> <a id="5013" class="Symbol">→</a> <a id="5015" href="Cubical.Core.Primitives.html#5145" class="Function">hfill</a> <a id="5021" href="Cubical.Foundations.Univalence.html#4802" class="Bound">u</a> <a id="5023" class="Symbol">(</a><a id="5024" href="Agda.Builtin.Cubical.Sub.html#223" class="Postulate">inS</a> <a id="5028" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a><a id="5029" class="Symbol">)</a> <a id="5031" class="Symbol">(</a><a id="5032" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="5034" href="Cubical.Foundations.Univalence.html#5011" class="Bound">j</a><a id="5035" class="Symbol">))</a>
<a id="5040" class="Keyword">in</a> <a id="5043" class="Symbol">(</a> <a id="5045" href="Cubical.Foundations.Univalence.html#4891" class="Bound">ctr</a>
<a id="5054" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5056" class="Symbol">λ</a> <a id="5058" class="Symbol">(</a><a id="5059" href="Cubical.Foundations.Univalence.html#5059" class="Bound">v</a> <a id="5061" class="Symbol">:</a> <a id="5063" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="5069" class="Symbol">(</a><a id="5070" href="Cubical.Core.Glue.html#1724" class="Function">unglue</a> <a id="5077" href="Cubical.Foundations.Univalence.html#4777" class="Bound">φ</a><a id="5078" class="Symbol">)</a> <a id="5080" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a><a id="5081" class="Symbol">)</a> <a id="5083" href="Cubical.Foundations.Univalence.html#5083" class="Bound">i</a> <a id="5085" class="Symbol">→</a>
<a id="5096" class="Keyword">let</a> <a id="5100" href="Cubical.Foundations.Univalence.html#5100" class="Bound">u'</a> <a id="5103" class="Symbol">:</a> <a id="5105" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a> <a id="5107" class="Symbol">→</a> <a id="5109" href="Agda.Primitive.Cubical.html#1072" class="Primitive">Partial</a> <a id="5117" class="Symbol">(</a><a id="5118" href="Cubical.Foundations.Univalence.html#4777" class="Bound">φ</a> <a id="5120" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="5122" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="5124" href="Cubical.Foundations.Univalence.html#5083" class="Bound">i</a> <a id="5126" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="5128" href="Cubical.Foundations.Univalence.html#5083" class="Bound">i</a><a id="5129" class="Symbol">)</a> <a id="5131" href="Cubical.Foundations.Univalence.html#4775" class="Bound">A</a>
<a id="5146" href="Cubical.Foundations.Univalence.html#5100" class="Bound">u'</a> <a id="5149" href="Cubical.Foundations.Univalence.html#5149" class="Bound">j</a> <a id="5151" class="Symbol">=</a> <a id="5153" class="Symbol">λ</a> <a id="5155" class="Symbol">{</a> <a id="5157" class="Symbol">(</a><a id="5158" href="Cubical.Foundations.Univalence.html#4777" class="Bound">φ</a> <a id="5160" class="Symbol">=</a> <a id="5162" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="5164" class="Symbol">)</a> <a id="5166" class="Symbol">→</a> <a id="5168" href="Cubical.Foundations.Equiv.html#995" class="Function">equivCtrPath</a> <a id="5181" class="Symbol">(</a><a id="5182" href="Cubical.Foundations.Univalence.html#4779" class="Bound">f</a> <a id="5184" href="Cubical.Core.Primitives.html#732" class="Postulate">1=1</a> <a id="5188" class="Symbol">.</a><a id="5189" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a><a id="5192" class="Symbol">)</a> <a id="5194" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a> <a id="5196" href="Cubical.Foundations.Univalence.html#5059" class="Bound">v</a> <a id="5198" href="Cubical.Foundations.Univalence.html#5083" class="Bound">i</a> <a id="5200" class="Symbol">.</a><a id="5201" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="5205" class="Symbol">(</a><a id="5206" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="5208" href="Cubical.Foundations.Univalence.html#5149" class="Bound">j</a><a id="5209" class="Symbol">)</a>
<a id="5233" class="Symbol">;</a> <a id="5235" class="Symbol">(</a><a id="5236" href="Cubical.Foundations.Univalence.html#5083" class="Bound">i</a> <a id="5238" class="Symbol">=</a> <a id="5240" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="5242" class="Symbol">)</a> <a id="5244" class="Symbol">→</a> <a id="5246" href="Cubical.Core.Primitives.html#5145" class="Function">hfill</a> <a id="5252" href="Cubical.Foundations.Univalence.html#4802" class="Bound">u</a> <a id="5254" class="Symbol">(</a><a id="5255" href="Agda.Builtin.Cubical.Sub.html#223" class="Postulate">inS</a> <a id="5259" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a><a id="5260" class="Symbol">)</a> <a id="5262" href="Cubical.Foundations.Univalence.html#5149" class="Bound">j</a>
<a id="5286" class="Symbol">;</a> <a id="5288" class="Symbol">(</a><a id="5289" href="Cubical.Foundations.Univalence.html#5083" class="Bound">i</a> <a id="5291" class="Symbol">=</a> <a id="5293" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="5295" class="Symbol">)</a> <a id="5297" class="Symbol">→</a> <a id="5299" href="Cubical.Foundations.Univalence.html#5059" class="Bound">v</a> <a id="5301" class="Symbol">.</a><a id="5302" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="5306" class="Symbol">(</a><a id="5307" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="5309" href="Cubical.Foundations.Univalence.html#5149" class="Bound">j</a><a id="5310" class="Symbol">)</a> <a id="5312" class="Symbol">}</a>
<a id="5323" class="Keyword">in</a> <a id="5326" class="Symbol">(</a> <a id="5328" href="Agda.Builtin.Cubical.Glue.html#2169" class="Primitive">glue</a> <a id="5333" class="Symbol">(λ</a> <a id="5336" class="Symbol">{</a> <a id="5338" class="Symbol">(</a><a id="5339" href="Cubical.Foundations.Univalence.html#4777" class="Bound">φ</a> <a id="5341" class="Symbol">=</a> <a id="5343" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="5345" class="Symbol">)</a> <a id="5347" class="Symbol">→</a> <a id="5349" href="Cubical.Foundations.Equiv.html#995" class="Function">equivCtrPath</a> <a id="5362" class="Symbol">(</a><a id="5363" href="Cubical.Foundations.Univalence.html#4779" class="Bound">f</a> <a id="5365" href="Cubical.Core.Primitives.html#732" class="Postulate">1=1</a> <a id="5369" class="Symbol">.</a><a id="5370" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a><a id="5373" class="Symbol">)</a> <a id="5375" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a> <a id="5377" href="Cubical.Foundations.Univalence.html#5059" class="Bound">v</a> <a id="5379" href="Cubical.Foundations.Univalence.html#5083" class="Bound">i</a> <a id="5381" class="Symbol">.</a><a id="5382" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="5386" class="Symbol">})</a> <a id="5389" class="Symbol">(</a><a id="5390" href="Cubical.Core.Primitives.html#657" class="Primitive">hcomp</a> <a id="5396" href="Cubical.Foundations.Univalence.html#5100" class="Bound">u'</a> <a id="5399" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a><a id="5400" class="Symbol">)</a>
<a id="5414" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5416" class="Symbol">λ</a> <a id="5418" href="Cubical.Foundations.Univalence.html#5418" class="Bound">j</a> <a id="5420" class="Symbol">→</a> <a id="5422" href="Cubical.Core.Primitives.html#5145" class="Function">hfill</a> <a id="5428" href="Cubical.Foundations.Univalence.html#5100" class="Bound">u'</a> <a id="5431" class="Symbol">(</a><a id="5432" href="Agda.Builtin.Cubical.Sub.html#223" class="Postulate">inS</a> <a id="5436" href="Cubical.Foundations.Univalence.html#4787" class="Bound">b</a><a id="5437" class="Symbol">)</a> <a id="5439" class="Symbol">(</a><a id="5440" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="5442" href="Cubical.Foundations.Univalence.html#5418" class="Bound">j</a><a id="5443" class="Symbol">)))</a>
<a id="5448" class="Comment">-- Any partial family of equivalences can be extended to a total one</a>
<a id="5517" class="Comment">-- from Glue [ φ ↦ (T,f) ] A to A</a>
<a id="unglueEquiv"></a><a id="5551" href="Cubical.Foundations.Univalence.html#5551" class="Function">unglueEquiv</a> <a id="5563" class="Symbol">:</a> <a id="5565" class="Symbol">∀</a> <a id="5567" class="Symbol">(</a><a id="5568" href="Cubical.Foundations.Univalence.html#5568" class="Bound">A</a> <a id="5570" class="Symbol">:</a> <a id="5572" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5577" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="5578" class="Symbol">)</a> <a id="5580" class="Symbol">(</a><a id="5581" href="Cubical.Foundations.Univalence.html#5581" class="Bound">φ</a> <a id="5583" class="Symbol">:</a> <a id="5585" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="5586" class="Symbol">)</a>
<a id="5602" class="Symbol">(</a><a id="5603" href="Cubical.Foundations.Univalence.html#5603" class="Bound">f</a> <a id="5605" class="Symbol">:</a> <a id="5607" href="Agda.Primitive.Cubical.html#1106" class="Primitive">PartialP</a> <a id="5616" href="Cubical.Foundations.Univalence.html#5581" class="Bound">φ</a> <a id="5618" class="Symbol">(λ</a> <a id="5621" href="Cubical.Foundations.Univalence.html#5621" class="Bound">o</a> <a id="5623" class="Symbol">→</a> <a id="5625" href="Cubical.Core.Primitives.html#6306" class="Function">Σ[</a> <a id="5628" href="Cubical.Foundations.Univalence.html#5628" class="Bound">T</a> <a id="5630" href="Cubical.Core.Primitives.html#6306" class="Function">∈</a> <a id="5632" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5637" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a> <a id="5639" href="Cubical.Core.Primitives.html#6306" class="Function">]</a> <a id="5641" href="Cubical.Foundations.Univalence.html#5628" class="Bound">T</a> <a id="5643" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="5645" href="Cubical.Foundations.Univalence.html#5568" class="Bound">A</a><a id="5646" class="Symbol">))</a> <a id="5649" class="Symbol">→</a>
<a id="5665" class="Symbol">(</a><a id="5666" href="Cubical.Core.Glue.html#1521" class="Function">Glue</a> <a id="5671" href="Cubical.Foundations.Univalence.html#5568" class="Bound">A</a> <a id="5673" href="Cubical.Foundations.Univalence.html#5603" class="Bound">f</a><a id="5674" class="Symbol">)</a> <a id="5676" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="5678" href="Cubical.Foundations.Univalence.html#5568" class="Bound">A</a>
<a id="5680" href="Cubical.Foundations.Univalence.html#5551" class="Function">unglueEquiv</a> <a id="5692" href="Cubical.Foundations.Univalence.html#5692" class="Bound">A</a> <a id="5694" href="Cubical.Foundations.Univalence.html#5694" class="Bound">φ</a> <a id="5696" href="Cubical.Foundations.Univalence.html#5696" class="Bound">f</a> <a id="5698" class="Symbol">=</a> <a id="5700" class="Symbol">(</a> <a id="5702" href="Cubical.Core.Glue.html#1724" class="Function">unglue</a> <a id="5709" href="Cubical.Foundations.Univalence.html#5694" class="Bound">φ</a> <a id="5711" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5713" href="Cubical.Foundations.Univalence.html#4594" class="Function">unglueIsEquiv</a> <a id="5727" href="Cubical.Foundations.Univalence.html#5692" class="Bound">A</a> <a id="5729" href="Cubical.Foundations.Univalence.html#5694" class="Bound">φ</a> <a id="5731" href="Cubical.Foundations.Univalence.html#5696" class="Bound">f</a> <a id="5733" class="Symbol">)</a>
<a id="5737" class="Comment">-- The following is a formulation of univalence proposed by Martín Escardó:</a>
<a id="5813" class="Comment">-- https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ</a>
<a id="5898" class="Comment">-- See also Theorem 5.8.4 of the HoTT Book.</a>
<a id="5942" class="Comment">--</a>
<a id="5945" class="Comment">-- The reason we have this formulation in the core library and not the</a>
<a id="6016" class="Comment">-- standard one is that this one is more direct to prove using that</a>
<a id="6084" class="Comment">-- unglue is an equivalence. The standard formulation can be found in</a>
<a id="6154" class="Comment">-- Cubical/Basics/Univalence.</a>
<a id="6184" class="Comment">--</a>
<a id="EquivContr"></a><a id="6187" href="Cubical.Foundations.Univalence.html#6187" class="Function">EquivContr</a> <a id="6198" class="Symbol">:</a> <a id="6200" class="Symbol">∀</a> <a id="6202" class="Symbol">(</a><a id="6203" href="Cubical.Foundations.Univalence.html#6203" class="Bound">A</a> <a id="6205" class="Symbol">:</a> <a id="6207" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6212" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="6213" class="Symbol">)</a> <a id="6215" class="Symbol">→</a> <a id="6217" href="Cubical.Data.Sigma.Base.html#943" class="Function">∃![</a> <a id="6221" href="Cubical.Foundations.Univalence.html#6221" class="Bound">T</a> <a id="6223" href="Cubical.Data.Sigma.Base.html#943" class="Function">∈</a> <a id="6225" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6230" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a> <a id="6232" href="Cubical.Data.Sigma.Base.html#943" class="Function">]</a> <a id="6234" class="Symbol">(</a><a id="6235" href="Cubical.Foundations.Univalence.html#6221" class="Bound">T</a> <a id="6237" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="6239" href="Cubical.Foundations.Univalence.html#6203" class="Bound">A</a><a id="6240" class="Symbol">)</a>
<a id="6242" href="Cubical.Foundations.Univalence.html#6187" class="Function">EquivContr</a> <a id="6253" class="Symbol">{</a><a id="6254" class="Argument">ℓ</a> <a id="6256" class="Symbol">=</a> <a id="6258" href="Cubical.Foundations.Univalence.html#6258" class="Bound">ℓ</a><a id="6259" class="Symbol">}</a> <a id="6261" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a> <a id="6263" class="Symbol">=</a>
<a id="6267" class="Symbol">(</a> <a id="6269" class="Symbol">(</a><a id="6270" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a> <a id="6272" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6274" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="6282" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a><a id="6283" class="Symbol">)</a>
<a id="6287" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6289" href="Cubical.Foundations.Univalence.html#6309" class="Function">idEquiv≡</a> <a id="6298" class="Symbol">)</a>
<a id="6301" class="Keyword">where</a>
<a id="6309" href="Cubical.Foundations.Univalence.html#6309" class="Function">idEquiv≡</a> <a id="6318" class="Symbol">:</a> <a id="6320" class="Symbol">(</a><a id="6321" href="Cubical.Foundations.Univalence.html#6321" class="Bound">y</a> <a id="6323" class="Symbol">:</a> <a id="6325" href="Agda.Builtin.Sigma.html#166" class="Record">Σ</a> <a id="6327" class="Symbol">(</a><a id="6328" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6333" href="Cubical.Foundations.Univalence.html#6258" class="Bound">ℓ</a><a id="6334" class="Symbol">)</a> <a id="6336" class="Symbol">(λ</a> <a id="6339" href="Cubical.Foundations.Univalence.html#6339" class="Bound">T</a> <a id="6341" class="Symbol">→</a> <a id="6343" href="Cubical.Foundations.Univalence.html#6339" class="Bound">T</a> <a id="6345" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="6347" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a><a id="6348" class="Symbol">))</a> <a id="6351" class="Symbol">→</a> <a id="6353" class="Symbol">(</a><a id="6354" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a> <a id="6356" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6358" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="6366" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a><a id="6367" class="Symbol">)</a> <a id="6369" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="6371" href="Cubical.Foundations.Univalence.html#6321" class="Bound">y</a>
<a id="6375" href="Cubical.Foundations.Univalence.html#6309" class="Function">idEquiv≡</a> <a id="6384" href="Cubical.Foundations.Univalence.html#6384" class="Bound">w</a> <a id="6386" class="Symbol">=</a> <a id="6388" class="Symbol">\</a> <a id="6390" class="Symbol">{</a> <a id="6392" href="Cubical.Foundations.Univalence.html#6392" class="Bound">i</a> <a id="6394" class="Symbol">.</a><a id="6395" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="6417" class="Symbol">→</a> <a id="6419" href="Cubical.Core.Glue.html#1521" class="Function">Glue</a> <a id="6424" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a> <a id="6426" class="Symbol">(</a><a id="6427" href="Cubical.Foundations.Univalence.html#6626" class="Function">f</a> <a id="6429" href="Cubical.Foundations.Univalence.html#6392" class="Bound">i</a><a id="6430" class="Symbol">)</a>
<a id="6449" class="Symbol">;</a> <a id="6451" href="Cubical.Foundations.Univalence.html#6451" class="Bound">i</a> <a id="6453" class="Symbol">.</a><a id="6454" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="6458" class="Symbol">.</a><a id="6459" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="6476" class="Symbol">→</a> <a id="6478" href="Cubical.Foundations.Univalence.html#5551" class="Function">unglueEquiv</a> <a id="6490" class="Symbol">_</a> <a id="6492" class="Symbol">_</a> <a id="6494" class="Symbol">(</a><a id="6495" href="Cubical.Foundations.Univalence.html#6626" class="Function">f</a> <a id="6497" href="Cubical.Foundations.Univalence.html#6451" class="Bound">i</a><a id="6498" class="Symbol">)</a> <a id="6500" class="Symbol">.</a><a id="6501" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a>
<a id="6522" class="Symbol">;</a> <a id="6524" href="Cubical.Foundations.Univalence.html#6524" class="Bound">i</a> <a id="6526" class="Symbol">.</a><a id="6527" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="6531" class="Symbol">.</a><a id="6532" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="6536" class="Symbol">.</a><a id="6537" href="Agda.Builtin.Cubical.Glue.html#971" class="Field">equiv-proof</a> <a id="6549" class="Symbol">→</a> <a id="6551" href="Cubical.Foundations.Univalence.html#5551" class="Function">unglueEquiv</a> <a id="6563" class="Symbol">_</a> <a id="6565" class="Symbol">_</a> <a id="6567" class="Symbol">(</a><a id="6568" href="Cubical.Foundations.Univalence.html#6626" class="Function">f</a> <a id="6570" href="Cubical.Foundations.Univalence.html#6524" class="Bound">i</a><a id="6571" class="Symbol">)</a> <a id="6573" class="Symbol">.</a><a id="6574" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="6578" class="Symbol">.</a><a id="6579" href="Agda.Builtin.Cubical.Glue.html#971" class="Field">equiv-proof</a>
<a id="6608" class="Symbol">}</a>
<a id="6614" class="Keyword">where</a>
<a id="6626" href="Cubical.Foundations.Univalence.html#6626" class="Function">f</a> <a id="6628" class="Symbol">:</a> <a id="6630" class="Symbol">∀</a> <a id="6632" href="Cubical.Foundations.Univalence.html#6632" class="Bound">i</a> <a id="6634" class="Symbol">→</a> <a id="6636" href="Agda.Primitive.Cubical.html#1106" class="Primitive">PartialP</a> <a id="6645" class="Symbol">(</a><a id="6646" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="6648" href="Cubical.Foundations.Univalence.html#6632" class="Bound">i</a> <a id="6650" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="6652" href="Cubical.Foundations.Univalence.html#6632" class="Bound">i</a><a id="6653" class="Symbol">)</a> <a id="6655" class="Symbol">(λ</a> <a id="6658" href="Cubical.Foundations.Univalence.html#6658" class="Bound">x</a> <a id="6660" class="Symbol">→</a> <a id="6662" href="Cubical.Core.Primitives.html#6306" class="Function">Σ[</a> <a id="6665" href="Cubical.Foundations.Univalence.html#6665" class="Bound">T</a> <a id="6667" href="Cubical.Core.Primitives.html#6306" class="Function">∈</a> <a id="6669" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6674" href="Cubical.Foundations.Univalence.html#6258" class="Bound">ℓ</a> <a id="6676" href="Cubical.Core.Primitives.html#6306" class="Function">]</a> <a id="6678" href="Cubical.Foundations.Univalence.html#6665" class="Bound">T</a> <a id="6680" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="6682" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a><a id="6683" class="Symbol">)</a>
<a id="6691" href="Cubical.Foundations.Univalence.html#6626" class="Function">f</a> <a id="6693" href="Cubical.Foundations.Univalence.html#6693" class="Bound">i</a> <a id="6695" class="Symbol">=</a> <a id="6697" class="Symbol">λ</a> <a id="6699" class="Symbol">{</a> <a id="6701" class="Symbol">(</a><a id="6702" href="Cubical.Foundations.Univalence.html#6693" class="Bound">i</a> <a id="6704" class="Symbol">=</a> <a id="6706" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="6708" class="Symbol">)</a> <a id="6710" class="Symbol">→</a> <a id="6712" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a> <a id="6714" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6716" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="6724" href="Cubical.Foundations.Univalence.html#6261" class="Bound">A</a> <a id="6726" class="Symbol">;</a> <a id="6728" class="Symbol">(</a><a id="6729" href="Cubical.Foundations.Univalence.html#6693" class="Bound">i</a> <a id="6731" class="Symbol">=</a> <a id="6733" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="6735" class="Symbol">)</a> <a id="6737" class="Symbol">→</a> <a id="6739" href="Cubical.Foundations.Univalence.html#6384" class="Bound">w</a> <a id="6741" class="Symbol">}</a>
<a id="contrSinglEquiv"></a><a id="6744" href="Cubical.Foundations.Univalence.html#6744" class="Function">contrSinglEquiv</a> <a id="6760" class="Symbol">:</a> <a id="6762" class="Symbol">{</a><a id="6763" href="Cubical.Foundations.Univalence.html#6763" class="Bound">A</a> <a id="6765" href="Cubical.Foundations.Univalence.html#6765" class="Bound">B</a> <a id="6767" class="Symbol">:</a> <a id="6769" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6774" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="6775" class="Symbol">}</a> <a id="6777" class="Symbol">(</a><a id="6778" href="Cubical.Foundations.Univalence.html#6778" class="Bound">e</a> <a id="6780" class="Symbol">:</a> <a id="6782" href="Cubical.Foundations.Univalence.html#6763" class="Bound">A</a> <a id="6784" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="6786" href="Cubical.Foundations.Univalence.html#6765" class="Bound">B</a><a id="6787" class="Symbol">)</a> <a id="6789" class="Symbol">→</a> <a id="6791" class="Symbol">(</a><a id="6792" href="Cubical.Foundations.Univalence.html#6765" class="Bound">B</a> <a id="6794" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6796" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="6804" href="Cubical.Foundations.Univalence.html#6765" class="Bound">B</a><a id="6805" class="Symbol">)</a> <a id="6807" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="6809" class="Symbol">(</a><a id="6810" href="Cubical.Foundations.Univalence.html#6763" class="Bound">A</a> <a id="6812" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6814" href="Cubical.Foundations.Univalence.html#6778" class="Bound">e</a><a id="6815" class="Symbol">)</a>
<a id="6817" href="Cubical.Foundations.Univalence.html#6744" class="Function">contrSinglEquiv</a> <a id="6833" class="Symbol">{</a><a id="6834" class="Argument">A</a> <a id="6836" class="Symbol">=</a> <a id="6838" href="Cubical.Foundations.Univalence.html#6838" class="Bound">A</a><a id="6839" class="Symbol">}</a> <a id="6841" class="Symbol">{</a><a id="6842" class="Argument">B</a> <a id="6844" class="Symbol">=</a> <a id="6846" href="Cubical.Foundations.Univalence.html#6846" class="Bound">B</a><a id="6847" class="Symbol">}</a> <a id="6849" href="Cubical.Foundations.Univalence.html#6849" class="Bound">e</a> <a id="6851" class="Symbol">=</a>
<a id="6855" href="Cubical.Foundations.Prelude.html#18232" class="Function">isContr→isProp</a> <a id="6870" class="Symbol">(</a><a id="6871" href="Cubical.Foundations.Univalence.html#6187" class="Function">EquivContr</a> <a id="6882" href="Cubical.Foundations.Univalence.html#6846" class="Bound">B</a><a id="6883" class="Symbol">)</a> <a id="6885" class="Symbol">(</a><a id="6886" href="Cubical.Foundations.Univalence.html#6846" class="Bound">B</a> <a id="6888" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6890" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="6898" href="Cubical.Foundations.Univalence.html#6846" class="Bound">B</a><a id="6899" class="Symbol">)</a> <a id="6901" class="Symbol">(</a><a id="6902" href="Cubical.Foundations.Univalence.html#6838" class="Bound">A</a> <a id="6904" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6906" href="Cubical.Foundations.Univalence.html#6849" class="Bound">e</a><a id="6907" class="Symbol">)</a>
<a id="6910" class="Comment">-- Equivalence induction</a>
<a id="EquivJ"></a><a id="6935" href="Cubical.Foundations.Univalence.html#6935" class="Function">EquivJ</a> <a id="6942" class="Symbol">:</a> <a id="6944" class="Symbol">{</a><a id="6945" href="Cubical.Foundations.Univalence.html#6945" class="Bound">A</a> <a id="6947" href="Cubical.Foundations.Univalence.html#6947" class="Bound">B</a> <a id="6949" class="Symbol">:</a> <a id="6951" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6956" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="6957" class="Symbol">}</a> <a id="6959" class="Symbol">(</a><a id="6960" href="Cubical.Foundations.Univalence.html#6960" class="Bound">P</a> <a id="6962" class="Symbol">:</a> <a id="6964" class="Symbol">(</a><a id="6965" href="Cubical.Foundations.Univalence.html#6965" class="Bound">A</a> <a id="6967" class="Symbol">:</a> <a id="6969" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6974" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="6975" class="Symbol">)</a> <a id="6977" class="Symbol">→</a> <a id="6979" class="Symbol">(</a><a id="6980" href="Cubical.Foundations.Univalence.html#6980" class="Bound">e</a> <a id="6982" class="Symbol">:</a> <a id="6984" href="Cubical.Foundations.Univalence.html#6965" class="Bound">A</a> <a id="6986" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="6988" href="Cubical.Foundations.Univalence.html#6947" class="Bound">B</a><a id="6989" class="Symbol">)</a> <a id="6991" class="Symbol">→</a> <a id="6993" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6998" href="Cubical.Foundations.Univalence.html#897" class="Generalizable">ℓ'</a><a id="7000" class="Symbol">)</a>
<a id="7009" class="Symbol">→</a> <a id="7011" class="Symbol">(</a><a id="7012" href="Cubical.Foundations.Univalence.html#7012" class="Bound">r</a> <a id="7014" class="Symbol">:</a> <a id="7016" href="Cubical.Foundations.Univalence.html#6960" class="Bound">P</a> <a id="7018" href="Cubical.Foundations.Univalence.html#6947" class="Bound">B</a> <a id="7020" class="Symbol">(</a><a id="7021" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="7029" href="Cubical.Foundations.Univalence.html#6947" class="Bound">B</a><a id="7030" class="Symbol">))</a> <a id="7033" class="Symbol">→</a> <a id="7035" class="Symbol">(</a><a id="7036" href="Cubical.Foundations.Univalence.html#7036" class="Bound">e</a> <a id="7038" class="Symbol">:</a> <a id="7040" href="Cubical.Foundations.Univalence.html#6945" class="Bound">A</a> <a id="7042" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="7044" href="Cubical.Foundations.Univalence.html#6947" class="Bound">B</a><a id="7045" class="Symbol">)</a> <a id="7047" class="Symbol">→</a> <a id="7049" href="Cubical.Foundations.Univalence.html#6960" class="Bound">P</a> <a id="7051" href="Cubical.Foundations.Univalence.html#6945" class="Bound">A</a> <a id="7053" href="Cubical.Foundations.Univalence.html#7036" class="Bound">e</a>
<a id="7055" href="Cubical.Foundations.Univalence.html#6935" class="Function">EquivJ</a> <a id="7062" href="Cubical.Foundations.Univalence.html#7062" class="Bound">P</a> <a id="7064" href="Cubical.Foundations.Univalence.html#7064" class="Bound">r</a> <a id="7066" href="Cubical.Foundations.Univalence.html#7066" class="Bound">e</a> <a id="7068" class="Symbol">=</a> <a id="7070" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="7076" class="Symbol">(λ</a> <a id="7079" href="Cubical.Foundations.Univalence.html#7079" class="Bound">x</a> <a id="7081" class="Symbol">→</a> <a id="7083" href="Cubical.Foundations.Univalence.html#7062" class="Bound">P</a> <a id="7085" class="Symbol">(</a><a id="7086" href="Cubical.Foundations.Univalence.html#7079" class="Bound">x</a> <a id="7088" class="Symbol">.</a><a id="7089" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a><a id="7092" class="Symbol">)</a> <a id="7094" class="Symbol">(</a><a id="7095" href="Cubical.Foundations.Univalence.html#7079" class="Bound">x</a> <a id="7097" class="Symbol">.</a><a id="7098" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a><a id="7101" class="Symbol">))</a> <a id="7104" class="Symbol">(</a><a id="7105" href="Cubical.Foundations.Univalence.html#6744" class="Function">contrSinglEquiv</a> <a id="7121" href="Cubical.Foundations.Univalence.html#7066" class="Bound">e</a><a id="7122" class="Symbol">)</a> <a id="7124" href="Cubical.Foundations.Univalence.html#7064" class="Bound">r</a>
<a id="7127" class="Comment">-- Assuming that we have an inverse to ua we can easily prove univalence</a>
<a id="7200" class="Keyword">module</a> <a id="Univalence"></a><a id="7207" href="Cubical.Foundations.Univalence.html#7207" class="Module">Univalence</a> <a id="7218" class="Symbol">(</a><a id="7219" href="Cubical.Foundations.Univalence.html#7219" class="Bound">au</a> <a id="7222" class="Symbol">:</a> <a id="7224" class="Symbol">∀</a> <a id="7226" class="Symbol">{</a><a id="7227" href="Cubical.Foundations.Univalence.html#7227" class="Bound">ℓ</a><a id="7228" class="Symbol">}</a> <a id="7230" class="Symbol">{</a><a id="7231" href="Cubical.Foundations.Univalence.html#7231" class="Bound">A</a> <a id="7233" href="Cubical.Foundations.Univalence.html#7233" class="Bound">B</a> <a id="7235" class="Symbol">:</a> <a id="7237" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7242" href="Cubical.Foundations.Univalence.html#7227" class="Bound">ℓ</a><a id="7243" class="Symbol">}</a> <a id="7245" class="Symbol">→</a> <a id="7247" href="Cubical.Foundations.Univalence.html#7231" class="Bound">A</a> <a id="7249" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7251" href="Cubical.Foundations.Univalence.html#7233" class="Bound">B</a> <a id="7253" class="Symbol">→</a> <a id="7255" href="Cubical.Foundations.Univalence.html#7231" class="Bound">A</a> <a id="7257" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="7259" href="Cubical.Foundations.Univalence.html#7233" class="Bound">B</a><a id="7260" class="Symbol">)</a>
<a id="7280" class="Symbol">(</a><a id="7281" href="Cubical.Foundations.Univalence.html#7281" class="Bound">aurefl</a> <a id="7288" class="Symbol">:</a> <a id="7290" class="Symbol">∀</a> <a id="7292" class="Symbol">{</a><a id="7293" href="Cubical.Foundations.Univalence.html#7293" class="Bound">ℓ</a><a id="7294" class="Symbol">}</a> <a id="7296" class="Symbol">{</a><a id="7297" href="Cubical.Foundations.Univalence.html#7297" class="Bound">A</a> <a id="7299" class="Symbol">:</a> <a id="7301" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7306" href="Cubical.Foundations.Univalence.html#7293" class="Bound">ℓ</a><a id="7307" class="Symbol">}</a> <a id="7309" class="Symbol">→</a> <a id="7311" href="Cubical.Foundations.Univalence.html#7219" class="Bound">au</a> <a id="7314" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="7319" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7321" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="7329" href="Cubical.Foundations.Univalence.html#7297" class="Bound">A</a><a id="7330" class="Symbol">)</a> <a id="7332" class="Keyword">where</a>
<a id="Univalence.ua-au"></a><a id="7341" href="Cubical.Foundations.Univalence.html#7341" class="Function">ua-au</a> <a id="7347" class="Symbol">:</a> <a id="7349" class="Symbol">{</a><a id="7350" href="Cubical.Foundations.Univalence.html#7350" class="Bound">A</a> <a id="7352" href="Cubical.Foundations.Univalence.html#7352" class="Bound">B</a> <a id="7354" class="Symbol">:</a> <a id="7356" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7361" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="7362" class="Symbol">}</a> <a id="7364" class="Symbol">(</a><a id="7365" href="Cubical.Foundations.Univalence.html#7365" class="Bound">p</a> <a id="7367" class="Symbol">:</a> <a id="7369" href="Cubical.Foundations.Univalence.html#7350" class="Bound">A</a> <a id="7371" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7373" href="Cubical.Foundations.Univalence.html#7352" class="Bound">B</a><a id="7374" class="Symbol">)</a> <a id="7376" class="Symbol">→</a> <a id="7378" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="7381" class="Symbol">(</a><a id="7382" href="Cubical.Foundations.Univalence.html#7219" class="Bound">au</a> <a id="7385" href="Cubical.Foundations.Univalence.html#7365" class="Bound">p</a><a id="7386" class="Symbol">)</a> <a id="7388" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7390" href="Cubical.Foundations.Univalence.html#7365" class="Bound">p</a>
<a id="7394" href="Cubical.Foundations.Univalence.html#7341" class="Function">ua-au</a> <a id="7400" class="Symbol">{</a><a id="7401" class="Argument">B</a> <a id="7403" class="Symbol">=</a> <a id="7405" href="Cubical.Foundations.Univalence.html#7405" class="Bound">B</a><a id="7406" class="Symbol">}</a> <a id="7408" class="Symbol">=</a> <a id="7410" href="Cubical.Foundations.Prelude.html#11155" class="Function">J</a> <a id="7412" class="Symbol">(λ</a> <a id="7415" href="Cubical.Foundations.Univalence.html#7415" class="Bound">_</a> <a id="7417" href="Cubical.Foundations.Univalence.html#7417" class="Bound">p</a> <a id="7419" class="Symbol">→</a> <a id="7421" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="7424" class="Symbol">(</a><a id="7425" href="Cubical.Foundations.Univalence.html#7219" class="Bound">au</a> <a id="7428" href="Cubical.Foundations.Univalence.html#7417" class="Bound">p</a><a id="7429" class="Symbol">)</a> <a id="7431" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7433" href="Cubical.Foundations.Univalence.html#7417" class="Bound">p</a><a id="7434" class="Symbol">)</a>
<a id="7456" class="Symbol">(</a><a id="7457" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="7462" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="7465" href="Cubical.Foundations.Univalence.html#7281" class="Bound">aurefl</a> <a id="7472" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7474" href="Cubical.Foundations.Univalence.html#1090" class="Function">uaIdEquiv</a><a id="7483" class="Symbol">)</a>
<a id="Univalence.au-ua"></a><a id="7488" href="Cubical.Foundations.Univalence.html#7488" class="Function">au-ua</a> <a id="7494" class="Symbol">:</a> <a id="7496" class="Symbol">{</a><a id="7497" href="Cubical.Foundations.Univalence.html#7497" class="Bound">A</a> <a id="7499" href="Cubical.Foundations.Univalence.html#7499" class="Bound">B</a> <a id="7501" class="Symbol">:</a> <a id="7503" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7508" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="7509" class="Symbol">}</a> <a id="7511" class="Symbol">(</a><a id="7512" href="Cubical.Foundations.Univalence.html#7512" class="Bound">e</a> <a id="7514" class="Symbol">:</a> <a id="7516" href="Cubical.Foundations.Univalence.html#7497" class="Bound">A</a> <a id="7518" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="7520" href="Cubical.Foundations.Univalence.html#7499" class="Bound">B</a><a id="7521" class="Symbol">)</a> <a id="7523" class="Symbol">→</a> <a id="7525" href="Cubical.Foundations.Univalence.html#7219" class="Bound">au</a> <a id="7528" class="Symbol">(</a><a id="7529" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="7532" href="Cubical.Foundations.Univalence.html#7512" class="Bound">e</a><a id="7533" class="Symbol">)</a> <a id="7535" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7537" href="Cubical.Foundations.Univalence.html#7512" class="Bound">e</a>
<a id="7541" href="Cubical.Foundations.Univalence.html#7488" class="Function">au-ua</a> <a id="7547" class="Symbol">{</a><a id="7548" class="Argument">B</a> <a id="7550" class="Symbol">=</a> <a id="7552" href="Cubical.Foundations.Univalence.html#7552" class="Bound">B</a><a id="7553" class="Symbol">}</a> <a id="7555" class="Symbol">=</a> <a id="7557" href="Cubical.Foundations.Univalence.html#6935" class="Function">EquivJ</a> <a id="7564" class="Symbol">(λ</a> <a id="7567" href="Cubical.Foundations.Univalence.html#7567" class="Bound">_</a> <a id="7569" href="Cubical.Foundations.Univalence.html#7569" class="Bound">f</a> <a id="7571" class="Symbol">→</a> <a id="7573" href="Cubical.Foundations.Univalence.html#7219" class="Bound">au</a> <a id="7576" class="Symbol">(</a><a id="7577" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="7580" href="Cubical.Foundations.Univalence.html#7569" class="Bound">f</a><a id="7581" class="Symbol">)</a> <a id="7583" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7585" href="Cubical.Foundations.Univalence.html#7569" class="Bound">f</a><a id="7586" class="Symbol">)</a>
<a id="7613" class="Symbol">(</a><a id="7614" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="7620" class="Symbol">(λ</a> <a id="7623" href="Cubical.Foundations.Univalence.html#7623" class="Bound">r</a> <a id="7625" class="Symbol">→</a> <a id="7627" href="Cubical.Foundations.Univalence.html#7219" class="Bound">au</a> <a id="7630" href="Cubical.Foundations.Univalence.html#7623" class="Bound">r</a> <a id="7632" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7634" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="7642" class="Symbol">_)</a> <a id="7645" class="Symbol">(</a><a id="7646" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="7650" href="Cubical.Foundations.Univalence.html#1090" class="Function">uaIdEquiv</a><a id="7659" class="Symbol">)</a> <a id="7661" href="Cubical.Foundations.Univalence.html#7281" class="Bound">aurefl</a><a id="7667" class="Symbol">)</a>
<a id="Univalence.isoThm"></a><a id="7672" href="Cubical.Foundations.Univalence.html#7672" class="Function">isoThm</a> <a id="7679" class="Symbol">:</a> <a id="7681" class="Symbol">∀</a> <a id="7683" class="Symbol">{</a><a id="7684" href="Cubical.Foundations.Univalence.html#7684" class="Bound">ℓ</a><a id="7685" class="Symbol">}</a> <a id="7687" class="Symbol">{</a><a id="7688" href="Cubical.Foundations.Univalence.html#7688" class="Bound">A</a> <a id="7690" href="Cubical.Foundations.Univalence.html#7690" class="Bound">B</a> <a id="7692" class="Symbol">:</a> <a id="7694" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7699" href="Cubical.Foundations.Univalence.html#7684" class="Bound">ℓ</a><a id="7700" class="Symbol">}</a> <a id="7702" class="Symbol">→</a> <a id="7704" href="Cubical.Foundations.Isomorphism.html#773" class="Record">Iso</a> <a id="7708" class="Symbol">(</a><a id="7709" href="Cubical.Foundations.Univalence.html#7688" class="Bound">A</a> <a id="7711" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7713" href="Cubical.Foundations.Univalence.html#7690" class="Bound">B</a><a id="7714" class="Symbol">)</a> <a id="7716" class="Symbol">(</a><a id="7717" href="Cubical.Foundations.Univalence.html#7688" class="Bound">A</a> <a id="7719" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="7721" href="Cubical.Foundations.Univalence.html#7690" class="Bound">B</a><a id="7722" class="Symbol">)</a>
<a id="7726" href="Cubical.Foundations.Univalence.html#7672" class="Function">isoThm</a> <a id="7733" class="Symbol">.</a><a id="7734" href="Cubical.Foundations.Isomorphism.html#885" class="Field">Iso.fun</a> <a id="7742" class="Symbol">=</a> <a id="7744" href="Cubical.Foundations.Univalence.html#7219" class="Bound">au</a>
<a id="7749" href="Cubical.Foundations.Univalence.html#7672" class="Function">isoThm</a> <a id="7756" class="Symbol">.</a><a id="7757" href="Cubical.Foundations.Isomorphism.html#901" class="Field">Iso.inv</a> <a id="7765" class="Symbol">=</a> <a id="7767" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a>
<a id="7772" href="Cubical.Foundations.Univalence.html#7672" class="Function">isoThm</a> <a id="7779" class="Symbol">.</a><a id="7780" href="Cubical.Foundations.Isomorphism.html#917" class="Field">Iso.rightInv</a> <a id="7793" class="Symbol">=</a> <a id="7795" href="Cubical.Foundations.Univalence.html#7488" class="Function">au-ua</a>
<a id="7803" href="Cubical.Foundations.Univalence.html#7672" class="Function">isoThm</a> <a id="7810" class="Symbol">.</a><a id="7811" href="Cubical.Foundations.Isomorphism.html#948" class="Field">Iso.leftInv</a> <a id="7823" class="Symbol">=</a> <a id="7825" href="Cubical.Foundations.Univalence.html#7341" class="Function">ua-au</a>
<a id="Univalence.thm"></a><a id="7834" href="Cubical.Foundations.Univalence.html#7834" class="Function">thm</a> <a id="7838" class="Symbol">:</a> <a id="7840" class="Symbol">∀</a> <a id="7842" class="Symbol">{</a><a id="7843" href="Cubical.Foundations.Univalence.html#7843" class="Bound">ℓ</a><a id="7844" class="Symbol">}</a> <a id="7846" class="Symbol">{</a><a id="7847" href="Cubical.Foundations.Univalence.html#7847" class="Bound">A</a> <a id="7849" href="Cubical.Foundations.Univalence.html#7849" class="Bound">B</a> <a id="7851" class="Symbol">:</a> <a id="7853" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7858" href="Cubical.Foundations.Univalence.html#7843" class="Bound">ℓ</a><a id="7859" class="Symbol">}</a> <a id="7861" class="Symbol">→</a> <a id="7863" href="Agda.Builtin.Cubical.Glue.html#868" class="Record">isEquiv</a> <a id="7871" href="Cubical.Foundations.Univalence.html#7219" class="Bound">au</a>
<a id="7876" href="Cubical.Foundations.Univalence.html#7834" class="Function">thm</a> <a id="7880" class="Symbol">{</a><a id="7881" class="Argument">A</a> <a id="7883" class="Symbol">=</a> <a id="7885" href="Cubical.Foundations.Univalence.html#7885" class="Bound">A</a><a id="7886" class="Symbol">}</a> <a id="7888" class="Symbol">{</a><a id="7889" class="Argument">B</a> <a id="7891" class="Symbol">=</a> <a id="7893" href="Cubical.Foundations.Univalence.html#7893" class="Bound">B</a><a id="7894" class="Symbol">}</a> <a id="7896" class="Symbol">=</a> <a id="7898" href="Cubical.Foundations.Isomorphism.html#2932" class="Function">isoToIsEquiv</a> <a id="7911" class="Symbol">{</a><a id="7912" class="Argument">B</a> <a id="7914" class="Symbol">=</a> <a id="7916" href="Cubical.Foundations.Univalence.html#7885" class="Bound">A</a> <a id="7918" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="7920" href="Cubical.Foundations.Univalence.html#7893" class="Bound">B</a><a id="7921" class="Symbol">}</a> <a id="7923" href="Cubical.Foundations.Univalence.html#7672" class="Function">isoThm</a>
<a id="isEquivTransport"></a><a id="7931" href="Cubical.Foundations.Univalence.html#7931" class="Function">isEquivTransport</a> <a id="7948" class="Symbol">:</a> <a id="7950" class="Symbol">{</a><a id="7951" href="Cubical.Foundations.Univalence.html#7951" class="Bound">A</a> <a id="7953" href="Cubical.Foundations.Univalence.html#7953" class="Bound">B</a> <a id="7955" class="Symbol">:</a> <a id="7957" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7962" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="7963" class="Symbol">}</a> <a id="7965" class="Symbol">(</a><a id="7966" href="Cubical.Foundations.Univalence.html#7966" class="Bound">p</a> <a id="7968" class="Symbol">:</a> <a id="7970" href="Cubical.Foundations.Univalence.html#7951" class="Bound">A</a> <a id="7972" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7974" href="Cubical.Foundations.Univalence.html#7953" class="Bound">B</a><a id="7975" class="Symbol">)</a> <a id="7977" class="Symbol">→</a> <a id="7979" href="Agda.Builtin.Cubical.Glue.html#868" class="Record">isEquiv</a> <a id="7987" class="Symbol">(</a><a id="7988" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="7998" href="Cubical.Foundations.Univalence.html#7966" class="Bound">p</a><a id="7999" class="Symbol">)</a>
<a id="8001" href="Cubical.Foundations.Univalence.html#7931" class="Function">isEquivTransport</a> <a id="8018" href="Cubical.Foundations.Univalence.html#8018" class="Bound">p</a> <a id="8020" class="Symbol">=</a>
<a id="8024" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="8034" class="Symbol">(λ</a> <a id="8037" href="Cubical.Foundations.Univalence.html#8037" class="Bound">i</a> <a id="8039" class="Symbol">→</a> <a id="8041" href="Agda.Builtin.Cubical.Glue.html#868" class="Record">isEquiv</a> <a id="8049" class="Symbol">(</a><a id="8050" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="8057" class="Symbol">(λ</a> <a id="8060" href="Cubical.Foundations.Univalence.html#8060" class="Bound">j</a> <a id="8062" class="Symbol">→</a> <a id="8064" href="Cubical.Foundations.Univalence.html#8018" class="Bound">p</a> <a id="8066" class="Symbol">(</a><a id="8067" href="Cubical.Foundations.Univalence.html#8037" class="Bound">i</a> <a id="8069" href="Cubical.Core.Primitives.html#441" class="Primitive Operator">∧</a> <a id="8071" href="Cubical.Foundations.Univalence.html#8060" class="Bound">j</a><a id="8072" class="Symbol">))</a> <a id="8075" class="Symbol">(</a><a id="8076" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="8078" href="Cubical.Foundations.Univalence.html#8037" class="Bound">i</a><a id="8079" class="Symbol">)))</a> <a id="8083" class="Symbol">(</a><a id="8084" href="Cubical.Foundations.Equiv.Base.html#947" class="Function">idIsEquiv</a> <a id="8094" class="Symbol">_)</a>
<a id="pathToEquiv"></a><a id="8098" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8110" class="Symbol">:</a> <a id="8112" class="Symbol">{</a><a id="8113" href="Cubical.Foundations.Univalence.html#8113" class="Bound">A</a> <a id="8115" href="Cubical.Foundations.Univalence.html#8115" class="Bound">B</a> <a id="8117" class="Symbol">:</a> <a id="8119" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8124" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="8125" class="Symbol">}</a> <a id="8127" class="Symbol">→</a> <a id="8129" href="Cubical.Foundations.Univalence.html#8113" class="Bound">A</a> <a id="8131" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8133" href="Cubical.Foundations.Univalence.html#8115" class="Bound">B</a> <a id="8135" class="Symbol">→</a> <a id="8137" href="Cubical.Foundations.Univalence.html#8113" class="Bound">A</a> <a id="8139" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="8141" href="Cubical.Foundations.Univalence.html#8115" class="Bound">B</a>
<a id="8143" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8155" href="Cubical.Foundations.Univalence.html#8155" class="Bound">p</a> <a id="8157" class="Symbol">.</a><a id="8158" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="8162" class="Symbol">=</a> <a id="8164" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="8174" href="Cubical.Foundations.Univalence.html#8155" class="Bound">p</a>
<a id="8176" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8188" href="Cubical.Foundations.Univalence.html#8188" class="Bound">p</a> <a id="8190" class="Symbol">.</a><a id="8191" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="8195" class="Symbol">=</a> <a id="8197" href="Cubical.Foundations.Univalence.html#7931" class="Function">isEquivTransport</a> <a id="8214" href="Cubical.Foundations.Univalence.html#8188" class="Bound">p</a>
<a id="pathToEquivRefl"></a><a id="8217" href="Cubical.Foundations.Univalence.html#8217" class="Function">pathToEquivRefl</a> <a id="8233" class="Symbol">:</a> <a id="8235" class="Symbol">{</a><a id="8236" href="Cubical.Foundations.Univalence.html#8236" class="Bound">A</a> <a id="8238" class="Symbol">:</a> <a id="8240" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8245" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="8246" class="Symbol">}</a> <a id="8248" class="Symbol">→</a> <a id="8250" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8262" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="8267" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8269" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="8277" href="Cubical.Foundations.Univalence.html#8236" class="Bound">A</a>
<a id="8279" href="Cubical.Foundations.Univalence.html#8217" class="Function">pathToEquivRefl</a> <a id="8295" class="Symbol">{</a><a id="8296" class="Argument">A</a> <a id="8298" class="Symbol">=</a> <a id="8300" href="Cubical.Foundations.Univalence.html#8300" class="Bound">A</a><a id="8301" class="Symbol">}</a> <a id="8303" class="Symbol">=</a> <a id="8305" href="Cubical.Foundations.Equiv.html#1981" class="Function">equivEq</a> <a id="8313" class="Symbol">(λ</a> <a id="8316" href="Cubical.Foundations.Univalence.html#8316" class="Bound">i</a> <a id="8318" href="Cubical.Foundations.Univalence.html#8318" class="Bound">x</a> <a id="8320" class="Symbol">→</a> <a id="8322" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="8329" class="Symbol">(λ</a> <a id="8332" href="Cubical.Foundations.Univalence.html#8332" class="Bound">_</a> <a id="8334" class="Symbol">→</a> <a id="8336" href="Cubical.Foundations.Univalence.html#8300" class="Bound">A</a><a id="8337" class="Symbol">)</a> <a id="8339" href="Cubical.Foundations.Univalence.html#8316" class="Bound">i</a> <a id="8341" href="Cubical.Foundations.Univalence.html#8318" class="Bound">x</a><a id="8342" class="Symbol">)</a>
<a id="pathToEquiv-ua"></a><a id="8345" href="Cubical.Foundations.Univalence.html#8345" class="Function">pathToEquiv-ua</a> <a id="8360" class="Symbol">:</a> <a id="8362" class="Symbol">{</a><a id="8363" href="Cubical.Foundations.Univalence.html#8363" class="Bound">A</a> <a id="8365" href="Cubical.Foundations.Univalence.html#8365" class="Bound">B</a> <a id="8367" class="Symbol">:</a> <a id="8369" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8374" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="8375" class="Symbol">}</a> <a id="8377" class="Symbol">(</a><a id="8378" href="Cubical.Foundations.Univalence.html#8378" class="Bound">e</a> <a id="8380" class="Symbol">:</a> <a id="8382" href="Cubical.Foundations.Univalence.html#8363" class="Bound">A</a> <a id="8384" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="8386" href="Cubical.Foundations.Univalence.html#8365" class="Bound">B</a><a id="8387" class="Symbol">)</a> <a id="8389" class="Symbol">→</a> <a id="8391" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8403" class="Symbol">(</a><a id="8404" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="8407" href="Cubical.Foundations.Univalence.html#8378" class="Bound">e</a><a id="8408" class="Symbol">)</a> <a id="8410" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8412" href="Cubical.Foundations.Univalence.html#8378" class="Bound">e</a>
<a id="8414" href="Cubical.Foundations.Univalence.html#8345" class="Function">pathToEquiv-ua</a> <a id="8429" class="Symbol">=</a> <a id="8431" href="Cubical.Foundations.Univalence.html#7488" class="Function">Univalence.au-ua</a> <a id="8448" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8460" href="Cubical.Foundations.Univalence.html#8217" class="Function">pathToEquivRefl</a>
<a id="ua-pathToEquiv"></a><a id="8477" href="Cubical.Foundations.Univalence.html#8477" class="Function">ua-pathToEquiv</a> <a id="8492" class="Symbol">:</a> <a id="8494" class="Symbol">{</a><a id="8495" href="Cubical.Foundations.Univalence.html#8495" class="Bound">A</a> <a id="8497" href="Cubical.Foundations.Univalence.html#8497" class="Bound">B</a> <a id="8499" class="Symbol">:</a> <a id="8501" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8506" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="8507" class="Symbol">}</a> <a id="8509" class="Symbol">(</a><a id="8510" href="Cubical.Foundations.Univalence.html#8510" class="Bound">p</a> <a id="8512" class="Symbol">:</a> <a id="8514" href="Cubical.Foundations.Univalence.html#8495" class="Bound">A</a> <a id="8516" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8518" href="Cubical.Foundations.Univalence.html#8497" class="Bound">B</a><a id="8519" class="Symbol">)</a> <a id="8521" class="Symbol">→</a> <a id="8523" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="8526" class="Symbol">(</a><a id="8527" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8539" href="Cubical.Foundations.Univalence.html#8510" class="Bound">p</a><a id="8540" class="Symbol">)</a> <a id="8542" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8544" href="Cubical.Foundations.Univalence.html#8510" class="Bound">p</a>
<a id="8546" href="Cubical.Foundations.Univalence.html#8477" class="Function">ua-pathToEquiv</a> <a id="8561" class="Symbol">=</a> <a id="8563" href="Cubical.Foundations.Univalence.html#7341" class="Function">Univalence.ua-au</a> <a id="8580" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8592" href="Cubical.Foundations.Univalence.html#8217" class="Function">pathToEquivRefl</a>
<a id="8609" class="Comment">-- Univalence</a>
<a id="univalenceIso"></a><a id="8623" href="Cubical.Foundations.Univalence.html#8623" class="Function">univalenceIso</a> <a id="8637" class="Symbol">:</a> <a id="8639" class="Symbol">{</a><a id="8640" href="Cubical.Foundations.Univalence.html#8640" class="Bound">A</a> <a id="8642" href="Cubical.Foundations.Univalence.html#8642" class="Bound">B</a> <a id="8644" class="Symbol">:</a> <a id="8646" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8651" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="8652" class="Symbol">}</a> <a id="8654" class="Symbol">→</a> <a id="8656" href="Cubical.Foundations.Isomorphism.html#773" class="Record">Iso</a> <a id="8660" class="Symbol">(</a><a id="8661" href="Cubical.Foundations.Univalence.html#8640" class="Bound">A</a> <a id="8663" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8665" href="Cubical.Foundations.Univalence.html#8642" class="Bound">B</a><a id="8666" class="Symbol">)</a> <a id="8668" class="Symbol">(</a><a id="8669" href="Cubical.Foundations.Univalence.html#8640" class="Bound">A</a> <a id="8671" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="8673" href="Cubical.Foundations.Univalence.html#8642" class="Bound">B</a><a id="8674" class="Symbol">)</a>
<a id="8676" href="Cubical.Foundations.Univalence.html#8623" class="Function">univalenceIso</a> <a id="8690" class="Symbol">=</a> <a id="8692" href="Cubical.Foundations.Univalence.html#7672" class="Function">Univalence.isoThm</a> <a id="8710" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8722" href="Cubical.Foundations.Univalence.html#8217" class="Function">pathToEquivRefl</a>
<a id="univalence"></a><a id="8739" href="Cubical.Foundations.Univalence.html#8739" class="Function">univalence</a> <a id="8750" class="Symbol">:</a> <a id="8752" class="Symbol">{</a><a id="8753" href="Cubical.Foundations.Univalence.html#8753" class="Bound">A</a> <a id="8755" href="Cubical.Foundations.Univalence.html#8755" class="Bound">B</a> <a id="8757" class="Symbol">:</a> <a id="8759" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8764" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="8765" class="Symbol">}</a> <a id="8767" class="Symbol">→</a> <a id="8769" class="Symbol">(</a><a id="8770" href="Cubical.Foundations.Univalence.html#8753" class="Bound">A</a> <a id="8772" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8774" href="Cubical.Foundations.Univalence.html#8755" class="Bound">B</a><a id="8775" class="Symbol">)</a> <a id="8777" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="8779" class="Symbol">(</a><a id="8780" href="Cubical.Foundations.Univalence.html#8753" class="Bound">A</a> <a id="8782" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="8784" href="Cubical.Foundations.Univalence.html#8755" class="Bound">B</a><a id="8785" class="Symbol">)</a>
<a id="8787" href="Cubical.Foundations.Univalence.html#8739" class="Function">univalence</a> <a id="8798" class="Symbol">=</a> <a id="8800" class="Symbol">(</a> <a id="8802" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8814" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="8816" href="Cubical.Foundations.Univalence.html#7834" class="Function">Univalence.thm</a> <a id="8831" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="8843" href="Cubical.Foundations.Univalence.html#8217" class="Function">pathToEquivRefl</a> <a id="8860" class="Symbol">)</a>
<a id="8863" class="Comment">-- The original map from UniMath/Foundations</a>
<a id="eqweqmap"></a><a id="8908" href="Cubical.Foundations.Univalence.html#8908" class="Function">eqweqmap</a> <a id="8917" class="Symbol">:</a> <a id="8919" class="Symbol">{</a><a id="8920" href="Cubical.Foundations.Univalence.html#8920" class="Bound">A</a> <a id="8922" href="Cubical.Foundations.Univalence.html#8922" class="Bound">B</a> <a id="8924" class="Symbol">:</a> <a id="8926" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8931" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="8932" class="Symbol">}</a> <a id="8934" class="Symbol">→</a> <a id="8936" href="Cubical.Foundations.Univalence.html#8920" class="Bound">A</a> <a id="8938" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8940" href="Cubical.Foundations.Univalence.html#8922" class="Bound">B</a> <a id="8942" class="Symbol">→</a> <a id="8944" href="Cubical.Foundations.Univalence.html#8920" class="Bound">A</a> <a id="8946" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="8948" href="Cubical.Foundations.Univalence.html#8922" class="Bound">B</a>
<a id="8950" href="Cubical.Foundations.Univalence.html#8908" class="Function">eqweqmap</a> <a id="8959" class="Symbol">{</a><a id="8960" class="Argument">A</a> <a id="8962" class="Symbol">=</a> <a id="8964" href="Cubical.Foundations.Univalence.html#8964" class="Bound">A</a><a id="8965" class="Symbol">}</a> <a id="8967" href="Cubical.Foundations.Univalence.html#8967" class="Bound">e</a> <a id="8969" class="Symbol">=</a> <a id="8971" href="Cubical.Foundations.Prelude.html#11155" class="Function">J</a> <a id="8973" class="Symbol">(λ</a> <a id="8976" href="Cubical.Foundations.Univalence.html#8976" class="Bound">X</a> <a id="8978" href="Cubical.Foundations.Univalence.html#8978" class="Bound">_</a> <a id="8980" class="Symbol">→</a> <a id="8982" href="Cubical.Foundations.Univalence.html#8964" class="Bound">A</a> <a id="8984" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="8986" href="Cubical.Foundations.Univalence.html#8976" class="Bound">X</a><a id="8987" class="Symbol">)</a> <a id="8989" class="Symbol">(</a><a id="8990" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="8998" href="Cubical.Foundations.Univalence.html#8964" class="Bound">A</a><a id="8999" class="Symbol">)</a> <a id="9001" href="Cubical.Foundations.Univalence.html#8967" class="Bound">e</a>
<a id="eqweqmapid"></a><a id="9004" href="Cubical.Foundations.Univalence.html#9004" class="Function">eqweqmapid</a> <a id="9015" class="Symbol">:</a> <a id="9017" class="Symbol">{</a><a id="9018" href="Cubical.Foundations.Univalence.html#9018" class="Bound">A</a> <a id="9020" class="Symbol">:</a> <a id="9022" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="9027" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="9028" class="Symbol">}</a> <a id="9030" class="Symbol">→</a> <a id="9032" href="Cubical.Foundations.Univalence.html#8908" class="Function">eqweqmap</a> <a id="9041" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="9046" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="9048" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="9056" href="Cubical.Foundations.Univalence.html#9018" class="Bound">A</a>
<a id="9058" href="Cubical.Foundations.Univalence.html#9004" class="Function">eqweqmapid</a> <a id="9069" class="Symbol">{</a><a id="9070" class="Argument">A</a> <a id="9072" class="Symbol">=</a> <a id="9074" href="Cubical.Foundations.Univalence.html#9074" class="Bound">A</a><a id="9075" class="Symbol">}</a> <a id="9077" class="Symbol">=</a> <a id="9079" href="Cubical.Foundations.Prelude.html#11236" class="Function">JRefl</a> <a id="9085" class="Symbol">(λ</a> <a id="9088" href="Cubical.Foundations.Univalence.html#9088" class="Bound">X</a> <a id="9090" href="Cubical.Foundations.Univalence.html#9090" class="Bound">_</a> <a id="9092" class="Symbol">→</a> <a id="9094" href="Cubical.Foundations.Univalence.html#9074" class="Bound">A</a> <a id="9096" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="9098" href="Cubical.Foundations.Univalence.html#9088" class="Bound">X</a><a id="9099" class="Symbol">)</a> <a id="9101" class="Symbol">(</a><a id="9102" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="9110" href="Cubical.Foundations.Univalence.html#9074" class="Bound">A</a><a id="9111" class="Symbol">)</a>
<a id="univalenceStatement"></a><a id="9114" href="Cubical.Foundations.Univalence.html#9114" class="Function">univalenceStatement</a> <a id="9134" class="Symbol">:</a> <a id="9136" class="Symbol">{</a><a id="9137" href="Cubical.Foundations.Univalence.html#9137" class="Bound">A</a> <a id="9139" href="Cubical.Foundations.Univalence.html#9139" class="Bound">B</a> <a id="9141" class="Symbol">:</a> <a id="9143" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="9148" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="9149" class="Symbol">}</a> <a id="9151" class="Symbol">→</a> <a id="9153" href="Agda.Builtin.Cubical.Glue.html#868" class="Record">isEquiv</a> <a id="9161" class="Symbol">(</a><a id="9162" href="Cubical.Foundations.Univalence.html#8908" class="Function">eqweqmap</a> <a id="9171" class="Symbol">{</a><a id="9172" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="9173" class="Symbol">}</a> <a id="9175" class="Symbol">{</a><a id="9176" href="Cubical.Foundations.Univalence.html#9137" class="Bound">A</a><a id="9177" class="Symbol">}</a> <a id="9179" class="Symbol">{</a><a id="9180" href="Cubical.Foundations.Univalence.html#9139" class="Bound">B</a><a id="9181" class="Symbol">})</a>
<a id="9184" href="Cubical.Foundations.Univalence.html#9114" class="Function">univalenceStatement</a> <a id="9204" class="Symbol">=</a> <a id="9206" href="Cubical.Foundations.Univalence.html#7834" class="Function">Univalence.thm</a> <a id="9221" href="Cubical.Foundations.Univalence.html#8908" class="Function">eqweqmap</a> <a id="9230" href="Cubical.Foundations.Univalence.html#9004" class="Function">eqweqmapid</a>
<a id="univalenceUAH"></a><a id="9242" href="Cubical.Foundations.Univalence.html#9242" class="Function">univalenceUAH</a> <a id="9256" class="Symbol">:</a> <a id="9258" class="Symbol">{</a><a id="9259" href="Cubical.Foundations.Univalence.html#9259" class="Bound">A</a> <a id="9261" href="Cubical.Foundations.Univalence.html#9261" class="Bound">B</a> <a id="9263" class="Symbol">:</a> <a id="9265" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="9270" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="9271" class="Symbol">}</a> <a id="9273" class="Symbol">→</a> <a id="9275" class="Symbol">(</a><a id="9276" href="Cubical.Foundations.Univalence.html#9259" class="Bound">A</a> <a id="9278" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="9280" href="Cubical.Foundations.Univalence.html#9261" class="Bound">B</a><a id="9281" class="Symbol">)</a> <a id="9283" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="9285" class="Symbol">(</a><a id="9286" href="Cubical.Foundations.Univalence.html#9259" class="Bound">A</a> <a id="9288" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="9290" href="Cubical.Foundations.Univalence.html#9261" class="Bound">B</a><a id="9291" class="Symbol">)</a>
<a id="9293" href="Cubical.Foundations.Univalence.html#9242" class="Function">univalenceUAH</a> <a id="9307" class="Symbol">=</a> <a id="9309" class="Symbol">(</a> <a id="9311" class="Symbol">_</a> <a id="9313" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="9315" href="Cubical.Foundations.Univalence.html#9114" class="Function">univalenceStatement</a> <a id="9335" class="Symbol">)</a>
<a id="univalencePath"></a><a id="9338" href="Cubical.Foundations.Univalence.html#9338" class="Function">univalencePath</a> <a id="9353" class="Symbol">:</a> <a id="9355" class="Symbol">{</a><a id="9356" href="Cubical.Foundations.Univalence.html#9356" class="Bound">A</a> <a id="9358" href="Cubical.Foundations.Univalence.html#9358" class="Bound">B</a> <a id="9360" class="Symbol">:</a> <a id="9362" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="9367" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="9368" class="Symbol">}</a> <a id="9370" class="Symbol">→</a> <a id="9372" class="Symbol">(</a><a id="9373" href="Cubical.Foundations.Univalence.html#9356" class="Bound">A</a> <a id="9375" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="9377" href="Cubical.Foundations.Univalence.html#9358" class="Bound">B</a><a id="9378" class="Symbol">)</a> <a id="9380" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="9382" href="Cubical.Foundations.Prelude.html#19116" class="Record">Lift</a> <a id="9387" class="Symbol">(</a><a id="9388" href="Cubical.Foundations.Univalence.html#9356" class="Bound">A</a> <a id="9390" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="9392" href="Cubical.Foundations.Univalence.html#9358" class="Bound">B</a><a id="9393" class="Symbol">)</a>
<a id="9395" href="Cubical.Foundations.Univalence.html#9338" class="Function">univalencePath</a> <a id="9410" class="Symbol">=</a> <a id="9412" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="9415" class="Symbol">(</a><a id="9416" href="Cubical.Foundations.Equiv.html#3542" class="Function">compEquiv</a> <a id="9426" href="Cubical.Foundations.Univalence.html#8739" class="Function">univalence</a> <a id="9437" href="Cubical.Foundations.Equiv.html#5297" class="Function">LiftEquiv</a><a id="9446" class="Symbol">)</a>
<a id="9449" class="Comment">-- The computation rule for ua. Because of "ghcomp" it is now very</a>
<a id="9516" class="Comment">-- simple compared to cubicaltt:</a>
<a id="9549" class="Comment">-- https://github.com/mortberg/cubicaltt/blob/master/examples/univalence.ctt#L202</a>
<a id="uaβ"></a><a id="9631" href="Cubical.Foundations.Univalence.html#9631" class="Function">uaβ</a> <a id="9635" class="Symbol">:</a> <a id="9637" class="Symbol">{</a><a id="9638" href="Cubical.Foundations.Univalence.html#9638" class="Bound">A</a> <a id="9640" href="Cubical.Foundations.Univalence.html#9640" class="Bound">B</a> <a id="9642" class="Symbol">:</a> <a id="9644" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="9649" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="9650" class="Symbol">}</a> <a id="9652" class="Symbol">(</a><a id="9653" href="Cubical.Foundations.Univalence.html#9653" class="Bound">e</a> <a id="9655" class="Symbol">:</a> <a id="9657" href="Cubical.Foundations.Univalence.html#9638" class="Bound">A</a> <a id="9659" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="9661" href="Cubical.Foundations.Univalence.html#9640" class="Bound">B</a><a id="9662" class="Symbol">)</a> <a id="9664" class="Symbol">(</a><a id="9665" href="Cubical.Foundations.Univalence.html#9665" class="Bound">x</a> <a id="9667" class="Symbol">:</a> <a id="9669" href="Cubical.Foundations.Univalence.html#9638" class="Bound">A</a><a id="9670" class="Symbol">)</a> <a id="9672" class="Symbol">→</a> <a id="9674" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="9684" class="Symbol">(</a><a id="9685" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="9688" href="Cubical.Foundations.Univalence.html#9653" class="Bound">e</a><a id="9689" class="Symbol">)</a> <a id="9691" href="Cubical.Foundations.Univalence.html#9665" class="Bound">x</a> <a id="9693" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="9695" href="Agda.Builtin.Cubical.Glue.html#1143" class="Function">equivFun</a> <a id="9704" href="Cubical.Foundations.Univalence.html#9653" class="Bound">e</a> <a id="9706" href="Cubical.Foundations.Univalence.html#9665" class="Bound">x</a>
<a id="9708" href="Cubical.Foundations.Univalence.html#9631" class="Function">uaβ</a> <a id="9712" href="Cubical.Foundations.Univalence.html#9712" class="Bound">e</a> <a id="9714" href="Cubical.Foundations.Univalence.html#9714" class="Bound">x</a> <a id="9716" class="Symbol">=</a> <a id="9718" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="9732" class="Symbol">(</a><a id="9733" href="Agda.Builtin.Cubical.Glue.html#1143" class="Function">equivFun</a> <a id="9742" href="Cubical.Foundations.Univalence.html#9712" class="Bound">e</a> <a id="9744" href="Cubical.Foundations.Univalence.html#9714" class="Bound">x</a><a id="9745" class="Symbol">)</a>
<a id="uaη"></a><a id="9748" href="Cubical.Foundations.Univalence.html#9748" class="Function">uaη</a> <a id="9752" class="Symbol">:</a> <a id="9754" class="Symbol">∀</a> <a id="9756" class="Symbol">{</a><a id="9757" href="Cubical.Foundations.Univalence.html#9757" class="Bound">A</a> <a id="9759" href="Cubical.Foundations.Univalence.html#9759" class="Bound">B</a> <a id="9761" class="Symbol">:</a> <a id="9763" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="9768" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="9769" class="Symbol">}</a> <a id="9771" class="Symbol">→</a> <a id="9773" class="Symbol">(</a><a id="9774" href="Cubical.Foundations.Univalence.html#9774" class="Bound">P</a> <a id="9776" class="Symbol">:</a> <a id="9778" href="Cubical.Foundations.Univalence.html#9757" class="Bound">A</a> <a id="9780" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="9782" href="Cubical.Foundations.Univalence.html#9759" class="Bound">B</a><a id="9783" class="Symbol">)</a> <a id="9785" class="Symbol">→</a> <a id="9787" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="9790" class="Symbol">(</a><a id="9791" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="9803" href="Cubical.Foundations.Univalence.html#9774" class="Bound">P</a><a id="9804" class="Symbol">)</a> <a id="9806" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="9808" href="Cubical.Foundations.Univalence.html#9774" class="Bound">P</a>
<a id="9810" href="Cubical.Foundations.Univalence.html#9748" class="Function">uaη</a> <a id="9814" class="Symbol">=</a> <a id="9816" href="Cubical.Foundations.Prelude.html#11155" class="Function">J</a> <a id="9818" class="Symbol">(λ</a> <a id="9821" href="Cubical.Foundations.Univalence.html#9821" class="Bound">_</a> <a id="9823" href="Cubical.Foundations.Univalence.html#9823" class="Bound">q</a> <a id="9825" class="Symbol">→</a> <a id="9827" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="9830" class="Symbol">(</a><a id="9831" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="9843" href="Cubical.Foundations.Univalence.html#9823" class="Bound">q</a><a id="9844" class="Symbol">)</a> <a id="9846" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="9848" href="Cubical.Foundations.Univalence.html#9823" class="Bound">q</a><a id="9849" class="Symbol">)</a> <a id="9851" class="Symbol">(</a><a id="9852" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="9857" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="9860" href="Cubical.Foundations.Univalence.html#8217" class="Function">pathToEquivRefl</a> <a id="9876" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="9878" href="Cubical.Foundations.Univalence.html#1090" class="Function">uaIdEquiv</a><a id="9887" class="Symbol">)</a>
<a id="9890" class="Comment">-- Lemmas for constructing and destructing dependent paths in a function type where the domain is ua.</a>
<a id="ua→"></a><a id="9992" href="Cubical.Foundations.Univalence.html#9992" class="Function">ua→</a> <a id="9996" class="Symbol">:</a> <a id="9998" class="Symbol">∀</a> <a id="10000" class="Symbol">{</a><a id="10001" href="Cubical.Foundations.Univalence.html#10001" class="Bound">ℓ</a> <a id="10003" href="Cubical.Foundations.Univalence.html#10003" class="Bound">ℓ'</a><a id="10005" class="Symbol">}</a> <a id="10007" class="Symbol">{</a><a id="10008" href="Cubical.Foundations.Univalence.html#10008" class="Bound">A₀</a> <a id="10011" href="Cubical.Foundations.Univalence.html#10011" class="Bound">A₁</a> <a id="10014" class="Symbol">:</a> <a id="10016" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="10021" href="Cubical.Foundations.Univalence.html#10001" class="Bound">ℓ</a><a id="10022" class="Symbol">}</a> <a id="10024" class="Symbol">{</a><a id="10025" href="Cubical.Foundations.Univalence.html#10025" class="Bound">e</a> <a id="10027" class="Symbol">:</a> <a id="10029" href="Cubical.Foundations.Univalence.html#10008" class="Bound">A₀</a> <a id="10032" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="10034" href="Cubical.Foundations.Univalence.html#10011" class="Bound">A₁</a><a id="10036" class="Symbol">}</a> <a id="10038" class="Symbol">{</a><a id="10039" href="Cubical.Foundations.Univalence.html#10039" class="Bound">B</a> <a id="10041" class="Symbol">:</a> <a id="10043" class="Symbol">(</a><a id="10044" href="Cubical.Foundations.Univalence.html#10044" class="Bound">i</a> <a id="10046" class="Symbol">:</a> <a id="10048" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="10049" class="Symbol">)</a> <a id="10051" class="Symbol">→</a> <a id="10053" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="10058" href="Cubical.Foundations.Univalence.html#10003" class="Bound">ℓ'</a><a id="10060" class="Symbol">}</a>
<a id="10064" class="Symbol">{</a><a id="10065" href="Cubical.Foundations.Univalence.html#10065" class="Bound">f₀</a> <a id="10068" class="Symbol">:</a> <a id="10070" href="Cubical.Foundations.Univalence.html#10008" class="Bound">A₀</a> <a id="10073" class="Symbol">→</a> <a id="10075" href="Cubical.Foundations.Univalence.html#10039" class="Bound">B</a> <a id="10077" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="10079" class="Symbol">}</a> <a id="10081" class="Symbol">{</a><a id="10082" href="Cubical.Foundations.Univalence.html#10082" class="Bound">f₁</a> <a id="10085" class="Symbol">:</a> <a id="10087" href="Cubical.Foundations.Univalence.html#10011" class="Bound">A₁</a> <a id="10090" class="Symbol">→</a> <a id="10092" href="Cubical.Foundations.Univalence.html#10039" class="Bound">B</a> <a id="10094" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="10096" class="Symbol">}</a>
<a id="10100" class="Symbol">→</a> <a id="10102" class="Symbol">((</a><a id="10104" href="Cubical.Foundations.Univalence.html#10104" class="Bound">a</a> <a id="10106" class="Symbol">:</a> <a id="10108" href="Cubical.Foundations.Univalence.html#10008" class="Bound">A₀</a><a id="10110" class="Symbol">)</a> <a id="10112" class="Symbol">→</a> <a id="10114" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="10120" href="Cubical.Foundations.Univalence.html#10039" class="Bound">B</a> <a id="10122" class="Symbol">(</a><a id="10123" href="Cubical.Foundations.Univalence.html#10065" class="Bound">f₀</a> <a id="10126" href="Cubical.Foundations.Univalence.html#10104" class="Bound">a</a><a id="10127" class="Symbol">)</a> <a id="10129" class="Symbol">(</a><a id="10130" href="Cubical.Foundations.Univalence.html#10082" class="Bound">f₁</a> <a id="10133" class="Symbol">(</a><a id="10134" href="Cubical.Foundations.Univalence.html#10025" class="Bound">e</a> <a id="10136" class="Symbol">.</a><a id="10137" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="10141" href="Cubical.Foundations.Univalence.html#10104" class="Bound">a</a><a id="10142" class="Symbol">)))</a>
<a id="10148" class="Symbol">→</a> <a id="10150" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="10156" class="Symbol">(λ</a> <a id="10159" href="Cubical.Foundations.Univalence.html#10159" class="Bound">i</a> <a id="10161" class="Symbol">→</a> <a id="10163" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="10166" href="Cubical.Foundations.Univalence.html#10025" class="Bound">e</a> <a id="10168" href="Cubical.Foundations.Univalence.html#10159" class="Bound">i</a> <a id="10170" class="Symbol">→</a> <a id="10172" href="Cubical.Foundations.Univalence.html#10039" class="Bound">B</a> <a id="10174" href="Cubical.Foundations.Univalence.html#10159" class="Bound">i</a><a id="10175" class="Symbol">)</a> <a id="10177" href="Cubical.Foundations.Univalence.html#10065" class="Bound">f₀</a> <a id="10180" href="Cubical.Foundations.Univalence.html#10082" class="Bound">f₁</a>
<a id="10183" href="Cubical.Foundations.Univalence.html#9992" class="Function">ua→</a> <a id="10187" class="Symbol">{</a><a id="10188" class="Argument">e</a> <a id="10190" class="Symbol">=</a> <a id="10192" href="Cubical.Foundations.Univalence.html#10192" class="Bound">e</a><a id="10193" class="Symbol">}</a> <a id="10195" class="Symbol">{</a><a id="10196" class="Argument">f₀</a> <a id="10199" class="Symbol">=</a> <a id="10201" href="Cubical.Foundations.Univalence.html#10201" class="Bound">f₀</a><a id="10203" class="Symbol">}</a> <a id="10205" class="Symbol">{</a><a id="10206" href="Cubical.Foundations.Univalence.html#10206" class="Bound">f₁</a><a id="10208" class="Symbol">}</a> <a id="10210" href="Cubical.Foundations.Univalence.html#10210" class="Bound">h</a> <a id="10212" href="Cubical.Foundations.Univalence.html#10212" class="Bound">i</a> <a id="10214" href="Cubical.Foundations.Univalence.html#10214" class="Bound">a</a> <a id="10216" class="Symbol">=</a>
<a id="10220" href="Cubical.Core.Primitives.html#657" class="Primitive">hcomp</a>
<a id="10230" class="Symbol">(λ</a> <a id="10233" href="Cubical.Foundations.Univalence.html#10233" class="Bound">j</a> <a id="10235" class="Symbol">→</a> <a id="10237" class="Symbol">λ</a>
<a id="10245" class="Symbol">{</a> <a id="10247" class="Symbol">(</a><a id="10248" href="Cubical.Foundations.Univalence.html#10212" class="Bound">i</a> <a id="10250" class="Symbol">=</a> <a id="10252" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="10254" class="Symbol">)</a> <a id="10256" class="Symbol">→</a> <a id="10258" href="Cubical.Foundations.Univalence.html#10201" class="Bound">f₀</a> <a id="10261" href="Cubical.Foundations.Univalence.html#10214" class="Bound">a</a>
<a id="10269" class="Symbol">;</a> <a id="10271" class="Symbol">(</a><a id="10272" href="Cubical.Foundations.Univalence.html#10212" class="Bound">i</a> <a id="10274" class="Symbol">=</a> <a id="10276" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="10278" class="Symbol">)</a> <a id="10280" class="Symbol">→</a> <a id="10282" href="Cubical.Foundations.Univalence.html#10206" class="Bound">f₁</a> <a id="10285" class="Symbol">(</a><a id="10286" href="Cubical.Foundations.Univalence.html#10364" class="Function">lem</a> <a id="10290" href="Cubical.Foundations.Univalence.html#10214" class="Bound">a</a> <a id="10292" href="Cubical.Foundations.Univalence.html#10233" class="Bound">j</a><a id="10293" class="Symbol">)</a>
<a id="10301" class="Symbol">})</a>
<a id="10308" class="Symbol">(</a><a id="10309" href="Cubical.Foundations.Univalence.html#10210" class="Bound">h</a> <a id="10311" class="Symbol">(</a><a id="10312" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="10319" class="Symbol">(λ</a> <a id="10322" href="Cubical.Foundations.Univalence.html#10322" class="Bound">j</a> <a id="10324" class="Symbol">→</a> <a id="10326" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="10329" href="Cubical.Foundations.Univalence.html#10192" class="Bound">e</a> <a id="10331" class="Symbol">(</a><a id="10332" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="10334" href="Cubical.Foundations.Univalence.html#10322" class="Bound">j</a> <a id="10336" href="Cubical.Core.Primitives.html#441" class="Primitive Operator">∧</a> <a id="10338" href="Cubical.Foundations.Univalence.html#10212" class="Bound">i</a><a id="10339" class="Symbol">))</a> <a id="10342" class="Symbol">(</a><a id="10343" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="10345" href="Cubical.Foundations.Univalence.html#10212" class="Bound">i</a><a id="10346" class="Symbol">)</a> <a id="10348" href="Cubical.Foundations.Univalence.html#10214" class="Bound">a</a><a id="10349" class="Symbol">)</a> <a id="10351" href="Cubical.Foundations.Univalence.html#10212" class="Bound">i</a><a id="10352" class="Symbol">)</a>
<a id="10356" class="Keyword">where</a>
<a id="10364" href="Cubical.Foundations.Univalence.html#10364" class="Function">lem</a> <a id="10368" class="Symbol">:</a> <a id="10370" class="Symbol">∀</a> <a id="10372" href="Cubical.Foundations.Univalence.html#10372" class="Bound">a₁</a> <a id="10375" class="Symbol">→</a> <a id="10377" href="Cubical.Foundations.Univalence.html#10192" class="Bound">e</a> <a id="10379" class="Symbol">.</a><a id="10380" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="10384" class="Symbol">(</a><a id="10385" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="10395" class="Symbol">(</a><a id="10396" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="10400" class="Symbol">(</a><a id="10401" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="10404" href="Cubical.Foundations.Univalence.html#10192" class="Bound">e</a><a id="10405" class="Symbol">))</a> <a id="10408" href="Cubical.Foundations.Univalence.html#10372" class="Bound">a₁</a><a id="10410" class="Symbol">)</a> <a id="10412" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="10414" href="Cubical.Foundations.Univalence.html#10372" class="Bound">a₁</a>
<a id="10419" href="Cubical.Foundations.Univalence.html#10364" class="Function">lem</a> <a id="10423" href="Cubical.Foundations.Univalence.html#10423" class="Bound">a₁</a> <a id="10426" class="Symbol">=</a> <a id="10428" href="Cubical.Foundations.Equiv.html#3031" class="Function">secEq</a> <a id="10434" href="Cubical.Foundations.Univalence.html#10192" class="Bound">e</a> <a id="10436" class="Symbol">_</a> <a id="10438" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="10440" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="10454" class="Symbol">_</a>
<a id="ua→⁻"></a><a id="10457" href="Cubical.Foundations.Univalence.html#10457" class="Function">ua→⁻</a> <a id="10462" class="Symbol">:</a> <a id="10464" class="Symbol">∀</a> <a id="10466" class="Symbol">{</a><a id="10467" href="Cubical.Foundations.Univalence.html#10467" class="Bound">ℓ</a> <a id="10469" href="Cubical.Foundations.Univalence.html#10469" class="Bound">ℓ'</a><a id="10471" class="Symbol">}</a> <a id="10473" class="Symbol">{</a><a id="10474" href="Cubical.Foundations.Univalence.html#10474" class="Bound">A₀</a> <a id="10477" href="Cubical.Foundations.Univalence.html#10477" class="Bound">A₁</a> <a id="10480" class="Symbol">:</a> <a id="10482" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="10487" href="Cubical.Foundations.Univalence.html#10467" class="Bound">ℓ</a><a id="10488" class="Symbol">}</a> <a id="10490" class="Symbol">{</a><a id="10491" href="Cubical.Foundations.Univalence.html#10491" class="Bound">e</a> <a id="10493" class="Symbol">:</a> <a id="10495" href="Cubical.Foundations.Univalence.html#10474" class="Bound">A₀</a> <a id="10498" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="10500" href="Cubical.Foundations.Univalence.html#10477" class="Bound">A₁</a><a id="10502" class="Symbol">}</a> <a id="10504" class="Symbol">{</a><a id="10505" href="Cubical.Foundations.Univalence.html#10505" class="Bound">B</a> <a id="10507" class="Symbol">:</a> <a id="10509" class="Symbol">(</a><a id="10510" href="Cubical.Foundations.Univalence.html#10510" class="Bound">i</a> <a id="10512" class="Symbol">:</a> <a id="10514" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="10515" class="Symbol">)</a> <a id="10517" class="Symbol">→</a> <a id="10519" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="10524" href="Cubical.Foundations.Univalence.html#10469" class="Bound">ℓ'</a><a id="10526" class="Symbol">}</a>
<a id="10530" class="Symbol">{</a><a id="10531" href="Cubical.Foundations.Univalence.html#10531" class="Bound">f₀</a> <a id="10534" class="Symbol">:</a> <a id="10536" href="Cubical.Foundations.Univalence.html#10474" class="Bound">A₀</a> <a id="10539" class="Symbol">→</a> <a id="10541" href="Cubical.Foundations.Univalence.html#10505" class="Bound">B</a> <a id="10543" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="10545" class="Symbol">}</a> <a id="10547" class="Symbol">{</a><a id="10548" href="Cubical.Foundations.Univalence.html#10548" class="Bound">f₁</a> <a id="10551" class="Symbol">:</a> <a id="10553" href="Cubical.Foundations.Univalence.html#10477" class="Bound">A₁</a> <a id="10556" class="Symbol">→</a> <a id="10558" href="Cubical.Foundations.Univalence.html#10505" class="Bound">B</a> <a id="10560" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="10562" class="Symbol">}</a>
<a id="10566" class="Symbol">→</a> <a id="10568" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="10574" class="Symbol">(λ</a> <a id="10577" href="Cubical.Foundations.Univalence.html#10577" class="Bound">i</a> <a id="10579" class="Symbol">→</a> <a id="10581" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="10584" href="Cubical.Foundations.Univalence.html#10491" class="Bound">e</a> <a id="10586" href="Cubical.Foundations.Univalence.html#10577" class="Bound">i</a> <a id="10588" class="Symbol">→</a> <a id="10590" href="Cubical.Foundations.Univalence.html#10505" class="Bound">B</a> <a id="10592" href="Cubical.Foundations.Univalence.html#10577" class="Bound">i</a><a id="10593" class="Symbol">)</a> <a id="10595" href="Cubical.Foundations.Univalence.html#10531" class="Bound">f₀</a> <a id="10598" href="Cubical.Foundations.Univalence.html#10548" class="Bound">f₁</a>
<a id="10603" class="Symbol">→</a> <a id="10605" class="Symbol">((</a><a id="10607" href="Cubical.Foundations.Univalence.html#10607" class="Bound">a</a> <a id="10609" class="Symbol">:</a> <a id="10611" href="Cubical.Foundations.Univalence.html#10474" class="Bound">A₀</a><a id="10613" class="Symbol">)</a> <a id="10615" class="Symbol">→</a> <a id="10617" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="10623" href="Cubical.Foundations.Univalence.html#10505" class="Bound">B</a> <a id="10625" class="Symbol">(</a><a id="10626" href="Cubical.Foundations.Univalence.html#10531" class="Bound">f₀</a> <a id="10629" href="Cubical.Foundations.Univalence.html#10607" class="Bound">a</a><a id="10630" class="Symbol">)</a> <a id="10632" class="Symbol">(</a><a id="10633" href="Cubical.Foundations.Univalence.html#10548" class="Bound">f₁</a> <a id="10636" class="Symbol">(</a><a id="10637" href="Cubical.Foundations.Univalence.html#10491" class="Bound">e</a> <a id="10639" class="Symbol">.</a><a id="10640" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="10644" href="Cubical.Foundations.Univalence.html#10607" class="Bound">a</a><a id="10645" class="Symbol">)))</a>
<a id="10649" href="Cubical.Foundations.Univalence.html#10457" class="Function">ua→⁻</a> <a id="10654" class="Symbol">{</a><a id="10655" class="Argument">e</a> <a id="10657" class="Symbol">=</a> <a id="10659" href="Cubical.Foundations.Univalence.html#10659" class="Bound">e</a><a id="10660" class="Symbol">}</a> <a id="10662" class="Symbol">{</a><a id="10663" class="Argument">f₀</a> <a id="10666" class="Symbol">=</a> <a id="10668" href="Cubical.Foundations.Univalence.html#10668" class="Bound">f₀</a><a id="10670" class="Symbol">}</a> <a id="10672" class="Symbol">{</a><a id="10673" href="Cubical.Foundations.Univalence.html#10673" class="Bound">f₁</a><a id="10675" class="Symbol">}</a> <a id="10677" href="Cubical.Foundations.Univalence.html#10677" class="Bound">p</a> <a id="10679" href="Cubical.Foundations.Univalence.html#10679" class="Bound">a</a> <a id="10681" href="Cubical.Foundations.Univalence.html#10681" class="Bound">i</a> <a id="10683" class="Symbol">=</a>
<a id="10687" href="Cubical.Core.Primitives.html#657" class="Primitive">hcomp</a>
<a id="10697" class="Symbol">(λ</a> <a id="10700" href="Cubical.Foundations.Univalence.html#10700" class="Bound">k</a> <a id="10702" class="Symbol">→</a> <a id="10704" class="Symbol">λ</a>
<a id="10712" class="Symbol">{</a> <a id="10714" class="Symbol">(</a><a id="10715" href="Cubical.Foundations.Univalence.html#10681" class="Bound">i</a> <a id="10717" class="Symbol">=</a> <a id="10719" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="10721" class="Symbol">)</a> <a id="10723" class="Symbol">→</a> <a id="10725" href="Cubical.Foundations.Univalence.html#10668" class="Bound">f₀</a> <a id="10728" href="Cubical.Foundations.Univalence.html#10679" class="Bound">a</a>
<a id="10736" class="Symbol">;</a> <a id="10738" class="Symbol">(</a><a id="10739" href="Cubical.Foundations.Univalence.html#10681" class="Bound">i</a> <a id="10741" class="Symbol">=</a> <a id="10743" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="10745" class="Symbol">)</a> <a id="10747" class="Symbol">→</a> <a id="10749" href="Cubical.Foundations.Univalence.html#10673" class="Bound">f₁</a> <a id="10752" class="Symbol">(</a><a id="10753" href="Cubical.Foundations.Univalence.html#9631" class="Function">uaβ</a> <a id="10757" href="Cubical.Foundations.Univalence.html#10659" class="Bound">e</a> <a id="10759" href="Cubical.Foundations.Univalence.html#10679" class="Bound">a</a> <a id="10761" href="Cubical.Foundations.Univalence.html#10700" class="Bound">k</a><a id="10762" class="Symbol">)</a>
<a id="10770" class="Symbol">})</a>
<a id="10777" class="Symbol">(</a><a id="10778" href="Cubical.Foundations.Univalence.html#10677" class="Bound">p</a> <a id="10780" href="Cubical.Foundations.Univalence.html#10681" class="Bound">i</a> <a id="10782" class="Symbol">(</a><a id="10783" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="10790" class="Symbol">(λ</a> <a id="10793" href="Cubical.Foundations.Univalence.html#10793" class="Bound">j</a> <a id="10795" class="Symbol">→</a> <a id="10797" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="10800" href="Cubical.Foundations.Univalence.html#10659" class="Bound">e</a> <a id="10802" class="Symbol">(</a><a id="10803" href="Cubical.Foundations.Univalence.html#10793" class="Bound">j</a> <a id="10805" href="Cubical.Core.Primitives.html#441" class="Primitive Operator">∧</a> <a id="10807" href="Cubical.Foundations.Univalence.html#10681" class="Bound">i</a><a id="10808" class="Symbol">))</a> <a id="10811" class="Symbol">(</a><a id="10812" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="10814" href="Cubical.Foundations.Univalence.html#10681" class="Bound">i</a><a id="10815" class="Symbol">)</a> <a id="10817" href="Cubical.Foundations.Univalence.html#10679" class="Bound">a</a><a id="10818" class="Symbol">))</a>
<a id="ua→2"></a><a id="10822" href="Cubical.Foundations.Univalence.html#10822" class="Function">ua→2</a> <a id="10827" class="Symbol">:</a> <a id="10829" class="Symbol">∀</a> <a id="10831" class="Symbol">{</a><a id="10832" href="Cubical.Foundations.Univalence.html#10832" class="Bound">ℓ</a> <a id="10834" href="Cubical.Foundations.Univalence.html#10834" class="Bound">ℓ'</a> <a id="10837" href="Cubical.Foundations.Univalence.html#10837" class="Bound">ℓ''</a><a id="10840" class="Symbol">}</a> <a id="10842" class="Symbol">{</a><a id="10843" href="Cubical.Foundations.Univalence.html#10843" class="Bound">A₀</a> <a id="10846" href="Cubical.Foundations.Univalence.html#10846" class="Bound">A₁</a> <a id="10849" class="Symbol">:</a> <a id="10851" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="10856" href="Cubical.Foundations.Univalence.html#10832" class="Bound">ℓ</a><a id="10857" class="Symbol">}</a> <a id="10859" class="Symbol">{</a><a id="10860" href="Cubical.Foundations.Univalence.html#10860" class="Bound">e₁</a> <a id="10863" class="Symbol">:</a> <a id="10865" href="Cubical.Foundations.Univalence.html#10843" class="Bound">A₀</a> <a id="10868" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="10870" href="Cubical.Foundations.Univalence.html#10846" class="Bound">A₁</a><a id="10872" class="Symbol">}</a>
<a id="10876" class="Symbol">{</a><a id="10877" href="Cubical.Foundations.Univalence.html#10877" class="Bound">B₀</a> <a id="10880" href="Cubical.Foundations.Univalence.html#10880" class="Bound">B₁</a> <a id="10883" class="Symbol">:</a> <a id="10885" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="10890" href="Cubical.Foundations.Univalence.html#10834" class="Bound">ℓ'</a><a id="10892" class="Symbol">}</a> <a id="10894" class="Symbol">{</a><a id="10895" href="Cubical.Foundations.Univalence.html#10895" class="Bound">e₂</a> <a id="10898" class="Symbol">:</a> <a id="10900" href="Cubical.Foundations.Univalence.html#10877" class="Bound">B₀</a> <a id="10903" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="10905" href="Cubical.Foundations.Univalence.html#10880" class="Bound">B₁</a><a id="10907" class="Symbol">}</a>
<a id="10911" class="Symbol">{</a><a id="10912" href="Cubical.Foundations.Univalence.html#10912" class="Bound">C</a> <a id="10914" class="Symbol">:</a> <a id="10916" class="Symbol">(</a><a id="10917" href="Cubical.Foundations.Univalence.html#10917" class="Bound">i</a> <a id="10919" class="Symbol">:</a> <a id="10921" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="10922" class="Symbol">)</a> <a id="10924" class="Symbol">→</a> <a id="10926" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="10931" href="Cubical.Foundations.Univalence.html#10837" class="Bound">ℓ''</a><a id="10934" class="Symbol">}</a>
<a id="10938" class="Symbol">{</a><a id="10939" href="Cubical.Foundations.Univalence.html#10939" class="Bound">f₀</a> <a id="10942" class="Symbol">:</a> <a id="10944" href="Cubical.Foundations.Univalence.html#10843" class="Bound">A₀</a> <a id="10947" class="Symbol">→</a> <a id="10949" href="Cubical.Foundations.Univalence.html#10877" class="Bound">B₀</a> <a id="10952" class="Symbol">→</a> <a id="10954" href="Cubical.Foundations.Univalence.html#10912" class="Bound">C</a> <a id="10956" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="10958" class="Symbol">}</a> <a id="10960" class="Symbol">{</a><a id="10961" href="Cubical.Foundations.Univalence.html#10961" class="Bound">f₁</a> <a id="10964" class="Symbol">:</a> <a id="10966" href="Cubical.Foundations.Univalence.html#10846" class="Bound">A₁</a> <a id="10969" class="Symbol">→</a> <a id="10971" href="Cubical.Foundations.Univalence.html#10880" class="Bound">B₁</a> <a id="10974" class="Symbol">→</a> <a id="10976" href="Cubical.Foundations.Univalence.html#10912" class="Bound">C</a> <a id="10978" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="10980" class="Symbol">}</a>
<a id="10984" class="Symbol">→</a> <a id="10986" class="Symbol">(∀</a> <a id="10989" href="Cubical.Foundations.Univalence.html#10989" class="Bound">a</a> <a id="10991" href="Cubical.Foundations.Univalence.html#10991" class="Bound">b</a> <a id="10993" class="Symbol">→</a> <a id="10995" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="11001" href="Cubical.Foundations.Univalence.html#10912" class="Bound">C</a> <a id="11003" class="Symbol">(</a><a id="11004" href="Cubical.Foundations.Univalence.html#10939" class="Bound">f₀</a> <a id="11007" href="Cubical.Foundations.Univalence.html#10989" class="Bound">a</a> <a id="11009" href="Cubical.Foundations.Univalence.html#10991" class="Bound">b</a><a id="11010" class="Symbol">)</a> <a id="11012" class="Symbol">(</a><a id="11013" href="Cubical.Foundations.Univalence.html#10961" class="Bound">f₁</a> <a id="11016" class="Symbol">(</a><a id="11017" href="Cubical.Foundations.Univalence.html#10860" class="Bound">e₁</a> <a id="11020" class="Symbol">.</a><a id="11021" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="11025" href="Cubical.Foundations.Univalence.html#10989" class="Bound">a</a><a id="11026" class="Symbol">)</a> <a id="11028" class="Symbol">(</a><a id="11029" href="Cubical.Foundations.Univalence.html#10895" class="Bound">e₂</a> <a id="11032" class="Symbol">.</a><a id="11033" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="11037" href="Cubical.Foundations.Univalence.html#10991" class="Bound">b</a><a id="11038" class="Symbol">)))</a>
<a id="11044" class="Symbol">→</a> <a id="11046" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="11052" class="Symbol">(λ</a> <a id="11055" href="Cubical.Foundations.Univalence.html#11055" class="Bound">i</a> <a id="11057" class="Symbol">→</a> <a id="11059" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="11062" href="Cubical.Foundations.Univalence.html#10860" class="Bound">e₁</a> <a id="11065" href="Cubical.Foundations.Univalence.html#11055" class="Bound">i</a> <a id="11067" class="Symbol">→</a> <a id="11069" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="11072" href="Cubical.Foundations.Univalence.html#10895" class="Bound">e₂</a> <a id="11075" href="Cubical.Foundations.Univalence.html#11055" class="Bound">i</a> <a id="11077" class="Symbol">→</a> <a id="11079" href="Cubical.Foundations.Univalence.html#10912" class="Bound">C</a> <a id="11081" href="Cubical.Foundations.Univalence.html#11055" class="Bound">i</a><a id="11082" class="Symbol">)</a> <a id="11084" href="Cubical.Foundations.Univalence.html#10939" class="Bound">f₀</a> <a id="11087" href="Cubical.Foundations.Univalence.html#10961" class="Bound">f₁</a>
<a id="11090" href="Cubical.Foundations.Univalence.html#10822" class="Function">ua→2</a> <a id="11095" href="Cubical.Foundations.Univalence.html#11095" class="Bound">h</a> <a id="11097" class="Symbol">=</a> <a id="11099" href="Cubical.Foundations.Univalence.html#9992" class="Function">ua→</a> <a id="11103" class="Symbol">(</a><a id="11104" href="Cubical.Foundations.Univalence.html#9992" class="Function">ua→</a> <a id="11108" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="11110" href="Cubical.Foundations.Univalence.html#11095" class="Bound">h</a><a id="11111" class="Symbol">)</a>
<a id="11114" class="Comment">-- Useful lemma for unfolding a transported function over ua</a>
<a id="11175" class="Comment">-- If we would have regularity this would be refl</a>
<a id="transportUAop₁"></a><a id="11225" href="Cubical.Foundations.Univalence.html#11225" class="Function">transportUAop₁</a> <a id="11240" class="Symbol">:</a> <a id="11242" class="Symbol">∀</a> <a id="11244" class="Symbol">{</a><a id="11245" href="Cubical.Foundations.Univalence.html#11245" class="Bound">A</a> <a id="11247" href="Cubical.Foundations.Univalence.html#11247" class="Bound">B</a> <a id="11249" class="Symbol">:</a> <a id="11251" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="11256" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="11257" class="Symbol">}</a> <a id="11259" class="Symbol">→</a> <a id="11261" class="Symbol">(</a><a id="11262" href="Cubical.Foundations.Univalence.html#11262" class="Bound">e</a> <a id="11264" class="Symbol">:</a> <a id="11266" href="Cubical.Foundations.Univalence.html#11245" class="Bound">A</a> <a id="11268" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="11270" href="Cubical.Foundations.Univalence.html#11247" class="Bound">B</a><a id="11271" class="Symbol">)</a> <a id="11273" class="Symbol">(</a><a id="11274" href="Cubical.Foundations.Univalence.html#11274" class="Bound">f</a> <a id="11276" class="Symbol">:</a> <a id="11278" href="Cubical.Foundations.Univalence.html#11245" class="Bound">A</a> <a id="11280" class="Symbol">→</a> <a id="11282" href="Cubical.Foundations.Univalence.html#11245" class="Bound">A</a><a id="11283" class="Symbol">)</a> <a id="11285" class="Symbol">(</a><a id="11286" href="Cubical.Foundations.Univalence.html#11286" class="Bound">x</a> <a id="11288" class="Symbol">:</a> <a id="11290" href="Cubical.Foundations.Univalence.html#11247" class="Bound">B</a><a id="11291" class="Symbol">)</a>
<a id="11308" class="Symbol">→</a> <a id="11310" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="11320" class="Symbol">(λ</a> <a id="11323" href="Cubical.Foundations.Univalence.html#11323" class="Bound">i</a> <a id="11325" class="Symbol">→</a> <a id="11327" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="11330" href="Cubical.Foundations.Univalence.html#11262" class="Bound">e</a> <a id="11332" href="Cubical.Foundations.Univalence.html#11323" class="Bound">i</a> <a id="11334" class="Symbol">→</a> <a id="11336" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="11339" href="Cubical.Foundations.Univalence.html#11262" class="Bound">e</a> <a id="11341" href="Cubical.Foundations.Univalence.html#11323" class="Bound">i</a><a id="11342" class="Symbol">)</a> <a id="11344" href="Cubical.Foundations.Univalence.html#11274" class="Bound">f</a> <a id="11346" href="Cubical.Foundations.Univalence.html#11286" class="Bound">x</a> <a id="11348" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="11350" href="Agda.Builtin.Cubical.Glue.html#1143" class="Function">equivFun</a> <a id="11359" href="Cubical.Foundations.Univalence.html#11262" class="Bound">e</a> <a id="11361" class="Symbol">(</a><a id="11362" href="Cubical.Foundations.Univalence.html#11274" class="Bound">f</a> <a id="11364" class="Symbol">(</a><a id="11365" href="Cubical.Foundations.Equiv.html#2928" class="Function">invEq</a> <a id="11371" href="Cubical.Foundations.Univalence.html#11262" class="Bound">e</a> <a id="11373" href="Cubical.Foundations.Univalence.html#11286" class="Bound">x</a><a id="11374" class="Symbol">))</a>
<a id="11377" href="Cubical.Foundations.Univalence.html#11225" class="Function">transportUAop₁</a> <a id="11392" href="Cubical.Foundations.Univalence.html#11392" class="Bound">e</a> <a id="11394" href="Cubical.Foundations.Univalence.html#11394" class="Bound">f</a> <a id="11396" href="Cubical.Foundations.Univalence.html#11396" class="Bound">x</a> <a id="11398" href="Cubical.Foundations.Univalence.html#11398" class="Bound">i</a> <a id="11400" class="Symbol">=</a> <a id="11402" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="11416" class="Symbol">(</a><a id="11417" href="Agda.Builtin.Cubical.Glue.html#1143" class="Function">equivFun</a> <a id="11426" href="Cubical.Foundations.Univalence.html#11392" class="Bound">e</a> <a id="11428" class="Symbol">(</a><a id="11429" href="Cubical.Foundations.Univalence.html#11394" class="Bound">f</a> <a id="11431" class="Symbol">(</a><a id="11432" href="Cubical.Foundations.Equiv.html#2928" class="Function">invEq</a> <a id="11438" href="Cubical.Foundations.Univalence.html#11392" class="Bound">e</a> <a id="11440" class="Symbol">(</a><a id="11441" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="11455" href="Cubical.Foundations.Univalence.html#11396" class="Bound">x</a> <a id="11457" href="Cubical.Foundations.Univalence.html#11398" class="Bound">i</a><a id="11458" class="Symbol">))))</a> <a id="11463" href="Cubical.Foundations.Univalence.html#11398" class="Bound">i</a>
<a id="11466" class="Comment">-- Binary version</a>
<a id="transportUAop₂"></a><a id="11484" href="Cubical.Foundations.Univalence.html#11484" class="Function">transportUAop₂</a> <a id="11499" class="Symbol">:</a> <a id="11501" class="Symbol">∀</a> <a id="11503" class="Symbol">{</a><a id="11504" href="Cubical.Foundations.Univalence.html#11504" class="Bound">ℓ</a><a id="11505" class="Symbol">}</a> <a id="11507" class="Symbol">{</a><a id="11508" href="Cubical.Foundations.Univalence.html#11508" class="Bound">A</a> <a id="11510" href="Cubical.Foundations.Univalence.html#11510" class="Bound">B</a> <a id="11512" class="Symbol">:</a> <a id="11514" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="11519" href="Cubical.Foundations.Univalence.html#11504" class="Bound">ℓ</a><a id="11520" class="Symbol">}</a> <a id="11522" class="Symbol">→</a> <a id="11524" class="Symbol">(</a><a id="11525" href="Cubical.Foundations.Univalence.html#11525" class="Bound">e</a> <a id="11527" class="Symbol">:</a> <a id="11529" href="Cubical.Foundations.Univalence.html#11508" class="Bound">A</a> <a id="11531" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="11533" href="Cubical.Foundations.Univalence.html#11510" class="Bound">B</a><a id="11534" class="Symbol">)</a> <a id="11536" class="Symbol">(</a><a id="11537" href="Cubical.Foundations.Univalence.html#11537" class="Bound">f</a> <a id="11539" class="Symbol">:</a> <a id="11541" href="Cubical.Foundations.Univalence.html#11508" class="Bound">A</a> <a id="11543" class="Symbol">→</a> <a id="11545" href="Cubical.Foundations.Univalence.html#11508" class="Bound">A</a> <a id="11547" class="Symbol">→</a> <a id="11549" href="Cubical.Foundations.Univalence.html#11508" class="Bound">A</a><a id="11550" class="Symbol">)</a> <a id="11552" class="Symbol">(</a><a id="11553" href="Cubical.Foundations.Univalence.html#11553" class="Bound">x</a> <a id="11555" href="Cubical.Foundations.Univalence.html#11555" class="Bound">y</a> <a id="11557" class="Symbol">:</a> <a id="11559" href="Cubical.Foundations.Univalence.html#11510" class="Bound">B</a><a id="11560" class="Symbol">)</a>
<a id="11577" class="Symbol">→</a> <a id="11579" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="11589" class="Symbol">(λ</a> <a id="11592" href="Cubical.Foundations.Univalence.html#11592" class="Bound">i</a> <a id="11594" class="Symbol">→</a> <a id="11596" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="11599" href="Cubical.Foundations.Univalence.html#11525" class="Bound">e</a> <a id="11601" href="Cubical.Foundations.Univalence.html#11592" class="Bound">i</a> <a id="11603" class="Symbol">→</a> <a id="11605" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="11608" href="Cubical.Foundations.Univalence.html#11525" class="Bound">e</a> <a id="11610" href="Cubical.Foundations.Univalence.html#11592" class="Bound">i</a> <a id="11612" class="Symbol">→</a> <a id="11614" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="11617" href="Cubical.Foundations.Univalence.html#11525" class="Bound">e</a> <a id="11619" href="Cubical.Foundations.Univalence.html#11592" class="Bound">i</a><a id="11620" class="Symbol">)</a> <a id="11622" href="Cubical.Foundations.Univalence.html#11537" class="Bound">f</a> <a id="11624" href="Cubical.Foundations.Univalence.html#11553" class="Bound">x</a> <a id="11626" href="Cubical.Foundations.Univalence.html#11555" class="Bound">y</a> <a id="11628" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a>
<a id="11647" href="Agda.Builtin.Cubical.Glue.html#1143" class="Function">equivFun</a> <a id="11656" href="Cubical.Foundations.Univalence.html#11525" class="Bound">e</a> <a id="11658" class="Symbol">(</a><a id="11659" href="Cubical.Foundations.Univalence.html#11537" class="Bound">f</a> <a id="11661" class="Symbol">(</a><a id="11662" href="Cubical.Foundations.Equiv.html#2928" class="Function">invEq</a> <a id="11668" href="Cubical.Foundations.Univalence.html#11525" class="Bound">e</a> <a id="11670" href="Cubical.Foundations.Univalence.html#11553" class="Bound">x</a><a id="11671" class="Symbol">)</a> <a id="11673" class="Symbol">(</a><a id="11674" href="Cubical.Foundations.Equiv.html#2928" class="Function">invEq</a> <a id="11680" href="Cubical.Foundations.Univalence.html#11525" class="Bound">e</a> <a id="11682" href="Cubical.Foundations.Univalence.html#11555" class="Bound">y</a><a id="11683" class="Symbol">))</a>
<a id="11686" href="Cubical.Foundations.Univalence.html#11484" class="Function">transportUAop₂</a> <a id="11701" href="Cubical.Foundations.Univalence.html#11701" class="Bound">e</a> <a id="11703" href="Cubical.Foundations.Univalence.html#11703" class="Bound">f</a> <a id="11705" href="Cubical.Foundations.Univalence.html#11705" class="Bound">x</a> <a id="11707" href="Cubical.Foundations.Univalence.html#11707" class="Bound">y</a> <a id="11709" href="Cubical.Foundations.Univalence.html#11709" class="Bound">i</a> <a id="11711" class="Symbol">=</a>
<a id="11717" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="11731" class="Symbol">(</a><a id="11732" href="Agda.Builtin.Cubical.Glue.html#1143" class="Function">equivFun</a> <a id="11741" href="Cubical.Foundations.Univalence.html#11701" class="Bound">e</a> <a id="11743" class="Symbol">(</a><a id="11744" href="Cubical.Foundations.Univalence.html#11703" class="Bound">f</a> <a id="11746" class="Symbol">(</a><a id="11747" href="Cubical.Foundations.Equiv.html#2928" class="Function">invEq</a> <a id="11753" href="Cubical.Foundations.Univalence.html#11701" class="Bound">e</a> <a id="11755" class="Symbol">(</a><a id="11756" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="11770" href="Cubical.Foundations.Univalence.html#11705" class="Bound">x</a> <a id="11772" href="Cubical.Foundations.Univalence.html#11709" class="Bound">i</a><a id="11773" class="Symbol">))</a>
<a id="11809" class="Symbol">(</a><a id="11810" href="Cubical.Foundations.Equiv.html#2928" class="Function">invEq</a> <a id="11816" href="Cubical.Foundations.Univalence.html#11701" class="Bound">e</a> <a id="11818" class="Symbol">(</a><a id="11819" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="11833" href="Cubical.Foundations.Univalence.html#11707" class="Bound">y</a> <a id="11835" href="Cubical.Foundations.Univalence.html#11709" class="Bound">i</a><a id="11836" class="Symbol">))))</a> <a id="11841" href="Cubical.Foundations.Univalence.html#11709" class="Bound">i</a>
<a id="11844" class="Comment">-- Alternative version of EquivJ that only requires a predicate on functions</a>
<a id="elimEquivFun"></a><a id="11921" href="Cubical.Foundations.Univalence.html#11921" class="Function">elimEquivFun</a> <a id="11934" class="Symbol">:</a> <a id="11936" class="Symbol">{</a><a id="11937" href="Cubical.Foundations.Univalence.html#11937" class="Bound">A</a> <a id="11939" href="Cubical.Foundations.Univalence.html#11939" class="Bound">B</a> <a id="11941" class="Symbol">:</a> <a id="11943" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="11948" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="11949" class="Symbol">}</a> <a id="11951" class="Symbol">(</a><a id="11952" href="Cubical.Foundations.Univalence.html#11952" class="Bound">P</a> <a id="11954" class="Symbol">:</a> <a id="11956" class="Symbol">(</a><a id="11957" href="Cubical.Foundations.Univalence.html#11957" class="Bound">A</a> <a id="11959" class="Symbol">:</a> <a id="11961" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="11966" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="11967" class="Symbol">)</a> <a id="11969" class="Symbol">→</a> <a id="11971" class="Symbol">(</a><a id="11972" href="Cubical.Foundations.Univalence.html#11957" class="Bound">A</a> <a id="11974" class="Symbol">→</a> <a id="11976" href="Cubical.Foundations.Univalence.html#11939" class="Bound">B</a><a id="11977" class="Symbol">)</a> <a id="11979" class="Symbol">→</a> <a id="11981" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="11986" href="Cubical.Foundations.Univalence.html#897" class="Generalizable">ℓ'</a><a id="11988" class="Symbol">)</a>
<a id="12003" class="Symbol">→</a> <a id="12005" class="Symbol">(</a><a id="12006" href="Cubical.Foundations.Univalence.html#12006" class="Bound">r</a> <a id="12008" class="Symbol">:</a> <a id="12010" href="Cubical.Foundations.Univalence.html#11952" class="Bound">P</a> <a id="12012" href="Cubical.Foundations.Univalence.html#11939" class="Bound">B</a> <a id="12014" class="Symbol">(</a><a id="12015" href="Cubical.Foundations.Function.html#468" class="Function">idfun</a> <a id="12021" href="Cubical.Foundations.Univalence.html#11939" class="Bound">B</a><a id="12022" class="Symbol">))</a> <a id="12025" class="Symbol">→</a> <a id="12027" class="Symbol">(</a><a id="12028" href="Cubical.Foundations.Univalence.html#12028" class="Bound">e</a> <a id="12030" class="Symbol">:</a> <a id="12032" href="Cubical.Foundations.Univalence.html#11937" class="Bound">A</a> <a id="12034" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="12036" href="Cubical.Foundations.Univalence.html#11939" class="Bound">B</a><a id="12037" class="Symbol">)</a> <a id="12039" class="Symbol">→</a> <a id="12041" href="Cubical.Foundations.Univalence.html#11952" class="Bound">P</a> <a id="12043" href="Cubical.Foundations.Univalence.html#11937" class="Bound">A</a> <a id="12045" class="Symbol">(</a><a id="12046" href="Cubical.Foundations.Univalence.html#12028" class="Bound">e</a> <a id="12048" class="Symbol">.</a><a id="12049" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a><a id="12052" class="Symbol">)</a>
<a id="12054" href="Cubical.Foundations.Univalence.html#11921" class="Function">elimEquivFun</a> <a id="12067" href="Cubical.Foundations.Univalence.html#12067" class="Bound">P</a> <a id="12069" href="Cubical.Foundations.Univalence.html#12069" class="Bound">r</a> <a id="12071" href="Cubical.Foundations.Univalence.html#12071" class="Bound">e</a> <a id="12073" class="Symbol">=</a> <a id="12075" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="12081" class="Symbol">(λ</a> <a id="12084" href="Cubical.Foundations.Univalence.html#12084" class="Bound">x</a> <a id="12086" class="Symbol">→</a> <a id="12088" href="Cubical.Foundations.Univalence.html#12067" class="Bound">P</a> <a id="12090" class="Symbol">(</a><a id="12091" href="Cubical.Foundations.Univalence.html#12084" class="Bound">x</a> <a id="12093" class="Symbol">.</a><a id="12094" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a><a id="12097" class="Symbol">)</a> <a id="12099" class="Symbol">(</a><a id="12100" href="Cubical.Foundations.Univalence.html#12084" class="Bound">x</a> <a id="12102" class="Symbol">.</a><a id="12103" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="12107" class="Symbol">.</a><a id="12108" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a><a id="12111" class="Symbol">))</a> <a id="12114" class="Symbol">(</a><a id="12115" href="Cubical.Foundations.Univalence.html#6744" class="Function">contrSinglEquiv</a> <a id="12131" href="Cubical.Foundations.Univalence.html#12071" class="Bound">e</a><a id="12132" class="Symbol">)</a> <a id="12134" href="Cubical.Foundations.Univalence.html#12069" class="Bound">r</a>
<a id="12137" class="Comment">-- Isomorphism induction</a>
<a id="elimIso"></a><a id="12162" href="Cubical.Foundations.Univalence.html#12162" class="Function">elimIso</a> <a id="12170" class="Symbol">:</a> <a id="12172" class="Symbol">{</a><a id="12173" href="Cubical.Foundations.Univalence.html#12173" class="Bound">B</a> <a id="12175" class="Symbol">:</a> <a id="12177" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="12182" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="12183" class="Symbol">}</a> <a id="12185" class="Symbol">→</a> <a id="12187" class="Symbol">(</a><a id="12188" href="Cubical.Foundations.Univalence.html#12188" class="Bound">Q</a> <a id="12190" class="Symbol">:</a> <a id="12192" class="Symbol">{</a><a id="12193" href="Cubical.Foundations.Univalence.html#12193" class="Bound">A</a> <a id="12195" class="Symbol">:</a> <a id="12197" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="12202" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="12203" class="Symbol">}</a> <a id="12205" class="Symbol">→</a> <a id="12207" class="Symbol">(</a><a id="12208" href="Cubical.Foundations.Univalence.html#12193" class="Bound">A</a> <a id="12210" class="Symbol">→</a> <a id="12212" href="Cubical.Foundations.Univalence.html#12173" class="Bound">B</a><a id="12213" class="Symbol">)</a> <a id="12215" class="Symbol">→</a> <a id="12217" class="Symbol">(</a><a id="12218" href="Cubical.Foundations.Univalence.html#12173" class="Bound">B</a> <a id="12220" class="Symbol">→</a> <a id="12222" href="Cubical.Foundations.Univalence.html#12193" class="Bound">A</a><a id="12223" class="Symbol">)</a> <a id="12225" class="Symbol">→</a> <a id="12227" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="12232" href="Cubical.Foundations.Univalence.html#897" class="Generalizable">ℓ'</a><a id="12234" class="Symbol">)</a> <a id="12236" class="Symbol">→</a>
<a id="12248" class="Symbol">(</a><a id="12249" href="Cubical.Foundations.Univalence.html#12249" class="Bound">h</a> <a id="12251" class="Symbol">:</a> <a id="12253" href="Cubical.Foundations.Univalence.html#12188" class="Bound">Q</a> <a id="12255" class="Symbol">(</a><a id="12256" href="Cubical.Foundations.Function.html#468" class="Function">idfun</a> <a id="12262" href="Cubical.Foundations.Univalence.html#12173" class="Bound">B</a><a id="12263" class="Symbol">)</a> <a id="12265" class="Symbol">(</a><a id="12266" href="Cubical.Foundations.Function.html#468" class="Function">idfun</a> <a id="12272" href="Cubical.Foundations.Univalence.html#12173" class="Bound">B</a><a id="12273" class="Symbol">))</a> <a id="12276" class="Symbol">→</a> <a id="12278" class="Symbol">{</a><a id="12279" href="Cubical.Foundations.Univalence.html#12279" class="Bound">A</a> <a id="12281" class="Symbol">:</a> <a id="12283" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="12288" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="12289" class="Symbol">}</a> <a id="12291" class="Symbol">→</a>
<a id="12303" class="Symbol">(</a><a id="12304" href="Cubical.Foundations.Univalence.html#12304" class="Bound">f</a> <a id="12306" class="Symbol">:</a> <a id="12308" href="Cubical.Foundations.Univalence.html#12279" class="Bound">A</a> <a id="12310" class="Symbol">→</a> <a id="12312" href="Cubical.Foundations.Univalence.html#12173" class="Bound">B</a><a id="12313" class="Symbol">)</a> <a id="12315" class="Symbol">→</a> <a id="12317" class="Symbol">(</a><a id="12318" href="Cubical.Foundations.Univalence.html#12318" class="Bound">g</a> <a id="12320" class="Symbol">:</a> <a id="12322" href="Cubical.Foundations.Univalence.html#12173" class="Bound">B</a> <a id="12324" class="Symbol">→</a> <a id="12326" href="Cubical.Foundations.Univalence.html#12279" class="Bound">A</a><a id="12327" class="Symbol">)</a> <a id="12329" class="Symbol">→</a> <a id="12331" href="Cubical.Foundations.Isomorphism.html#571" class="Function">section</a> <a id="12339" href="Cubical.Foundations.Univalence.html#12304" class="Bound">f</a> <a id="12341" href="Cubical.Foundations.Univalence.html#12318" class="Bound">g</a> <a id="12343" class="Symbol">→</a> <a id="12345" href="Cubical.Foundations.Isomorphism.html#686" class="Function">retract</a> <a id="12353" href="Cubical.Foundations.Univalence.html#12304" class="Bound">f</a> <a id="12355" href="Cubical.Foundations.Univalence.html#12318" class="Bound">g</a> <a id="12357" class="Symbol">→</a> <a id="12359" href="Cubical.Foundations.Univalence.html#12188" class="Bound">Q</a> <a id="12361" href="Cubical.Foundations.Univalence.html#12304" class="Bound">f</a> <a id="12363" href="Cubical.Foundations.Univalence.html#12318" class="Bound">g</a>
<a id="12365" href="Cubical.Foundations.Univalence.html#12162" class="Function">elimIso</a> <a id="12373" class="Symbol">{</a><a id="12374" href="Cubical.Foundations.Univalence.html#12374" class="Bound">ℓ</a><a id="12375" class="Symbol">}</a> <a id="12377" class="Symbol">{</a><a id="12378" href="Cubical.Foundations.Univalence.html#12378" class="Bound">ℓ'</a><a id="12380" class="Symbol">}</a> <a id="12382" class="Symbol">{</a><a id="12383" href="Cubical.Foundations.Univalence.html#12383" class="Bound">B</a><a id="12384" class="Symbol">}</a> <a id="12386" href="Cubical.Foundations.Univalence.html#12386" class="Bound">Q</a> <a id="12388" href="Cubical.Foundations.Univalence.html#12388" class="Bound">h</a> <a id="12390" class="Symbol">{</a><a id="12391" href="Cubical.Foundations.Univalence.html#12391" class="Bound">A</a><a id="12392" class="Symbol">}</a> <a id="12394" href="Cubical.Foundations.Univalence.html#12394" class="Bound">f</a> <a id="12396" href="Cubical.Foundations.Univalence.html#12396" class="Bound">g</a> <a id="12398" href="Cubical.Foundations.Univalence.html#12398" class="Bound">sfg</a> <a id="12402" href="Cubical.Foundations.Univalence.html#12402" class="Bound">rfg</a> <a id="12406" class="Symbol">=</a> <a id="12408" href="Cubical.Foundations.Univalence.html#12634" class="Function">rem1</a> <a id="12413" href="Cubical.Foundations.Univalence.html#12394" class="Bound">f</a> <a id="12415" href="Cubical.Foundations.Univalence.html#12396" class="Bound">g</a> <a id="12417" href="Cubical.Foundations.Univalence.html#12398" class="Bound">sfg</a> <a id="12421" href="Cubical.Foundations.Univalence.html#12402" class="Bound">rfg</a>
<a id="12427" class="Keyword">where</a>
<a id="12435" href="Cubical.Foundations.Univalence.html#12435" class="Function">P</a> <a id="12437" class="Symbol">:</a> <a id="12439" class="Symbol">(</a><a id="12440" href="Cubical.Foundations.Univalence.html#12440" class="Bound">A</a> <a id="12442" class="Symbol">:</a> <a id="12444" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="12449" href="Cubical.Foundations.Univalence.html#12374" class="Bound">ℓ</a><a id="12450" class="Symbol">)</a> <a id="12452" class="Symbol">→</a> <a id="12454" class="Symbol">(</a><a id="12455" href="Cubical.Foundations.Univalence.html#12455" class="Bound">f</a> <a id="12457" class="Symbol">:</a> <a id="12459" href="Cubical.Foundations.Univalence.html#12440" class="Bound">A</a> <a id="12461" class="Symbol">→</a> <a id="12463" href="Cubical.Foundations.Univalence.html#12383" class="Bound">B</a><a id="12464" class="Symbol">)</a> <a id="12466" class="Symbol">→</a> <a id="12468" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="12473" class="Symbol">(</a><a id="12474" href="Agda.Primitive.html#810" class="Primitive">ℓ-max</a> <a id="12480" href="Cubical.Foundations.Univalence.html#12378" class="Bound">ℓ'</a> <a id="12483" href="Cubical.Foundations.Univalence.html#12374" class="Bound">ℓ</a><a id="12484" class="Symbol">)</a>
<a id="12488" href="Cubical.Foundations.Univalence.html#12435" class="Function">P</a> <a id="12490" href="Cubical.Foundations.Univalence.html#12490" class="Bound">A</a> <a id="12492" href="Cubical.Foundations.Univalence.html#12492" class="Bound">f</a> <a id="12494" class="Symbol">=</a> <a id="12496" class="Symbol">(</a><a id="12497" href="Cubical.Foundations.Univalence.html#12497" class="Bound">g</a> <a id="12499" class="Symbol">:</a> <a id="12501" href="Cubical.Foundations.Univalence.html#12383" class="Bound">B</a> <a id="12503" class="Symbol">→</a> <a id="12505" href="Cubical.Foundations.Univalence.html#12490" class="Bound">A</a><a id="12506" class="Symbol">)</a> <a id="12508" class="Symbol">→</a> <a id="12510" href="Cubical.Foundations.Isomorphism.html#571" class="Function">section</a> <a id="12518" href="Cubical.Foundations.Univalence.html#12492" class="Bound">f</a> <a id="12520" href="Cubical.Foundations.Univalence.html#12497" class="Bound">g</a> <a id="12522" class="Symbol">→</a> <a id="12524" href="Cubical.Foundations.Isomorphism.html#686" class="Function">retract</a> <a id="12532" href="Cubical.Foundations.Univalence.html#12492" class="Bound">f</a> <a id="12534" href="Cubical.Foundations.Univalence.html#12497" class="Bound">g</a> <a id="12536" class="Symbol">→</a> <a id="12538" href="Cubical.Foundations.Univalence.html#12386" class="Bound">Q</a> <a id="12540" href="Cubical.Foundations.Univalence.html#12492" class="Bound">f</a> <a id="12542" href="Cubical.Foundations.Univalence.html#12497" class="Bound">g</a>
<a id="12547" href="Cubical.Foundations.Univalence.html#12547" class="Function">rem</a> <a id="12551" class="Symbol">:</a> <a id="12553" href="Cubical.Foundations.Univalence.html#12435" class="Function">P</a> <a id="12555" href="Cubical.Foundations.Univalence.html#12383" class="Bound">B</a> <a id="12557" class="Symbol">(</a><a id="12558" href="Cubical.Foundations.Function.html#468" class="Function">idfun</a> <a id="12564" href="Cubical.Foundations.Univalence.html#12383" class="Bound">B</a><a id="12565" class="Symbol">)</a>
<a id="12569" href="Cubical.Foundations.Univalence.html#12547" class="Function">rem</a> <a id="12573" href="Cubical.Foundations.Univalence.html#12573" class="Bound">g</a> <a id="12575" href="Cubical.Foundations.Univalence.html#12575" class="Bound">sfg</a> <a id="12579" href="Cubical.Foundations.Univalence.html#12579" class="Bound">rfg</a> <a id="12583" class="Symbol">=</a> <a id="12585" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="12591" class="Symbol">(</a><a id="12592" href="Cubical.Foundations.Univalence.html#12386" class="Bound">Q</a> <a id="12594" class="Symbol">(</a><a id="12595" href="Cubical.Foundations.Function.html#468" class="Function">idfun</a> <a id="12601" href="Cubical.Foundations.Univalence.html#12383" class="Bound">B</a><a id="12602" class="Symbol">))</a> <a id="12605" class="Symbol">(λ</a> <a id="12608" href="Cubical.Foundations.Univalence.html#12608" class="Bound">i</a> <a id="12610" href="Cubical.Foundations.Univalence.html#12610" class="Bound">b</a> <a id="12612" class="Symbol">→</a> <a id="12614" class="Symbol">(</a><a id="12615" href="Cubical.Foundations.Univalence.html#12575" class="Bound">sfg</a> <a id="12619" href="Cubical.Foundations.Univalence.html#12610" class="Bound">b</a><a id="12620" class="Symbol">)</a> <a id="12622" class="Symbol">(</a><a id="12623" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="12625" href="Cubical.Foundations.Univalence.html#12608" class="Bound">i</a><a id="12626" class="Symbol">))</a> <a id="12629" href="Cubical.Foundations.Univalence.html#12388" class="Bound">h</a>
<a id="12634" href="Cubical.Foundations.Univalence.html#12634" class="Function">rem1</a> <a id="12639" class="Symbol">:</a> <a id="12641" class="Symbol">{</a><a id="12642" href="Cubical.Foundations.Univalence.html#12642" class="Bound">A</a> <a id="12644" class="Symbol">:</a> <a id="12646" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="12651" href="Cubical.Foundations.Univalence.html#12374" class="Bound">ℓ</a><a id="12652" class="Symbol">}</a> <a id="12654" class="Symbol">→</a> <a id="12656" class="Symbol">(</a><a id="12657" href="Cubical.Foundations.Univalence.html#12657" class="Bound">f</a> <a id="12659" class="Symbol">:</a> <a id="12661" href="Cubical.Foundations.Univalence.html#12642" class="Bound">A</a> <a id="12663" class="Symbol">→</a> <a id="12665" href="Cubical.Foundations.Univalence.html#12383" class="Bound">B</a><a id="12666" class="Symbol">)</a> <a id="12668" class="Symbol">→</a> <a id="12670" href="Cubical.Foundations.Univalence.html#12435" class="Function">P</a> <a id="12672" href="Cubical.Foundations.Univalence.html#12642" class="Bound">A</a> <a id="12674" href="Cubical.Foundations.Univalence.html#12657" class="Bound">f</a>
<a id="12678" href="Cubical.Foundations.Univalence.html#12634" class="Function">rem1</a> <a id="12683" href="Cubical.Foundations.Univalence.html#12683" class="Bound">f</a> <a id="12685" href="Cubical.Foundations.Univalence.html#12685" class="Bound">g</a> <a id="12687" href="Cubical.Foundations.Univalence.html#12687" class="Bound">sfg</a> <a id="12691" href="Cubical.Foundations.Univalence.html#12691" class="Bound">rfg</a> <a id="12695" class="Symbol">=</a> <a id="12697" href="Cubical.Foundations.Univalence.html#11921" class="Function">elimEquivFun</a> <a id="12710" href="Cubical.Foundations.Univalence.html#12435" class="Function">P</a> <a id="12712" href="Cubical.Foundations.Univalence.html#12547" class="Function">rem</a> <a id="12716" class="Symbol">(</a><a id="12717" href="Cubical.Foundations.Univalence.html#12683" class="Bound">f</a> <a id="12719" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="12721" href="Cubical.Foundations.Isomorphism.html#2932" class="Function">isoToIsEquiv</a> <a id="12734" class="Symbol">(</a><a id="12735" href="Cubical.Foundations.Isomorphism.html#869" class="InductiveConstructor">iso</a> <a id="12739" href="Cubical.Foundations.Univalence.html#12683" class="Bound">f</a> <a id="12741" href="Cubical.Foundations.Univalence.html#12685" class="Bound">g</a> <a id="12743" href="Cubical.Foundations.Univalence.html#12687" class="Bound">sfg</a> <a id="12747" href="Cubical.Foundations.Univalence.html#12691" class="Bound">rfg</a><a id="12750" class="Symbol">))</a> <a id="12753" href="Cubical.Foundations.Univalence.html#12685" class="Bound">g</a> <a id="12755" href="Cubical.Foundations.Univalence.html#12687" class="Bound">sfg</a> <a id="12759" href="Cubical.Foundations.Univalence.html#12691" class="Bound">rfg</a>
<a id="uaInvEquiv"></a><a id="12765" href="Cubical.Foundations.Univalence.html#12765" class="Function">uaInvEquiv</a> <a id="12776" class="Symbol">:</a> <a id="12778" class="Symbol">∀</a> <a id="12780" class="Symbol">{</a><a id="12781" href="Cubical.Foundations.Univalence.html#12781" class="Bound">A</a> <a id="12783" href="Cubical.Foundations.Univalence.html#12783" class="Bound">B</a> <a id="12785" class="Symbol">:</a> <a id="12787" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="12792" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="12793" class="Symbol">}</a> <a id="12795" class="Symbol">→</a> <a id="12797" class="Symbol">(</a><a id="12798" href="Cubical.Foundations.Univalence.html#12798" class="Bound">e</a> <a id="12800" class="Symbol">:</a> <a id="12802" href="Cubical.Foundations.Univalence.html#12781" class="Bound">A</a> <a id="12804" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="12806" href="Cubical.Foundations.Univalence.html#12783" class="Bound">B</a><a id="12807" class="Symbol">)</a> <a id="12809" class="Symbol">→</a> <a id="12811" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="12814" class="Symbol">(</a><a id="12815" href="Cubical.Foundations.Equiv.html#3368" class="Function">invEquiv</a> <a id="12824" href="Cubical.Foundations.Univalence.html#12798" class="Bound">e</a><a id="12825" class="Symbol">)</a> <a id="12827" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="12829" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12833" class="Symbol">(</a><a id="12834" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="12837" href="Cubical.Foundations.Univalence.html#12798" class="Bound">e</a><a id="12838" class="Symbol">)</a>
<a id="12840" href="Cubical.Foundations.Univalence.html#12765" class="Function">uaInvEquiv</a> <a id="12851" class="Symbol">{</a><a id="12852" class="Argument">B</a> <a id="12854" class="Symbol">=</a> <a id="12856" href="Cubical.Foundations.Univalence.html#12856" class="Bound">B</a><a id="12857" class="Symbol">}</a> <a id="12859" class="Symbol">=</a> <a id="12861" href="Cubical.Foundations.Univalence.html#6935" class="Function">EquivJ</a> <a id="12868" class="Symbol">(λ</a> <a id="12871" href="Cubical.Foundations.Univalence.html#12871" class="Bound">_</a> <a id="12873" href="Cubical.Foundations.Univalence.html#12873" class="Bound">e</a> <a id="12875" class="Symbol">→</a> <a id="12877" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="12880" class="Symbol">(</a><a id="12881" href="Cubical.Foundations.Equiv.html#3368" class="Function">invEquiv</a> <a id="12890" href="Cubical.Foundations.Univalence.html#12873" class="Bound">e</a><a id="12891" class="Symbol">)</a> <a id="12893" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="12895" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12899" class="Symbol">(</a><a id="12900" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="12903" href="Cubical.Foundations.Univalence.html#12873" class="Bound">e</a><a id="12904" class="Symbol">))</a>
<a id="12935" class="Symbol">(</a><a id="12936" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="12941" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="12944" class="Symbol">(</a><a id="12945" href="Cubical.Foundations.Equiv.html#3442" class="Function">invEquivIdEquiv</a> <a id="12961" href="Cubical.Foundations.Univalence.html#12856" class="Bound">B</a><a id="12962" class="Symbol">))</a>
<a id="uaCompEquiv"></a><a id="12966" href="Cubical.Foundations.Univalence.html#12966" class="Function">uaCompEquiv</a> <a id="12978" class="Symbol">:</a> <a id="12980" class="Symbol">∀</a> <a id="12982" class="Symbol">{</a><a id="12983" href="Cubical.Foundations.Univalence.html#12983" class="Bound">A</a> <a id="12985" href="Cubical.Foundations.Univalence.html#12985" class="Bound">B</a> <a id="12987" href="Cubical.Foundations.Univalence.html#12987" class="Bound">C</a> <a id="12989" class="Symbol">:</a> <a id="12991" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="12996" href="Cubical.Foundations.Univalence.html#895" class="Generalizable">ℓ</a><a id="12997" class="Symbol">}</a> <a id="12999" class="Symbol">→</a> <a id="13001" class="Symbol">(</a><a id="13002" href="Cubical.Foundations.Univalence.html#13002" class="Bound">e</a> <a id="13004" class="Symbol">:</a> <a id="13006" href="Cubical.Foundations.Univalence.html#12983" class="Bound">A</a> <a id="13008" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="13010" href="Cubical.Foundations.Univalence.html#12985" class="Bound">B</a><a id="13011" class="Symbol">)</a> <a id="13013" class="Symbol">(</a><a id="13014" href="Cubical.Foundations.Univalence.html#13014" class="Bound">f</a> <a id="13016" class="Symbol">:</a> <a id="13018" href="Cubical.Foundations.Univalence.html#12985" class="Bound">B</a> <a id="13020" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="13022" href="Cubical.Foundations.Univalence.html#12987" class="Bound">C</a><a id="13023" class="Symbol">)</a> <a id="13025" class="Symbol">→</a> <a id="13027" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="13030" class="Symbol">(</a><a id="13031" href="Cubical.Foundations.Equiv.html#3542" class="Function">compEquiv</a> <a id="13041" href="Cubical.Foundations.Univalence.html#13002" class="Bound">e</a> <a id="13043" href="Cubical.Foundations.Univalence.html#13014" class="Bound">f</a><a id="13044" class="Symbol">)</a> <a id="13046" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="13048" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="13051" href="Cubical.Foundations.Univalence.html#13002" class="Bound">e</a> <a id="13053" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="13055" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="13058" href="Cubical.Foundations.Univalence.html#13014" class="Bound">f</a>
<a id="13060" href="Cubical.Foundations.Univalence.html#12966" class="Function">uaCompEquiv</a> <a id="13072" class="Symbol">{</a><a id="13073" class="Argument">B</a> <a id="13075" class="Symbol">=</a> <a id="13077" href="Cubical.Foundations.Univalence.html#13077" class="Bound">B</a><a id="13078" class="Symbol">}</a> <a id="13080" class="Symbol">{</a><a id="13081" href="Cubical.Foundations.Univalence.html#13081" class="Bound">C</a><a id="13082" class="Symbol">}</a> <a id="13084" class="Symbol">=</a> <a id="13086" href="Cubical.Foundations.Univalence.html#6935" class="Function">EquivJ</a> <a id="13093" class="Symbol">(λ</a> <a id="13096" href="Cubical.Foundations.Univalence.html#13096" class="Bound">_</a> <a id="13098" href="Cubical.Foundations.Univalence.html#13098" class="Bound">e</a> <a id="13100" class="Symbol">→</a> <a id="13102" class="Symbol">(</a><a id="13103" href="Cubical.Foundations.Univalence.html#13103" class="Bound">f</a> <a id="13105" class="Symbol">:</a> <a id="13107" href="Cubical.Foundations.Univalence.html#13077" class="Bound">B</a> <a id="13109" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="13111" href="Cubical.Foundations.Univalence.html#13081" class="Bound">C</a><a id="13112" class="Symbol">)</a> <a id="13114" class="Symbol">→</a> <a id="13116" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="13119" class="Symbol">(</a><a id="13120" href="Cubical.Foundations.Equiv.html#3542" class="Function">compEquiv</a> <a id="13130" href="Cubical.Foundations.Univalence.html#13098" class="Bound">e</a> <a id="13132" href="Cubical.Foundations.Univalence.html#13103" class="Bound">f</a><a id="13133" class="Symbol">)</a> <a id="13135" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="13137" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="13140" href="Cubical.Foundations.Univalence.html#13098" class="Bound">e</a> <a id="13142" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="13144" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="13147" href="Cubical.Foundations.Univalence.html#13103" class="Bound">f</a><a id="13148" class="Symbol">)</a>
<a id="13183" class="Symbol">(λ</a> <a id="13186" href="Cubical.Foundations.Univalence.html#13186" class="Bound">f</a> <a id="13188" class="Symbol">→</a> <a id="13190" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="13195" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="13198" class="Symbol">(</a><a id="13199" href="Cubical.Foundations.Equiv.html#4699" class="Function">compEquivIdEquiv</a> <a id="13216" href="Cubical.Foundations.Univalence.html#13186" class="Bound">f</a><a id="13217" class="Symbol">)</a>
<a id="13259" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="13261" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="13265" class="Symbol">(</a><a id="13266" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="13271" class="Symbol">(λ</a> <a id="13274" href="Cubical.Foundations.Univalence.html#13274" class="Bound">x</a> <a id="13276" class="Symbol">→</a> <a id="13278" href="Cubical.Foundations.Univalence.html#13274" class="Bound">x</a> <a id="13280" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="13282" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="13285" href="Cubical.Foundations.Univalence.html#13186" class="Bound">f</a><a id="13286" class="Symbol">)</a> <a id="13288" href="Cubical.Foundations.Univalence.html#1090" class="Function">uaIdEquiv</a>
<a id="13338" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="13340" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="13344" class="Symbol">(</a><a id="13345" href="Cubical.Foundations.GroupoidLaws.html#989" class="Function">lUnit</a> <a id="13351" class="Symbol">(</a><a id="13352" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="13355" href="Cubical.Foundations.Univalence.html#13186" class="Bound">f</a><a id="13356" class="Symbol">))))</a>
</pre></body></html>