Skip to content

Commit

Permalink
Update HTML
Browse files Browse the repository at this point in the history
  • Loading branch information
Rahul Chhabra authored and Rahul Chhabra committed Dec 20, 2023
1 parent 5d89fa5 commit 95f6fbc
Show file tree
Hide file tree
Showing 57 changed files with 3,062 additions and 966 deletions.
300 changes: 150 additions & 150 deletions docs/Cubical.Displayed.Auto.html
View file

Large diffs are not rendered by default.

42 changes: 21 additions & 21 deletions docs/Cubical.Displayed.Base.html
View file

Large diffs are not rendered by default.

10 changes: 5 additions & 5 deletions docs/Cubical.Displayed.Constant.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,12 @@

<a id="274" class="Keyword">private</a>
<a id="284" class="Keyword">variable</a>
<a id="297" href="Cubical.Displayed.Constant.html#297" class="Generalizable">ℓ</a> <a id="299" href="Cubical.Displayed.Constant.html#299" class="Generalizable">ℓA</a> <a id="302" href="Cubical.Displayed.Constant.html#302" class="Generalizable">ℓA&#39;</a> <a id="306" href="Cubical.Displayed.Constant.html#306" class="Generalizable">ℓP</a> <a id="309" href="Cubical.Displayed.Constant.html#309" class="Generalizable">ℓ≅A</a> <a id="313" href="Cubical.Displayed.Constant.html#313" class="Generalizable">ℓ≅A&#39;</a> <a id="318" href="Cubical.Displayed.Constant.html#318" class="Generalizable">ℓB</a> <a id="321" href="Cubical.Displayed.Constant.html#321" class="Generalizable">ℓB&#39;</a> <a id="325" href="Cubical.Displayed.Constant.html#325" class="Generalizable">ℓ≅B</a> <a id="329" href="Cubical.Displayed.Constant.html#329" class="Generalizable">ℓ≅B&#39;</a> <a id="334" href="Cubical.Displayed.Constant.html#334" class="Generalizable">ℓC</a> <a id="337" href="Cubical.Displayed.Constant.html#337" class="Generalizable">ℓ≅C</a> <a id="341" class="Symbol">:</a> <a id="343" href="Agda.Primitive.html#591" class="Postulate">Level</a>
<a id="297" href="Cubical.Displayed.Constant.html#297" class="Generalizable">ℓ</a> <a id="299" href="Cubical.Displayed.Constant.html#299" class="Generalizable">ℓA</a> <a id="302" href="Cubical.Displayed.Constant.html#302" class="Generalizable">ℓA&#39;</a> <a id="306" href="Cubical.Displayed.Constant.html#306" class="Generalizable">ℓP</a> <a id="309" href="Cubical.Displayed.Constant.html#309" class="Generalizable">ℓ≅A</a> <a id="313" href="Cubical.Displayed.Constant.html#313" class="Generalizable">ℓ≅A&#39;</a> <a id="318" href="Cubical.Displayed.Constant.html#318" class="Generalizable">ℓB</a> <a id="321" href="Cubical.Displayed.Constant.html#321" class="Generalizable">ℓB&#39;</a> <a id="325" href="Cubical.Displayed.Constant.html#325" class="Generalizable">ℓ≅B</a> <a id="329" href="Cubical.Displayed.Constant.html#329" class="Generalizable">ℓ≅B&#39;</a> <a id="334" href="Cubical.Displayed.Constant.html#334" class="Generalizable">ℓC</a> <a id="337" href="Cubical.Displayed.Constant.html#337" class="Generalizable">ℓ≅C</a> <a id="341" class="Symbol">:</a> <a id="343" href="Agda.Primitive.html#742" class="Postulate">Level</a>

<a id="350" class="Comment">-- constant DUARel</a>

