-
Notifications
You must be signed in to change notification settings - Fork 139
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deploying to gh-pages from @ 6d6870c 🚀
- Loading branch information
Showing
10 changed files
with
750 additions
and
88 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,30 @@ | ||
| <!DOCTYPE HTML> | ||
| <html><head><meta charset="utf-8"><title>Cubical.Codata.Containers.Coalgebras</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">--guardedness</a> <a id="34" class="Symbol">#-}</a> | ||
|
|
||
| <a id="39" class="Keyword">module</a> <a id="46" href="Cubical.Codata.Containers.Coalgebras.html" class="Module">Cubical.Codata.Containers.Coalgebras</a> <a id="83" class="Keyword">where</a> | ||
|
|
||
| <a id="90" class="Keyword">open</a> <a id="95" class="Keyword">import</a> <a id="102" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a> | ||
| <a id="130" class="Keyword">open</a> <a id="135" class="Keyword">import</a> <a id="142" href="Cubical.Foundations.Isomorphism.html" class="Module">Cubical.Foundations.Isomorphism</a> | ||
| <a id="174" class="Keyword">open</a> <a id="179" class="Keyword">import</a> <a id="186" href="Cubical.Foundations.Function.html" class="Module">Cubical.Foundations.Function</a> | ||
|
|
||
| <a id="216" class="Keyword">open</a> <a id="221" class="Keyword">import</a> <a id="228" href="Cubical.Codata.M.MRecord.html" class="Module">Cubical.Codata.M.MRecord</a> | ||
| <a id="253" class="Keyword">open</a> <a id="258" class="Keyword">import</a> <a id="265" href="Cubical.Data.Containers.Algebras.html" class="Module">Cubical.Data.Containers.Algebras</a> | ||
|
|
||
| <a id="299" class="Keyword">private</a> | ||
| <a id="309" class="Keyword">variable</a> | ||
| <a id="322" href="Cubical.Codata.Containers.Coalgebras.html#322" class="Generalizable">ℓ</a> <a id="324" href="Cubical.Codata.Containers.Coalgebras.html#324" class="Generalizable">ℓ'</a> <a id="327" class="Symbol">:</a> <a id="329" href="Agda.Primitive.html#742" class="Postulate">Level</a> | ||
|
|
||
| <a id="336" class="Keyword">module</a> <a id="Coalgs"></a><a id="343" href="Cubical.Codata.Containers.Coalgebras.html#343" class="Module">Coalgs</a> <a id="350" class="Symbol">(</a><a id="351" href="Cubical.Codata.Containers.Coalgebras.html#351" class="Bound">S</a> <a id="353" class="Symbol">:</a> <a id="355" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="360" href="Cubical.Codata.Containers.Coalgebras.html#322" class="Generalizable">ℓ</a><a id="361" class="Symbol">)</a> <a id="363" class="Symbol">(</a><a id="364" href="Cubical.Codata.Containers.Coalgebras.html#364" class="Bound">Q</a> <a id="366" class="Symbol">:</a> <a id="368" href="Cubical.Codata.Containers.Coalgebras.html#351" class="Bound">S</a> <a id="370" class="Symbol">→</a> <a id="372" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="377" href="Cubical.Codata.Containers.Coalgebras.html#324" class="Generalizable">ℓ'</a><a id="379" class="Symbol">)</a> <a id="381" class="Keyword">where</a> | ||
| <a id="389" class="Keyword">open</a> <a id="394" href="Cubical.Data.Containers.Algebras.html#370" class="Module">Algs</a> <a id="399" href="Cubical.Codata.Containers.Coalgebras.html#351" class="Bound">S</a> <a id="401" href="Cubical.Codata.Containers.Coalgebras.html#364" class="Bound">Q</a> | ||
| <a id="405" class="Keyword">open</a> <a id="410" href="Cubical.Foundations.Isomorphism.html#767" class="Module">Iso</a> | ||
| <a id="416" class="Keyword">open</a> <a id="421" href="Cubical.Codata.M.MRecord.html#258" class="Module">M</a> | ||
|
|
||
| <a id="Coalgs.MAlg"></a><a id="426" href="Cubical.Codata.Containers.Coalgebras.html#426" class="Function">MAlg</a> <a id="431" class="Symbol">:</a> <a id="433" href="Cubical.Data.Containers.Algebras.html#472" class="Record">ContFuncIso</a> | ||
| <a id="447" href="Cubical.Codata.Containers.Coalgebras.html#426" class="Function">MAlg</a> <a id="452" class="Symbol">=</a> <a id="454" href="Cubical.Data.Containers.Algebras.html#546" class="InductiveConstructor">iso</a> <a id="458" class="Symbol">(</a><a id="459" href="Cubical.Codata.M.MRecord.html#258" class="Record">M</a> <a id="461" href="Cubical.Codata.Containers.Coalgebras.html#351" class="Bound">S</a> <a id="463" href="Cubical.Codata.Containers.Coalgebras.html#364" class="Bound">Q</a><a id="464" class="Symbol">)</a> <a id="466" href="Cubical.Codata.Containers.Coalgebras.html#487" class="Function">isom</a> | ||
| <a id="475" class="Keyword">where</a> | ||
| <a id="487" href="Cubical.Codata.Containers.Coalgebras.html#487" class="Function">isom</a> <a id="492" class="Symbol">:</a> <a id="494" href="Cubical.Foundations.Isomorphism.html#767" class="Record">Iso</a> <a id="498" class="Symbol">(</a><a id="499" href="Cubical.Core.Primitives.html#6268" class="Function">Σ[</a> <a id="502" href="Cubical.Codata.Containers.Coalgebras.html#502" class="Bound">s</a> <a id="504" href="Cubical.Core.Primitives.html#6268" class="Function">∈</a> <a id="506" href="Cubical.Codata.Containers.Coalgebras.html#351" class="Bound">S</a> <a id="508" href="Cubical.Core.Primitives.html#6268" class="Function">]</a> <a id="510" class="Symbol">(</a><a id="511" href="Cubical.Codata.Containers.Coalgebras.html#364" class="Bound">Q</a> <a id="513" href="Cubical.Codata.Containers.Coalgebras.html#502" class="Bound">s</a> <a id="515" class="Symbol">→</a> <a id="517" href="Cubical.Codata.M.MRecord.html#258" class="Record">M</a> <a id="519" href="Cubical.Codata.Containers.Coalgebras.html#351" class="Bound">S</a> <a id="521" href="Cubical.Codata.Containers.Coalgebras.html#364" class="Bound">Q</a><a id="522" class="Symbol">))</a> <a id="525" class="Symbol">(</a><a id="526" href="Cubical.Codata.M.MRecord.html#258" class="Record">M</a> <a id="528" href="Cubical.Codata.Containers.Coalgebras.html#351" class="Bound">S</a> <a id="530" href="Cubical.Codata.Containers.Coalgebras.html#364" class="Bound">Q</a><a id="531" class="Symbol">)</a> | ||
| <a id="539" href="Cubical.Foundations.Isomorphism.html#879" class="Field">fun</a> <a id="543" href="Cubical.Codata.Containers.Coalgebras.html#487" class="Function">isom</a> <a id="548" class="Symbol">=</a> <a id="550" href="Cubical.Foundations.Function.html#1708" class="Function">uncurry</a> <a id="558" href="Cubical.Codata.M.MRecord.html#331" class="CoinductiveConstructor">sup-M</a> | ||
| <a id="570" href="Cubical.Foundations.Isomorphism.html#895" class="Field">inv</a> <a id="574" href="Cubical.Codata.Containers.Coalgebras.html#487" class="Function">isom</a> <a id="579" href="Cubical.Codata.Containers.Coalgebras.html#579" class="Bound">m</a> <a id="581" class="Symbol">=</a> <a id="583" href="Cubical.Codata.M.MRecord.html#363" class="Field">shape</a> <a id="589" href="Cubical.Codata.Containers.Coalgebras.html#579" class="Bound">m</a> <a id="591" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="593" href="Cubical.Codata.M.MRecord.html#377" class="Field">pos</a> <a id="597" href="Cubical.Codata.Containers.Coalgebras.html#579" class="Bound">m</a> | ||
| <a id="605" href="Cubical.Foundations.Isomorphism.html#911" class="Field">rightInv</a> <a id="614" href="Cubical.Codata.Containers.Coalgebras.html#487" class="Function">isom</a> <a id="619" href="Cubical.Codata.Containers.Coalgebras.html#619" class="Bound">m</a> <a id="621" class="Symbol">=</a> <a id="623" href="Cubical.Codata.M.MRecord.html#783" class="Function">ηEqM</a> <a id="628" href="Cubical.Codata.Containers.Coalgebras.html#619" class="Bound">m</a> | ||
| <a id="636" href="Cubical.Foundations.Isomorphism.html#942" class="Field">leftInv</a> <a id="644" href="Cubical.Codata.Containers.Coalgebras.html#487" class="Function">isom</a> <a id="649" class="Symbol">(</a><a id="650" href="Cubical.Codata.Containers.Coalgebras.html#650" class="Bound">s</a> <a id="652" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="654" href="Cubical.Codata.Containers.Coalgebras.html#654" class="Bound">f</a><a id="655" class="Symbol">)</a> <a id="657" class="Symbol">=</a> <a id="659" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> | ||
| </pre></body></html> |
Oops, something went wrong.