-
Notifications
You must be signed in to change notification settings - Fork 0
/
Cubical.Foundations.Transport.html
207 lines (172 loc) · 158 KB
/
Cubical.Foundations.Transport.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
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Foundations.Transport</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">{- Basic theory about transport:
- transport is invertible
- transport is an equivalence ([pathToEquiv])
-}</a>
<a id="111" class="Symbol">{-#</a> <a id="115" class="Keyword">OPTIONS</a> <a id="123" class="Pragma">--safe</a> <a id="130" class="Symbol">#-}</a>
<a id="134" class="Keyword">module</a> <a id="141" href="Cubical.Foundations.Transport.html" class="Module">Cubical.Foundations.Transport</a> <a id="171" class="Keyword">where</a>
<a id="178" class="Keyword">open</a> <a id="183" class="Keyword">import</a> <a id="190" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>
<a id="218" class="Keyword">open</a> <a id="223" class="Keyword">import</a> <a id="230" href="Cubical.Foundations.Equiv.html" class="Module">Cubical.Foundations.Equiv</a>
<a id="256" class="Keyword">open</a> <a id="261" class="Keyword">import</a> <a id="268" href="Cubical.Foundations.Isomorphism.html" class="Module">Cubical.Foundations.Isomorphism</a>
<a id="300" class="Keyword">open</a> <a id="305" class="Keyword">import</a> <a id="312" href="Cubical.Foundations.Univalence.html" class="Module">Cubical.Foundations.Univalence</a>
<a id="343" class="Keyword">open</a> <a id="348" class="Keyword">import</a> <a id="355" href="Cubical.Foundations.GroupoidLaws.html" class="Module">Cubical.Foundations.GroupoidLaws</a>
<a id="388" class="Keyword">open</a> <a id="393" class="Keyword">import</a> <a id="400" href="Cubical.Foundations.Function.html" class="Module">Cubical.Foundations.Function</a> <a id="429" class="Keyword">using</a> <a id="435" class="Symbol">(</a><a id="436" href="Cubical.Foundations.Function.html#526" class="Function Operator">_∘_</a><a id="439" class="Symbol">)</a>
<a id="442" class="Comment">-- Direct definition of transport filler, note that we have to</a>
<a id="505" class="Comment">-- explicitly tell Agda that the type is constant (like in CHM)</a>
<a id="transpFill"></a><a id="569" href="Cubical.Foundations.Transport.html#569" class="Function">transpFill</a> <a id="580" class="Symbol">:</a> <a id="582" class="Symbol">∀</a> <a id="584" class="Symbol">{</a><a id="585" href="Cubical.Foundations.Transport.html#585" class="Bound">ℓ</a><a id="586" class="Symbol">}</a> <a id="588" class="Symbol">{</a><a id="589" href="Cubical.Foundations.Transport.html#589" class="Bound">A</a> <a id="591" class="Symbol">:</a> <a id="593" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="598" href="Cubical.Foundations.Transport.html#585" class="Bound">ℓ</a><a id="599" class="Symbol">}</a>
<a id="614" class="Symbol">(</a><a id="615" href="Cubical.Foundations.Transport.html#615" class="Bound">φ</a> <a id="617" class="Symbol">:</a> <a id="619" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="620" class="Symbol">)</a>
<a id="635" class="Symbol">(</a><a id="636" href="Cubical.Foundations.Transport.html#636" class="Bound">A</a> <a id="638" class="Symbol">:</a> <a id="640" class="Symbol">(</a><a id="641" href="Cubical.Foundations.Transport.html#641" class="Bound">i</a> <a id="643" class="Symbol">:</a> <a id="645" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a><a id="646" class="Symbol">)</a> <a id="648" class="Symbol">→</a> <a id="650" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="655" href="Cubical.Foundations.Transport.html#585" class="Bound">ℓ</a> <a id="657" href="Cubical.Core.Primitives.html#3508" class="Function Operator">[</a> <a id="659" href="Cubical.Foundations.Transport.html#615" class="Bound">φ</a> <a id="661" href="Cubical.Core.Primitives.html#3508" class="Function Operator">↦</a> <a id="663" class="Symbol">(λ</a> <a id="666" href="Cubical.Foundations.Transport.html#666" class="Bound">_</a> <a id="668" class="Symbol">→</a> <a id="670" href="Cubical.Foundations.Transport.html#589" class="Bound">A</a><a id="671" class="Symbol">)</a> <a id="673" href="Cubical.Core.Primitives.html#3508" class="Function Operator">]</a><a id="674" class="Symbol">)</a>
<a id="689" class="Symbol">(</a><a id="690" href="Cubical.Foundations.Transport.html#690" class="Bound">u0</a> <a id="693" class="Symbol">:</a> <a id="695" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="700" class="Symbol">(</a><a id="701" href="Cubical.Foundations.Transport.html#636" class="Bound">A</a> <a id="703" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="705" class="Symbol">))</a>
<a id="719" class="Symbol">→</a> <a id="721" class="Comment">--------------------------------------</a>
<a id="773" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="779" class="Symbol">(λ</a> <a id="782" href="Cubical.Foundations.Transport.html#782" class="Bound">i</a> <a id="784" class="Symbol">→</a> <a id="786" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="791" class="Symbol">(</a><a id="792" href="Cubical.Foundations.Transport.html#636" class="Bound">A</a> <a id="794" href="Cubical.Foundations.Transport.html#782" class="Bound">i</a><a id="795" class="Symbol">))</a> <a id="798" href="Cubical.Foundations.Transport.html#690" class="Bound">u0</a> <a id="801" class="Symbol">(</a><a id="802" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="809" class="Symbol">(λ</a> <a id="812" href="Cubical.Foundations.Transport.html#812" class="Bound">i</a> <a id="814" class="Symbol">→</a> <a id="816" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="821" class="Symbol">(</a><a id="822" href="Cubical.Foundations.Transport.html#636" class="Bound">A</a> <a id="824" href="Cubical.Foundations.Transport.html#812" class="Bound">i</a><a id="825" class="Symbol">))</a> <a id="828" href="Cubical.Foundations.Transport.html#615" class="Bound">φ</a> <a id="830" href="Cubical.Foundations.Transport.html#690" class="Bound">u0</a><a id="832" class="Symbol">)</a>
<a id="834" href="Cubical.Foundations.Transport.html#569" class="Function">transpFill</a> <a id="845" href="Cubical.Foundations.Transport.html#845" class="Bound">φ</a> <a id="847" href="Cubical.Foundations.Transport.html#847" class="Bound">A</a> <a id="849" href="Cubical.Foundations.Transport.html#849" class="Bound">u0</a> <a id="852" href="Cubical.Foundations.Transport.html#852" class="Bound">i</a> <a id="854" class="Symbol">=</a> <a id="856" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="863" class="Symbol">(λ</a> <a id="866" href="Cubical.Foundations.Transport.html#866" class="Bound">j</a> <a id="868" class="Symbol">→</a> <a id="870" href="Agda.Builtin.Cubical.Sub.html#407" class="Primitive">outS</a> <a id="875" class="Symbol">(</a><a id="876" href="Cubical.Foundations.Transport.html#847" class="Bound">A</a> <a id="878" class="Symbol">(</a><a id="879" href="Cubical.Foundations.Transport.html#852" class="Bound">i</a> <a id="881" href="Cubical.Core.Primitives.html#441" class="Primitive Operator">∧</a> <a id="883" href="Cubical.Foundations.Transport.html#866" class="Bound">j</a><a id="884" class="Symbol">)))</a> <a id="888" class="Symbol">(</a><a id="889" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="891" href="Cubical.Foundations.Transport.html#852" class="Bound">i</a> <a id="893" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="895" href="Cubical.Foundations.Transport.html#845" class="Bound">φ</a><a id="896" class="Symbol">)</a> <a id="898" href="Cubical.Foundations.Transport.html#849" class="Bound">u0</a>
<a id="transport⁻"></a><a id="902" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="913" class="Symbol">:</a> <a id="915" class="Symbol">∀</a> <a id="917" class="Symbol">{</a><a id="918" href="Cubical.Foundations.Transport.html#918" class="Bound">ℓ</a><a id="919" class="Symbol">}</a> <a id="921" class="Symbol">{</a><a id="922" href="Cubical.Foundations.Transport.html#922" class="Bound">A</a> <a id="924" href="Cubical.Foundations.Transport.html#924" class="Bound">B</a> <a id="926" class="Symbol">:</a> <a id="928" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="933" href="Cubical.Foundations.Transport.html#918" class="Bound">ℓ</a><a id="934" class="Symbol">}</a> <a id="936" class="Symbol">→</a> <a id="938" href="Cubical.Foundations.Transport.html#922" class="Bound">A</a> <a id="940" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="942" href="Cubical.Foundations.Transport.html#924" class="Bound">B</a> <a id="944" class="Symbol">→</a> <a id="946" href="Cubical.Foundations.Transport.html#924" class="Bound">B</a> <a id="948" class="Symbol">→</a> <a id="950" href="Cubical.Foundations.Transport.html#922" class="Bound">A</a>
<a id="952" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="963" href="Cubical.Foundations.Transport.html#963" class="Bound">p</a> <a id="965" class="Symbol">=</a> <a id="967" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="977" class="Symbol">(λ</a> <a id="980" href="Cubical.Foundations.Transport.html#980" class="Bound">i</a> <a id="982" class="Symbol">→</a> <a id="984" href="Cubical.Foundations.Transport.html#963" class="Bound">p</a> <a id="986" class="Symbol">(</a><a id="987" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="989" href="Cubical.Foundations.Transport.html#980" class="Bound">i</a><a id="990" class="Symbol">))</a>
<a id="subst⁻"></a><a id="994" href="Cubical.Foundations.Transport.html#994" class="Function">subst⁻</a> <a id="1001" class="Symbol">:</a> <a id="1003" class="Symbol">∀</a> <a id="1005" class="Symbol">{</a><a id="1006" href="Cubical.Foundations.Transport.html#1006" class="Bound">ℓ</a> <a id="1008" href="Cubical.Foundations.Transport.html#1008" class="Bound">ℓ'</a><a id="1010" class="Symbol">}</a> <a id="1012" class="Symbol">{</a><a id="1013" href="Cubical.Foundations.Transport.html#1013" class="Bound">A</a> <a id="1015" class="Symbol">:</a> <a id="1017" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1022" href="Cubical.Foundations.Transport.html#1006" class="Bound">ℓ</a><a id="1023" class="Symbol">}</a> <a id="1025" class="Symbol">{</a><a id="1026" href="Cubical.Foundations.Transport.html#1026" class="Bound">x</a> <a id="1028" href="Cubical.Foundations.Transport.html#1028" class="Bound">y</a> <a id="1030" class="Symbol">:</a> <a id="1032" href="Cubical.Foundations.Transport.html#1013" class="Bound">A</a><a id="1033" class="Symbol">}</a> <a id="1035" class="Symbol">(</a><a id="1036" href="Cubical.Foundations.Transport.html#1036" class="Bound">B</a> <a id="1038" class="Symbol">:</a> <a id="1040" href="Cubical.Foundations.Transport.html#1013" class="Bound">A</a> <a id="1042" class="Symbol">→</a> <a id="1044" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1049" href="Cubical.Foundations.Transport.html#1008" class="Bound">ℓ'</a><a id="1051" class="Symbol">)</a> <a id="1053" class="Symbol">(</a><a id="1054" href="Cubical.Foundations.Transport.html#1054" class="Bound">p</a> <a id="1056" class="Symbol">:</a> <a id="1058" href="Cubical.Foundations.Transport.html#1026" class="Bound">x</a> <a id="1060" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1062" href="Cubical.Foundations.Transport.html#1028" class="Bound">y</a><a id="1063" class="Symbol">)</a> <a id="1065" class="Symbol">→</a> <a id="1067" href="Cubical.Foundations.Transport.html#1036" class="Bound">B</a> <a id="1069" href="Cubical.Foundations.Transport.html#1028" class="Bound">y</a> <a id="1071" class="Symbol">→</a> <a id="1073" href="Cubical.Foundations.Transport.html#1036" class="Bound">B</a> <a id="1075" href="Cubical.Foundations.Transport.html#1026" class="Bound">x</a>
<a id="1077" href="Cubical.Foundations.Transport.html#994" class="Function">subst⁻</a> <a id="1084" href="Cubical.Foundations.Transport.html#1084" class="Bound">B</a> <a id="1086" href="Cubical.Foundations.Transport.html#1086" class="Bound">p</a> <a id="1088" href="Cubical.Foundations.Transport.html#1088" class="Bound">pa</a> <a id="1091" class="Symbol">=</a> <a id="1093" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="1104" class="Symbol">(λ</a> <a id="1107" href="Cubical.Foundations.Transport.html#1107" class="Bound">i</a> <a id="1109" class="Symbol">→</a> <a id="1111" href="Cubical.Foundations.Transport.html#1084" class="Bound">B</a> <a id="1113" class="Symbol">(</a><a id="1114" href="Cubical.Foundations.Transport.html#1086" class="Bound">p</a> <a id="1116" href="Cubical.Foundations.Transport.html#1107" class="Bound">i</a><a id="1117" class="Symbol">))</a> <a id="1120" href="Cubical.Foundations.Transport.html#1088" class="Bound">pa</a>
<a id="subst⁻-filler"></a><a id="1124" href="Cubical.Foundations.Transport.html#1124" class="Function">subst⁻-filler</a> <a id="1138" class="Symbol">:</a> <a id="1140" class="Symbol">∀</a> <a id="1142" class="Symbol">{</a><a id="1143" href="Cubical.Foundations.Transport.html#1143" class="Bound">ℓ</a> <a id="1145" href="Cubical.Foundations.Transport.html#1145" class="Bound">ℓ'</a><a id="1147" class="Symbol">}</a> <a id="1149" class="Symbol">{</a><a id="1150" href="Cubical.Foundations.Transport.html#1150" class="Bound">A</a> <a id="1152" class="Symbol">:</a> <a id="1154" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1159" href="Cubical.Foundations.Transport.html#1143" class="Bound">ℓ</a><a id="1160" class="Symbol">}</a> <a id="1162" class="Symbol">{</a><a id="1163" href="Cubical.Foundations.Transport.html#1163" class="Bound">x</a> <a id="1165" href="Cubical.Foundations.Transport.html#1165" class="Bound">y</a> <a id="1167" class="Symbol">:</a> <a id="1169" href="Cubical.Foundations.Transport.html#1150" class="Bound">A</a><a id="1170" class="Symbol">}</a> <a id="1172" class="Symbol">(</a><a id="1173" href="Cubical.Foundations.Transport.html#1173" class="Bound">B</a> <a id="1175" class="Symbol">:</a> <a id="1177" href="Cubical.Foundations.Transport.html#1150" class="Bound">A</a> <a id="1179" class="Symbol">→</a> <a id="1181" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1186" href="Cubical.Foundations.Transport.html#1145" class="Bound">ℓ'</a><a id="1188" class="Symbol">)</a> <a id="1190" class="Symbol">(</a><a id="1191" href="Cubical.Foundations.Transport.html#1191" class="Bound">p</a> <a id="1193" class="Symbol">:</a> <a id="1195" href="Cubical.Foundations.Transport.html#1163" class="Bound">x</a> <a id="1197" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1199" href="Cubical.Foundations.Transport.html#1165" class="Bound">y</a><a id="1200" class="Symbol">)</a> <a id="1202" class="Symbol">(</a><a id="1203" href="Cubical.Foundations.Transport.html#1203" class="Bound">b</a> <a id="1205" class="Symbol">:</a> <a id="1207" href="Cubical.Foundations.Transport.html#1173" class="Bound">B</a> <a id="1209" href="Cubical.Foundations.Transport.html#1165" class="Bound">y</a><a id="1210" class="Symbol">)</a>
<a id="1214" class="Symbol">→</a> <a id="1216" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="1222" class="Symbol">(λ</a> <a id="1225" href="Cubical.Foundations.Transport.html#1225" class="Bound">i</a> <a id="1227" class="Symbol">→</a> <a id="1229" href="Cubical.Foundations.Transport.html#1173" class="Bound">B</a> <a id="1231" class="Symbol">(</a><a id="1232" href="Cubical.Foundations.Transport.html#1191" class="Bound">p</a> <a id="1234" class="Symbol">(</a><a id="1235" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="1237" href="Cubical.Foundations.Transport.html#1225" class="Bound">i</a><a id="1238" class="Symbol">)))</a> <a id="1242" href="Cubical.Foundations.Transport.html#1203" class="Bound">b</a> <a id="1244" class="Symbol">(</a><a id="1245" href="Cubical.Foundations.Transport.html#994" class="Function">subst⁻</a> <a id="1252" href="Cubical.Foundations.Transport.html#1173" class="Bound">B</a> <a id="1254" href="Cubical.Foundations.Transport.html#1191" class="Bound">p</a> <a id="1256" href="Cubical.Foundations.Transport.html#1203" class="Bound">b</a><a id="1257" class="Symbol">)</a>
<a id="1259" href="Cubical.Foundations.Transport.html#1124" class="Function">subst⁻-filler</a> <a id="1273" href="Cubical.Foundations.Transport.html#1273" class="Bound">B</a> <a id="1275" href="Cubical.Foundations.Transport.html#1275" class="Bound">p</a> <a id="1277" class="Symbol">=</a> <a id="1279" href="Cubical.Foundations.Prelude.html#9494" class="Function">subst-filler</a> <a id="1292" href="Cubical.Foundations.Transport.html#1273" class="Bound">B</a> <a id="1294" class="Symbol">(</a><a id="1295" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="1299" href="Cubical.Foundations.Transport.html#1275" class="Bound">p</a><a id="1300" class="Symbol">)</a>
<a id="transport-fillerExt"></a><a id="1303" href="Cubical.Foundations.Transport.html#1303" class="Function">transport-fillerExt</a> <a id="1323" class="Symbol">:</a> <a id="1325" class="Symbol">∀</a> <a id="1327" class="Symbol">{</a><a id="1328" href="Cubical.Foundations.Transport.html#1328" class="Bound">ℓ</a><a id="1329" class="Symbol">}</a> <a id="1331" class="Symbol">{</a><a id="1332" href="Cubical.Foundations.Transport.html#1332" class="Bound">A</a> <a id="1334" href="Cubical.Foundations.Transport.html#1334" class="Bound">B</a> <a id="1336" class="Symbol">:</a> <a id="1338" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1343" href="Cubical.Foundations.Transport.html#1328" class="Bound">ℓ</a><a id="1344" class="Symbol">}</a> <a id="1346" class="Symbol">(</a><a id="1347" href="Cubical.Foundations.Transport.html#1347" class="Bound">p</a> <a id="1349" class="Symbol">:</a> <a id="1351" href="Cubical.Foundations.Transport.html#1332" class="Bound">A</a> <a id="1353" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1355" href="Cubical.Foundations.Transport.html#1334" class="Bound">B</a><a id="1356" class="Symbol">)</a>
<a id="1378" class="Symbol">→</a> <a id="1380" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="1386" class="Symbol">(λ</a> <a id="1389" href="Cubical.Foundations.Transport.html#1389" class="Bound">i</a> <a id="1391" class="Symbol">→</a> <a id="1393" href="Cubical.Foundations.Transport.html#1332" class="Bound">A</a> <a id="1395" class="Symbol">→</a> <a id="1397" href="Cubical.Foundations.Transport.html#1347" class="Bound">p</a> <a id="1399" href="Cubical.Foundations.Transport.html#1389" class="Bound">i</a><a id="1400" class="Symbol">)</a> <a id="1402" class="Symbol">(λ</a> <a id="1405" href="Cubical.Foundations.Transport.html#1405" class="Bound">x</a> <a id="1407" class="Symbol">→</a> <a id="1409" href="Cubical.Foundations.Transport.html#1405" class="Bound">x</a><a id="1410" class="Symbol">)</a> <a id="1412" class="Symbol">(</a><a id="1413" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="1423" href="Cubical.Foundations.Transport.html#1347" class="Bound">p</a><a id="1424" class="Symbol">)</a>
<a id="1426" href="Cubical.Foundations.Transport.html#1303" class="Function">transport-fillerExt</a> <a id="1446" href="Cubical.Foundations.Transport.html#1446" class="Bound">p</a> <a id="1448" href="Cubical.Foundations.Transport.html#1448" class="Bound">i</a> <a id="1450" href="Cubical.Foundations.Transport.html#1450" class="Bound">x</a> <a id="1452" class="Symbol">=</a> <a id="1454" href="Cubical.Foundations.Prelude.html#8915" class="Function">transport-filler</a> <a id="1471" href="Cubical.Foundations.Transport.html#1446" class="Bound">p</a> <a id="1473" href="Cubical.Foundations.Transport.html#1450" class="Bound">x</a> <a id="1475" href="Cubical.Foundations.Transport.html#1448" class="Bound">i</a>
<a id="transport⁻-fillerExt"></a><a id="1478" href="Cubical.Foundations.Transport.html#1478" class="Function">transport⁻-fillerExt</a> <a id="1499" class="Symbol">:</a> <a id="1501" class="Symbol">∀</a> <a id="1503" class="Symbol">{</a><a id="1504" href="Cubical.Foundations.Transport.html#1504" class="Bound">ℓ</a><a id="1505" class="Symbol">}</a> <a id="1507" class="Symbol">{</a><a id="1508" href="Cubical.Foundations.Transport.html#1508" class="Bound">A</a> <a id="1510" href="Cubical.Foundations.Transport.html#1510" class="Bound">B</a> <a id="1512" class="Symbol">:</a> <a id="1514" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1519" href="Cubical.Foundations.Transport.html#1504" class="Bound">ℓ</a><a id="1520" class="Symbol">}</a> <a id="1522" class="Symbol">(</a><a id="1523" href="Cubical.Foundations.Transport.html#1523" class="Bound">p</a> <a id="1525" class="Symbol">:</a> <a id="1527" href="Cubical.Foundations.Transport.html#1508" class="Bound">A</a> <a id="1529" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1531" href="Cubical.Foundations.Transport.html#1510" class="Bound">B</a><a id="1532" class="Symbol">)</a>
<a id="1555" class="Symbol">→</a> <a id="1557" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="1563" class="Symbol">(λ</a> <a id="1566" href="Cubical.Foundations.Transport.html#1566" class="Bound">i</a> <a id="1568" class="Symbol">→</a> <a id="1570" href="Cubical.Foundations.Transport.html#1523" class="Bound">p</a> <a id="1572" href="Cubical.Foundations.Transport.html#1566" class="Bound">i</a> <a id="1574" class="Symbol">→</a> <a id="1576" href="Cubical.Foundations.Transport.html#1508" class="Bound">A</a><a id="1577" class="Symbol">)</a> <a id="1579" class="Symbol">(λ</a> <a id="1582" href="Cubical.Foundations.Transport.html#1582" class="Bound">x</a> <a id="1584" class="Symbol">→</a> <a id="1586" href="Cubical.Foundations.Transport.html#1582" class="Bound">x</a><a id="1587" class="Symbol">)</a> <a id="1589" class="Symbol">(</a><a id="1590" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="1601" href="Cubical.Foundations.Transport.html#1523" class="Bound">p</a><a id="1602" class="Symbol">)</a>
<a id="1604" href="Cubical.Foundations.Transport.html#1478" class="Function">transport⁻-fillerExt</a> <a id="1625" href="Cubical.Foundations.Transport.html#1625" class="Bound">p</a> <a id="1627" href="Cubical.Foundations.Transport.html#1627" class="Bound">i</a> <a id="1629" href="Cubical.Foundations.Transport.html#1629" class="Bound">x</a> <a id="1631" class="Symbol">=</a> <a id="1633" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="1640" class="Symbol">(λ</a> <a id="1643" href="Cubical.Foundations.Transport.html#1643" class="Bound">j</a> <a id="1645" class="Symbol">→</a> <a id="1647" href="Cubical.Foundations.Transport.html#1625" class="Bound">p</a> <a id="1649" class="Symbol">(</a><a id="1650" href="Cubical.Foundations.Transport.html#1627" class="Bound">i</a> <a id="1652" href="Cubical.Core.Primitives.html#441" class="Primitive Operator">∧</a> <a id="1654" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="1656" href="Cubical.Foundations.Transport.html#1643" class="Bound">j</a><a id="1657" class="Symbol">))</a> <a id="1660" class="Symbol">(</a><a id="1661" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="1663" href="Cubical.Foundations.Transport.html#1627" class="Bound">i</a><a id="1664" class="Symbol">)</a> <a id="1666" href="Cubical.Foundations.Transport.html#1629" class="Bound">x</a>
<a id="transport-fillerExt⁻"></a><a id="1669" href="Cubical.Foundations.Transport.html#1669" class="Function">transport-fillerExt⁻</a> <a id="1690" class="Symbol">:</a> <a id="1692" class="Symbol">∀</a> <a id="1694" class="Symbol">{</a><a id="1695" href="Cubical.Foundations.Transport.html#1695" class="Bound">ℓ</a><a id="1696" class="Symbol">}</a> <a id="1698" class="Symbol">{</a><a id="1699" href="Cubical.Foundations.Transport.html#1699" class="Bound">A</a> <a id="1701" href="Cubical.Foundations.Transport.html#1701" class="Bound">B</a> <a id="1703" class="Symbol">:</a> <a id="1705" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1710" href="Cubical.Foundations.Transport.html#1695" class="Bound">ℓ</a><a id="1711" class="Symbol">}</a> <a id="1713" class="Symbol">(</a><a id="1714" href="Cubical.Foundations.Transport.html#1714" class="Bound">p</a> <a id="1716" class="Symbol">:</a> <a id="1718" href="Cubical.Foundations.Transport.html#1699" class="Bound">A</a> <a id="1720" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1722" href="Cubical.Foundations.Transport.html#1701" class="Bound">B</a><a id="1723" class="Symbol">)</a>
<a id="1745" class="Symbol">→</a> <a id="1747" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="1753" class="Symbol">(λ</a> <a id="1756" href="Cubical.Foundations.Transport.html#1756" class="Bound">i</a> <a id="1758" class="Symbol">→</a> <a id="1760" href="Cubical.Foundations.Transport.html#1714" class="Bound">p</a> <a id="1762" href="Cubical.Foundations.Transport.html#1756" class="Bound">i</a> <a id="1764" class="Symbol">→</a> <a id="1766" href="Cubical.Foundations.Transport.html#1701" class="Bound">B</a><a id="1767" class="Symbol">)</a> <a id="1769" class="Symbol">(</a><a id="1770" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="1780" href="Cubical.Foundations.Transport.html#1714" class="Bound">p</a><a id="1781" class="Symbol">)</a> <a id="1783" class="Symbol">(λ</a> <a id="1786" href="Cubical.Foundations.Transport.html#1786" class="Bound">x</a> <a id="1788" class="Symbol">→</a> <a id="1790" href="Cubical.Foundations.Transport.html#1786" class="Bound">x</a><a id="1791" class="Symbol">)</a>
<a id="1793" href="Cubical.Foundations.Transport.html#1669" class="Function">transport-fillerExt⁻</a> <a id="1814" href="Cubical.Foundations.Transport.html#1814" class="Bound">p</a> <a id="1816" class="Symbol">=</a> <a id="1818" href="Cubical.Foundations.Prelude.html#1094" class="Function">symP</a> <a id="1823" class="Symbol">(</a><a id="1824" href="Cubical.Foundations.Transport.html#1478" class="Function">transport⁻-fillerExt</a> <a id="1845" class="Symbol">(</a><a id="1846" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="1850" href="Cubical.Foundations.Transport.html#1814" class="Bound">p</a><a id="1851" class="Symbol">))</a>
<a id="transport⁻-fillerExt⁻"></a><a id="1855" href="Cubical.Foundations.Transport.html#1855" class="Function">transport⁻-fillerExt⁻</a> <a id="1877" class="Symbol">:</a> <a id="1879" class="Symbol">∀</a> <a id="1881" class="Symbol">{</a><a id="1882" href="Cubical.Foundations.Transport.html#1882" class="Bound">ℓ</a><a id="1883" class="Symbol">}</a> <a id="1885" class="Symbol">{</a><a id="1886" href="Cubical.Foundations.Transport.html#1886" class="Bound">A</a> <a id="1888" href="Cubical.Foundations.Transport.html#1888" class="Bound">B</a> <a id="1890" class="Symbol">:</a> <a id="1892" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1897" href="Cubical.Foundations.Transport.html#1882" class="Bound">ℓ</a><a id="1898" class="Symbol">}</a> <a id="1900" class="Symbol">(</a><a id="1901" href="Cubical.Foundations.Transport.html#1901" class="Bound">p</a> <a id="1903" class="Symbol">:</a> <a id="1905" href="Cubical.Foundations.Transport.html#1886" class="Bound">A</a> <a id="1907" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="1909" href="Cubical.Foundations.Transport.html#1888" class="Bound">B</a><a id="1910" class="Symbol">)</a>
<a id="1933" class="Symbol">→</a> <a id="1935" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="1941" class="Symbol">(λ</a> <a id="1944" href="Cubical.Foundations.Transport.html#1944" class="Bound">i</a> <a id="1946" class="Symbol">→</a> <a id="1948" href="Cubical.Foundations.Transport.html#1888" class="Bound">B</a> <a id="1950" class="Symbol">→</a> <a id="1952" href="Cubical.Foundations.Transport.html#1901" class="Bound">p</a> <a id="1954" href="Cubical.Foundations.Transport.html#1944" class="Bound">i</a><a id="1955" class="Symbol">)</a> <a id="1957" class="Symbol">(</a><a id="1958" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="1969" href="Cubical.Foundations.Transport.html#1901" class="Bound">p</a><a id="1970" class="Symbol">)</a> <a id="1972" class="Symbol">(λ</a> <a id="1975" href="Cubical.Foundations.Transport.html#1975" class="Bound">x</a> <a id="1977" class="Symbol">→</a> <a id="1979" href="Cubical.Foundations.Transport.html#1975" class="Bound">x</a><a id="1980" class="Symbol">)</a>
<a id="1982" href="Cubical.Foundations.Transport.html#1855" class="Function">transport⁻-fillerExt⁻</a> <a id="2004" href="Cubical.Foundations.Transport.html#2004" class="Bound">p</a> <a id="2006" class="Symbol">=</a> <a id="2008" href="Cubical.Foundations.Prelude.html#1094" class="Function">symP</a> <a id="2013" class="Symbol">(</a><a id="2014" href="Cubical.Foundations.Transport.html#1303" class="Function">transport-fillerExt</a> <a id="2034" class="Symbol">(</a><a id="2035" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="2039" href="Cubical.Foundations.Transport.html#2004" class="Bound">p</a><a id="2040" class="Symbol">))</a>
<a id="transport⁻-filler"></a><a id="2045" href="Cubical.Foundations.Transport.html#2045" class="Function">transport⁻-filler</a> <a id="2063" class="Symbol">:</a> <a id="2065" class="Symbol">∀</a> <a id="2067" class="Symbol">{</a><a id="2068" href="Cubical.Foundations.Transport.html#2068" class="Bound">ℓ</a><a id="2069" class="Symbol">}</a> <a id="2071" class="Symbol">{</a><a id="2072" href="Cubical.Foundations.Transport.html#2072" class="Bound">A</a> <a id="2074" href="Cubical.Foundations.Transport.html#2074" class="Bound">B</a> <a id="2076" class="Symbol">:</a> <a id="2078" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2083" href="Cubical.Foundations.Transport.html#2068" class="Bound">ℓ</a><a id="2084" class="Symbol">}</a> <a id="2086" class="Symbol">(</a><a id="2087" href="Cubical.Foundations.Transport.html#2087" class="Bound">p</a> <a id="2089" class="Symbol">:</a> <a id="2091" href="Cubical.Foundations.Transport.html#2072" class="Bound">A</a> <a id="2093" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2095" href="Cubical.Foundations.Transport.html#2074" class="Bound">B</a><a id="2096" class="Symbol">)</a> <a id="2098" class="Symbol">(</a><a id="2099" href="Cubical.Foundations.Transport.html#2099" class="Bound">x</a> <a id="2101" class="Symbol">:</a> <a id="2103" href="Cubical.Foundations.Transport.html#2074" class="Bound">B</a><a id="2104" class="Symbol">)</a>
<a id="2125" class="Symbol">→</a> <a id="2127" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="2133" class="Symbol">(λ</a> <a id="2136" href="Cubical.Foundations.Transport.html#2136" class="Bound">i</a> <a id="2138" class="Symbol">→</a> <a id="2140" href="Cubical.Foundations.Transport.html#2087" class="Bound">p</a> <a id="2142" class="Symbol">(</a><a id="2143" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="2145" href="Cubical.Foundations.Transport.html#2136" class="Bound">i</a><a id="2146" class="Symbol">))</a> <a id="2149" href="Cubical.Foundations.Transport.html#2099" class="Bound">x</a> <a id="2151" class="Symbol">(</a><a id="2152" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="2163" href="Cubical.Foundations.Transport.html#2087" class="Bound">p</a> <a id="2165" href="Cubical.Foundations.Transport.html#2099" class="Bound">x</a><a id="2166" class="Symbol">)</a>
<a id="2168" href="Cubical.Foundations.Transport.html#2045" class="Function">transport⁻-filler</a> <a id="2186" href="Cubical.Foundations.Transport.html#2186" class="Bound">p</a> <a id="2188" href="Cubical.Foundations.Transport.html#2188" class="Bound">x</a> <a id="2190" class="Symbol">=</a> <a id="2192" href="Cubical.Foundations.Prelude.html#8915" class="Function">transport-filler</a> <a id="2209" class="Symbol">(λ</a> <a id="2212" href="Cubical.Foundations.Transport.html#2212" class="Bound">i</a> <a id="2214" class="Symbol">→</a> <a id="2216" href="Cubical.Foundations.Transport.html#2186" class="Bound">p</a> <a id="2218" class="Symbol">(</a><a id="2219" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="2221" href="Cubical.Foundations.Transport.html#2212" class="Bound">i</a><a id="2222" class="Symbol">))</a> <a id="2225" href="Cubical.Foundations.Transport.html#2188" class="Bound">x</a>
<a id="transport⁻Transport"></a><a id="2228" href="Cubical.Foundations.Transport.html#2228" class="Function">transport⁻Transport</a> <a id="2248" class="Symbol">:</a> <a id="2250" class="Symbol">∀</a> <a id="2252" class="Symbol">{</a><a id="2253" href="Cubical.Foundations.Transport.html#2253" class="Bound">ℓ</a><a id="2254" class="Symbol">}</a> <a id="2256" class="Symbol">{</a><a id="2257" href="Cubical.Foundations.Transport.html#2257" class="Bound">A</a> <a id="2259" href="Cubical.Foundations.Transport.html#2259" class="Bound">B</a> <a id="2261" class="Symbol">:</a> <a id="2263" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2268" href="Cubical.Foundations.Transport.html#2253" class="Bound">ℓ</a><a id="2269" class="Symbol">}</a> <a id="2271" class="Symbol">→</a> <a id="2273" class="Symbol">(</a><a id="2274" href="Cubical.Foundations.Transport.html#2274" class="Bound">p</a> <a id="2276" class="Symbol">:</a> <a id="2278" href="Cubical.Foundations.Transport.html#2257" class="Bound">A</a> <a id="2280" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2282" href="Cubical.Foundations.Transport.html#2259" class="Bound">B</a><a id="2283" class="Symbol">)</a> <a id="2285" class="Symbol">→</a> <a id="2287" class="Symbol">(</a><a id="2288" href="Cubical.Foundations.Transport.html#2288" class="Bound">a</a> <a id="2290" class="Symbol">:</a> <a id="2292" href="Cubical.Foundations.Transport.html#2257" class="Bound">A</a><a id="2293" class="Symbol">)</a> <a id="2295" class="Symbol">→</a>
<a id="2323" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="2334" href="Cubical.Foundations.Transport.html#2274" class="Bound">p</a> <a id="2336" class="Symbol">(</a><a id="2337" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="2347" href="Cubical.Foundations.Transport.html#2274" class="Bound">p</a> <a id="2349" href="Cubical.Foundations.Transport.html#2288" class="Bound">a</a><a id="2350" class="Symbol">)</a> <a id="2352" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2354" href="Cubical.Foundations.Transport.html#2288" class="Bound">a</a>
<a id="2356" href="Cubical.Foundations.Transport.html#2228" class="Function">transport⁻Transport</a> <a id="2376" href="Cubical.Foundations.Transport.html#2376" class="Bound">p</a> <a id="2378" href="Cubical.Foundations.Transport.html#2378" class="Bound">a</a> <a id="2380" href="Cubical.Foundations.Transport.html#2380" class="Bound">j</a> <a id="2382" class="Symbol">=</a> <a id="2384" href="Cubical.Foundations.Transport.html#1478" class="Function">transport⁻-fillerExt</a> <a id="2405" href="Cubical.Foundations.Transport.html#2376" class="Bound">p</a> <a id="2407" class="Symbol">(</a><a id="2408" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="2410" href="Cubical.Foundations.Transport.html#2380" class="Bound">j</a><a id="2411" class="Symbol">)</a> <a id="2413" class="Symbol">(</a><a id="2414" href="Cubical.Foundations.Transport.html#1303" class="Function">transport-fillerExt</a> <a id="2434" href="Cubical.Foundations.Transport.html#2376" class="Bound">p</a> <a id="2436" class="Symbol">(</a><a id="2437" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="2439" href="Cubical.Foundations.Transport.html#2380" class="Bound">j</a><a id="2440" class="Symbol">)</a> <a id="2442" href="Cubical.Foundations.Transport.html#2378" class="Bound">a</a><a id="2443" class="Symbol">)</a>
<a id="transportTransport⁻"></a><a id="2446" href="Cubical.Foundations.Transport.html#2446" class="Function">transportTransport⁻</a> <a id="2466" class="Symbol">:</a> <a id="2468" class="Symbol">∀</a> <a id="2470" class="Symbol">{</a><a id="2471" href="Cubical.Foundations.Transport.html#2471" class="Bound">ℓ</a><a id="2472" class="Symbol">}</a> <a id="2474" class="Symbol">{</a><a id="2475" href="Cubical.Foundations.Transport.html#2475" class="Bound">A</a> <a id="2477" href="Cubical.Foundations.Transport.html#2477" class="Bound">B</a> <a id="2479" class="Symbol">:</a> <a id="2481" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2486" href="Cubical.Foundations.Transport.html#2471" class="Bound">ℓ</a><a id="2487" class="Symbol">}</a> <a id="2489" class="Symbol">→</a> <a id="2491" class="Symbol">(</a><a id="2492" href="Cubical.Foundations.Transport.html#2492" class="Bound">p</a> <a id="2494" class="Symbol">:</a> <a id="2496" href="Cubical.Foundations.Transport.html#2475" class="Bound">A</a> <a id="2498" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2500" href="Cubical.Foundations.Transport.html#2477" class="Bound">B</a><a id="2501" class="Symbol">)</a> <a id="2503" class="Symbol">→</a> <a id="2505" class="Symbol">(</a><a id="2506" href="Cubical.Foundations.Transport.html#2506" class="Bound">b</a> <a id="2508" class="Symbol">:</a> <a id="2510" href="Cubical.Foundations.Transport.html#2477" class="Bound">B</a><a id="2511" class="Symbol">)</a> <a id="2513" class="Symbol">→</a>
<a id="2539" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="2549" href="Cubical.Foundations.Transport.html#2492" class="Bound">p</a> <a id="2551" class="Symbol">(</a><a id="2552" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="2563" href="Cubical.Foundations.Transport.html#2492" class="Bound">p</a> <a id="2565" href="Cubical.Foundations.Transport.html#2506" class="Bound">b</a><a id="2566" class="Symbol">)</a> <a id="2568" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2570" href="Cubical.Foundations.Transport.html#2506" class="Bound">b</a>
<a id="2572" href="Cubical.Foundations.Transport.html#2446" class="Function">transportTransport⁻</a> <a id="2592" href="Cubical.Foundations.Transport.html#2592" class="Bound">p</a> <a id="2594" href="Cubical.Foundations.Transport.html#2594" class="Bound">b</a> <a id="2596" href="Cubical.Foundations.Transport.html#2596" class="Bound">j</a> <a id="2598" class="Symbol">=</a> <a id="2600" href="Cubical.Foundations.Transport.html#1669" class="Function">transport-fillerExt⁻</a> <a id="2621" href="Cubical.Foundations.Transport.html#2592" class="Bound">p</a> <a id="2623" href="Cubical.Foundations.Transport.html#2596" class="Bound">j</a> <a id="2625" class="Symbol">(</a><a id="2626" href="Cubical.Foundations.Transport.html#1855" class="Function">transport⁻-fillerExt⁻</a> <a id="2648" href="Cubical.Foundations.Transport.html#2592" class="Bound">p</a> <a id="2650" href="Cubical.Foundations.Transport.html#2596" class="Bound">j</a> <a id="2652" href="Cubical.Foundations.Transport.html#2594" class="Bound">b</a><a id="2653" class="Symbol">)</a>
<a id="subst⁻Subst"></a><a id="2656" href="Cubical.Foundations.Transport.html#2656" class="Function">subst⁻Subst</a> <a id="2668" class="Symbol">:</a> <a id="2670" class="Symbol">∀</a> <a id="2672" class="Symbol">{</a><a id="2673" href="Cubical.Foundations.Transport.html#2673" class="Bound">ℓ</a> <a id="2675" href="Cubical.Foundations.Transport.html#2675" class="Bound">ℓ'</a><a id="2677" class="Symbol">}</a> <a id="2679" class="Symbol">{</a><a id="2680" href="Cubical.Foundations.Transport.html#2680" class="Bound">A</a> <a id="2682" class="Symbol">:</a> <a id="2684" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2689" href="Cubical.Foundations.Transport.html#2673" class="Bound">ℓ</a><a id="2690" class="Symbol">}</a> <a id="2692" class="Symbol">{</a><a id="2693" href="Cubical.Foundations.Transport.html#2693" class="Bound">x</a> <a id="2695" href="Cubical.Foundations.Transport.html#2695" class="Bound">y</a> <a id="2697" class="Symbol">:</a> <a id="2699" href="Cubical.Foundations.Transport.html#2680" class="Bound">A</a><a id="2700" class="Symbol">}</a> <a id="2702" class="Symbol">(</a><a id="2703" href="Cubical.Foundations.Transport.html#2703" class="Bound">B</a> <a id="2705" class="Symbol">:</a> <a id="2707" href="Cubical.Foundations.Transport.html#2680" class="Bound">A</a> <a id="2709" class="Symbol">→</a> <a id="2711" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2716" href="Cubical.Foundations.Transport.html#2675" class="Bound">ℓ'</a><a id="2718" class="Symbol">)</a> <a id="2720" class="Symbol">(</a><a id="2721" href="Cubical.Foundations.Transport.html#2721" class="Bound">p</a> <a id="2723" class="Symbol">:</a> <a id="2725" href="Cubical.Foundations.Transport.html#2693" class="Bound">x</a> <a id="2727" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2729" href="Cubical.Foundations.Transport.html#2695" class="Bound">y</a><a id="2730" class="Symbol">)</a>
<a id="2746" class="Symbol">→</a> <a id="2748" class="Symbol">(</a><a id="2749" href="Cubical.Foundations.Transport.html#2749" class="Bound">u</a> <a id="2751" class="Symbol">:</a> <a id="2753" href="Cubical.Foundations.Transport.html#2703" class="Bound">B</a> <a id="2755" href="Cubical.Foundations.Transport.html#2693" class="Bound">x</a><a id="2756" class="Symbol">)</a> <a id="2758" class="Symbol">→</a> <a id="2760" href="Cubical.Foundations.Transport.html#994" class="Function">subst⁻</a> <a id="2767" href="Cubical.Foundations.Transport.html#2703" class="Bound">B</a> <a id="2769" href="Cubical.Foundations.Transport.html#2721" class="Bound">p</a> <a id="2771" class="Symbol">(</a><a id="2772" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="2778" href="Cubical.Foundations.Transport.html#2703" class="Bound">B</a> <a id="2780" href="Cubical.Foundations.Transport.html#2721" class="Bound">p</a> <a id="2782" href="Cubical.Foundations.Transport.html#2749" class="Bound">u</a><a id="2783" class="Symbol">)</a> <a id="2785" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2787" href="Cubical.Foundations.Transport.html#2749" class="Bound">u</a>
<a id="2789" href="Cubical.Foundations.Transport.html#2656" class="Function">subst⁻Subst</a> <a id="2801" class="Symbol">{</a><a id="2802" class="Argument">x</a> <a id="2804" class="Symbol">=</a> <a id="2806" href="Cubical.Foundations.Transport.html#2806" class="Bound">x</a><a id="2807" class="Symbol">}</a> <a id="2809" class="Symbol">{</a><a id="2810" class="Argument">y</a> <a id="2812" class="Symbol">=</a> <a id="2814" href="Cubical.Foundations.Transport.html#2814" class="Bound">y</a><a id="2815" class="Symbol">}</a> <a id="2817" href="Cubical.Foundations.Transport.html#2817" class="Bound">B</a> <a id="2819" href="Cubical.Foundations.Transport.html#2819" class="Bound">p</a> <a id="2821" href="Cubical.Foundations.Transport.html#2821" class="Bound">u</a> <a id="2823" class="Symbol">=</a> <a id="2825" href="Cubical.Foundations.Transport.html#2228" class="Function">transport⁻Transport</a> <a id="2845" class="Symbol">{</a><a id="2846" class="Argument">A</a> <a id="2848" class="Symbol">=</a> <a id="2850" href="Cubical.Foundations.Transport.html#2817" class="Bound">B</a> <a id="2852" href="Cubical.Foundations.Transport.html#2806" class="Bound">x</a><a id="2853" class="Symbol">}</a> <a id="2855" class="Symbol">{</a><a id="2856" class="Argument">B</a> <a id="2858" class="Symbol">=</a> <a id="2860" href="Cubical.Foundations.Transport.html#2817" class="Bound">B</a> <a id="2862" href="Cubical.Foundations.Transport.html#2814" class="Bound">y</a><a id="2863" class="Symbol">}</a> <a id="2865" class="Symbol">(</a><a id="2866" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="2871" href="Cubical.Foundations.Transport.html#2817" class="Bound">B</a> <a id="2873" href="Cubical.Foundations.Transport.html#2819" class="Bound">p</a><a id="2874" class="Symbol">)</a> <a id="2876" href="Cubical.Foundations.Transport.html#2821" class="Bound">u</a>
<a id="substSubst⁻"></a><a id="2879" href="Cubical.Foundations.Transport.html#2879" class="Function">substSubst⁻</a> <a id="2891" class="Symbol">:</a> <a id="2893" class="Symbol">∀</a> <a id="2895" class="Symbol">{</a><a id="2896" href="Cubical.Foundations.Transport.html#2896" class="Bound">ℓ</a> <a id="2898" href="Cubical.Foundations.Transport.html#2898" class="Bound">ℓ'</a><a id="2900" class="Symbol">}</a> <a id="2902" class="Symbol">{</a><a id="2903" href="Cubical.Foundations.Transport.html#2903" class="Bound">A</a> <a id="2905" class="Symbol">:</a> <a id="2907" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2912" href="Cubical.Foundations.Transport.html#2896" class="Bound">ℓ</a><a id="2913" class="Symbol">}</a> <a id="2915" class="Symbol">{</a><a id="2916" href="Cubical.Foundations.Transport.html#2916" class="Bound">x</a> <a id="2918" href="Cubical.Foundations.Transport.html#2918" class="Bound">y</a> <a id="2920" class="Symbol">:</a> <a id="2922" href="Cubical.Foundations.Transport.html#2903" class="Bound">A</a><a id="2923" class="Symbol">}</a> <a id="2925" class="Symbol">(</a><a id="2926" href="Cubical.Foundations.Transport.html#2926" class="Bound">B</a> <a id="2928" class="Symbol">:</a> <a id="2930" href="Cubical.Foundations.Transport.html#2903" class="Bound">A</a> <a id="2932" class="Symbol">→</a> <a id="2934" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="2939" href="Cubical.Foundations.Transport.html#2898" class="Bound">ℓ'</a><a id="2941" class="Symbol">)</a> <a id="2943" class="Symbol">(</a><a id="2944" href="Cubical.Foundations.Transport.html#2944" class="Bound">p</a> <a id="2946" class="Symbol">:</a> <a id="2948" href="Cubical.Foundations.Transport.html#2916" class="Bound">x</a> <a id="2950" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="2952" href="Cubical.Foundations.Transport.html#2918" class="Bound">y</a><a id="2953" class="Symbol">)</a>
<a id="2969" class="Symbol">→</a> <a id="2971" class="Symbol">(</a><a id="2972" href="Cubical.Foundations.Transport.html#2972" class="Bound">v</a> <a id="2974" class="Symbol">:</a> <a id="2976" href="Cubical.Foundations.Transport.html#2926" class="Bound">B</a> <a id="2978" href="Cubical.Foundations.Transport.html#2918" class="Bound">y</a><a id="2979" class="Symbol">)</a> <a id="2981" class="Symbol">→</a> <a id="2983" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="2989" href="Cubical.Foundations.Transport.html#2926" class="Bound">B</a> <a id="2991" href="Cubical.Foundations.Transport.html#2944" class="Bound">p</a> <a id="2993" class="Symbol">(</a><a id="2994" href="Cubical.Foundations.Transport.html#994" class="Function">subst⁻</a> <a id="3001" href="Cubical.Foundations.Transport.html#2926" class="Bound">B</a> <a id="3003" href="Cubical.Foundations.Transport.html#2944" class="Bound">p</a> <a id="3005" href="Cubical.Foundations.Transport.html#2972" class="Bound">v</a><a id="3006" class="Symbol">)</a> <a id="3008" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="3010" href="Cubical.Foundations.Transport.html#2972" class="Bound">v</a>
<a id="3012" href="Cubical.Foundations.Transport.html#2879" class="Function">substSubst⁻</a> <a id="3024" class="Symbol">{</a><a id="3025" class="Argument">x</a> <a id="3027" class="Symbol">=</a> <a id="3029" href="Cubical.Foundations.Transport.html#3029" class="Bound">x</a><a id="3030" class="Symbol">}</a> <a id="3032" class="Symbol">{</a><a id="3033" class="Argument">y</a> <a id="3035" class="Symbol">=</a> <a id="3037" href="Cubical.Foundations.Transport.html#3037" class="Bound">y</a><a id="3038" class="Symbol">}</a> <a id="3040" href="Cubical.Foundations.Transport.html#3040" class="Bound">B</a> <a id="3042" href="Cubical.Foundations.Transport.html#3042" class="Bound">p</a> <a id="3044" href="Cubical.Foundations.Transport.html#3044" class="Bound">v</a> <a id="3046" class="Symbol">=</a> <a id="3048" href="Cubical.Foundations.Transport.html#2446" class="Function">transportTransport⁻</a> <a id="3068" class="Symbol">{</a><a id="3069" class="Argument">A</a> <a id="3071" class="Symbol">=</a> <a id="3073" href="Cubical.Foundations.Transport.html#3040" class="Bound">B</a> <a id="3075" href="Cubical.Foundations.Transport.html#3029" class="Bound">x</a><a id="3076" class="Symbol">}</a> <a id="3078" class="Symbol">{</a><a id="3079" class="Argument">B</a> <a id="3081" class="Symbol">=</a> <a id="3083" href="Cubical.Foundations.Transport.html#3040" class="Bound">B</a> <a id="3085" href="Cubical.Foundations.Transport.html#3037" class="Bound">y</a><a id="3086" class="Symbol">}</a> <a id="3088" class="Symbol">(</a><a id="3089" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="3094" href="Cubical.Foundations.Transport.html#3040" class="Bound">B</a> <a id="3096" href="Cubical.Foundations.Transport.html#3042" class="Bound">p</a><a id="3097" class="Symbol">)</a> <a id="3099" href="Cubical.Foundations.Transport.html#3044" class="Bound">v</a>
<a id="substEquiv"></a><a id="3102" href="Cubical.Foundations.Transport.html#3102" class="Function">substEquiv</a> <a id="3113" class="Symbol">:</a> <a id="3115" class="Symbol">∀</a> <a id="3117" class="Symbol">{</a><a id="3118" href="Cubical.Foundations.Transport.html#3118" class="Bound">ℓ</a> <a id="3120" href="Cubical.Foundations.Transport.html#3120" class="Bound">ℓ'</a><a id="3122" class="Symbol">}</a> <a id="3124" class="Symbol">{</a><a id="3125" href="Cubical.Foundations.Transport.html#3125" class="Bound">A</a> <a id="3127" class="Symbol">:</a> <a id="3129" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3134" href="Cubical.Foundations.Transport.html#3118" class="Bound">ℓ</a><a id="3135" class="Symbol">}</a> <a id="3137" class="Symbol">{</a><a id="3138" href="Cubical.Foundations.Transport.html#3138" class="Bound">a</a> <a id="3140" href="Cubical.Foundations.Transport.html#3140" class="Bound">a'</a> <a id="3143" class="Symbol">:</a> <a id="3145" href="Cubical.Foundations.Transport.html#3125" class="Bound">A</a><a id="3146" class="Symbol">}</a> <a id="3148" class="Symbol">(</a><a id="3149" href="Cubical.Foundations.Transport.html#3149" class="Bound">P</a> <a id="3151" class="Symbol">:</a> <a id="3153" href="Cubical.Foundations.Transport.html#3125" class="Bound">A</a> <a id="3155" class="Symbol">→</a> <a id="3157" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3162" href="Cubical.Foundations.Transport.html#3120" class="Bound">ℓ'</a><a id="3164" class="Symbol">)</a> <a id="3166" class="Symbol">(</a><a id="3167" href="Cubical.Foundations.Transport.html#3167" class="Bound">p</a> <a id="3169" class="Symbol">:</a> <a id="3171" href="Cubical.Foundations.Transport.html#3138" class="Bound">a</a> <a id="3173" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="3175" href="Cubical.Foundations.Transport.html#3140" class="Bound">a'</a><a id="3177" class="Symbol">)</a> <a id="3179" class="Symbol">→</a> <a id="3181" href="Cubical.Foundations.Transport.html#3149" class="Bound">P</a> <a id="3183" href="Cubical.Foundations.Transport.html#3138" class="Bound">a</a> <a id="3185" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="3187" href="Cubical.Foundations.Transport.html#3149" class="Bound">P</a> <a id="3189" href="Cubical.Foundations.Transport.html#3140" class="Bound">a'</a>
<a id="3192" href="Cubical.Foundations.Transport.html#3102" class="Function">substEquiv</a> <a id="3203" href="Cubical.Foundations.Transport.html#3203" class="Bound">P</a> <a id="3205" href="Cubical.Foundations.Transport.html#3205" class="Bound">p</a> <a id="3207" class="Symbol">=</a> <a id="3209" class="Symbol">(</a><a id="3210" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="3216" href="Cubical.Foundations.Transport.html#3203" class="Bound">P</a> <a id="3218" href="Cubical.Foundations.Transport.html#3205" class="Bound">p</a> <a id="3220" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3222" href="Cubical.Foundations.Univalence.html#7931" class="Function">isEquivTransport</a> <a id="3239" class="Symbol">(λ</a> <a id="3242" href="Cubical.Foundations.Transport.html#3242" class="Bound">i</a> <a id="3244" class="Symbol">→</a> <a id="3246" href="Cubical.Foundations.Transport.html#3203" class="Bound">P</a> <a id="3248" class="Symbol">(</a><a id="3249" href="Cubical.Foundations.Transport.html#3205" class="Bound">p</a> <a id="3251" href="Cubical.Foundations.Transport.html#3242" class="Bound">i</a><a id="3252" class="Symbol">)))</a>
<a id="liftEquiv"></a><a id="3257" href="Cubical.Foundations.Transport.html#3257" class="Function">liftEquiv</a> <a id="3267" class="Symbol">:</a> <a id="3269" class="Symbol">∀</a> <a id="3271" class="Symbol">{</a><a id="3272" href="Cubical.Foundations.Transport.html#3272" class="Bound">ℓ</a> <a id="3274" href="Cubical.Foundations.Transport.html#3274" class="Bound">ℓ'</a><a id="3276" class="Symbol">}</a> <a id="3278" class="Symbol">{</a><a id="3279" href="Cubical.Foundations.Transport.html#3279" class="Bound">A</a> <a id="3281" href="Cubical.Foundations.Transport.html#3281" class="Bound">B</a> <a id="3283" class="Symbol">:</a> <a id="3285" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3290" href="Cubical.Foundations.Transport.html#3272" class="Bound">ℓ</a><a id="3291" class="Symbol">}</a> <a id="3293" class="Symbol">(</a><a id="3294" href="Cubical.Foundations.Transport.html#3294" class="Bound">P</a> <a id="3296" class="Symbol">:</a> <a id="3298" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3303" href="Cubical.Foundations.Transport.html#3272" class="Bound">ℓ</a> <a id="3305" class="Symbol">→</a> <a id="3307" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3312" href="Cubical.Foundations.Transport.html#3274" class="Bound">ℓ'</a><a id="3314" class="Symbol">)</a> <a id="3316" class="Symbol">(</a><a id="3317" href="Cubical.Foundations.Transport.html#3317" class="Bound">e</a> <a id="3319" class="Symbol">:</a> <a id="3321" href="Cubical.Foundations.Transport.html#3279" class="Bound">A</a> <a id="3323" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="3325" href="Cubical.Foundations.Transport.html#3281" class="Bound">B</a><a id="3326" class="Symbol">)</a> <a id="3328" class="Symbol">→</a> <a id="3330" href="Cubical.Foundations.Transport.html#3294" class="Bound">P</a> <a id="3332" href="Cubical.Foundations.Transport.html#3279" class="Bound">A</a> <a id="3334" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="3336" href="Cubical.Foundations.Transport.html#3294" class="Bound">P</a> <a id="3338" href="Cubical.Foundations.Transport.html#3281" class="Bound">B</a>
<a id="3340" href="Cubical.Foundations.Transport.html#3257" class="Function">liftEquiv</a> <a id="3350" href="Cubical.Foundations.Transport.html#3350" class="Bound">P</a> <a id="3352" href="Cubical.Foundations.Transport.html#3352" class="Bound">e</a> <a id="3354" class="Symbol">=</a> <a id="3356" href="Cubical.Foundations.Transport.html#3102" class="Function">substEquiv</a> <a id="3367" href="Cubical.Foundations.Transport.html#3350" class="Bound">P</a> <a id="3369" class="Symbol">(</a><a id="3370" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="3373" href="Cubical.Foundations.Transport.html#3352" class="Bound">e</a><a id="3374" class="Symbol">)</a>
<a id="transpEquiv"></a><a id="3377" href="Cubical.Foundations.Transport.html#3377" class="Function">transpEquiv</a> <a id="3389" class="Symbol">:</a> <a id="3391" class="Symbol">∀</a> <a id="3393" class="Symbol">{</a><a id="3394" href="Cubical.Foundations.Transport.html#3394" class="Bound">ℓ</a><a id="3395" class="Symbol">}</a> <a id="3397" class="Symbol">{</a><a id="3398" href="Cubical.Foundations.Transport.html#3398" class="Bound">A</a> <a id="3400" href="Cubical.Foundations.Transport.html#3400" class="Bound">B</a> <a id="3402" class="Symbol">:</a> <a id="3404" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3409" href="Cubical.Foundations.Transport.html#3394" class="Bound">ℓ</a><a id="3410" class="Symbol">}</a> <a id="3412" class="Symbol">(</a><a id="3413" href="Cubical.Foundations.Transport.html#3413" class="Bound">p</a> <a id="3415" class="Symbol">:</a> <a id="3417" href="Cubical.Foundations.Transport.html#3398" class="Bound">A</a> <a id="3419" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="3421" href="Cubical.Foundations.Transport.html#3400" class="Bound">B</a><a id="3422" class="Symbol">)</a> <a id="3424" class="Symbol">→</a> <a id="3426" class="Symbol">∀</a> <a id="3428" href="Cubical.Foundations.Transport.html#3428" class="Bound">i</a> <a id="3430" class="Symbol">→</a> <a id="3432" href="Cubical.Foundations.Transport.html#3413" class="Bound">p</a> <a id="3434" href="Cubical.Foundations.Transport.html#3428" class="Bound">i</a> <a id="3436" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="3438" href="Cubical.Foundations.Transport.html#3400" class="Bound">B</a>
<a id="3440" href="Cubical.Foundations.Transport.html#3377" class="Function">transpEquiv</a> <a id="3452" href="Cubical.Foundations.Transport.html#3452" class="Bound">P</a> <a id="3454" href="Cubical.Foundations.Transport.html#3454" class="Bound">i</a> <a id="3456" class="Symbol">.</a><a id="3457" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="3461" class="Symbol">=</a> <a id="3463" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="3470" class="Symbol">(λ</a> <a id="3473" href="Cubical.Foundations.Transport.html#3473" class="Bound">j</a> <a id="3475" class="Symbol">→</a> <a id="3477" href="Cubical.Foundations.Transport.html#3452" class="Bound">P</a> <a id="3479" class="Symbol">(</a><a id="3480" href="Cubical.Foundations.Transport.html#3454" class="Bound">i</a> <a id="3482" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="3484" href="Cubical.Foundations.Transport.html#3473" class="Bound">j</a><a id="3485" class="Symbol">))</a> <a id="3488" href="Cubical.Foundations.Transport.html#3454" class="Bound">i</a>
<a id="3490" href="Cubical.Foundations.Transport.html#3377" class="Function">transpEquiv</a> <a id="3502" href="Cubical.Foundations.Transport.html#3502" class="Bound">P</a> <a id="3504" href="Cubical.Foundations.Transport.html#3504" class="Bound">i</a> <a id="3506" class="Symbol">.</a><a id="3507" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a>
<a id="3513" class="Symbol">=</a> <a id="3515" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="3522" class="Symbol">(λ</a> <a id="3525" href="Cubical.Foundations.Transport.html#3525" class="Bound">k</a> <a id="3527" class="Symbol">→</a> <a id="3529" href="Agda.Builtin.Cubical.Glue.html#868" class="Record">isEquiv</a> <a id="3537" class="Symbol">(</a><a id="3538" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="3545" class="Symbol">(λ</a> <a id="3548" href="Cubical.Foundations.Transport.html#3548" class="Bound">j</a> <a id="3550" class="Symbol">→</a> <a id="3552" href="Cubical.Foundations.Transport.html#3502" class="Bound">P</a> <a id="3554" class="Symbol">(</a><a id="3555" href="Cubical.Foundations.Transport.html#3504" class="Bound">i</a> <a id="3557" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="3559" class="Symbol">(</a><a id="3560" href="Cubical.Foundations.Transport.html#3548" class="Bound">j</a> <a id="3562" href="Cubical.Core.Primitives.html#441" class="Primitive Operator">∧</a> <a id="3564" href="Cubical.Foundations.Transport.html#3525" class="Bound">k</a><a id="3565" class="Symbol">)))</a> <a id="3569" class="Symbol">(</a><a id="3570" href="Cubical.Foundations.Transport.html#3504" class="Bound">i</a> <a id="3572" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="3574" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="3576" href="Cubical.Foundations.Transport.html#3525" class="Bound">k</a><a id="3577" class="Symbol">)))</a>
<a id="3587" href="Cubical.Foundations.Transport.html#3504" class="Bound">i</a> <a id="3589" class="Symbol">(</a><a id="3590" href="Cubical.Foundations.Equiv.Base.html#947" class="Function">idIsEquiv</a> <a id="3600" class="Symbol">(</a><a id="3601" href="Cubical.Foundations.Transport.html#3502" class="Bound">P</a> <a id="3603" href="Cubical.Foundations.Transport.html#3504" class="Bound">i</a><a id="3604" class="Symbol">))</a>
<a id="uaTransportη"></a><a id="3608" href="Cubical.Foundations.Transport.html#3608" class="Function">uaTransportη</a> <a id="3621" class="Symbol">:</a> <a id="3623" class="Symbol">∀</a> <a id="3625" class="Symbol">{</a><a id="3626" href="Cubical.Foundations.Transport.html#3626" class="Bound">ℓ</a><a id="3627" class="Symbol">}</a> <a id="3629" class="Symbol">{</a><a id="3630" href="Cubical.Foundations.Transport.html#3630" class="Bound">A</a> <a id="3632" href="Cubical.Foundations.Transport.html#3632" class="Bound">B</a> <a id="3634" class="Symbol">:</a> <a id="3636" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3641" href="Cubical.Foundations.Transport.html#3626" class="Bound">ℓ</a><a id="3642" class="Symbol">}</a> <a id="3644" class="Symbol">(</a><a id="3645" href="Cubical.Foundations.Transport.html#3645" class="Bound">P</a> <a id="3647" class="Symbol">:</a> <a id="3649" href="Cubical.Foundations.Transport.html#3630" class="Bound">A</a> <a id="3651" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="3653" href="Cubical.Foundations.Transport.html#3632" class="Bound">B</a><a id="3654" class="Symbol">)</a> <a id="3656" class="Symbol">→</a> <a id="3658" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="3661" class="Symbol">(</a><a id="3662" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="3674" href="Cubical.Foundations.Transport.html#3645" class="Bound">P</a><a id="3675" class="Symbol">)</a> <a id="3677" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="3679" href="Cubical.Foundations.Transport.html#3645" class="Bound">P</a>
<a id="3681" href="Cubical.Foundations.Transport.html#3608" class="Function">uaTransportη</a> <a id="3694" href="Cubical.Foundations.Transport.html#3694" class="Bound">P</a> <a id="3696" href="Cubical.Foundations.Transport.html#3696" class="Bound">i</a> <a id="3698" href="Cubical.Foundations.Transport.html#3698" class="Bound">j</a>
<a id="3702" class="Symbol">=</a> <a id="3704" href="Cubical.Core.Glue.html#1521" class="Function">Glue</a> <a id="3709" class="Symbol">(</a><a id="3710" href="Cubical.Foundations.Transport.html#3694" class="Bound">P</a> <a id="3712" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="3714" class="Symbol">)</a> <a id="3716" class="Symbol">λ</a> <a id="3718" class="Keyword">where</a>
<a id="3730" class="Symbol">(</a><a id="3731" href="Cubical.Foundations.Transport.html#3698" class="Bound">j</a> <a id="3733" class="Symbol">=</a> <a id="3735" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="3737" class="Symbol">)</a> <a id="3739" class="Symbol">→</a> <a id="3741" href="Cubical.Foundations.Transport.html#3694" class="Bound">P</a> <a id="3743" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a> <a id="3746" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3748" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="3760" href="Cubical.Foundations.Transport.html#3694" class="Bound">P</a>
<a id="3768" class="Symbol">(</a><a id="3769" href="Cubical.Foundations.Transport.html#3696" class="Bound">i</a> <a id="3771" class="Symbol">=</a> <a id="3773" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="3775" class="Symbol">)</a> <a id="3777" class="Symbol">→</a> <a id="3779" href="Cubical.Foundations.Transport.html#3694" class="Bound">P</a> <a id="3781" href="Cubical.Foundations.Transport.html#3698" class="Bound">j</a> <a id="3783" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3785" href="Cubical.Foundations.Transport.html#3377" class="Function">transpEquiv</a> <a id="3797" href="Cubical.Foundations.Transport.html#3694" class="Bound">P</a> <a id="3799" href="Cubical.Foundations.Transport.html#3698" class="Bound">j</a>
<a id="3807" class="Symbol">(</a><a id="3808" href="Cubical.Foundations.Transport.html#3698" class="Bound">j</a> <a id="3810" class="Symbol">=</a> <a id="3812" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="3814" class="Symbol">)</a> <a id="3816" class="Symbol">→</a> <a id="3818" href="Cubical.Foundations.Transport.html#3694" class="Bound">P</a> <a id="3820" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a> <a id="3823" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3825" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="3833" class="Symbol">(</a><a id="3834" href="Cubical.Foundations.Transport.html#3694" class="Bound">P</a> <a id="3836" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="3838" class="Symbol">)</a>
<a id="pathToIso"></a><a id="3841" href="Cubical.Foundations.Transport.html#3841" class="Function">pathToIso</a> <a id="3851" class="Symbol">:</a> <a id="3853" class="Symbol">∀</a> <a id="3855" class="Symbol">{</a><a id="3856" href="Cubical.Foundations.Transport.html#3856" class="Bound">ℓ</a><a id="3857" class="Symbol">}</a> <a id="3859" class="Symbol">{</a><a id="3860" href="Cubical.Foundations.Transport.html#3860" class="Bound">A</a> <a id="3862" href="Cubical.Foundations.Transport.html#3862" class="Bound">B</a> <a id="3864" class="Symbol">:</a> <a id="3866" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="3871" href="Cubical.Foundations.Transport.html#3856" class="Bound">ℓ</a><a id="3872" class="Symbol">}</a> <a id="3874" class="Symbol">→</a> <a id="3876" href="Cubical.Foundations.Transport.html#3860" class="Bound">A</a> <a id="3878" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="3880" href="Cubical.Foundations.Transport.html#3862" class="Bound">B</a> <a id="3882" class="Symbol">→</a> <a id="3884" href="Cubical.Foundations.Isomorphism.html#773" class="Record">Iso</a> <a id="3888" href="Cubical.Foundations.Transport.html#3860" class="Bound">A</a> <a id="3890" href="Cubical.Foundations.Transport.html#3862" class="Bound">B</a>
<a id="3892" href="Cubical.Foundations.Isomorphism.html#885" class="Field">Iso.fun</a> <a id="3900" class="Symbol">(</a><a id="3901" href="Cubical.Foundations.Transport.html#3841" class="Function">pathToIso</a> <a id="3911" href="Cubical.Foundations.Transport.html#3911" class="Bound">x</a><a id="3912" class="Symbol">)</a> <a id="3914" class="Symbol">=</a> <a id="3916" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="3926" href="Cubical.Foundations.Transport.html#3911" class="Bound">x</a>
<a id="3928" href="Cubical.Foundations.Isomorphism.html#901" class="Field">Iso.inv</a> <a id="3936" class="Symbol">(</a><a id="3937" href="Cubical.Foundations.Transport.html#3841" class="Function">pathToIso</a> <a id="3947" href="Cubical.Foundations.Transport.html#3947" class="Bound">x</a><a id="3948" class="Symbol">)</a> <a id="3950" class="Symbol">=</a> <a id="3952" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="3963" href="Cubical.Foundations.Transport.html#3947" class="Bound">x</a>
<a id="3965" href="Cubical.Foundations.Isomorphism.html#917" class="Field">Iso.rightInv</a> <a id="3978" class="Symbol">(</a><a id="3979" href="Cubical.Foundations.Transport.html#3841" class="Function">pathToIso</a> <a id="3989" href="Cubical.Foundations.Transport.html#3989" class="Bound">x</a><a id="3990" class="Symbol">)</a> <a id="3992" class="Symbol">=</a> <a id="3994" href="Cubical.Foundations.Transport.html#2446" class="Function">transportTransport⁻</a> <a id="4014" href="Cubical.Foundations.Transport.html#3989" class="Bound">x</a>
<a id="4016" href="Cubical.Foundations.Isomorphism.html#948" class="Field">Iso.leftInv</a> <a id="4028" class="Symbol">(</a><a id="4029" href="Cubical.Foundations.Transport.html#3841" class="Function">pathToIso</a> <a id="4039" href="Cubical.Foundations.Transport.html#4039" class="Bound">x</a><a id="4040" class="Symbol">)</a> <a id="4042" class="Symbol">=</a> <a id="4044" href="Cubical.Foundations.Transport.html#2228" class="Function">transport⁻Transport</a> <a id="4064" href="Cubical.Foundations.Transport.html#4039" class="Bound">x</a>
<a id="isInjectiveTransport"></a><a id="4067" href="Cubical.Foundations.Transport.html#4067" class="Function">isInjectiveTransport</a> <a id="4088" class="Symbol">:</a> <a id="4090" class="Symbol">∀</a> <a id="4092" class="Symbol">{</a><a id="4093" href="Cubical.Foundations.Transport.html#4093" class="Bound">ℓ</a> <a id="4095" class="Symbol">:</a> <a id="4097" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="4102" class="Symbol">}</a> <a id="4104" class="Symbol">{</a><a id="4105" href="Cubical.Foundations.Transport.html#4105" class="Bound">A</a> <a id="4107" href="Cubical.Foundations.Transport.html#4107" class="Bound">B</a> <a id="4109" class="Symbol">:</a> <a id="4111" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="4116" href="Cubical.Foundations.Transport.html#4093" class="Bound">ℓ</a><a id="4117" class="Symbol">}</a> <a id="4119" class="Symbol">{</a><a id="4120" href="Cubical.Foundations.Transport.html#4120" class="Bound">p</a> <a id="4122" href="Cubical.Foundations.Transport.html#4122" class="Bound">q</a> <a id="4124" class="Symbol">:</a> <a id="4126" href="Cubical.Foundations.Transport.html#4105" class="Bound">A</a> <a id="4128" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="4130" href="Cubical.Foundations.Transport.html#4107" class="Bound">B</a><a id="4131" class="Symbol">}</a>
<a id="4135" class="Symbol">→</a> <a id="4137" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="4147" href="Cubical.Foundations.Transport.html#4120" class="Bound">p</a> <a id="4149" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="4151" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="4161" href="Cubical.Foundations.Transport.html#4122" class="Bound">q</a> <a id="4163" class="Symbol">→</a> <a id="4165" href="Cubical.Foundations.Transport.html#4120" class="Bound">p</a> <a id="4167" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="4169" href="Cubical.Foundations.Transport.html#4122" class="Bound">q</a>
<a id="4171" href="Cubical.Foundations.Transport.html#4067" class="Function">isInjectiveTransport</a> <a id="4192" class="Symbol">{</a><a id="4193" class="Argument">p</a> <a id="4195" class="Symbol">=</a> <a id="4197" href="Cubical.Foundations.Transport.html#4197" class="Bound">p</a><a id="4198" class="Symbol">}</a> <a id="4200" class="Symbol">{</a><a id="4201" href="Cubical.Foundations.Transport.html#4201" class="Bound">q</a><a id="4202" class="Symbol">}</a> <a id="4204" href="Cubical.Foundations.Transport.html#4204" class="Bound">α</a> <a id="4206" href="Cubical.Foundations.Transport.html#4206" class="Bound">i</a> <a id="4208" class="Symbol">=</a>
<a id="4212" href="Cubical.Core.Primitives.html#657" class="Primitive">hcomp</a>
<a id="4222" class="Symbol">(λ</a> <a id="4225" href="Cubical.Foundations.Transport.html#4225" class="Bound">j</a> <a id="4227" class="Symbol">→</a> <a id="4229" class="Symbol">λ</a>
<a id="4237" class="Symbol">{</a> <a id="4239" class="Symbol">(</a><a id="4240" href="Cubical.Foundations.Transport.html#4206" class="Bound">i</a> <a id="4242" class="Symbol">=</a> <a id="4244" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="4246" class="Symbol">)</a> <a id="4248" class="Symbol">→</a> <a id="4250" href="Cubical.Foundations.Equiv.html#2971" class="Function">retEq</a> <a id="4256" href="Cubical.Foundations.Univalence.html#8739" class="Function">univalence</a> <a id="4267" href="Cubical.Foundations.Transport.html#4197" class="Bound">p</a> <a id="4269" href="Cubical.Foundations.Transport.html#4225" class="Bound">j</a>
<a id="4277" class="Symbol">;</a> <a id="4279" class="Symbol">(</a><a id="4280" href="Cubical.Foundations.Transport.html#4206" class="Bound">i</a> <a id="4282" class="Symbol">=</a> <a id="4284" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="4286" class="Symbol">)</a> <a id="4288" class="Symbol">→</a> <a id="4290" href="Cubical.Foundations.Equiv.html#2971" class="Function">retEq</a> <a id="4296" href="Cubical.Foundations.Univalence.html#8739" class="Function">univalence</a> <a id="4307" href="Cubical.Foundations.Transport.html#4201" class="Bound">q</a> <a id="4309" href="Cubical.Foundations.Transport.html#4225" class="Bound">j</a>
<a id="4317" class="Symbol">})</a>
<a id="4324" class="Symbol">(</a><a id="4325" href="Cubical.Foundations.Equiv.html#2928" class="Function">invEq</a> <a id="4331" href="Cubical.Foundations.Univalence.html#8739" class="Function">univalence</a> <a id="4342" class="Symbol">((λ</a> <a id="4346" href="Cubical.Foundations.Transport.html#4346" class="Bound">a</a> <a id="4348" class="Symbol">→</a> <a id="4350" href="Cubical.Foundations.Transport.html#4204" class="Bound">α</a> <a id="4352" href="Cubical.Foundations.Transport.html#4206" class="Bound">i</a> <a id="4354" href="Cubical.Foundations.Transport.html#4346" class="Bound">a</a><a id="4355" class="Symbol">)</a> <a id="4357" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="4359" href="Cubical.Foundations.Transport.html#4375" class="Function">t</a> <a id="4361" href="Cubical.Foundations.Transport.html#4206" class="Bound">i</a><a id="4362" class="Symbol">))</a>
<a id="4367" class="Keyword">where</a>
<a id="4375" href="Cubical.Foundations.Transport.html#4375" class="Function">t</a> <a id="4377" class="Symbol">:</a> <a id="4379" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="4385" class="Symbol">(λ</a> <a id="4388" href="Cubical.Foundations.Transport.html#4388" class="Bound">i</a> <a id="4390" class="Symbol">→</a> <a id="4392" href="Agda.Builtin.Cubical.Glue.html#868" class="Record">isEquiv</a> <a id="4400" class="Symbol">(λ</a> <a id="4403" href="Cubical.Foundations.Transport.html#4403" class="Bound">a</a> <a id="4405" class="Symbol">→</a> <a id="4407" href="Cubical.Foundations.Transport.html#4204" class="Bound">α</a> <a id="4409" href="Cubical.Foundations.Transport.html#4388" class="Bound">i</a> <a id="4411" href="Cubical.Foundations.Transport.html#4403" class="Bound">a</a><a id="4412" class="Symbol">))</a> <a id="4415" class="Symbol">(</a><a id="4416" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="4428" href="Cubical.Foundations.Transport.html#4197" class="Bound">p</a> <a id="4430" class="Symbol">.</a><a id="4431" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a><a id="4434" class="Symbol">)</a> <a id="4436" class="Symbol">(</a><a id="4437" href="Cubical.Foundations.Univalence.html#8098" class="Function">pathToEquiv</a> <a id="4449" href="Cubical.Foundations.Transport.html#4201" class="Bound">q</a> <a id="4451" class="Symbol">.</a><a id="4452" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a><a id="4455" class="Symbol">)</a>
<a id="4459" href="Cubical.Foundations.Transport.html#4375" class="Function">t</a> <a id="4461" class="Symbol">=</a> <a id="4463" href="Cubical.Foundations.Prelude.html#17730" class="Function">isProp→PathP</a> <a id="4476" class="Symbol">(λ</a> <a id="4479" href="Cubical.Foundations.Transport.html#4479" class="Bound">i</a> <a id="4481" class="Symbol">→</a> <a id="4483" href="Cubical.Foundations.Equiv.html#1548" class="Function">isPropIsEquiv</a> <a id="4497" class="Symbol">(λ</a> <a id="4500" href="Cubical.Foundations.Transport.html#4500" class="Bound">a</a> <a id="4502" class="Symbol">→</a> <a id="4504" href="Cubical.Foundations.Transport.html#4204" class="Bound">α</a> <a id="4506" href="Cubical.Foundations.Transport.html#4479" class="Bound">i</a> <a id="4508" href="Cubical.Foundations.Transport.html#4500" class="Bound">a</a><a id="4509" class="Symbol">))</a> <a id="4512" class="Symbol">_</a> <a id="4514" class="Symbol">_</a>
<a id="transportUaInv"></a><a id="4517" href="Cubical.Foundations.Transport.html#4517" class="Function">transportUaInv</a> <a id="4532" class="Symbol">:</a> <a id="4534" class="Symbol">∀</a> <a id="4536" class="Symbol">{</a><a id="4537" href="Cubical.Foundations.Transport.html#4537" class="Bound">ℓ</a><a id="4538" class="Symbol">}</a> <a id="4540" class="Symbol">{</a><a id="4541" href="Cubical.Foundations.Transport.html#4541" class="Bound">A</a> <a id="4543" href="Cubical.Foundations.Transport.html#4543" class="Bound">B</a> <a id="4545" class="Symbol">:</a> <a id="4547" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="4552" href="Cubical.Foundations.Transport.html#4537" class="Bound">ℓ</a><a id="4553" class="Symbol">}</a> <a id="4555" class="Symbol">(</a><a id="4556" href="Cubical.Foundations.Transport.html#4556" class="Bound">e</a> <a id="4558" class="Symbol">:</a> <a id="4560" href="Cubical.Foundations.Transport.html#4541" class="Bound">A</a> <a id="4562" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="4564" href="Cubical.Foundations.Transport.html#4543" class="Bound">B</a><a id="4565" class="Symbol">)</a> <a id="4567" class="Symbol">→</a> <a id="4569" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="4579" class="Symbol">(</a><a id="4580" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="4583" class="Symbol">(</a><a id="4584" href="Cubical.Foundations.Equiv.html#3368" class="Function">invEquiv</a> <a id="4593" href="Cubical.Foundations.Transport.html#4556" class="Bound">e</a><a id="4594" class="Symbol">))</a> <a id="4597" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="4599" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="4609" class="Symbol">(</a><a id="4610" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="4614" class="Symbol">(</a><a id="4615" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="4618" href="Cubical.Foundations.Transport.html#4556" class="Bound">e</a><a id="4619" class="Symbol">))</a>
<a id="4622" href="Cubical.Foundations.Transport.html#4517" class="Function">transportUaInv</a> <a id="4637" href="Cubical.Foundations.Transport.html#4637" class="Bound">e</a> <a id="4639" class="Symbol">=</a> <a id="4641" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="4646" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="4656" class="Symbol">(</a><a id="4657" href="Cubical.Foundations.Univalence.html#12765" class="Function">uaInvEquiv</a> <a id="4668" href="Cubical.Foundations.Transport.html#4637" class="Bound">e</a><a id="4669" class="Symbol">)</a>
<a id="4671" class="Comment">-- notice that transport (ua e) would reduce, thus an alternative definition using EquivJ can give</a>
<a id="4770" class="Comment">-- refl for the case of idEquiv:</a>
<a id="4803" class="Comment">-- transportUaInv e = EquivJ (λ _ e → transport (ua (invEquiv e)) ≡ transport (sym (ua e))) refl e</a>
<a id="isSet-subst"></a><a id="4903" href="Cubical.Foundations.Transport.html#4903" class="Function">isSet-subst</a> <a id="4915" class="Symbol">:</a> <a id="4917" class="Symbol">∀</a> <a id="4919" class="Symbol">{</a><a id="4920" href="Cubical.Foundations.Transport.html#4920" class="Bound">ℓ</a> <a id="4922" href="Cubical.Foundations.Transport.html#4922" class="Bound">ℓ'</a><a id="4924" class="Symbol">}</a> <a id="4926" class="Symbol">{</a><a id="4927" href="Cubical.Foundations.Transport.html#4927" class="Bound">A</a> <a id="4929" class="Symbol">:</a> <a id="4931" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="4936" href="Cubical.Foundations.Transport.html#4920" class="Bound">ℓ</a><a id="4937" class="Symbol">}</a> <a id="4939" class="Symbol">{</a><a id="4940" href="Cubical.Foundations.Transport.html#4940" class="Bound">B</a> <a id="4942" class="Symbol">:</a> <a id="4944" href="Cubical.Foundations.Transport.html#4927" class="Bound">A</a> <a id="4946" class="Symbol">→</a> <a id="4948" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="4953" href="Cubical.Foundations.Transport.html#4922" class="Bound">ℓ'</a><a id="4955" class="Symbol">}</a>
<a id="4973" class="Symbol">→</a> <a id="4975" class="Symbol">(</a><a id="4976" href="Cubical.Foundations.Transport.html#4976" class="Bound">isSet-A</a> <a id="4984" class="Symbol">:</a> <a id="4986" href="Cubical.Foundations.Prelude.html#14094" class="Function">isSet</a> <a id="4992" href="Cubical.Foundations.Transport.html#4927" class="Bound">A</a><a id="4993" class="Symbol">)</a>
<a id="5011" class="Symbol">→</a> <a id="5013" class="Symbol">∀</a> <a id="5015" class="Symbol">{</a><a id="5016" href="Cubical.Foundations.Transport.html#5016" class="Bound">a</a> <a id="5018" class="Symbol">:</a> <a id="5020" href="Cubical.Foundations.Transport.html#4927" class="Bound">A</a><a id="5021" class="Symbol">}</a>
<a id="5039" class="Symbol">→</a> <a id="5041" class="Symbol">(</a><a id="5042" href="Cubical.Foundations.Transport.html#5042" class="Bound">p</a> <a id="5044" class="Symbol">:</a> <a id="5046" href="Cubical.Foundations.Transport.html#5016" class="Bound">a</a> <a id="5048" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="5050" href="Cubical.Foundations.Transport.html#5016" class="Bound">a</a><a id="5051" class="Symbol">)</a> <a id="5053" class="Symbol">→</a> <a id="5055" class="Symbol">(</a><a id="5056" href="Cubical.Foundations.Transport.html#5056" class="Bound">x</a> <a id="5058" class="Symbol">:</a> <a id="5060" href="Cubical.Foundations.Transport.html#4940" class="Bound">B</a> <a id="5062" href="Cubical.Foundations.Transport.html#5016" class="Bound">a</a><a id="5063" class="Symbol">)</a> <a id="5065" class="Symbol">→</a> <a id="5067" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="5073" href="Cubical.Foundations.Transport.html#4940" class="Bound">B</a> <a id="5075" href="Cubical.Foundations.Transport.html#5042" class="Bound">p</a> <a id="5077" href="Cubical.Foundations.Transport.html#5056" class="Bound">x</a> <a id="5079" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="5081" href="Cubical.Foundations.Transport.html#5056" class="Bound">x</a>
<a id="5083" href="Cubical.Foundations.Transport.html#4903" class="Function">isSet-subst</a> <a id="5095" class="Symbol">{</a><a id="5096" class="Argument">B</a> <a id="5098" class="Symbol">=</a> <a id="5100" href="Cubical.Foundations.Transport.html#5100" class="Bound">B</a><a id="5101" class="Symbol">}</a> <a id="5103" href="Cubical.Foundations.Transport.html#5103" class="Bound">isSet-A</a> <a id="5111" href="Cubical.Foundations.Transport.html#5111" class="Bound">p</a> <a id="5113" href="Cubical.Foundations.Transport.html#5113" class="Bound">x</a> <a id="5115" class="Symbol">=</a> <a id="5117" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="5123" class="Symbol">(λ</a> <a id="5126" href="Cubical.Foundations.Transport.html#5126" class="Bound">p′</a> <a id="5129" class="Symbol">→</a> <a id="5131" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="5137" href="Cubical.Foundations.Transport.html#5100" class="Bound">B</a> <a id="5139" href="Cubical.Foundations.Transport.html#5126" class="Bound">p′</a> <a id="5142" href="Cubical.Foundations.Transport.html#5113" class="Bound">x</a> <a id="5144" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="5146" href="Cubical.Foundations.Transport.html#5113" class="Bound">x</a><a id="5147" class="Symbol">)</a> <a id="5149" class="Symbol">(</a><a id="5150" href="Cubical.Foundations.Transport.html#5103" class="Bound">isSet-A</a> <a id="5158" class="Symbol">_</a> <a id="5160" class="Symbol">_</a> <a id="5162" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="5167" href="Cubical.Foundations.Transport.html#5111" class="Bound">p</a><a id="5168" class="Symbol">)</a> <a id="5170" class="Symbol">(</a><a id="5171" href="Cubical.Foundations.Prelude.html#9390" class="Function">substRefl</a> <a id="5181" class="Symbol">{</a><a id="5182" class="Argument">B</a> <a id="5184" class="Symbol">=</a> <a id="5186" href="Cubical.Foundations.Transport.html#5100" class="Bound">B</a><a id="5187" class="Symbol">}</a> <a id="5189" href="Cubical.Foundations.Transport.html#5113" class="Bound">x</a><a id="5190" class="Symbol">)</a>
<a id="5193" class="Comment">-- substituting along a composite path is equivalent to substituting twice</a>
<a id="substComposite"></a><a id="5268" href="Cubical.Foundations.Transport.html#5268" class="Function">substComposite</a> <a id="5283" class="Symbol">:</a> <a id="5285" class="Symbol">∀</a> <a id="5287" class="Symbol">{</a><a id="5288" href="Cubical.Foundations.Transport.html#5288" class="Bound">ℓ</a> <a id="5290" href="Cubical.Foundations.Transport.html#5290" class="Bound">ℓ'</a><a id="5292" class="Symbol">}</a> <a id="5294" class="Symbol">{</a><a id="5295" href="Cubical.Foundations.Transport.html#5295" class="Bound">A</a> <a id="5297" class="Symbol">:</a> <a id="5299" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5304" href="Cubical.Foundations.Transport.html#5288" class="Bound">ℓ</a><a id="5305" class="Symbol">}</a> <a id="5307" class="Symbol">→</a> <a id="5309" class="Symbol">(</a><a id="5310" href="Cubical.Foundations.Transport.html#5310" class="Bound">B</a> <a id="5312" class="Symbol">:</a> <a id="5314" href="Cubical.Foundations.Transport.html#5295" class="Bound">A</a> <a id="5316" class="Symbol">→</a> <a id="5318" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5323" href="Cubical.Foundations.Transport.html#5290" class="Bound">ℓ'</a><a id="5325" class="Symbol">)</a>
<a id="5344" class="Symbol">→</a> <a id="5346" class="Symbol">{</a><a id="5347" href="Cubical.Foundations.Transport.html#5347" class="Bound">x</a> <a id="5349" href="Cubical.Foundations.Transport.html#5349" class="Bound">y</a> <a id="5351" href="Cubical.Foundations.Transport.html#5351" class="Bound">z</a> <a id="5353" class="Symbol">:</a> <a id="5355" href="Cubical.Foundations.Transport.html#5295" class="Bound">A</a><a id="5356" class="Symbol">}</a> <a id="5358" class="Symbol">(</a><a id="5359" href="Cubical.Foundations.Transport.html#5359" class="Bound">p</a> <a id="5361" class="Symbol">:</a> <a id="5363" href="Cubical.Foundations.Transport.html#5347" class="Bound">x</a> <a id="5365" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="5367" href="Cubical.Foundations.Transport.html#5349" class="Bound">y</a><a id="5368" class="Symbol">)</a> <a id="5370" class="Symbol">(</a><a id="5371" href="Cubical.Foundations.Transport.html#5371" class="Bound">q</a> <a id="5373" class="Symbol">:</a> <a id="5375" href="Cubical.Foundations.Transport.html#5349" class="Bound">y</a> <a id="5377" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="5379" href="Cubical.Foundations.Transport.html#5351" class="Bound">z</a><a id="5380" class="Symbol">)</a> <a id="5382" class="Symbol">(</a><a id="5383" href="Cubical.Foundations.Transport.html#5383" class="Bound">u</a> <a id="5385" class="Symbol">:</a> <a id="5387" href="Cubical.Foundations.Transport.html#5310" class="Bound">B</a> <a id="5389" href="Cubical.Foundations.Transport.html#5347" class="Bound">x</a><a id="5390" class="Symbol">)</a>
<a id="5409" class="Symbol">→</a> <a id="5411" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="5417" href="Cubical.Foundations.Transport.html#5310" class="Bound">B</a> <a id="5419" class="Symbol">(</a><a id="5420" href="Cubical.Foundations.Transport.html#5359" class="Bound">p</a> <a id="5422" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="5424" href="Cubical.Foundations.Transport.html#5371" class="Bound">q</a><a id="5425" class="Symbol">)</a> <a id="5427" href="Cubical.Foundations.Transport.html#5383" class="Bound">u</a> <a id="5429" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="5431" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="5437" href="Cubical.Foundations.Transport.html#5310" class="Bound">B</a> <a id="5439" href="Cubical.Foundations.Transport.html#5371" class="Bound">q</a> <a id="5441" class="Symbol">(</a><a id="5442" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="5448" href="Cubical.Foundations.Transport.html#5310" class="Bound">B</a> <a id="5450" href="Cubical.Foundations.Transport.html#5359" class="Bound">p</a> <a id="5452" href="Cubical.Foundations.Transport.html#5383" class="Bound">u</a><a id="5453" class="Symbol">)</a>
<a id="5455" href="Cubical.Foundations.Transport.html#5268" class="Function">substComposite</a> <a id="5470" href="Cubical.Foundations.Transport.html#5470" class="Bound">B</a> <a id="5472" href="Cubical.Foundations.Transport.html#5472" class="Bound">p</a> <a id="5474" href="Cubical.Foundations.Transport.html#5474" class="Bound">q</a> <a id="5476" href="Cubical.Foundations.Transport.html#5476" class="Bound">Bx</a> <a id="5479" href="Cubical.Foundations.Transport.html#5479" class="Bound">i</a> <a id="5481" class="Symbol">=</a>
<a id="5485" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="5495" class="Symbol">(</a><a id="5496" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="5501" href="Cubical.Foundations.Transport.html#5470" class="Bound">B</a> <a id="5503" class="Symbol">(</a><a id="5504" href="Cubical.Foundations.Prelude.html#4950" class="Function">compPath-filler'</a> <a id="5521" href="Cubical.Foundations.Transport.html#5472" class="Bound">p</a> <a id="5523" href="Cubical.Foundations.Transport.html#5474" class="Bound">q</a> <a id="5525" class="Symbol">(</a><a id="5526" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="5528" href="Cubical.Foundations.Transport.html#5479" class="Bound">i</a><a id="5529" class="Symbol">)))</a> <a id="5533" class="Symbol">(</a><a id="5534" href="Cubical.Foundations.Transport.html#1303" class="Function">transport-fillerExt</a> <a id="5554" class="Symbol">(</a><a id="5555" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="5560" href="Cubical.Foundations.Transport.html#5470" class="Bound">B</a> <a id="5562" href="Cubical.Foundations.Transport.html#5472" class="Bound">p</a><a id="5563" class="Symbol">)</a> <a id="5565" href="Cubical.Foundations.Transport.html#5479" class="Bound">i</a> <a id="5567" href="Cubical.Foundations.Transport.html#5476" class="Bound">Bx</a><a id="5569" class="Symbol">)</a>
<a id="5572" class="Comment">-- transporting along a composite path is equivalent to transporting twice</a>
<a id="transportComposite"></a><a id="5647" href="Cubical.Foundations.Transport.html#5647" class="Function">transportComposite</a> <a id="5666" class="Symbol">:</a> <a id="5668" class="Symbol">∀</a> <a id="5670" class="Symbol">{</a><a id="5671" href="Cubical.Foundations.Transport.html#5671" class="Bound">ℓ</a><a id="5672" class="Symbol">}</a> <a id="5674" class="Symbol">{</a><a id="5675" href="Cubical.Foundations.Transport.html#5675" class="Bound">A</a> <a id="5677" href="Cubical.Foundations.Transport.html#5677" class="Bound">B</a> <a id="5679" href="Cubical.Foundations.Transport.html#5679" class="Bound">C</a> <a id="5681" class="Symbol">:</a> <a id="5683" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5688" href="Cubical.Foundations.Transport.html#5671" class="Bound">ℓ</a><a id="5689" class="Symbol">}</a> <a id="5691" class="Symbol">(</a><a id="5692" href="Cubical.Foundations.Transport.html#5692" class="Bound">p</a> <a id="5694" class="Symbol">:</a> <a id="5696" href="Cubical.Foundations.Transport.html#5675" class="Bound">A</a> <a id="5698" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="5700" href="Cubical.Foundations.Transport.html#5677" class="Bound">B</a><a id="5701" class="Symbol">)</a> <a id="5703" class="Symbol">(</a><a id="5704" href="Cubical.Foundations.Transport.html#5704" class="Bound">q</a> <a id="5706" class="Symbol">:</a> <a id="5708" href="Cubical.Foundations.Transport.html#5677" class="Bound">B</a> <a id="5710" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="5712" href="Cubical.Foundations.Transport.html#5679" class="Bound">C</a><a id="5713" class="Symbol">)</a> <a id="5715" class="Symbol">(</a><a id="5716" href="Cubical.Foundations.Transport.html#5716" class="Bound">x</a> <a id="5718" class="Symbol">:</a> <a id="5720" href="Cubical.Foundations.Transport.html#5675" class="Bound">A</a><a id="5721" class="Symbol">)</a>
<a id="5740" class="Symbol">→</a> <a id="5742" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="5752" class="Symbol">(</a><a id="5753" href="Cubical.Foundations.Transport.html#5692" class="Bound">p</a> <a id="5755" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="5757" href="Cubical.Foundations.Transport.html#5704" class="Bound">q</a><a id="5758" class="Symbol">)</a> <a id="5760" href="Cubical.Foundations.Transport.html#5716" class="Bound">x</a> <a id="5762" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="5764" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="5774" href="Cubical.Foundations.Transport.html#5704" class="Bound">q</a> <a id="5776" class="Symbol">(</a><a id="5777" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="5787" href="Cubical.Foundations.Transport.html#5692" class="Bound">p</a> <a id="5789" href="Cubical.Foundations.Transport.html#5716" class="Bound">x</a><a id="5790" class="Symbol">)</a>
<a id="5792" href="Cubical.Foundations.Transport.html#5647" class="Function">transportComposite</a> <a id="5811" class="Symbol">=</a> <a id="5813" href="Cubical.Foundations.Transport.html#5268" class="Function">substComposite</a> <a id="5828" class="Symbol">(λ</a> <a id="5831" href="Cubical.Foundations.Transport.html#5831" class="Bound">D</a> <a id="5833" class="Symbol">→</a> <a id="5835" href="Cubical.Foundations.Transport.html#5831" class="Bound">D</a><a id="5836" class="Symbol">)</a>
<a id="5839" class="Comment">-- substitution commutes with morphisms in slices</a>
<a id="substCommSlice"></a><a id="5889" href="Cubical.Foundations.Transport.html#5889" class="Function">substCommSlice</a> <a id="5904" class="Symbol">:</a> <a id="5906" class="Symbol">∀</a> <a id="5908" class="Symbol">{</a><a id="5909" href="Cubical.Foundations.Transport.html#5909" class="Bound">ℓ</a> <a id="5911" href="Cubical.Foundations.Transport.html#5911" class="Bound">ℓ'</a> <a id="5914" href="Cubical.Foundations.Transport.html#5914" class="Bound">ℓ''</a><a id="5917" class="Symbol">}</a> <a id="5919" class="Symbol">{</a><a id="5920" href="Cubical.Foundations.Transport.html#5920" class="Bound">A</a> <a id="5922" class="Symbol">:</a> <a id="5924" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5929" href="Cubical.Foundations.Transport.html#5909" class="Bound">ℓ</a><a id="5930" class="Symbol">}</a>
<a id="5951" class="Symbol">→</a> <a id="5953" class="Symbol">(</a><a id="5954" href="Cubical.Foundations.Transport.html#5954" class="Bound">B</a> <a id="5956" class="Symbol">:</a> <a id="5958" href="Cubical.Foundations.Transport.html#5920" class="Bound">A</a> <a id="5960" class="Symbol">→</a> <a id="5962" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5967" href="Cubical.Foundations.Transport.html#5911" class="Bound">ℓ'</a><a id="5969" class="Symbol">)</a> <a id="5971" class="Symbol">(</a><a id="5972" href="Cubical.Foundations.Transport.html#5972" class="Bound">C</a> <a id="5974" class="Symbol">:</a> <a id="5976" href="Cubical.Foundations.Transport.html#5920" class="Bound">A</a> <a id="5978" class="Symbol">→</a> <a id="5980" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="5985" href="Cubical.Foundations.Transport.html#5914" class="Bound">ℓ''</a><a id="5988" class="Symbol">)</a>
<a id="6009" class="Symbol">→</a> <a id="6011" class="Symbol">(</a><a id="6012" href="Cubical.Foundations.Transport.html#6012" class="Bound">F</a> <a id="6014" class="Symbol">:</a> <a id="6016" class="Symbol">∀</a> <a id="6018" href="Cubical.Foundations.Transport.html#6018" class="Bound">a</a> <a id="6020" class="Symbol">→</a> <a id="6022" href="Cubical.Foundations.Transport.html#5954" class="Bound">B</a> <a id="6024" href="Cubical.Foundations.Transport.html#6018" class="Bound">a</a> <a id="6026" class="Symbol">→</a> <a id="6028" href="Cubical.Foundations.Transport.html#5972" class="Bound">C</a> <a id="6030" href="Cubical.Foundations.Transport.html#6018" class="Bound">a</a><a id="6031" class="Symbol">)</a>
<a id="6052" class="Symbol">→</a> <a id="6054" class="Symbol">{</a><a id="6055" href="Cubical.Foundations.Transport.html#6055" class="Bound">x</a> <a id="6057" href="Cubical.Foundations.Transport.html#6057" class="Bound">y</a> <a id="6059" class="Symbol">:</a> <a id="6061" href="Cubical.Foundations.Transport.html#5920" class="Bound">A</a><a id="6062" class="Symbol">}</a> <a id="6064" class="Symbol">(</a><a id="6065" href="Cubical.Foundations.Transport.html#6065" class="Bound">p</a> <a id="6067" class="Symbol">:</a> <a id="6069" href="Cubical.Foundations.Transport.html#6055" class="Bound">x</a> <a id="6071" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="6073" href="Cubical.Foundations.Transport.html#6057" class="Bound">y</a><a id="6074" class="Symbol">)</a> <a id="6076" class="Symbol">(</a><a id="6077" href="Cubical.Foundations.Transport.html#6077" class="Bound">u</a> <a id="6079" class="Symbol">:</a> <a id="6081" href="Cubical.Foundations.Transport.html#5954" class="Bound">B</a> <a id="6083" href="Cubical.Foundations.Transport.html#6055" class="Bound">x</a><a id="6084" class="Symbol">)</a>
<a id="6105" class="Symbol">→</a> <a id="6107" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="6113" href="Cubical.Foundations.Transport.html#5972" class="Bound">C</a> <a id="6115" href="Cubical.Foundations.Transport.html#6065" class="Bound">p</a> <a id="6117" class="Symbol">(</a><a id="6118" href="Cubical.Foundations.Transport.html#6012" class="Bound">F</a> <a id="6120" href="Cubical.Foundations.Transport.html#6055" class="Bound">x</a> <a id="6122" href="Cubical.Foundations.Transport.html#6077" class="Bound">u</a><a id="6123" class="Symbol">)</a> <a id="6125" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="6127" href="Cubical.Foundations.Transport.html#6012" class="Bound">F</a> <a id="6129" href="Cubical.Foundations.Transport.html#6057" class="Bound">y</a> <a id="6131" class="Symbol">(</a><a id="6132" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="6138" href="Cubical.Foundations.Transport.html#5954" class="Bound">B</a> <a id="6140" href="Cubical.Foundations.Transport.html#6065" class="Bound">p</a> <a id="6142" href="Cubical.Foundations.Transport.html#6077" class="Bound">u</a><a id="6143" class="Symbol">)</a>
<a id="6145" href="Cubical.Foundations.Transport.html#5889" class="Function">substCommSlice</a> <a id="6160" href="Cubical.Foundations.Transport.html#6160" class="Bound">B</a> <a id="6162" href="Cubical.Foundations.Transport.html#6162" class="Bound">C</a> <a id="6164" href="Cubical.Foundations.Transport.html#6164" class="Bound">F</a> <a id="6166" href="Cubical.Foundations.Transport.html#6166" class="Bound">p</a> <a id="6168" href="Cubical.Foundations.Transport.html#6168" class="Bound">Bx</a> <a id="6171" href="Cubical.Foundations.Transport.html#6171" class="Bound">a</a> <a id="6173" class="Symbol">=</a>
<a id="6177" href="Cubical.Foundations.Transport.html#1669" class="Function">transport-fillerExt⁻</a> <a id="6198" class="Symbol">(</a><a id="6199" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="6204" href="Cubical.Foundations.Transport.html#6162" class="Bound">C</a> <a id="6206" href="Cubical.Foundations.Transport.html#6166" class="Bound">p</a><a id="6207" class="Symbol">)</a> <a id="6209" href="Cubical.Foundations.Transport.html#6171" class="Bound">a</a> <a id="6211" class="Symbol">(</a><a id="6212" href="Cubical.Foundations.Transport.html#6164" class="Bound">F</a> <a id="6214" class="Symbol">_</a> <a id="6216" class="Symbol">(</a><a id="6217" href="Cubical.Foundations.Transport.html#1303" class="Function">transport-fillerExt</a> <a id="6237" class="Symbol">(</a><a id="6238" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="6243" href="Cubical.Foundations.Transport.html#6160" class="Bound">B</a> <a id="6245" href="Cubical.Foundations.Transport.html#6166" class="Bound">p</a><a id="6246" class="Symbol">)</a> <a id="6248" href="Cubical.Foundations.Transport.html#6171" class="Bound">a</a> <a id="6250" href="Cubical.Foundations.Transport.html#6168" class="Bound">Bx</a><a id="6252" class="Symbol">))</a>
<a id="constSubstCommSlice"></a><a id="6256" href="Cubical.Foundations.Transport.html#6256" class="Function">constSubstCommSlice</a> <a id="6276" class="Symbol">:</a> <a id="6278" class="Symbol">∀</a> <a id="6280" class="Symbol">{</a><a id="6281" href="Cubical.Foundations.Transport.html#6281" class="Bound">ℓ</a> <a id="6283" href="Cubical.Foundations.Transport.html#6283" class="Bound">ℓ'</a> <a id="6286" href="Cubical.Foundations.Transport.html#6286" class="Bound">ℓ''</a><a id="6289" class="Symbol">}</a> <a id="6291" class="Symbol">{</a><a id="6292" href="Cubical.Foundations.Transport.html#6292" class="Bound">A</a> <a id="6294" class="Symbol">:</a> <a id="6296" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6301" href="Cubical.Foundations.Transport.html#6281" class="Bound">ℓ</a><a id="6302" class="Symbol">}</a>
<a id="6323" class="Symbol">→</a> <a id="6325" class="Symbol">(</a><a id="6326" href="Cubical.Foundations.Transport.html#6326" class="Bound">B</a> <a id="6328" class="Symbol">:</a> <a id="6330" href="Cubical.Foundations.Transport.html#6292" class="Bound">A</a> <a id="6332" class="Symbol">→</a> <a id="6334" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6339" href="Cubical.Foundations.Transport.html#6283" class="Bound">ℓ'</a><a id="6341" class="Symbol">)</a>
<a id="6362" class="Symbol">→</a> <a id="6364" class="Symbol">(</a><a id="6365" href="Cubical.Foundations.Transport.html#6365" class="Bound">C</a> <a id="6367" class="Symbol">:</a> <a id="6369" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6374" href="Cubical.Foundations.Transport.html#6286" class="Bound">ℓ''</a><a id="6377" class="Symbol">)</a>
<a id="6398" class="Symbol">→</a> <a id="6400" class="Symbol">(</a><a id="6401" href="Cubical.Foundations.Transport.html#6401" class="Bound">F</a> <a id="6403" class="Symbol">:</a> <a id="6405" class="Symbol">∀</a> <a id="6407" href="Cubical.Foundations.Transport.html#6407" class="Bound">a</a> <a id="6409" class="Symbol">→</a> <a id="6411" href="Cubical.Foundations.Transport.html#6326" class="Bound">B</a> <a id="6413" href="Cubical.Foundations.Transport.html#6407" class="Bound">a</a> <a id="6415" class="Symbol">→</a> <a id="6417" href="Cubical.Foundations.Transport.html#6365" class="Bound">C</a><a id="6418" class="Symbol">)</a>
<a id="6439" class="Symbol">→</a> <a id="6441" class="Symbol">{</a><a id="6442" href="Cubical.Foundations.Transport.html#6442" class="Bound">x</a> <a id="6444" href="Cubical.Foundations.Transport.html#6444" class="Bound">y</a> <a id="6446" class="Symbol">:</a> <a id="6448" href="Cubical.Foundations.Transport.html#6292" class="Bound">A</a><a id="6449" class="Symbol">}</a> <a id="6451" class="Symbol">(</a><a id="6452" href="Cubical.Foundations.Transport.html#6452" class="Bound">p</a> <a id="6454" class="Symbol">:</a> <a id="6456" href="Cubical.Foundations.Transport.html#6442" class="Bound">x</a> <a id="6458" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="6460" href="Cubical.Foundations.Transport.html#6444" class="Bound">y</a><a id="6461" class="Symbol">)</a> <a id="6463" class="Symbol">(</a><a id="6464" href="Cubical.Foundations.Transport.html#6464" class="Bound">u</a> <a id="6466" class="Symbol">:</a> <a id="6468" href="Cubical.Foundations.Transport.html#6326" class="Bound">B</a> <a id="6470" href="Cubical.Foundations.Transport.html#6442" class="Bound">x</a><a id="6471" class="Symbol">)</a>
<a id="6492" class="Symbol">→</a> <a id="6495" class="Symbol">(</a><a id="6496" href="Cubical.Foundations.Transport.html#6401" class="Bound">F</a> <a id="6498" href="Cubical.Foundations.Transport.html#6442" class="Bound">x</a> <a id="6500" href="Cubical.Foundations.Transport.html#6464" class="Bound">u</a><a id="6501" class="Symbol">)</a> <a id="6503" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="6505" href="Cubical.Foundations.Transport.html#6401" class="Bound">F</a> <a id="6507" href="Cubical.Foundations.Transport.html#6444" class="Bound">y</a> <a id="6509" class="Symbol">(</a><a id="6510" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="6516" href="Cubical.Foundations.Transport.html#6326" class="Bound">B</a> <a id="6518" href="Cubical.Foundations.Transport.html#6452" class="Bound">p</a> <a id="6520" href="Cubical.Foundations.Transport.html#6464" class="Bound">u</a><a id="6521" class="Symbol">)</a>
<a id="6523" href="Cubical.Foundations.Transport.html#6256" class="Function">constSubstCommSlice</a> <a id="6543" href="Cubical.Foundations.Transport.html#6543" class="Bound">B</a> <a id="6545" href="Cubical.Foundations.Transport.html#6545" class="Bound">C</a> <a id="6547" href="Cubical.Foundations.Transport.html#6547" class="Bound">F</a> <a id="6549" href="Cubical.Foundations.Transport.html#6549" class="Bound">p</a> <a id="6551" href="Cubical.Foundations.Transport.html#6551" class="Bound">Bx</a> <a id="6554" class="Symbol">=</a> <a id="6556" class="Symbol">(</a><a id="6557" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="6561" class="Symbol">(</a><a id="6562" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="6576" class="Symbol">(</a><a id="6577" href="Cubical.Foundations.Transport.html#6547" class="Bound">F</a> <a id="6579" class="Symbol">_</a> <a id="6581" href="Cubical.Foundations.Transport.html#6551" class="Bound">Bx</a><a id="6583" class="Symbol">))</a> <a id="6586" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="6588" href="Cubical.Foundations.Transport.html#5889" class="Function">substCommSlice</a> <a id="6603" href="Cubical.Foundations.Transport.html#6543" class="Bound">B</a> <a id="6605" class="Symbol">(λ</a> <a id="6608" href="Cubical.Foundations.Transport.html#6608" class="Bound">_</a> <a id="6610" class="Symbol">→</a> <a id="6612" href="Cubical.Foundations.Transport.html#6545" class="Bound">C</a><a id="6613" class="Symbol">)</a> <a id="6615" href="Cubical.Foundations.Transport.html#6547" class="Bound">F</a> <a id="6617" href="Cubical.Foundations.Transport.html#6549" class="Bound">p</a> <a id="6619" href="Cubical.Foundations.Transport.html#6551" class="Bound">Bx</a><a id="6621" class="Symbol">)</a>
<a id="6624" class="Comment">-- transporting over (λ i → B (p i) → C (p i)) divides the transport into</a>
<a id="6698" class="Comment">-- transports over (λ i → C (p i)) and (λ i → B (p (~ i)))</a>
<a id="funTypeTransp"></a><a id="6757" href="Cubical.Foundations.Transport.html#6757" class="Function">funTypeTransp</a> <a id="6771" class="Symbol">:</a> <a id="6773" class="Symbol">∀</a> <a id="6775" class="Symbol">{</a><a id="6776" href="Cubical.Foundations.Transport.html#6776" class="Bound">ℓ</a> <a id="6778" href="Cubical.Foundations.Transport.html#6778" class="Bound">ℓ'</a><a id="6780" class="Symbol">}</a> <a id="6782" class="Symbol">{</a><a id="6783" href="Cubical.Foundations.Transport.html#6783" class="Bound">A</a> <a id="6785" class="Symbol">:</a> <a id="6787" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6792" href="Cubical.Foundations.Transport.html#6776" class="Bound">ℓ</a><a id="6793" class="Symbol">}</a> <a id="6795" class="Symbol">(</a><a id="6796" href="Cubical.Foundations.Transport.html#6796" class="Bound">B</a> <a id="6798" href="Cubical.Foundations.Transport.html#6798" class="Bound">C</a> <a id="6800" class="Symbol">:</a> <a id="6802" href="Cubical.Foundations.Transport.html#6783" class="Bound">A</a> <a id="6804" class="Symbol">→</a> <a id="6806" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="6811" href="Cubical.Foundations.Transport.html#6778" class="Bound">ℓ'</a><a id="6813" class="Symbol">)</a> <a id="6815" class="Symbol">{</a><a id="6816" href="Cubical.Foundations.Transport.html#6816" class="Bound">x</a> <a id="6818" href="Cubical.Foundations.Transport.html#6818" class="Bound">y</a> <a id="6820" class="Symbol">:</a> <a id="6822" href="Cubical.Foundations.Transport.html#6783" class="Bound">A</a><a id="6823" class="Symbol">}</a> <a id="6825" class="Symbol">(</a><a id="6826" href="Cubical.Foundations.Transport.html#6826" class="Bound">p</a> <a id="6828" class="Symbol">:</a> <a id="6830" href="Cubical.Foundations.Transport.html#6816" class="Bound">x</a> <a id="6832" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="6834" href="Cubical.Foundations.Transport.html#6818" class="Bound">y</a><a id="6835" class="Symbol">)</a> <a id="6837" class="Symbol">(</a><a id="6838" href="Cubical.Foundations.Transport.html#6838" class="Bound">f</a> <a id="6840" class="Symbol">:</a> <a id="6842" href="Cubical.Foundations.Transport.html#6796" class="Bound">B</a> <a id="6844" href="Cubical.Foundations.Transport.html#6816" class="Bound">x</a> <a id="6846" class="Symbol">→</a> <a id="6848" href="Cubical.Foundations.Transport.html#6798" class="Bound">C</a> <a id="6850" href="Cubical.Foundations.Transport.html#6816" class="Bound">x</a><a id="6851" class="Symbol">)</a>
<a id="6862" class="Symbol">→</a> <a id="6864" href="Agda.Builtin.Cubical.Path.html#197" class="Postulate">PathP</a> <a id="6870" class="Symbol">(λ</a> <a id="6873" href="Cubical.Foundations.Transport.html#6873" class="Bound">i</a> <a id="6875" class="Symbol">→</a> <a id="6877" href="Cubical.Foundations.Transport.html#6796" class="Bound">B</a> <a id="6879" class="Symbol">(</a><a id="6880" href="Cubical.Foundations.Transport.html#6826" class="Bound">p</a> <a id="6882" href="Cubical.Foundations.Transport.html#6873" class="Bound">i</a><a id="6883" class="Symbol">)</a> <a id="6885" class="Symbol">→</a> <a id="6887" href="Cubical.Foundations.Transport.html#6798" class="Bound">C</a> <a id="6889" class="Symbol">(</a><a id="6890" href="Cubical.Foundations.Transport.html#6826" class="Bound">p</a> <a id="6892" href="Cubical.Foundations.Transport.html#6873" class="Bound">i</a><a id="6893" class="Symbol">))</a> <a id="6896" href="Cubical.Foundations.Transport.html#6838" class="Bound">f</a> <a id="6898" class="Symbol">(</a><a id="6899" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="6905" href="Cubical.Foundations.Transport.html#6798" class="Bound">C</a> <a id="6907" href="Cubical.Foundations.Transport.html#6826" class="Bound">p</a> <a id="6909" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="6911" href="Cubical.Foundations.Transport.html#6838" class="Bound">f</a> <a id="6913" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="6915" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="6921" href="Cubical.Foundations.Transport.html#6796" class="Bound">B</a> <a id="6923" class="Symbol">(</a><a id="6924" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="6928" href="Cubical.Foundations.Transport.html#6826" class="Bound">p</a><a id="6929" class="Symbol">))</a>
<a id="6932" href="Cubical.Foundations.Transport.html#6757" class="Function">funTypeTransp</a> <a id="6946" href="Cubical.Foundations.Transport.html#6946" class="Bound">B</a> <a id="6948" href="Cubical.Foundations.Transport.html#6948" class="Bound">C</a> <a id="6950" class="Symbol">{</a><a id="6951" class="Argument">x</a> <a id="6953" class="Symbol">=</a> <a id="6955" href="Cubical.Foundations.Transport.html#6955" class="Bound">x</a><a id="6956" class="Symbol">}</a> <a id="6958" href="Cubical.Foundations.Transport.html#6958" class="Bound">p</a> <a id="6960" href="Cubical.Foundations.Transport.html#6960" class="Bound">f</a> <a id="6962" href="Cubical.Foundations.Transport.html#6962" class="Bound">i</a> <a id="6964" href="Cubical.Foundations.Transport.html#6964" class="Bound">b</a> <a id="6966" class="Symbol">=</a>
<a id="6970" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="6977" class="Symbol">(λ</a> <a id="6980" href="Cubical.Foundations.Transport.html#6980" class="Bound">j</a> <a id="6982" class="Symbol">→</a> <a id="6984" href="Cubical.Foundations.Transport.html#6948" class="Bound">C</a> <a id="6986" class="Symbol">(</a><a id="6987" href="Cubical.Foundations.Transport.html#6958" class="Bound">p</a> <a id="6989" class="Symbol">(</a><a id="6990" href="Cubical.Foundations.Transport.html#6980" class="Bound">j</a> <a id="6992" href="Cubical.Core.Primitives.html#441" class="Primitive Operator">∧</a> <a id="6994" href="Cubical.Foundations.Transport.html#6962" class="Bound">i</a><a id="6995" class="Symbol">)))</a> <a id="6999" class="Symbol">(</a><a id="7000" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="7002" href="Cubical.Foundations.Transport.html#6962" class="Bound">i</a><a id="7003" class="Symbol">)</a> <a id="7005" class="Symbol">(</a><a id="7006" href="Cubical.Foundations.Transport.html#6960" class="Bound">f</a> <a id="7008" class="Symbol">(</a><a id="7009" href="Cubical.Core.Primitives.html#694" class="Primitive">transp</a> <a id="7016" class="Symbol">(λ</a> <a id="7019" href="Cubical.Foundations.Transport.html#7019" class="Bound">j</a> <a id="7021" class="Symbol">→</a> <a id="7023" href="Cubical.Foundations.Transport.html#6946" class="Bound">B</a> <a id="7025" class="Symbol">(</a><a id="7026" href="Cubical.Foundations.Transport.html#6958" class="Bound">p</a> <a id="7028" class="Symbol">(</a><a id="7029" href="Cubical.Foundations.Transport.html#6962" class="Bound">i</a> <a id="7031" href="Cubical.Core.Primitives.html#441" class="Primitive Operator">∧</a> <a id="7033" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="7035" href="Cubical.Foundations.Transport.html#7019" class="Bound">j</a><a id="7036" class="Symbol">)))</a> <a id="7040" class="Symbol">(</a><a id="7041" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="7043" href="Cubical.Foundations.Transport.html#6962" class="Bound">i</a><a id="7044" class="Symbol">)</a> <a id="7046" href="Cubical.Foundations.Transport.html#6964" class="Bound">b</a><a id="7047" class="Symbol">))</a>
<a id="7051" class="Comment">-- transports between loop spaces preserve path composition</a>
<a id="overPathFunct"></a><a id="7111" href="Cubical.Foundations.Transport.html#7111" class="Function">overPathFunct</a> <a id="7125" class="Symbol">:</a> <a id="7127" class="Symbol">∀</a> <a id="7129" class="Symbol">{</a><a id="7130" href="Cubical.Foundations.Transport.html#7130" class="Bound">ℓ</a><a id="7131" class="Symbol">}</a> <a id="7133" class="Symbol">{</a><a id="7134" href="Cubical.Foundations.Transport.html#7134" class="Bound">A</a> <a id="7136" class="Symbol">:</a> <a id="7138" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7143" href="Cubical.Foundations.Transport.html#7130" class="Bound">ℓ</a><a id="7144" class="Symbol">}</a> <a id="7146" class="Symbol">{</a><a id="7147" href="Cubical.Foundations.Transport.html#7147" class="Bound">x</a> <a id="7149" href="Cubical.Foundations.Transport.html#7149" class="Bound">y</a> <a id="7151" class="Symbol">:</a> <a id="7153" href="Cubical.Foundations.Transport.html#7134" class="Bound">A</a><a id="7154" class="Symbol">}</a> <a id="7156" class="Symbol">(</a><a id="7157" href="Cubical.Foundations.Transport.html#7157" class="Bound">p</a> <a id="7159" href="Cubical.Foundations.Transport.html#7159" class="Bound">q</a> <a id="7161" class="Symbol">:</a> <a id="7163" href="Cubical.Foundations.Transport.html#7147" class="Bound">x</a> <a id="7165" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7167" href="Cubical.Foundations.Transport.html#7147" class="Bound">x</a><a id="7168" class="Symbol">)</a> <a id="7170" class="Symbol">(</a><a id="7171" href="Cubical.Foundations.Transport.html#7171" class="Bound">P</a> <a id="7173" class="Symbol">:</a> <a id="7175" href="Cubical.Foundations.Transport.html#7147" class="Bound">x</a> <a id="7177" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7179" href="Cubical.Foundations.Transport.html#7149" class="Bound">y</a><a id="7180" class="Symbol">)</a>
<a id="7193" class="Symbol">→</a> <a id="7195" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="7205" class="Symbol">(λ</a> <a id="7208" href="Cubical.Foundations.Transport.html#7208" class="Bound">i</a> <a id="7210" class="Symbol">→</a> <a id="7212" href="Cubical.Foundations.Transport.html#7171" class="Bound">P</a> <a id="7214" href="Cubical.Foundations.Transport.html#7208" class="Bound">i</a> <a id="7216" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7218" href="Cubical.Foundations.Transport.html#7171" class="Bound">P</a> <a id="7220" href="Cubical.Foundations.Transport.html#7208" class="Bound">i</a><a id="7221" class="Symbol">)</a> <a id="7223" class="Symbol">(</a><a id="7224" href="Cubical.Foundations.Transport.html#7157" class="Bound">p</a> <a id="7226" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7228" href="Cubical.Foundations.Transport.html#7159" class="Bound">q</a><a id="7229" class="Symbol">)</a>
<a id="7243" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7245" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="7255" class="Symbol">(λ</a> <a id="7258" href="Cubical.Foundations.Transport.html#7258" class="Bound">i</a> <a id="7260" class="Symbol">→</a> <a id="7262" href="Cubical.Foundations.Transport.html#7171" class="Bound">P</a> <a id="7264" href="Cubical.Foundations.Transport.html#7258" class="Bound">i</a> <a id="7266" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7268" href="Cubical.Foundations.Transport.html#7171" class="Bound">P</a> <a id="7270" href="Cubical.Foundations.Transport.html#7258" class="Bound">i</a><a id="7271" class="Symbol">)</a> <a id="7273" href="Cubical.Foundations.Transport.html#7157" class="Bound">p</a> <a id="7275" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7277" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="7287" class="Symbol">(λ</a> <a id="7290" href="Cubical.Foundations.Transport.html#7290" class="Bound">i</a> <a id="7292" class="Symbol">→</a> <a id="7294" href="Cubical.Foundations.Transport.html#7171" class="Bound">P</a> <a id="7296" href="Cubical.Foundations.Transport.html#7290" class="Bound">i</a> <a id="7298" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7300" href="Cubical.Foundations.Transport.html#7171" class="Bound">P</a> <a id="7302" href="Cubical.Foundations.Transport.html#7290" class="Bound">i</a><a id="7303" class="Symbol">)</a> <a id="7305" href="Cubical.Foundations.Transport.html#7159" class="Bound">q</a>
<a id="7307" href="Cubical.Foundations.Transport.html#7111" class="Function">overPathFunct</a> <a id="7321" href="Cubical.Foundations.Transport.html#7321" class="Bound">p</a> <a id="7323" href="Cubical.Foundations.Transport.html#7323" class="Bound">q</a> <a id="7325" class="Symbol">=</a>
<a id="7329" href="Cubical.Foundations.Prelude.html#11155" class="Function">J</a> <a id="7331" class="Symbol">(λ</a> <a id="7334" href="Cubical.Foundations.Transport.html#7334" class="Bound">y</a> <a id="7336" href="Cubical.Foundations.Transport.html#7336" class="Bound">P</a> <a id="7338" class="Symbol">→</a> <a id="7340" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="7350" class="Symbol">(λ</a> <a id="7353" href="Cubical.Foundations.Transport.html#7353" class="Bound">i</a> <a id="7355" class="Symbol">→</a> <a id="7357" href="Cubical.Foundations.Transport.html#7336" class="Bound">P</a> <a id="7359" href="Cubical.Foundations.Transport.html#7353" class="Bound">i</a> <a id="7361" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7363" href="Cubical.Foundations.Transport.html#7336" class="Bound">P</a> <a id="7365" href="Cubical.Foundations.Transport.html#7353" class="Bound">i</a><a id="7366" class="Symbol">)</a> <a id="7368" class="Symbol">(</a><a id="7369" href="Cubical.Foundations.Transport.html#7321" class="Bound">p</a> <a id="7371" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7373" href="Cubical.Foundations.Transport.html#7323" class="Bound">q</a><a id="7374" class="Symbol">)</a> <a id="7376" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7378" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="7388" class="Symbol">(λ</a> <a id="7391" href="Cubical.Foundations.Transport.html#7391" class="Bound">i</a> <a id="7393" class="Symbol">→</a> <a id="7395" href="Cubical.Foundations.Transport.html#7336" class="Bound">P</a> <a id="7397" href="Cubical.Foundations.Transport.html#7391" class="Bound">i</a> <a id="7399" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7401" href="Cubical.Foundations.Transport.html#7336" class="Bound">P</a> <a id="7403" href="Cubical.Foundations.Transport.html#7391" class="Bound">i</a><a id="7404" class="Symbol">)</a> <a id="7406" href="Cubical.Foundations.Transport.html#7321" class="Bound">p</a> <a id="7408" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7410" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="7420" class="Symbol">(λ</a> <a id="7423" href="Cubical.Foundations.Transport.html#7423" class="Bound">i</a> <a id="7425" class="Symbol">→</a> <a id="7427" href="Cubical.Foundations.Transport.html#7336" class="Bound">P</a> <a id="7429" href="Cubical.Foundations.Transport.html#7423" class="Bound">i</a> <a id="7431" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7433" href="Cubical.Foundations.Transport.html#7336" class="Bound">P</a> <a id="7435" href="Cubical.Foundations.Transport.html#7423" class="Bound">i</a><a id="7436" class="Symbol">)</a> <a id="7438" href="Cubical.Foundations.Transport.html#7323" class="Bound">q</a><a id="7439" class="Symbol">)</a>
<a id="7445" class="Symbol">(</a><a id="7446" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="7460" class="Symbol">(</a><a id="7461" href="Cubical.Foundations.Transport.html#7321" class="Bound">p</a> <a id="7463" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7465" href="Cubical.Foundations.Transport.html#7323" class="Bound">q</a><a id="7466" class="Symbol">)</a> <a id="7468" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7470" href="Cubical.Foundations.Prelude.html#2025" class="Function">cong₂</a> <a id="7476" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">_∙_</a> <a id="7480" class="Symbol">(</a><a id="7481" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="7485" class="Symbol">(</a><a id="7486" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="7500" href="Cubical.Foundations.Transport.html#7321" class="Bound">p</a><a id="7501" class="Symbol">))</a> <a id="7504" class="Symbol">(</a><a id="7505" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="7509" class="Symbol">(</a><a id="7510" href="Cubical.Foundations.Prelude.html#8818" class="Function">transportRefl</a> <a id="7524" href="Cubical.Foundations.Transport.html#7323" class="Bound">q</a><a id="7525" class="Symbol">)))</a>
<a id="7530" class="Comment">-- substition over families of paths</a>
<a id="7567" class="Comment">-- theorem 2.11.3 in The Book</a>
<a id="substInPaths"></a><a id="7597" href="Cubical.Foundations.Transport.html#7597" class="Function">substInPaths</a> <a id="7610" class="Symbol">:</a> <a id="7612" class="Symbol">∀</a> <a id="7614" class="Symbol">{</a><a id="7615" href="Cubical.Foundations.Transport.html#7615" class="Bound">ℓ</a><a id="7616" class="Symbol">}</a> <a id="7618" class="Symbol">{</a><a id="7619" href="Cubical.Foundations.Transport.html#7619" class="Bound">A</a> <a id="7621" href="Cubical.Foundations.Transport.html#7621" class="Bound">B</a> <a id="7623" class="Symbol">:</a> <a id="7625" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="7630" href="Cubical.Foundations.Transport.html#7615" class="Bound">ℓ</a><a id="7631" class="Symbol">}</a> <a id="7633" class="Symbol">{</a><a id="7634" href="Cubical.Foundations.Transport.html#7634" class="Bound">a</a> <a id="7636" href="Cubical.Foundations.Transport.html#7636" class="Bound">a'</a> <a id="7639" class="Symbol">:</a> <a id="7641" href="Cubical.Foundations.Transport.html#7619" class="Bound">A</a><a id="7642" class="Symbol">}</a>
<a id="7661" class="Symbol">→</a> <a id="7663" class="Symbol">(</a><a id="7664" href="Cubical.Foundations.Transport.html#7664" class="Bound">f</a> <a id="7666" href="Cubical.Foundations.Transport.html#7666" class="Bound">g</a> <a id="7668" class="Symbol">:</a> <a id="7670" href="Cubical.Foundations.Transport.html#7619" class="Bound">A</a> <a id="7672" class="Symbol">→</a> <a id="7674" href="Cubical.Foundations.Transport.html#7621" class="Bound">B</a><a id="7675" class="Symbol">)</a> <a id="7677" class="Symbol">→</a> <a id="7679" class="Symbol">(</a><a id="7680" href="Cubical.Foundations.Transport.html#7680" class="Bound">p</a> <a id="7682" class="Symbol">:</a> <a id="7684" href="Cubical.Foundations.Transport.html#7634" class="Bound">a</a> <a id="7686" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7688" href="Cubical.Foundations.Transport.html#7636" class="Bound">a'</a><a id="7690" class="Symbol">)</a> <a id="7692" class="Symbol">(</a><a id="7693" href="Cubical.Foundations.Transport.html#7693" class="Bound">q</a> <a id="7695" class="Symbol">:</a> <a id="7697" href="Cubical.Foundations.Transport.html#7664" class="Bound">f</a> <a id="7699" href="Cubical.Foundations.Transport.html#7634" class="Bound">a</a> <a id="7701" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7703" href="Cubical.Foundations.Transport.html#7666" class="Bound">g</a> <a id="7705" href="Cubical.Foundations.Transport.html#7634" class="Bound">a</a><a id="7706" class="Symbol">)</a>
<a id="7725" class="Symbol">→</a> <a id="7727" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="7733" class="Symbol">(λ</a> <a id="7736" href="Cubical.Foundations.Transport.html#7736" class="Bound">x</a> <a id="7738" class="Symbol">→</a> <a id="7740" href="Cubical.Foundations.Transport.html#7664" class="Bound">f</a> <a id="7742" href="Cubical.Foundations.Transport.html#7736" class="Bound">x</a> <a id="7744" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7746" href="Cubical.Foundations.Transport.html#7666" class="Bound">g</a> <a id="7748" href="Cubical.Foundations.Transport.html#7736" class="Bound">x</a><a id="7749" class="Symbol">)</a> <a id="7751" href="Cubical.Foundations.Transport.html#7680" class="Bound">p</a> <a id="7753" href="Cubical.Foundations.Transport.html#7693" class="Bound">q</a> <a id="7755" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7757" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="7761" class="Symbol">(</a><a id="7762" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="7767" href="Cubical.Foundations.Transport.html#7664" class="Bound">f</a> <a id="7769" href="Cubical.Foundations.Transport.html#7680" class="Bound">p</a><a id="7770" class="Symbol">)</a> <a id="7772" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7774" href="Cubical.Foundations.Transport.html#7693" class="Bound">q</a> <a id="7776" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7778" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="7783" href="Cubical.Foundations.Transport.html#7666" class="Bound">g</a> <a id="7785" href="Cubical.Foundations.Transport.html#7680" class="Bound">p</a>
<a id="7787" href="Cubical.Foundations.Transport.html#7597" class="Function">substInPaths</a> <a id="7800" class="Symbol">{</a><a id="7801" class="Argument">a</a> <a id="7803" class="Symbol">=</a> <a id="7805" href="Cubical.Foundations.Transport.html#7805" class="Bound">a</a><a id="7806" class="Symbol">}</a> <a id="7808" href="Cubical.Foundations.Transport.html#7808" class="Bound">f</a> <a id="7810" href="Cubical.Foundations.Transport.html#7810" class="Bound">g</a> <a id="7812" href="Cubical.Foundations.Transport.html#7812" class="Bound">p</a> <a id="7814" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a> <a id="7816" class="Symbol">=</a>
<a id="7820" href="Cubical.Foundations.Prelude.html#11155" class="Function">J</a> <a id="7822" class="Symbol">(λ</a> <a id="7825" href="Cubical.Foundations.Transport.html#7825" class="Bound">x</a> <a id="7827" href="Cubical.Foundations.Transport.html#7827" class="Bound">p'</a> <a id="7830" class="Symbol">→</a> <a id="7832" class="Symbol">(</a><a id="7833" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="7839" class="Symbol">(λ</a> <a id="7842" href="Cubical.Foundations.Transport.html#7842" class="Bound">y</a> <a id="7844" class="Symbol">→</a> <a id="7846" href="Cubical.Foundations.Transport.html#7808" class="Bound">f</a> <a id="7848" href="Cubical.Foundations.Transport.html#7842" class="Bound">y</a> <a id="7850" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7852" href="Cubical.Foundations.Transport.html#7810" class="Bound">g</a> <a id="7854" href="Cubical.Foundations.Transport.html#7842" class="Bound">y</a><a id="7855" class="Symbol">)</a> <a id="7857" href="Cubical.Foundations.Transport.html#7827" class="Bound">p'</a> <a id="7860" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a><a id="7861" class="Symbol">)</a> <a id="7863" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7865" class="Symbol">(</a><a id="7866" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="7870" class="Symbol">(</a><a id="7871" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="7876" href="Cubical.Foundations.Transport.html#7808" class="Bound">f</a> <a id="7878" href="Cubical.Foundations.Transport.html#7827" class="Bound">p'</a><a id="7880" class="Symbol">)</a> <a id="7882" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7884" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a> <a id="7886" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7888" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="7893" href="Cubical.Foundations.Transport.html#7810" class="Bound">g</a> <a id="7895" href="Cubical.Foundations.Transport.html#7827" class="Bound">p'</a><a id="7897" class="Symbol">))</a>
<a id="7904" href="Cubical.Foundations.Transport.html#7927" class="Function">p=refl</a> <a id="7911" href="Cubical.Foundations.Transport.html#7812" class="Bound">p</a>
<a id="7917" class="Keyword">where</a>
<a id="7927" href="Cubical.Foundations.Transport.html#7927" class="Function">p=refl</a> <a id="7934" class="Symbol">:</a> <a id="7936" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="7942" class="Symbol">(λ</a> <a id="7945" href="Cubical.Foundations.Transport.html#7945" class="Bound">y</a> <a id="7947" class="Symbol">→</a> <a id="7949" href="Cubical.Foundations.Transport.html#7808" class="Bound">f</a> <a id="7951" href="Cubical.Foundations.Transport.html#7945" class="Bound">y</a> <a id="7953" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7955" href="Cubical.Foundations.Transport.html#7810" class="Bound">g</a> <a id="7957" href="Cubical.Foundations.Transport.html#7945" class="Bound">y</a><a id="7958" class="Symbol">)</a> <a id="7960" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="7965" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a>
<a id="7978" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="7980" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="7985" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7987" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a> <a id="7989" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="7991" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="8000" href="Cubical.Foundations.Transport.html#7927" class="Function">p=refl</a> <a id="8007" class="Symbol">=</a> <a id="8009" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="8015" class="Symbol">(λ</a> <a id="8018" href="Cubical.Foundations.Transport.html#8018" class="Bound">y</a> <a id="8020" class="Symbol">→</a> <a id="8022" href="Cubical.Foundations.Transport.html#7808" class="Bound">f</a> <a id="8024" href="Cubical.Foundations.Transport.html#8018" class="Bound">y</a> <a id="8026" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8028" href="Cubical.Foundations.Transport.html#7810" class="Bound">g</a> <a id="8030" href="Cubical.Foundations.Transport.html#8018" class="Bound">y</a><a id="8031" class="Symbol">)</a> <a id="8033" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="8038" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a>
<a id="8051" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">≡⟨</a> <a id="8054" href="Cubical.Foundations.Prelude.html#9390" class="Function">substRefl</a> <a id="8064" class="Symbol">{</a><a id="8065" class="Argument">B</a> <a id="8067" class="Symbol">=</a> <a id="8069" class="Symbol">(λ</a> <a id="8072" href="Cubical.Foundations.Transport.html#8072" class="Bound">y</a> <a id="8074" class="Symbol">→</a> <a id="8076" href="Cubical.Foundations.Transport.html#7808" class="Bound">f</a> <a id="8078" href="Cubical.Foundations.Transport.html#8072" class="Bound">y</a> <a id="8080" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8082" href="Cubical.Foundations.Transport.html#7810" class="Bound">g</a> <a id="8084" href="Cubical.Foundations.Transport.html#8072" class="Bound">y</a><a id="8085" class="Symbol">)}</a> <a id="8088" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a> <a id="8090" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">⟩</a> <a id="8092" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a>
<a id="8105" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">≡⟨</a> <a id="8108" class="Symbol">(</a><a id="8109" href="Cubical.Foundations.GroupoidLaws.html#423" class="Function">rUnit</a> <a id="8115" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a><a id="8116" class="Symbol">)</a> <a id="8118" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8120" href="Cubical.Foundations.GroupoidLaws.html#989" class="Function">lUnit</a> <a id="8126" class="Symbol">(</a><a id="8127" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a> <a id="8129" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8131" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a><a id="8135" class="Symbol">)</a> <a id="8137" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">⟩</a> <a id="8139" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="8144" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8146" href="Cubical.Foundations.Transport.html#7814" class="Bound">q</a> <a id="8148" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8150" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="8155" href="Cubical.Foundations.Prelude.html#8499" class="Function Operator">∎</a>
<a id="flipTransport"></a><a id="8158" href="Cubical.Foundations.Transport.html#8158" class="Function">flipTransport</a> <a id="8172" class="Symbol">:</a> <a id="8174" class="Symbol">∀</a> <a id="8176" class="Symbol">{</a><a id="8177" href="Cubical.Foundations.Transport.html#8177" class="Bound">ℓ</a><a id="8178" class="Symbol">}</a> <a id="8180" class="Symbol">{</a><a id="8181" href="Cubical.Foundations.Transport.html#8181" class="Bound">A</a> <a id="8183" class="Symbol">:</a> <a id="8185" href="Agda.Primitive.Cubical.html#108" class="Datatype">I</a> <a id="8187" class="Symbol">→</a> <a id="8189" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8194" href="Cubical.Foundations.Transport.html#8177" class="Bound">ℓ</a><a id="8195" class="Symbol">}</a> <a id="8197" class="Symbol">{</a><a id="8198" href="Cubical.Foundations.Transport.html#8198" class="Bound">x</a> <a id="8200" class="Symbol">:</a> <a id="8202" href="Cubical.Foundations.Transport.html#8181" class="Bound">A</a> <a id="8204" href="Agda.Primitive.Cubical.html#150" class="InductiveConstructor">i0</a><a id="8206" class="Symbol">}</a> <a id="8208" class="Symbol">{</a><a id="8209" href="Cubical.Foundations.Transport.html#8209" class="Bound">y</a> <a id="8211" class="Symbol">:</a> <a id="8213" href="Cubical.Foundations.Transport.html#8181" class="Bound">A</a> <a id="8215" href="Agda.Primitive.Cubical.html#178" class="InductiveConstructor">i1</a><a id="8217" class="Symbol">}</a>
<a id="8221" class="Symbol">→</a> <a id="8223" href="Cubical.Foundations.Transport.html#8198" class="Bound">x</a> <a id="8225" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8227" href="Cubical.Foundations.Transport.html#902" class="Function">transport⁻</a> <a id="8238" class="Symbol">(λ</a> <a id="8241" href="Cubical.Foundations.Transport.html#8241" class="Bound">i</a> <a id="8243" class="Symbol">→</a> <a id="8245" href="Cubical.Foundations.Transport.html#8181" class="Bound">A</a> <a id="8247" href="Cubical.Foundations.Transport.html#8241" class="Bound">i</a><a id="8248" class="Symbol">)</a> <a id="8250" href="Cubical.Foundations.Transport.html#8209" class="Bound">y</a>
<a id="8254" class="Symbol">→</a> <a id="8256" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="8266" class="Symbol">(λ</a> <a id="8269" href="Cubical.Foundations.Transport.html#8269" class="Bound">i</a> <a id="8271" class="Symbol">→</a> <a id="8273" href="Cubical.Foundations.Transport.html#8181" class="Bound">A</a> <a id="8275" href="Cubical.Foundations.Transport.html#8269" class="Bound">i</a><a id="8276" class="Symbol">)</a> <a id="8278" href="Cubical.Foundations.Transport.html#8198" class="Bound">x</a> <a id="8280" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8282" href="Cubical.Foundations.Transport.html#8209" class="Bound">y</a>
<a id="8284" href="Cubical.Foundations.Transport.html#8158" class="Function">flipTransport</a> <a id="8298" class="Symbol">{</a><a id="8299" class="Argument">A</a> <a id="8301" class="Symbol">=</a> <a id="8303" href="Cubical.Foundations.Transport.html#8303" class="Bound">A</a><a id="8304" class="Symbol">}</a> <a id="8306" class="Symbol">{</a><a id="8307" class="Argument">y</a> <a id="8309" class="Symbol">=</a> <a id="8311" href="Cubical.Foundations.Transport.html#8311" class="Bound">y</a><a id="8312" class="Symbol">}</a> <a id="8314" href="Cubical.Foundations.Transport.html#8314" class="Bound">p</a> <a id="8316" class="Symbol">=</a>
<a id="8320" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="8325" class="Symbol">(</a><a id="8326" href="Cubical.Foundations.Prelude.html#8597" class="Function">transport</a> <a id="8336" class="Symbol">(λ</a> <a id="8339" href="Cubical.Foundations.Transport.html#8339" class="Bound">i</a> <a id="8341" class="Symbol">→</a> <a id="8343" href="Cubical.Foundations.Transport.html#8303" class="Bound">A</a> <a id="8345" href="Cubical.Foundations.Transport.html#8339" class="Bound">i</a><a id="8346" class="Symbol">))</a> <a id="8349" href="Cubical.Foundations.Transport.html#8314" class="Bound">p</a> <a id="8351" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8353" href="Cubical.Foundations.Transport.html#2446" class="Function">transportTransport⁻</a> <a id="8373" class="Symbol">(λ</a> <a id="8376" href="Cubical.Foundations.Transport.html#8376" class="Bound">i</a> <a id="8378" class="Symbol">→</a> <a id="8380" href="Cubical.Foundations.Transport.html#8303" class="Bound">A</a> <a id="8382" href="Cubical.Foundations.Transport.html#8376" class="Bound">i</a><a id="8383" class="Symbol">)</a> <a id="8385" href="Cubical.Foundations.Transport.html#8311" class="Bound">y</a>
<a id="8388" class="Comment">-- special cases of substInPaths from lemma 2.11.2 in The Book</a>
<a id="8451" class="Keyword">module</a> <a id="8458" href="Cubical.Foundations.Transport.html#8458" class="Module">_</a> <a id="8460" class="Symbol">{</a><a id="8461" href="Cubical.Foundations.Transport.html#8461" class="Bound">ℓ</a> <a id="8463" class="Symbol">:</a> <a id="8465" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="8470" class="Symbol">}</a> <a id="8472" class="Symbol">{</a><a id="8473" href="Cubical.Foundations.Transport.html#8473" class="Bound">A</a> <a id="8475" class="Symbol">:</a> <a id="8477" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="8482" href="Cubical.Foundations.Transport.html#8461" class="Bound">ℓ</a><a id="8483" class="Symbol">}</a> <a id="8485" class="Symbol">{</a><a id="8486" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a> <a id="8488" href="Cubical.Foundations.Transport.html#8488" class="Bound">x1</a> <a id="8491" href="Cubical.Foundations.Transport.html#8491" class="Bound">x2</a> <a id="8494" class="Symbol">:</a> <a id="8496" href="Cubical.Foundations.Transport.html#8473" class="Bound">A</a><a id="8497" class="Symbol">}</a> <a id="8499" class="Symbol">(</a><a id="8500" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8502" class="Symbol">:</a> <a id="8504" href="Cubical.Foundations.Transport.html#8488" class="Bound">x1</a> <a id="8507" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8509" href="Cubical.Foundations.Transport.html#8491" class="Bound">x2</a><a id="8511" class="Symbol">)</a> <a id="8513" class="Keyword">where</a>
<a id="8521" href="Cubical.Foundations.Transport.html#8521" class="Function">substInPathsL</a> <a id="8535" class="Symbol">:</a> <a id="8537" class="Symbol">(</a><a id="8538" href="Cubical.Foundations.Transport.html#8538" class="Bound">q</a> <a id="8540" class="Symbol">:</a> <a id="8542" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a> <a id="8544" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8546" href="Cubical.Foundations.Transport.html#8488" class="Bound">x1</a><a id="8548" class="Symbol">)</a> <a id="8550" class="Symbol">→</a> <a id="8552" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="8558" class="Symbol">(λ</a> <a id="8561" href="Cubical.Foundations.Transport.html#8561" class="Bound">x</a> <a id="8563" class="Symbol">→</a> <a id="8565" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a> <a id="8567" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8569" href="Cubical.Foundations.Transport.html#8561" class="Bound">x</a><a id="8570" class="Symbol">)</a> <a id="8572" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8574" href="Cubical.Foundations.Transport.html#8538" class="Bound">q</a> <a id="8576" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8578" href="Cubical.Foundations.Transport.html#8538" class="Bound">q</a> <a id="8580" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8582" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a>
<a id="8586" href="Cubical.Foundations.Transport.html#8521" class="Function">substInPathsL</a> <a id="8600" href="Cubical.Foundations.Transport.html#8600" class="Bound">q</a> <a id="8602" class="Symbol">=</a> <a id="8604" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="8610" class="Symbol">(λ</a> <a id="8613" href="Cubical.Foundations.Transport.html#8613" class="Bound">x</a> <a id="8615" class="Symbol">→</a> <a id="8617" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a> <a id="8619" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8621" href="Cubical.Foundations.Transport.html#8613" class="Bound">x</a><a id="8622" class="Symbol">)</a> <a id="8624" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8626" href="Cubical.Foundations.Transport.html#8600" class="Bound">q</a>
<a id="8632" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">≡⟨</a> <a id="8635" href="Cubical.Foundations.Transport.html#7597" class="Function">substInPaths</a> <a id="8648" class="Symbol">(λ</a> <a id="8651" href="Cubical.Foundations.Transport.html#8651" class="Bound">_</a> <a id="8653" class="Symbol">→</a> <a id="8655" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a><a id="8656" class="Symbol">)</a> <a id="8658" class="Symbol">(λ</a> <a id="8661" href="Cubical.Foundations.Transport.html#8661" class="Bound">x</a> <a id="8663" class="Symbol">→</a> <a id="8665" href="Cubical.Foundations.Transport.html#8661" class="Bound">x</a><a id="8666" class="Symbol">)</a> <a id="8668" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8670" href="Cubical.Foundations.Transport.html#8600" class="Bound">q</a> <a id="8672" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">⟩</a>
<a id="8680" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="8684" class="Symbol">(</a><a id="8685" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="8690" class="Symbol">(λ</a> <a id="8693" href="Cubical.Foundations.Transport.html#8693" class="Bound">_</a> <a id="8695" class="Symbol">→</a> <a id="8697" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a><a id="8698" class="Symbol">)</a> <a id="8700" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a><a id="8701" class="Symbol">)</a> <a id="8703" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8705" href="Cubical.Foundations.Transport.html#8600" class="Bound">q</a> <a id="8707" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8709" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="8714" class="Symbol">(λ</a> <a id="8717" href="Cubical.Foundations.Transport.html#8717" class="Bound">x</a> <a id="8719" class="Symbol">→</a> <a id="8721" href="Cubical.Foundations.Transport.html#8717" class="Bound">x</a><a id="8722" class="Symbol">)</a> <a id="8724" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a>
<a id="8730" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">≡⟨</a> <a id="8733" href="Cubical.Foundations.GroupoidLaws.html#2215" class="Function">assoc</a> <a id="8739" class="Symbol">(λ</a> <a id="8742" href="Cubical.Foundations.Transport.html#8742" class="Bound">_</a> <a id="8744" class="Symbol">→</a> <a id="8746" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a><a id="8747" class="Symbol">)</a> <a id="8749" href="Cubical.Foundations.Transport.html#8600" class="Bound">q</a> <a id="8751" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8753" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">⟩</a>
<a id="8761" class="Symbol">(</a><a id="8762" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="8767" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8769" href="Cubical.Foundations.Transport.html#8600" class="Bound">q</a><a id="8770" class="Symbol">)</a> <a id="8772" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8774" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a>
<a id="8780" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">≡⟨</a> <a id="8783" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="8788" class="Symbol">(</a><a id="8789" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">_∙</a> <a id="8792" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a><a id="8793" class="Symbol">)</a> <a id="8795" class="Symbol">(</a><a id="8796" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="8800" class="Symbol">(</a><a id="8801" href="Cubical.Foundations.GroupoidLaws.html#989" class="Function">lUnit</a> <a id="8807" href="Cubical.Foundations.Transport.html#8600" class="Bound">q</a><a id="8808" class="Symbol">))</a> <a id="8811" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">⟩</a> <a id="8813" href="Cubical.Foundations.Transport.html#8600" class="Bound">q</a> <a id="8815" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8817" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8819" href="Cubical.Foundations.Prelude.html#8499" class="Function Operator">∎</a>
<a id="8824" href="Cubical.Foundations.Transport.html#8824" class="Function">substInPathsR</a> <a id="8838" class="Symbol">:</a> <a id="8840" class="Symbol">(</a><a id="8841" href="Cubical.Foundations.Transport.html#8841" class="Bound">q</a> <a id="8843" class="Symbol">:</a> <a id="8845" href="Cubical.Foundations.Transport.html#8488" class="Bound">x1</a> <a id="8848" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8850" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a><a id="8851" class="Symbol">)</a> <a id="8853" class="Symbol">→</a> <a id="8855" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="8861" class="Symbol">(λ</a> <a id="8864" href="Cubical.Foundations.Transport.html#8864" class="Bound">x</a> <a id="8866" class="Symbol">→</a> <a id="8868" href="Cubical.Foundations.Transport.html#8864" class="Bound">x</a> <a id="8870" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8872" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a><a id="8873" class="Symbol">)</a> <a id="8875" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8877" href="Cubical.Foundations.Transport.html#8841" class="Bound">q</a> <a id="8879" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8881" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="8885" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8887" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="8889" href="Cubical.Foundations.Transport.html#8841" class="Bound">q</a>
<a id="8893" href="Cubical.Foundations.Transport.html#8824" class="Function">substInPathsR</a> <a id="8907" href="Cubical.Foundations.Transport.html#8907" class="Bound">q</a> <a id="8909" class="Symbol">=</a> <a id="8911" href="Cubical.Foundations.Prelude.html#9128" class="Function">subst</a> <a id="8917" class="Symbol">(λ</a> <a id="8920" href="Cubical.Foundations.Transport.html#8920" class="Bound">x</a> <a id="8922" class="Symbol">→</a> <a id="8924" href="Cubical.Foundations.Transport.html#8920" class="Bound">x</a> <a id="8926" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="8928" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a><a id="8929" class="Symbol">)</a> <a id="8931" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8933" href="Cubical.Foundations.Transport.html#8907" class="Bound">q</a>
<a id="8939" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">≡⟨</a> <a id="8942" href="Cubical.Foundations.Transport.html#7597" class="Function">substInPaths</a> <a id="8955" class="Symbol">(λ</a> <a id="8958" href="Cubical.Foundations.Transport.html#8958" class="Bound">x</a> <a id="8960" class="Symbol">→</a> <a id="8962" href="Cubical.Foundations.Transport.html#8958" class="Bound">x</a><a id="8963" class="Symbol">)</a> <a id="8965" class="Symbol">(λ</a> <a id="8968" href="Cubical.Foundations.Transport.html#8968" class="Bound">_</a> <a id="8970" class="Symbol">→</a> <a id="8972" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a><a id="8973" class="Symbol">)</a> <a id="8975" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="8977" href="Cubical.Foundations.Transport.html#8907" class="Bound">q</a> <a id="8979" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">⟩</a>
<a id="8987" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="8991" class="Symbol">(</a><a id="8992" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="8997" class="Symbol">(λ</a> <a id="9000" href="Cubical.Foundations.Transport.html#9000" class="Bound">x</a> <a id="9002" class="Symbol">→</a> <a id="9004" href="Cubical.Foundations.Transport.html#9000" class="Bound">x</a><a id="9005" class="Symbol">)</a> <a id="9007" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a><a id="9008" class="Symbol">)</a> <a id="9010" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="9012" href="Cubical.Foundations.Transport.html#8907" class="Bound">q</a> <a id="9014" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="9016" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="9021" class="Symbol">(λ</a> <a id="9024" href="Cubical.Foundations.Transport.html#9024" class="Bound">_</a> <a id="9026" class="Symbol">→</a> <a id="9028" href="Cubical.Foundations.Transport.html#8486" class="Bound">a</a><a id="9029" class="Symbol">)</a> <a id="9031" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a>
<a id="9037" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">≡⟨</a> <a id="9040" href="Cubical.Foundations.GroupoidLaws.html#2215" class="Function">assoc</a> <a id="9046" class="Symbol">(</a><a id="9047" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="9051" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a><a id="9052" class="Symbol">)</a> <a id="9054" href="Cubical.Foundations.Transport.html#8907" class="Bound">q</a> <a id="9056" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="9061" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">⟩</a>
<a id="9069" class="Symbol">(</a><a id="9070" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="9074" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="9076" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="9078" href="Cubical.Foundations.Transport.html#8907" class="Bound">q</a><a id="9079" class="Symbol">)</a> <a id="9081" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="9083" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="9092" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">≡⟨</a> <a id="9095" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="9099" class="Symbol">(</a><a id="9100" href="Cubical.Foundations.GroupoidLaws.html#423" class="Function">rUnit</a> <a id="9106" class="Symbol">(</a><a id="9107" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="9111" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="9113" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="9115" href="Cubical.Foundations.Transport.html#8907" class="Bound">q</a><a id="9116" class="Symbol">))</a><a id="9118" href="Cubical.Foundations.Prelude.html#7981" class="Function Operator">⟩</a> <a id="9120" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="9124" href="Cubical.Foundations.Transport.html#8500" class="Bound">p</a> <a id="9126" href="Cubical.Foundations.Prelude.html#4447" class="Function Operator">∙</a> <a id="9128" href="Cubical.Foundations.Transport.html#8907" class="Bound">q</a> <a id="9130" href="Cubical.Foundations.Prelude.html#8499" class="Function Operator">∎</a>
</pre></body></html>