<a id="370" class="Keyword">module</a> <a id="377" href="Cubical.Displayed.Constant.html#377" class="Module">_</a> <a id="379" class="Symbol">{</a><a id="380" href="Cubical.Displayed.Constant.html#380" class="Bound">A</a> <a id="382" class="Symbol">:</a> <a id="384" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="389" href="Cubical.Displayed.Constant.html#299" class="Generalizable">ℓA</a><a id="391" class="Symbol">}</a> <a id="393" class="Symbol">(</a><a id="394" href="Cubical.Displayed.Constant.html#394" class="Bound">𝒮-A</a> <a id="398" class="Symbol">:</a> <a id="400" href="Cubical.Displayed.Base.html#433" class="Record">UARel</a> <a id="406" href="Cubical.Displayed.Constant.html#380" class="Bound">A</a> <a id="408" href="Cubical.Displayed.Constant.html#309" class="Generalizable">ℓ≅A</a><a id="411" class="Symbol">)</a>
<a id="415" class="Symbol">{</a><a id="416" href="Cubical.Displayed.Constant.html#416" class="Bound">B</a> <a id="418" class="Symbol">:</a> <a id="420" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="425" href="Cubical.Displayed.Constant.html#318" class="Generalizable">ℓB</a><a id="427" class="Symbol">}</a> <a id="429" class="Symbol">(</a><a id="430" href="Cubical.Displayed.Constant.html#430" class="Bound">𝒮-B</a> <a id="434" class="Symbol">:</a> <a id="436" href="Cubical.Displayed.Base.html#433" class="Record">UARel</a> <a id="442" href="Cubical.Displayed.Constant.html#416" class="Bound">B</a> <a id="444" href="Cubical.Displayed.Constant.html#325" class="Generalizable">ℓ≅B</a><a id="447" class="Symbol">)</a> <a id="450" class="Keyword">where</a>
<a id="370" class="Keyword">module</a> <a id="377" href="Cubical.Displayed.Constant.html#377" class="Module">_</a> <a id="379" class="Symbol">{</a><a id="380" href="Cubical.Displayed.Constant.html#380" class="Bound">A</a> <a id="382" class="Symbol">:</a> <a id="384" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="389" href="Cubical.Displayed.Constant.html#299" class="Generalizable">ℓA</a><a id="391" class="Symbol">}</a> <a id="393" class="Symbol">(</a><a id="394" href="Cubical.Displayed.Constant.html#394" class="Bound">𝒮-A</a> <a id="398" class="Symbol">:</a> <a id="400" href="Cubical.Displayed.Base.html#433" class="Record">UARel</a> <a id="406" href="Cubical.Displayed.Constant.html#380" class="Bound">A</a> <a id="408" href="Cubical.Displayed.Constant.html#309" class="Generalizable">ℓ≅A</a><a id="411" class="Symbol">)</a>
<a id="415" class="Symbol">{</a><a id="416" href="Cubical.Displayed.Constant.html#416" class="Bound">B</a> <a id="418" class="Symbol">:</a> <a id="420" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="425" href="Cubical.Displayed.Constant.html#318" class="Generalizable">ℓB</a><a id="427" class="Symbol">}</a> <a id="429" class="Symbol">(</a><a id="430" href="Cubical.Displayed.Constant.html#430" class="Bound">𝒮-B</a> <a id="434" class="Symbol">:</a> <a id="436" href="Cubical.Displayed.Base.html#433" class="Record">UARel</a> <a id="442" href="Cubical.Displayed.Constant.html#416" class="Bound">B</a> <a id="444" href="Cubical.Displayed.Constant.html#325" class="Generalizable">ℓ≅B</a><a id="447" class="Symbol">)</a> <a id="450" class="Keyword">where</a>

<a id="459" class="Keyword">open</a> <a id="464" href="Cubical.Displayed.Base.html#433" class="Module">UARel</a> <a id="470" href="Cubical.Displayed.Constant.html#430" class="Bound">𝒮-B</a>
<a id="476" class="Keyword">open</a> <a id="481" href="Cubical.Displayed.Base.html#1242" class="Module">DUARel</a>
Expand All @@ -31,11 +31,11 @@

<a id="597" class="Comment">-- SubstRel for an arbitrary constant family</a>

