blob: 1be20f5c866f42c47bab9008b969245b68c8da0d (
plain) (
blame)
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
|
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Agda.Primitive.Cubical</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical</a> <a id="23" class="Pragma">--no-subtyping</a> <a id="38" class="Symbol">#-}</a>
<a id="43" class="Keyword">module</a> <a id="50" href="Agda.Primitive.Cubical.html" class="Module">Agda.Primitive.Cubical</a> <a id="73" class="Keyword">where</a>
<a id="80" class="Symbol">{-#</a> <a id="84" class="Keyword">BUILTIN</a> <a id="92" class="Keyword">INTERVAL</a> <a id="I"></a><a id="101" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="104" class="Symbol">#-}</a> <a id="109" class="Comment">-- I : Setω</a>
<a id="122" class="Symbol">{-#</a> <a id="126" class="Keyword">BUILTIN</a> <a id="134" class="Keyword">IZERO</a> <a id="i0"></a><a id="143" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a> <a id="146" class="Symbol">#-}</a>
<a id="150" class="Symbol">{-#</a> <a id="154" class="Keyword">BUILTIN</a> <a id="162" class="Keyword">IONE</a> <a id="i1"></a><a id="171" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a> <a id="174" class="Symbol">#-}</a>
<a id="179" class="Keyword">infix</a> <a id="186" class="Number">30</a> <a id="189" href="Agda.Primitive.Cubical.html#291" class="Primitive">primINeg</a>
<a id="198" class="Keyword">infixr</a> <a id="205" class="Number">20</a> <a id="208" href="Agda.Primitive.Cubical.html#241" class="Primitive">primIMin</a> <a id="217" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a>
<a id="227" class="Keyword">primitive</a>
<a id="primIMin"></a><a id="241" href="Agda.Primitive.Cubical.html#241" class="Primitive">primIMin</a> <a id="250" class="Symbol">:</a> <a id="252" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="254" class="Symbol">→</a> <a id="256" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="258" class="Symbol">→</a> <a id="260" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a>
<a id="primIMax"></a><a id="266" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="275" class="Symbol">:</a> <a id="277" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="279" class="Symbol">→</a> <a id="281" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="283" class="Symbol">→</a> <a id="285" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a>
<a id="primINeg"></a><a id="291" href="Agda.Primitive.Cubical.html#291" class="Primitive">primINeg</a> <a id="300" class="Symbol">:</a> <a id="302" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="304" class="Symbol">→</a> <a id="306" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a>
<a id="309" class="Symbol">{-#</a> <a id="313" class="Keyword">BUILTIN</a> <a id="321" class="Keyword">ISONE</a> <a id="IsOne"></a><a id="330" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="339" class="Symbol">#-}</a> <a id="344" class="Comment">-- IsOne : I → Setω</a>
<a id="365" class="Keyword">postulate</a>
<a id="itIsOne"></a><a id="377" href="Agda.Primitive.Cubical.html#377" class="Postulate">itIsOne</a> <a id="385" class="Symbol">:</a> <a id="387" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="393" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a>
<a id="IsOne1"></a><a id="398" href="Agda.Primitive.Cubical.html#398" class="Postulate">IsOne1</a> <a id="406" class="Symbol">:</a> <a id="408" class="Symbol">∀</a> <a id="410" href="Agda.Primitive.Cubical.html#410" class="Bound">i</a> <a id="412" href="Agda.Primitive.Cubical.html#412" class="Bound">j</a> <a id="414" class="Symbol">→</a> <a id="416" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="422" href="Agda.Primitive.Cubical.html#410" class="Bound">i</a> <a id="424" class="Symbol">→</a> <a id="426" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="432" class="Symbol">(</a><a id="433" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="442" href="Agda.Primitive.Cubical.html#410" class="Bound">i</a> <a id="444" href="Agda.Primitive.Cubical.html#412" class="Bound">j</a><a id="445" class="Symbol">)</a>
<a id="IsOne2"></a><a id="449" href="Agda.Primitive.Cubical.html#449" class="Postulate">IsOne2</a> <a id="457" class="Symbol">:</a> <a id="459" class="Symbol">∀</a> <a id="461" href="Agda.Primitive.Cubical.html#461" class="Bound">i</a> <a id="463" href="Agda.Primitive.Cubical.html#463" class="Bound">j</a> <a id="465" class="Symbol">→</a> <a id="467" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="473" href="Agda.Primitive.Cubical.html#463" class="Bound">j</a> <a id="475" class="Symbol">→</a> <a id="477" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="483" class="Symbol">(</a><a id="484" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="493" href="Agda.Primitive.Cubical.html#461" class="Bound">i</a> <a id="495" href="Agda.Primitive.Cubical.html#463" class="Bound">j</a><a id="496" class="Symbol">)</a>
<a id="499" class="Symbol">{-#</a> <a id="503" class="Keyword">BUILTIN</a> <a id="511" class="Keyword">ITISONE</a> <a id="520" href="Agda.Primitive.Cubical.html#377" class="Postulate">itIsOne</a> <a id="529" class="Symbol">#-}</a>
<a id="533" class="Symbol">{-#</a> <a id="537" class="Keyword">BUILTIN</a> <a id="545" class="Keyword">ISONE1</a> <a id="554" href="Agda.Primitive.Cubical.html#398" class="Postulate">IsOne1</a> <a id="563" class="Symbol">#-}</a>
<a id="567" class="Symbol">{-#</a> <a id="571" class="Keyword">BUILTIN</a> <a id="579" class="Keyword">ISONE2</a> <a id="588" href="Agda.Primitive.Cubical.html#449" class="Postulate">IsOne2</a> <a id="597" class="Symbol">#-}</a>
<a id="602" class="Comment">-- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ</a>
<a id="648" class="Comment">-- Partial i A = IsOne i → A</a>
<a id="678" class="Symbol">{-#</a> <a id="682" class="Keyword">BUILTIN</a> <a id="690" class="Keyword">PARTIAL</a> <a id="Partial"></a><a id="699" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="708" class="Symbol">#-}</a>
<a id="712" class="Symbol">{-#</a> <a id="716" class="Keyword">BUILTIN</a> <a id="724" class="Keyword">PARTIALP</a> <a id="PartialP"></a><a id="733" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="742" class="Symbol">#-}</a>
<a id="747" class="Keyword">postulate</a>
<a id="isOneEmpty"></a><a id="759" href="Agda.Primitive.Cubical.html#759" class="Postulate">isOneEmpty</a> <a id="770" class="Symbol">:</a> <a id="772" class="Symbol">∀</a> <a id="774" class="Symbol">{</a><a id="775" href="Agda.Primitive.Cubical.html#775" class="Bound">ℓ</a><a id="776" class="Symbol">}</a> <a id="778" class="Symbol">{</a><a id="779" href="Agda.Primitive.Cubical.html#779" class="Bound">A</a> <a id="781" class="Symbol">:</a> <a id="783" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="791" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a> <a id="794" class="Symbol">(</a><a id="795" class="PrimitiveType">Set</a> <a id="799" href="Agda.Primitive.Cubical.html#775" class="Bound">ℓ</a><a id="800" class="Symbol">)}</a> <a id="803" class="Symbol">→</a> <a id="805" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="814" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a> <a id="817" href="Agda.Primitive.Cubical.html#779" class="Bound">A</a>
<a id="820" class="Symbol">{-#</a> <a id="824" class="Keyword">BUILTIN</a> <a id="832" class="Keyword">ISONEEMPTY</a> <a id="843" href="Agda.Primitive.Cubical.html#759" class="Postulate">isOneEmpty</a> <a id="854" class="Symbol">#-}</a>
<a id="859" class="Keyword">primitive</a>
<a id="primPOr"></a><a id="871" href="Agda.Primitive.Cubical.html#871" class="Primitive">primPOr</a> <a id="879" class="Symbol">:</a> <a id="881" class="Symbol">∀</a> <a id="883" class="Symbol">{</a><a id="884" href="Agda.Primitive.Cubical.html#884" class="Bound">ℓ</a><a id="885" class="Symbol">}</a> <a id="887" class="Symbol">(</a><a id="888" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="890" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="892" class="Symbol">:</a> <a id="894" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="895" class="Symbol">)</a> <a id="897" class="Symbol">{</a><a id="898" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> <a id="900" class="Symbol">:</a> <a id="902" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="910" class="Symbol">(</a><a id="911" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="920" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="922" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a><a id="923" class="Symbol">)</a> <a id="925" class="Symbol">(</a><a id="926" class="PrimitiveType">Set</a> <a id="930" href="Agda.Primitive.Cubical.html#884" class="Bound">ℓ</a><a id="931" class="Symbol">)}</a>
<a id="946" class="Symbol">→</a> <a id="948" class="Symbol">(</a><a id="949" href="Agda.Primitive.Cubical.html#949" class="Bound">u</a> <a id="951" class="Symbol">:</a> <a id="953" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="962" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="964" class="Symbol">(λ</a> <a id="967" href="Agda.Primitive.Cubical.html#967" class="Bound">z</a> <a id="969" class="Symbol">→</a> <a id="971" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> <a id="973" class="Symbol">(</a><a id="974" href="Agda.Primitive.Cubical.html#398" class="Postulate">IsOne1</a> <a id="981" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="983" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="985" href="Agda.Primitive.Cubical.html#967" class="Bound">z</a><a id="986" class="Symbol">)))</a>
<a id="1002" class="Symbol">→</a> <a id="1004" class="Symbol">(</a><a id="1005" href="Agda.Primitive.Cubical.html#1005" class="Bound">v</a> <a id="1007" class="Symbol">:</a> <a id="1009" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="1018" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="1020" class="Symbol">(λ</a> <a id="1023" href="Agda.Primitive.Cubical.html#1023" class="Bound">z</a> <a id="1025" class="Symbol">→</a> <a id="1027" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> <a id="1029" class="Symbol">(</a><a id="1030" href="Agda.Primitive.Cubical.html#449" class="Postulate">IsOne2</a> <a id="1037" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="1039" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="1041" href="Agda.Primitive.Cubical.html#1023" class="Bound">z</a><a id="1042" class="Symbol">)))</a>
<a id="1058" class="Symbol">→</a> <a id="1060" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="1069" class="Symbol">(</a><a id="1070" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="1079" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="1081" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a><a id="1082" class="Symbol">)</a> <a id="1084" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a>
<a id="1089" class="Comment">-- Computes in terms of primHComp and primTransp</a>
<a id="primComp"></a><a id="1140" href="Agda.Primitive.Cubical.html#1140" class="Primitive">primComp</a> <a id="1149" class="Symbol">:</a> <a id="1151" class="Symbol">∀</a> <a id="1153" class="Symbol">{</a><a id="1154" href="Agda.Primitive.Cubical.html#1154" class="Bound">ℓ</a><a id="1155" class="Symbol">}</a> <a id="1157" class="Symbol">(</a><a id="1158" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1160" class="Symbol">:</a> <a id="1162" class="Symbol">(</a><a id="1163" href="Agda.Primitive.Cubical.html#1163" class="Bound">i</a> <a id="1165" class="Symbol">:</a> <a id="1167" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1168" class="Symbol">)</a> <a id="1170" class="Symbol">→</a> <a id="1172" class="PrimitiveType">Set</a> <a id="1176" class="Symbol">(</a><a id="1177" href="Agda.Primitive.Cubical.html#1154" class="Bound">ℓ</a> <a id="1179" href="Agda.Primitive.Cubical.html#1163" class="Bound">i</a><a id="1180" class="Symbol">))</a> <a id="1183" class="Symbol">{</a><a id="1184" href="Agda.Primitive.Cubical.html#1184" class="Bound">φ</a> <a id="1186" class="Symbol">:</a> <a id="1188" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1189" class="Symbol">}</a> <a id="1191" class="Symbol">(</a><a id="1192" href="Agda.Primitive.Cubical.html#1192" class="Bound">u</a> <a id="1194" class="Symbol">:</a> <a id="1196" class="Symbol">∀</a> <a id="1198" href="Agda.Primitive.Cubical.html#1198" class="Bound">i</a> <a id="1200" class="Symbol">→</a> <a id="1202" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="1210" href="Agda.Primitive.Cubical.html#1184" class="Bound">φ</a> <a id="1212" class="Symbol">(</a><a id="1213" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1215" href="Agda.Primitive.Cubical.html#1198" class="Bound">i</a><a id="1216" class="Symbol">))</a> <a id="1219" class="Symbol">(</a><a id="1220" href="Agda.Primitive.Cubical.html#1220" class="Bound">a</a> <a id="1222" class="Symbol">:</a> <a id="1224" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1226" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a><a id="1228" class="Symbol">)</a> <a id="1230" class="Symbol">→</a> <a id="1232" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1234" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a>
<a id="1238" class="Keyword">syntax</a> <a id="1245" href="Agda.Primitive.Cubical.html#871" class="Primitive">primPOr</a> <a id="1253" class="Bound">p</a> <a id="1255" class="Bound">q</a> <a id="1257" class="Bound">u</a> <a id="1259" class="Bound">t</a> <a id="1261" class="Symbol">=</a> <a id="1263" class="Primitive">[</a> <a id="1265" class="Bound">p</a> <a id="1267" class="Primitive">↦</a> <a id="1269" class="Bound">u</a> <a id="1271" class="Primitive">,</a> <a id="1273" class="Bound">q</a> <a id="1275" class="Primitive">↦</a> <a id="1277" class="Bound">t</a> <a id="1279" class="Primitive">]</a>
<a id="1282" class="Keyword">primitive</a>
<a id="primTransp"></a><a id="1294" href="Agda.Primitive.Cubical.html#1294" class="Primitive">primTransp</a> <a id="1305" class="Symbol">:</a> <a id="1307" class="Symbol">∀</a> <a id="1309" class="Symbol">{</a><a id="1310" href="Agda.Primitive.Cubical.html#1310" class="Bound">ℓ</a><a id="1311" class="Symbol">}</a> <a id="1313" class="Symbol">(</a><a id="1314" href="Agda.Primitive.Cubical.html#1314" class="Bound">A</a> <a id="1316" class="Symbol">:</a> <a id="1318" class="Symbol">(</a><a id="1319" href="Agda.Primitive.Cubical.html#1319" class="Bound">i</a> <a id="1321" class="Symbol">:</a> <a id="1323" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1324" class="Symbol">)</a> <a id="1326" class="Symbol">→</a> <a id="1328" class="PrimitiveType">Set</a> <a id="1332" class="Symbol">(</a><a id="1333" href="Agda.Primitive.Cubical.html#1310" class="Bound">ℓ</a> <a id="1335" href="Agda.Primitive.Cubical.html#1319" class="Bound">i</a><a id="1336" class="Symbol">))</a> <a id="1339" class="Symbol">(</a><a id="1340" href="Agda.Primitive.Cubical.html#1340" class="Bound">φ</a> <a id="1342" class="Symbol">:</a> <a id="1344" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1345" class="Symbol">)</a> <a id="1347" class="Symbol">(</a><a id="1348" href="Agda.Primitive.Cubical.html#1348" class="Bound">a</a> <a id="1350" class="Symbol">:</a> <a id="1352" href="Agda.Primitive.Cubical.html#1314" class="Bound">A</a> <a id="1354" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a><a id="1356" class="Symbol">)</a> <a id="1358" class="Symbol">→</a> <a id="1360" href="Agda.Primitive.Cubical.html#1314" class="Bound">A</a> <a id="1362" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a>
<a id="primHComp"></a><a id="1367" href="Agda.Primitive.Cubical.html#1367" class="Primitive">primHComp</a> <a id="1378" class="Symbol">:</a> <a id="1380" class="Symbol">∀</a> <a id="1382" class="Symbol">{</a><a id="1383" href="Agda.Primitive.Cubical.html#1383" class="Bound">ℓ</a><a id="1384" class="Symbol">}</a> <a id="1386" class="Symbol">{</a><a id="1387" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a> <a id="1389" class="Symbol">:</a> <a id="1391" class="PrimitiveType">Set</a> <a id="1395" href="Agda.Primitive.Cubical.html#1383" class="Bound">ℓ</a><a id="1396" class="Symbol">}</a> <a id="1398" class="Symbol">{</a><a id="1399" href="Agda.Primitive.Cubical.html#1399" class="Bound">φ</a> <a id="1401" class="Symbol">:</a> <a id="1403" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1404" class="Symbol">}</a> <a id="1406" class="Symbol">(</a><a id="1407" href="Agda.Primitive.Cubical.html#1407" class="Bound">u</a> <a id="1409" class="Symbol">:</a> <a id="1411" class="Symbol">∀</a> <a id="1413" href="Agda.Primitive.Cubical.html#1413" class="Bound">i</a> <a id="1415" class="Symbol">→</a> <a id="1417" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="1425" href="Agda.Primitive.Cubical.html#1399" class="Bound">φ</a> <a id="1427" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a><a id="1428" class="Symbol">)</a> <a id="1430" class="Symbol">(</a><a id="1431" href="Agda.Primitive.Cubical.html#1431" class="Bound">a</a> <a id="1433" class="Symbol">:</a> <a id="1435" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a><a id="1436" class="Symbol">)</a> <a id="1438" class="Symbol">→</a> <a id="1440" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a>
</pre></body></html>
|