30 lines
5.0 KiB
HTML
30 lines
5.0 KiB
HTML
|
<!DOCTYPE HTML>
|
||
|
|
<html><head><meta charset="utf-8"><title>Function.Core</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><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">-- Core definitions for Functions</a>
|
||
|
|
<a id="140" class="Comment">------------------------------------------------------------------------</a>
|
||
|
|
|
||
|
|
<a id="214" class="Comment">-- The contents of this file should usually be accessed from `Function`.</a>
|
||
|
|
|
||
|
|
<a id="288" class="Symbol">{-#</a> <a id="292" class="Keyword">OPTIONS</a> <a id="300" class="Pragma">--without-K</a> <a id="312" class="Pragma">--safe</a> <a id="319" class="Symbol">#-}</a>
|
||
|
|
|
||
|
|
<a id="324" class="Keyword">module</a> <a id="331" href="Function.Core.html" class="Module">Function.Core</a> <a id="345" class="Keyword">where</a>
|
||
|
|
|
||
|
|
<a id="352" class="Keyword">open</a> <a id="357" class="Keyword">import</a> <a id="364" href="Level.html" class="Module">Level</a> <a id="370" class="Keyword">using</a> <a id="376" class="Symbol">(</a><a id="377" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="380" class="Symbol">)</a>
|
||
|
|
|
||
|
|
<a id="383" class="Comment">------------------------------------------------------------------------</a>
|
||
|
|
<a id="456" class="Comment">-- Types</a>
|
||
|
|
|
||
|
|
<a id="Fun₁"></a><a id="466" href="Function.Core.html#466" class="Function">Fun₁</a> <a id="471" class="Symbol">:</a> <a id="473" class="Symbol">∀</a> <a id="475" class="Symbol">{</a><a id="476" href="Function.Core.html#476" class="Bound">a</a><a id="477" class="Symbol">}</a> <a id="479" class="Symbol">→</a> <a id="481" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="485" href="Function.Core.html#476" class="Bound">a</a> <a id="487" class="Symbol">→</a> <a id="489" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="493" href="Function.Core.html#476" class="Bound">a</a>
|
||
|
|
<a id="495" href="Function.Core.html#466" class="Function">Fun₁</a> <a id="500" href="Function.Core.html#500" class="Bound">A</a> <a id="502" class="Symbol">=</a> <a id="504" href="Function.Core.html#500" class="Bound">A</a> <a id="506" class="Symbol">→</a> <a id="508" href="Function.Core.html#500" class="Bound">A</a>
|
||
|
|
|
||
|
|
<a id="Fun₂"></a><a id="511" href="Function.Core.html#511" class="Function">Fun₂</a> <a id="516" class="Symbol">:</a> <a id="518" class="Symbol">∀</a> <a id="520" class="Symbol">{</a><a id="521" href="Function.Core.html#521" class="Bound">a</a><a id="522" class="Symbol">}</a> <a id="524" class="Symbol">→</a> <a id="526" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="530" href="Function.Core.html#521" class="Bound">a</a> <a id="532" class="Symbol">→</a> <a id="534" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="538" href="Function.Core.html#521" class="Bound">a</a>
|
||
|
|
<a id="540" href="Function.Core.html#511" class="Function">Fun₂</a> <a id="545" href="Function.Core.html#545" class="Bound">A</a> <a id="547" class="Symbol">=</a> <a id="549" href="Function.Core.html#545" class="Bound">A</a> <a id="551" class="Symbol">→</a> <a id="553" href="Function.Core.html#545" class="Bound">A</a> <a id="555" class="Symbol">→</a> <a id="557" href="Function.Core.html#545" class="Bound">A</a>
|
||
|
|
|
||
|
|
<a id="560" class="Comment">------------------------------------------------------------------------</a>
|
||
|
|
<a id="633" class="Comment">-- Morphism</a>
|
||
|
|
|
||
|
|
<a id="Morphism"></a><a id="646" href="Function.Core.html#646" class="Function">Morphism</a> <a id="655" class="Symbol">:</a> <a id="657" class="Symbol">∀</a> <a id="659" class="Symbol">{</a><a id="660" href="Function.Core.html#660" class="Bound">a</a><a id="661" class="Symbol">}</a> <a id="663" class="Symbol">→</a> <a id="665" class="Symbol">∀</a> <a id="667" class="Symbol">{</a><a id="668" href="Function.Core.html#668" class="Bound">b</a><a id="669" class="Symbol">}</a> <a id="671" class="Symbol">→</a> <a id="673" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="677" href="Function.Core.html#660" class="Bound">a</a> <a id="679" class="Symbol">→</a> <a id="681" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="685" href="Function.Core.html#668" class="Bound">b</a> <a id="687" class="Symbol">→</a> <a id="689" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="693" class="Symbol">(</a><a id="694" href="Function.Core.html#660" class="Bound">a</a> <a id="696" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="698" href="Function.Core.html#668" class="Bound">b</a><a id="699" class="Symbol">)</a>
|
||
|
|
<a id="701" href="Function.Core.html#646" class="Function">Morphism</a> <a id="710" href="Function.Core.html#710" class="Bound">A</a> <a id="712" href="Function.Core.html#712" class="Bound">B</a> <a id="714" class="Symbol">=</a> <a id="716" href="Function.Core.html#710" class="Bound">A</a> <a id="718" class="Symbol">→</a> <a id="720" href="Function.Core.html#712" class="Bound">B</a>
|
||
|
|
</pre></body></html>
|