-
Notifications
You must be signed in to change notification settings - Fork 0
/
Cubical.Core.Everything.html
13 lines (10 loc) · 1.24 KB
/
Cubical.Core.Everything.html
1
2
3
4
5
6
7
8
9
10
11
12
13
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Core.Everything</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Symbol">#-}</a>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Core.Everything.html" class="Module">Cubical.Core.Everything</a> <a id="55" class="Keyword">where</a>
<a id="62" class="Comment">-- Basic primitives (some are from Agda.Primitive)</a>
<a id="113" class="Keyword">open</a> <a id="118" class="Keyword">import</a> <a id="125" href="Cubical.Core.Primitives.html" class="Module">Cubical.Core.Primitives</a> <a id="149" class="Keyword">public</a>
<a id="157" class="Comment">-- Definition of equivalences and Glue types</a>
<a id="202" class="Keyword">open</a> <a id="207" class="Keyword">import</a> <a id="214" href="Cubical.Core.Glue.html" class="Module">Cubical.Core.Glue</a> <a id="232" class="Keyword">public</a>
<a id="240" class="Comment">-- Definition of cubical Identity types</a>
<a id="280" class="Keyword">open</a> <a id="285" class="Keyword">import</a> <a id="292" href="Cubical.Core.Id.html" class="Module">Cubical.Core.Id</a>
</pre></body></html>