Skip to content

Commit

Permalink
Add Rendered HTML
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahulc29
rahulc29 committed Dec 7, 2023
1 parent b6559cb commit 8206079
Show file tree
Hide file tree
Showing 52 changed files with 4,215 additions and 1,690 deletions.
608 changes: 365 additions & 243 deletions docs/Cubical.Categories.Adjoint.html
View file

Large diffs are not rendered by default.

37 changes: 18 additions & 19 deletions docs/Cubical.Categories.Category.Base.html
View file

Large diffs are not rendered by default.

24 changes: 24 additions & 0 deletions docs/Cubical.Categories.Category.Properties.html
View file

Large diffs are not rendered by default.

58 changes: 29 additions & 29 deletions docs/Cubical.Categories.Constructions.BinProduct.html
View file

Large diffs are not rendered by default.

319 changes: 168 additions & 151 deletions docs/Cubical.Categories.Functor.Base.html
View file

Large diffs are not rendered by default.

88 changes: 44 additions & 44 deletions docs/Cubical.Categories.Functor.Compose.html
View file

Large diffs are not rendered by default.

160 changes: 80 additions & 80 deletions docs/Cubical.Categories.Functor.Properties.html
View file

Large diffs are not rendered by default.

10 changes: 5 additions & 5 deletions docs/Cubical.Categories.Functor.html
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Categories.Functor</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>
<html><head><meta charset="utf-8"><title>Cubical.Categories.Functor</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">--allow-unsolved-metas</a> <a id="36" class="Symbol">#-}</a>

<a id="25" class="Keyword">module</a> <a id="32" href="Cubical.Categories.Functor.html" class="Module">Cubical.Categories.Functor</a> <a id="59" class="Keyword">where</a>
<a id="41" class="Keyword">module</a> <a id="48" href="Cubical.Categories.Functor.html" class="Module">Cubical.Categories.Functor</a> <a id="75" class="Keyword">where</a>

<a id="66" class="Keyword">open</a> <a id="71" class="Keyword">import</a> <a id="78" href="Cubical.Categories.Functor.Base.html" class="Module">Cubical.Categories.Functor.Base</a> <a id="110" class="Keyword">public</a>
<a id="117" class="Keyword">open</a> <a id="122" class="Keyword">import</a> <a id="129" href="Cubical.Categories.Functor.Compose.html" class="Module">Cubical.Categories.Functor.Compose</a> <a id="164" class="Keyword">public</a>
<a id="171" class="Keyword">open</a> <a id="176" class="Keyword">import</a> <a id="183" href="Cubical.Categories.Functor.Properties.html" class="Module">Cubical.Categories.Functor.Properties</a> <a id="221" class="Keyword">public</a>
<a id="82" class="Keyword">open</a> <a id="87" class="Keyword">import</a> <a id="94" href="Cubical.Categories.Functor.Base.html" class="Module">Cubical.Categories.Functor.Base</a> <a id="126" class="Keyword">public</a>
<a id="133" class="Keyword">open</a> <a id="138" class="Keyword">import</a> <a id="145" href="Cubical.Categories.Functor.Compose.html" class="Module">Cubical.Categories.Functor.Compose</a> <a id="180" class="Keyword">public</a>
<a id="187" class="Keyword">open</a> <a id="192" class="Keyword">import</a> <a id="199" href="Cubical.Categories.Functor.Properties.html" class="Module">Cubical.Categories.Functor.Properties</a> <a id="237" class="Keyword">public</a>
</pre></body></html>
12 changes: 6 additions & 6 deletions docs/Cubical.Categories.Functors.Constant.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,11 @@
<a id="224" href="Cubical.Categories.Functors.Constant.html#224" class="Generalizable">ℓC</a> <a id="227" href="Cubical.Categories.Functors.Constant.html#227" class="Generalizable">ℓC&#39;</a> <a id="231" href="Cubical.Categories.Functors.Constant.html#231" class="Generalizable">ℓD</a> <a id="234" href="Cubical.Categories.Functors.Constant.html#234" class="Generalizable">ℓD&#39;</a> <a id="238" class="Symbol">:</a> <a id="240" href="Agda.Primitive.html#591" class="Postulate">Level</a>

<a id="247" class="Keyword">open</a> <a id="252" href="Cubical.Categories.Category.Base.html#334" class="Module">Category</a>
<a id="261" class="Keyword">open</a> <a id="266" href="Cubical.Categories.Functor.Base.html#397" class="Module">Functor</a>
<a id="261" class="Keyword">open</a> <a id="266" href="Cubical.Categories.Functor.Base.html#441" class="Module">Functor</a>

