/usr/share/doc/agda-stdlib-doc/html/Level.html is in agda-stdlib-doc 0.14-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Level</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Universe levels</a>
<a id="125" class="Comment">------------------------------------------------------------------------</a>
<a id="199" class="Keyword">module</a> <a id="206" href="Level.html" class="Module">Level</a> <a id="212" class="Keyword">where</a>
<a id="219" class="Comment">-- Levels.</a>
<a id="231" class="Keyword">open</a> <a id="236" class="Keyword">import</a> <a id="243" href="Agda.Primitive.html" class="Module">Agda.Primitive</a> <a id="258" class="Keyword">public</a>
<a id="267" class="Keyword">using</a> <a id="276" class="Symbol">(</a><a id="277" href="Agda.Primitive.html#Level" class="Postulate">Level</a><a id="282" class="Symbol">;</a> <a id="284" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">_⊔_</a><a id="287" class="Symbol">)</a>
<a id="291" class="Keyword">renaming</a> <a id="300" class="Symbol">(</a><a id="301" href="Agda.Primitive.html#lzero" class="Primitive">lzero</a> <a id="307" class="Symbol">to</a> <a id="310" href="Agda.Primitive.html#lzero" class="Primitive">zero</a><a id="314" class="Symbol">;</a> <a id="316" href="Agda.Primitive.html#lsuc" class="Primitive">lsuc</a> <a id="321" class="Symbol">to</a> <a id="324" href="Agda.Primitive.html#lsuc" class="Primitive">suc</a><a id="327" class="Symbol">)</a>
<a id="330" class="Comment">-- Lifting.</a>
<a id="343" class="Keyword">record</a> <a id="Lift" href="Level.html#Lift" class="Record">Lift</a> <a id="355" class="Symbol">{</a><a id="356" href="Level.html#356" class="Bound">a</a> <a id="358" href="Level.html#358" class="Bound">ℓ</a><a id="359" class="Symbol">}</a> <a id="361" class="Symbol">(</a><a id="362" href="Level.html#362" class="Bound">A</a> <a id="364" class="Symbol">:</a> <a id="366" class="PrimitiveType">Set</a> <a id="370" href="Level.html#356" class="Bound">a</a><a id="371" class="Symbol">)</a> <a id="373" class="Symbol">:</a> <a id="375" class="PrimitiveType">Set</a> <a id="379" class="Symbol">(</a><a id="380" href="Level.html#356" class="Bound">a</a> <a id="382" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">⊔</a> <a id="384" href="Level.html#358" class="Bound">ℓ</a><a id="385" class="Symbol">)</a> <a id="387" class="Keyword">where</a>
<a id="395" class="Keyword">constructor</a> <a id="Lift.lift" href="Level.html#Lift.lift" class="InductiveConstructor">lift</a>
<a id="414" class="Keyword">field</a> <a id="Lift.lower" href="Level.html#Lift.lower" class="Field">lower</a> <a id="426" class="Symbol">:</a> <a id="428" href="Level.html#362" class="Bound">A</a>
<a id="431" class="Keyword">open</a> <a id="436" href="Level.html#Lift" class="Module">Lift</a> <a id="441" class="Keyword">public</a>
</pre></body></html>
|