<a id="643" class="Keyword">module</a> <a id="650" href="Cubical.Displayed.Constant.html#650" class="Module">_</a> <a id="652" class="Symbol">{</a><a id="653" href="Cubical.Displayed.Constant.html#653" class="Bound">A</a> <a id="655" class="Symbol">:</a> <a id="657" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="662" href="Cubical.Displayed.Constant.html#299" class="Generalizable">ℓA</a><a id="664" class="Symbol">}</a> <a id="666" class="Symbol">(</a><a id="667" href="Cubical.Displayed.Constant.html#667" class="Bound">𝒮-A</a> <a id="671" class="Symbol">:</a> <a id="673" href="Cubical.Displayed.Base.html#433" class="Record">UARel</a> <a id="679" href="Cubical.Displayed.Constant.html#653" class="Bound">A</a> <a id="681" href="Cubical.Displayed.Constant.html#309" class="Generalizable">ℓ≅A</a><a id="684" class="Symbol">)</a> <a id="686" class="Symbol">(</a><a id="687" href="Cubical.Displayed.Constant.html#687" class="Bound">B</a> <a id="689" class="Symbol">:</a> <a id="691" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="696" href="Cubical.Displayed.Constant.html#318" class="Generalizable">ℓB</a><a id="698" class="Symbol">)</a> <a id="700" class="Keyword">where</a>
<a id="643" class="Keyword">module</a> <a id="650" href="Cubical.Displayed.Constant.html#650" class="Module">_</a> <a id="652" class="Symbol">{</a><a id="653" href="Cubical.Displayed.Constant.html#653" class="Bound">A</a> <a id="655" class="Symbol">:</a> <a id="657" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="662" href="Cubical.Displayed.Constant.html#299" class="Generalizable">ℓA</a><a id="664" class="Symbol">}</a> <a id="666" class="Symbol">(</a><a id="667" href="Cubical.Displayed.Constant.html#667" class="Bound">𝒮-A</a> <a id="671" class="Symbol">:</a> <a id="673" href="Cubical.Displayed.Base.html#433" class="Record">UARel</a> <a id="679" href="Cubical.Displayed.Constant.html#653" class="Bound">A</a> <a id="681" href="Cubical.Displayed.Constant.html#309" class="Generalizable">ℓ≅A</a><a id="684" class="Symbol">)</a> <a id="686" class="Symbol">(</a><a id="687" href="Cubical.Displayed.Constant.html#687" class="Bound">B</a> <a id="689" class="Symbol">:</a> <a id="691" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="696" href="Cubical.Displayed.Constant.html#318" class="Generalizable">ℓB</a><a id="698" class="Symbol">)</a> <a id="700" class="Keyword">where</a>

<a id="709" class="Keyword">open</a> <a id="714" href="Cubical.Displayed.Subst.html#682" class="Module">SubstRel</a>

<a id="726" href="Cubical.Displayed.Constant.html#726" class="Function">𝒮ˢ-const</a> <a id="735" class="Symbol">:</a> <a id="737" href="Cubical.Displayed.Subst.html#682" class="Record">SubstRel</a> <a id="746" href="Cubical.Displayed.Constant.html#667" class="Bound">𝒮-A</a> <a id="750" class="Symbol">(λ</a> <a id="753" href="Cubical.Displayed.Constant.html#753" class="Symbol">_</a> <a id="755" class="Symbol">→</a> <a id="757" href="Cubical.Displayed.Constant.html#687" class="Bound">B</a><a id="758" class="Symbol">)</a>
<a id="762" href="Cubical.Displayed.Constant.html#726" class="Function">𝒮ˢ-const</a> <a id="771" class="Symbol">.</a><a id="772" href="Cubical.Displayed.Subst.html#872" class="Field">SubstRel.act</a> <a id="785" class="Symbol">_</a> <a id="787" class="Symbol">=</a> <a id="789" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="797" href="Cubical.Displayed.Constant.html#687" class="Bound">B</a>
<a id="801" href="Cubical.Displayed.Constant.html#726" class="Function">𝒮ˢ-const</a> <a id="810" class="Symbol">.</a><a id="811" href="Cubical.Displayed.Subst.html#915" class="Field">SubstRel.uaˢ</a> <a id="824" href="Cubical.Displayed.Constant.html#824" class="Bound">p</a> <a id="826" href="Cubical.Displayed.Constant.html#826" class="Bound">b</a> <a id="828" class="Symbol">=</a> <a id="830" href="Cubical.Foundations.Prelude.html#8847" class="Function">transportRefl</a> <a id="844" href="Cubical.Displayed.Constant.html#826" class="Bound">b</a>
<a id="801" href="Cubical.Displayed.Constant.html#726" class="Function">𝒮ˢ-const</a> <a id="810" class="Symbol">.</a><a id="811" href="Cubical.Displayed.Subst.html#915" class="Field">SubstRel.uaˢ</a> <a id="824" href="Cubical.Displayed.Constant.html#824" class="Bound">p</a> <a id="826" href="Cubical.Displayed.Constant.html#826" class="Bound">b</a> <a id="828" class="Symbol">=</a> <a id="830" href="Cubical.Foundations.Prelude.html#9176" class="Function">transportRefl</a> <a id="844" href="Cubical.Displayed.Constant.html#826" class="Bound">b</a>
</pre></body></html>
Loading

0 comments on commit 95f6fbc

Please sign in to comment.