<a id="Constant"></a><a id="275" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="284" class="Symbol">:</a> <a id="286" class="Symbol">(</a><a id="287" href="Cubical.Categories.Functors.Constant.html#287" class="Bound">C</a> <a id="289" class="Symbol">:</a> <a id="291" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="300" href="Cubical.Categories.Functors.Constant.html#224" class="Generalizable">ℓC</a> <a id="303" href="Cubical.Categories.Functors.Constant.html#227" class="Generalizable">ℓC&#39;</a><a id="306" class="Symbol">)</a> <a id="308" class="Symbol">(</a><a id="309" href="Cubical.Categories.Functors.Constant.html#309" class="Bound">D</a> <a id="311" class="Symbol">:</a> <a id="313" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="322" href="Cubical.Categories.Functors.Constant.html#231" class="Generalizable">ℓD</a> <a id="325" href="Cubical.Categories.Functors.Constant.html#234" class="Generalizable">ℓD&#39;</a><a id="328" class="Symbol">)</a> <a id="330" class="Symbol">(</a><a id="331" href="Cubical.Categories.Functors.Constant.html#331" class="Bound">d</a> <a id="333" class="Symbol">:</a> <a id="335" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a> <a id="338" href="Cubical.Categories.Functors.Constant.html#309" class="Bound">D</a><a id="339" class="Symbol">)</a> <a id="341" class="Symbol">→</a> <a id="343" href="Cubical.Categories.Functor.Base.html#397" class="Record">Functor</a> <a id="351" href="Cubical.Categories.Functors.Constant.html#287" class="Bound">C</a> <a id="353" href="Cubical.Categories.Functors.Constant.html#309" class="Bound">D</a>
<a id="355" href="Cubical.Categories.Functor.Base.html#557" class="Field">F-ob</a> <a id="360" class="Symbol">(</a><a id="361" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="370" href="Cubical.Categories.Functors.Constant.html#370" class="Bound">C</a> <a id="372" href="Cubical.Categories.Functors.Constant.html#372" class="Bound">D</a> <a id="374" href="Cubical.Categories.Functors.Constant.html#374" class="Bound">d</a><a id="375" class="Symbol">)</a> <a id="377" href="Cubical.Categories.Functors.Constant.html#377" class="Bound">c</a> <a id="379" class="Symbol">=</a> <a id="381" href="Cubical.Categories.Functors.Constant.html#374" class="Bound">d</a>
<a id="383" href="Cubical.Categories.Functor.Base.html#583" class="Field">F-hom</a> <a id="389" class="Symbol">(</a><a id="390" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="399" href="Cubical.Categories.Functors.Constant.html#399" class="Bound">C</a> <a id="401" href="Cubical.Categories.Functors.Constant.html#401" class="Bound">D</a> <a id="403" href="Cubical.Categories.Functors.Constant.html#403" class="Bound">d</a><a id="404" class="Symbol">)</a> <a id="406" href="Cubical.Categories.Functors.Constant.html#406" class="Bound">φ</a> <a id="408" class="Symbol">=</a> <a id="410" href="Cubical.Categories.Category.Base.html#501" class="Field">id</a> <a id="413" href="Cubical.Categories.Functors.Constant.html#401" class="Bound">D</a>
<a id="415" href="Cubical.Categories.Functor.Base.html#647" class="Field">F-id</a> <a id="420" class="Symbol">(</a><a id="421" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="430" href="Cubical.Categories.Functors.Constant.html#430" class="Bound">C</a> <a id="432" href="Cubical.Categories.Functors.Constant.html#432" class="Bound">D</a> <a id="434" href="Cubical.Categories.Functors.Constant.html#434" class="Bound">d</a><a id="435" class="Symbol">)</a> <a id="437" class="Symbol">=</a> <a id="439" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="444" href="Cubical.Categories.Functor.Base.html#708" class="Field">F-seq</a> <a id="450" class="Symbol">(</a><a id="451" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="460" href="Cubical.Categories.Functors.Constant.html#460" class="Bound">C</a> <a id="462" href="Cubical.Categories.Functors.Constant.html#462" class="Bound">D</a> <a id="464" href="Cubical.Categories.Functors.Constant.html#464" class="Bound">d</a><a id="465" class="Symbol">)</a> <a id="467" href="Cubical.Categories.Functors.Constant.html#467" class="Bound">φ</a> <a id="469" href="Cubical.Categories.Functors.Constant.html#469" class="Bound">χ</a> <a id="471" class="Symbol">=</a> <a id="473" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="477" class="Symbol">(</a><a id="478" href="Cubical.Categories.Category.Base.html#658" class="Field">⋆IdR</a> <a id="483" href="Cubical.Categories.Functors.Constant.html#462" class="Bound">D</a> <a id="485" class="Symbol">_)</a>
<a id="Constant"></a><a id="275" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="284" class="Symbol">:</a> <a id="286" class="Symbol">(</a><a id="287" href="Cubical.Categories.Functors.Constant.html#287" class="Bound">C</a> <a id="289" class="Symbol">:</a> <a id="291" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="300" href="Cubical.Categories.Functors.Constant.html#224" class="Generalizable">ℓC</a> <a id="303" href="Cubical.Categories.Functors.Constant.html#227" class="Generalizable">ℓC&#39;</a><a id="306" class="Symbol">)</a> <a id="308" class="Symbol">(</a><a id="309" href="Cubical.Categories.Functors.Constant.html#309" class="Bound">D</a> <a id="311" class="Symbol">:</a> <a id="313" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="322" href="Cubical.Categories.Functors.Constant.html#231" class="Generalizable">ℓD</a> <a id="325" href="Cubical.Categories.Functors.Constant.html#234" class="Generalizable">ℓD&#39;</a><a id="328" class="Symbol">)</a> <a id="330" class="Symbol">(</a><a id="331" href="Cubical.Categories.Functors.Constant.html#331" class="Bound">d</a> <a id="333" class="Symbol">:</a> <a id="335" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a> <a id="338" href="Cubical.Categories.Functors.Constant.html#309" class="Bound">D</a><a id="339" class="Symbol">)</a> <a id="341" class="Symbol">→</a> <a id="343" href="Cubical.Categories.Functor.Base.html#441" class="Record">Functor</a> <a id="351" href="Cubical.Categories.Functors.Constant.html#287" class="Bound">C</a> <a id="353" href="Cubical.Categories.Functors.Constant.html#309" class="Bound">D</a>
<a id="355" href="Cubical.Categories.Functor.Base.html#601" class="Field">F-ob</a> <a id="360" class="Symbol">(</a><a id="361" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="370" href="Cubical.Categories.Functors.Constant.html#370" class="Bound">C</a> <a id="372" href="Cubical.Categories.Functors.Constant.html#372" class="Bound">D</a> <a id="374" href="Cubical.Categories.Functors.Constant.html#374" class="Bound">d</a><a id="375" class="Symbol">)</a> <a id="377" href="Cubical.Categories.Functors.Constant.html#377" class="Bound">c</a> <a id="379" class="Symbol">=</a> <a id="381" href="Cubical.Categories.Functors.Constant.html#374" class="Bound">d</a>
<a id="383" href="Cubical.Categories.Functor.Base.html#627" class="Field">F-hom</a> <a id="389" class="Symbol">(</a><a id="390" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="399" href="Cubical.Categories.Functors.Constant.html#399" class="Bound">C</a> <a id="401" href="Cubical.Categories.Functors.Constant.html#401" class="Bound">D</a> <a id="403" href="Cubical.Categories.Functors.Constant.html#403" class="Bound">d</a><a id="404" class="Symbol">)</a> <a id="406" href="Cubical.Categories.Functors.Constant.html#406" class="Bound">φ</a> <a id="408" class="Symbol">=</a> <a id="410" href="Cubical.Categories.Category.Base.html#501" class="Field">id</a> <a id="413" href="Cubical.Categories.Functors.Constant.html#401" class="Bound">D</a>
<a id="415" href="Cubical.Categories.Functor.Base.html#691" class="Field">F-id</a> <a id="420" class="Symbol">(</a><a id="421" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="430" href="Cubical.Categories.Functors.Constant.html#430" class="Bound">C</a> <a id="432" href="Cubical.Categories.Functors.Constant.html#432" class="Bound">D</a> <a id="434" href="Cubical.Categories.Functors.Constant.html#434" class="Bound">d</a><a id="435" class="Symbol">)</a> <a id="437" class="Symbol">=</a> <a id="439" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="444" href="Cubical.Categories.Functor.Base.html#752" class="Field">F-seq</a> <a id="450" class="Symbol">(</a><a id="451" href="Cubical.Categories.Functors.Constant.html#275" class="Function">Constant</a> <a id="460" href="Cubical.Categories.Functors.Constant.html#460" class="Bound">C</a> <a id="462" href="Cubical.Categories.Functors.Constant.html#462" class="Bound">D</a> <a id="464" href="Cubical.Categories.Functors.Constant.html#464" class="Bound">d</a><a id="465" class="Symbol">)</a> <a id="467" href="Cubical.Categories.Functors.Constant.html#467" class="Bound">φ</a> <a id="469" href="Cubical.Categories.Functors.Constant.html#469" class="Bound">χ</a> <a id="471" class="Symbol">=</a> <a id="473" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="477" class="Symbol">(</a><a id="478" href="Cubical.Categories.Category.Base.html#658" class="Field">⋆IdR</a> <a id="483" href="Cubical.Categories.Functors.Constant.html#462" class="Bound">D</a> <a id="485" class="Symbol">_)</a>
</pre></body></html>
Loading

0 comments on commit 8206079

Please sign in to comment.