22 lines
14 KiB
HTML
22 lines
14 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>UIPK</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="Pragma">--without-K</a> <a id="32" class="Symbol">#-}</a>
|
||
<a id="36" class="Keyword">open</a> <a id="41" class="Keyword">import</a> <a id="48" href="Agda.Primitive.html" class="Module">Agda.Primitive</a> <a id="63" class="Keyword">renaming</a> <a id="72" class="Symbol">(</a><a id="73" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="77" class="Symbol">to</a> <a id="80" class="Primitive">𝒰</a><a id="81" class="Symbol">)</a>
|
||
<a id="83" class="Keyword">open</a> <a id="88" class="Keyword">import</a> <a id="95" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a>
|
||
|
||
<a id="118" class="Keyword">module</a> <a id="125" href="UIPK.html" class="Module">UIPK</a> <a id="130" class="Symbol">(</a><a id="131" href="UIPK.html#131" class="Bound">UIP</a> <a id="135" class="Symbol">:</a> <a id="137" class="Symbol">∀</a> <a id="139" class="Symbol">{</a><a id="140" href="UIPK.html#140" class="Bound">ₙ</a><a id="141" class="Symbol">}</a> <a id="143" class="Symbol">{</a><a id="144" href="UIPK.html#144" class="Bound">A</a> <a id="146" class="Symbol">:</a> <a id="148" href="UIPK.html#80" class="Primitive">𝒰</a> <a id="150" href="UIPK.html#140" class="Bound">ₙ</a><a id="151" class="Symbol">}</a> <a id="153" class="Symbol">{</a><a id="154" href="UIPK.html#154" class="Bound">x</a> <a id="156" href="UIPK.html#156" class="Bound">y</a> <a id="158" class="Symbol">:</a> <a id="160" href="UIPK.html#144" class="Bound">A</a><a id="161" class="Symbol">}</a> <a id="163" class="Symbol">(</a><a id="164" href="UIPK.html#164" class="Bound">p</a> <a id="166" href="UIPK.html#166" class="Bound">q</a> <a id="168" class="Symbol">:</a> <a id="170" href="UIPK.html#154" class="Bound">x</a> <a id="172" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="174" href="UIPK.html#156" class="Bound">y</a><a id="175" class="Symbol">)</a> <a id="177" class="Symbol">→</a> <a id="179" href="UIPK.html#164" class="Bound">p</a> <a id="181" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="183" href="UIPK.html#166" class="Bound">q</a><a id="184" class="Symbol">)</a>
|
||
<a id="198" class="Keyword">where</a>
|
||
|
||
<a id="J"></a><a id="205" href="UIPK.html#205" class="Function">J</a> <a id="207" class="Symbol">:</a> <a id="209" class="Symbol">∀</a> <a id="211" class="Symbol">{</a><a id="212" href="UIPK.html#212" class="Bound">ₙ</a> <a id="214" href="UIPK.html#214" class="Bound">ₘ</a><a id="215" class="Symbol">}</a> <a id="217" class="Symbol">{</a><a id="218" href="UIPK.html#218" class="Bound">A</a> <a id="220" class="Symbol">:</a> <a id="222" href="UIPK.html#80" class="Primitive">𝒰</a> <a id="224" href="UIPK.html#212" class="Bound">ₙ</a><a id="225" class="Symbol">}</a> <a id="227" class="Symbol">{</a><a id="228" href="UIPK.html#228" class="Bound">x</a> <a id="230" href="UIPK.html#230" class="Bound">y</a> <a id="232" class="Symbol">:</a> <a id="234" href="UIPK.html#218" class="Bound">A</a><a id="235" class="Symbol">}</a> <a id="237" class="Symbol">(</a><a id="238" href="UIPK.html#238" class="Bound">P</a> <a id="240" class="Symbol">:</a> <a id="242" class="Symbol">(</a><a id="243" href="UIPK.html#243" class="Bound">a</a> <a id="245" href="UIPK.html#245" class="Bound">b</a> <a id="247" class="Symbol">:</a> <a id="249" href="UIPK.html#218" class="Bound">A</a><a id="250" class="Symbol">)</a> <a id="252" class="Symbol">→</a> <a id="254" href="UIPK.html#243" class="Bound">a</a> <a id="256" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="258" href="UIPK.html#245" class="Bound">b</a> <a id="260" class="Symbol">→</a> <a id="262" href="UIPK.html#80" class="Primitive">𝒰</a> <a id="264" href="UIPK.html#214" class="Bound">ₘ</a><a id="265" class="Symbol">)</a> <a id="267" class="Symbol">→</a> <a id="269" href="UIPK.html#238" class="Bound">P</a> <a id="271" href="UIPK.html#228" class="Bound">x</a> <a id="273" href="UIPK.html#228" class="Bound">x</a> <a id="275" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="280" class="Symbol">→</a> <a id="282" class="Symbol">(</a><a id="283" href="UIPK.html#283" class="Bound">p</a> <a id="285" class="Symbol">:</a> <a id="287" href="UIPK.html#228" class="Bound">x</a> <a id="289" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="291" href="UIPK.html#230" class="Bound">y</a><a id="292" class="Symbol">)</a> <a id="294" class="Symbol">→</a> <a id="296" href="UIPK.html#238" class="Bound">P</a> <a id="298" href="UIPK.html#228" class="Bound">x</a> <a id="300" href="UIPK.html#230" class="Bound">y</a> <a id="302" href="UIPK.html#283" class="Bound">p</a>
|
||
<a id="304" href="UIPK.html#205" class="Function">J</a> <a id="306" class="Symbol">_</a> <a id="308" href="UIPK.html#308" class="Bound">Prefl</a> <a id="314" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="319" class="Symbol">=</a> <a id="321" href="UIPK.html#308" class="Bound">Prefl</a>
|
||
|
||
<a id="square"></a><a id="328" href="UIPK.html#328" class="Function">square</a> <a id="335" class="Symbol">:</a> <a id="337" class="Symbol">∀</a> <a id="339" class="Symbol">{</a><a id="340" href="UIPK.html#340" class="Bound">ₙ</a><a id="341" class="Symbol">}</a> <a id="343" class="Symbol">{</a><a id="344" href="UIPK.html#344" class="Bound">A</a> <a id="346" class="Symbol">:</a> <a id="348" href="UIPK.html#80" class="Primitive">𝒰</a> <a id="350" href="UIPK.html#340" class="Bound">ₙ</a><a id="351" class="Symbol">}</a> <a id="353" class="Symbol">{</a><a id="354" href="UIPK.html#354" class="Bound">x</a> <a id="356" href="UIPK.html#356" class="Bound">y</a> <a id="358" href="UIPK.html#358" class="Bound">z</a> <a id="360" href="UIPK.html#360" class="Bound">w</a> <a id="362" class="Symbol">:</a> <a id="364" href="UIPK.html#344" class="Bound">A</a><a id="365" class="Symbol">}</a> <a id="367" class="Symbol">→</a> <a id="369" href="UIPK.html#354" class="Bound">x</a> <a id="371" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="373" href="UIPK.html#358" class="Bound">z</a> <a id="375" class="Symbol">→</a> <a id="377" href="UIPK.html#356" class="Bound">y</a> <a id="379" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="381" href="UIPK.html#360" class="Bound">w</a> <a id="383" class="Symbol">→</a> <a id="385" href="UIPK.html#354" class="Bound">x</a> <a id="387" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="389" href="UIPK.html#356" class="Bound">y</a> <a id="391" class="Symbol">→</a> <a id="393" href="UIPK.html#358" class="Bound">z</a> <a id="395" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="397" href="UIPK.html#360" class="Bound">w</a>
|
||
<a id="399" href="UIPK.html#328" class="Function">square</a> <a id="406" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="411" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="416" href="UIPK.html#416" class="Bound">p</a> <a id="418" class="Symbol">=</a> <a id="420" href="UIPK.html#416" class="Bound">p</a>
|
||
|
||
<a id="transp"></a><a id="423" href="UIPK.html#423" class="Function">transp</a> <a id="430" class="Symbol">:</a> <a id="432" class="Symbol">∀</a> <a id="434" class="Symbol">{</a><a id="435" href="UIPK.html#435" class="Bound">ₙ</a> <a id="437" href="UIPK.html#437" class="Bound">ₘ</a><a id="438" class="Symbol">}</a> <a id="440" class="Symbol">{</a><a id="441" href="UIPK.html#441" class="Bound">A</a> <a id="443" class="Symbol">:</a> <a id="445" href="UIPK.html#80" class="Primitive">𝒰</a> <a id="447" href="UIPK.html#435" class="Bound">ₙ</a><a id="448" class="Symbol">}</a> <a id="450" class="Symbol">{</a><a id="451" href="UIPK.html#451" class="Bound">x</a> <a id="453" href="UIPK.html#453" class="Bound">y</a> <a id="455" class="Symbol">:</a> <a id="457" href="UIPK.html#441" class="Bound">A</a><a id="458" class="Symbol">}</a> <a id="460" class="Symbol">(</a><a id="461" href="UIPK.html#461" class="Bound">P</a> <a id="463" class="Symbol">:</a> <a id="465" href="UIPK.html#441" class="Bound">A</a> <a id="467" class="Symbol">→</a> <a id="469" href="UIPK.html#80" class="Primitive">𝒰</a> <a id="471" href="UIPK.html#437" class="Bound">ₘ</a><a id="472" class="Symbol">)</a> <a id="474" class="Symbol">→</a> <a id="476" href="UIPK.html#451" class="Bound">x</a> <a id="478" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="480" href="UIPK.html#453" class="Bound">y</a> <a id="482" class="Symbol">→</a> <a id="484" href="UIPK.html#461" class="Bound">P</a> <a id="486" href="UIPK.html#451" class="Bound">x</a> <a id="488" class="Symbol">→</a> <a id="490" href="UIPK.html#461" class="Bound">P</a> <a id="492" href="UIPK.html#453" class="Bound">y</a>
|
||
<a id="494" href="UIPK.html#423" class="Function">transp</a> <a id="501" href="UIPK.html#501" class="Bound">P</a> <a id="503" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="508" href="UIPK.html#508" class="Bound">Px</a> <a id="511" class="Symbol">=</a> <a id="513" href="UIPK.html#508" class="Bound">Px</a>
|
||
|
||
<a id="K"></a><a id="517" href="UIPK.html#517" class="Function">K</a> <a id="519" class="Symbol">:</a> <a id="521" class="Symbol">∀</a> <a id="523" class="Symbol">{</a><a id="524" href="UIPK.html#524" class="Bound">ₙ</a> <a id="526" href="UIPK.html#526" class="Bound">ₘ</a><a id="527" class="Symbol">}</a> <a id="529" class="Symbol">{</a><a id="530" href="UIPK.html#530" class="Bound">A</a> <a id="532" class="Symbol">:</a> <a id="534" href="UIPK.html#80" class="Primitive">𝒰</a> <a id="536" href="UIPK.html#524" class="Bound">ₙ</a><a id="537" class="Symbol">}</a> <a id="539" class="Symbol">{</a><a id="540" href="UIPK.html#540" class="Bound">x</a> <a id="542" class="Symbol">:</a> <a id="544" href="UIPK.html#530" class="Bound">A</a><a id="545" class="Symbol">}</a> <a id="547" class="Symbol">(</a><a id="548" href="UIPK.html#548" class="Bound">P</a> <a id="550" class="Symbol">:</a> <a id="552" href="UIPK.html#540" class="Bound">x</a> <a id="554" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="556" href="UIPK.html#540" class="Bound">x</a> <a id="558" class="Symbol">→</a> <a id="560" href="UIPK.html#80" class="Primitive">𝒰</a> <a id="562" href="UIPK.html#526" class="Bound">ₘ</a><a id="563" class="Symbol">)</a> <a id="565" class="Symbol">→</a> <a id="567" href="UIPK.html#548" class="Bound">P</a> <a id="569" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="574" class="Symbol">→</a> <a id="576" class="Symbol">(</a><a id="577" href="UIPK.html#577" class="Bound">p</a> <a id="579" class="Symbol">:</a> <a id="581" href="UIPK.html#540" class="Bound">x</a> <a id="583" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="585" href="UIPK.html#540" class="Bound">x</a><a id="586" class="Symbol">)</a> <a id="588" class="Symbol">→</a> <a id="590" href="UIPK.html#548" class="Bound">P</a> <a id="592" href="UIPK.html#577" class="Bound">p</a>
|
||
<a id="594" href="UIPK.html#517" class="Function">K</a> <a id="596" class="Symbol">{</a><a id="597" class="Argument">x</a> <a id="599" class="Symbol">=</a> <a id="601" href="UIPK.html#601" class="Bound">x</a><a id="602" class="Symbol">}</a> <a id="604" href="UIPK.html#604" class="Bound">P</a> <a id="606" href="UIPK.html#606" class="Bound">Prefl</a> <a id="612" href="UIPK.html#612" class="Bound">p</a> <a id="614" class="Symbol">=</a> <a id="616" class="Symbol">(</a><a id="617" href="UIPK.html#205" class="Function">J</a> <a id="619" class="Symbol">(λ</a> <a id="622" href="UIPK.html#622" class="Bound">a</a> <a id="624" href="UIPK.html#624" class="Bound">b</a> <a id="626" href="UIPK.html#626" class="Bound">q</a> <a id="628" class="Symbol">→</a> <a id="630" class="Symbol">(</a><a id="631" href="UIPK.html#631" class="Bound">r</a> <a id="633" class="Symbol">:</a> <a id="635" href="UIPK.html#622" class="Bound">a</a> <a id="637" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="639" href="UIPK.html#601" class="Bound">x</a><a id="640" class="Symbol">)</a> <a id="642" class="Symbol">→</a> <a id="644" class="Symbol">(</a><a id="645" href="UIPK.html#645" class="Bound">s</a> <a id="647" class="Symbol">:</a> <a id="649" href="UIPK.html#624" class="Bound">b</a> <a id="651" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="653" href="UIPK.html#601" class="Bound">x</a><a id="654" class="Symbol">)</a> <a id="656" class="Symbol">→</a> <a id="658" href="UIPK.html#604" class="Bound">P</a> <a id="660" class="Symbol">(</a><a id="661" href="UIPK.html#328" class="Function">square</a> <a id="668" href="UIPK.html#631" class="Bound">r</a> <a id="670" href="UIPK.html#645" class="Bound">s</a> <a id="672" href="UIPK.html#626" class="Bound">q</a><a id="673" class="Symbol">))</a>
|
||
<a id="701" class="Symbol">(λ</a> <a id="704" href="UIPK.html#704" class="Bound">a</a> <a id="706" href="UIPK.html#706" class="Bound">b</a> <a id="708" class="Symbol">→</a> <a id="710" href="UIPK.html#423" class="Function">transp</a> <a id="717" href="UIPK.html#604" class="Bound">P</a> <a id="719" class="Symbol">(</a><a id="720" href="UIPK.html#131" class="Bound">UIP</a> <a id="724" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="729" class="Symbol">(</a><a id="730" href="UIPK.html#328" class="Function">square</a> <a id="737" href="UIPK.html#704" class="Bound">a</a> <a id="739" href="UIPK.html#706" class="Bound">b</a> <a id="741" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a><a id="745" class="Symbol">))</a> <a id="748" href="UIPK.html#606" class="Bound">Prefl</a><a id="753" class="Symbol">)</a>
|
||
<a id="780" href="UIPK.html#612" class="Bound">p</a><a id="781" class="Symbol">)</a> <a id="783" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="788" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
</pre></body></html> |