Skip to content

Commit

Permalink
Add HTML
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahulc29
rahulc29 committed Nov 3, 2023
1 parent 90b6984 commit ba55a8f
Show file tree
Hide file tree
Showing 85 changed files with 5,501 additions and 4,931 deletions.
447 changes: 227 additions & 220 deletions docs/Cubical.Categories.Adjoint.html
View file

Large diffs are not rendered by default.

24 changes: 12 additions & 12 deletions docs/Cubical.Categories.Category.Base.html
View file

Large diffs are not rendered by default.

16 changes: 8 additions & 8 deletions docs/Cubical.Categories.Category.Properties.html
View file

Large diffs are not rendered by default.

12 changes: 6 additions & 6 deletions docs/Cubical.Categories.Commutativity.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,15 @@
<a id="442" class="Symbol">→</a> <a id="444" href="Cubical.Categories.Commutativity.html#272" class="Bound">f</a> <a id="446" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="448" class="Symbol">(</a><a id="449" href="Cubical.Categories.Commutativity.html#290" class="Bound">g</a> <a id="451" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="453" href="Cubical.Categories.Commutativity.html#314" class="Bound">l</a><a id="454" class="Symbol">)</a> <a id="456" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="458" class="Symbol">(</a><a id="459" href="Cubical.Categories.Commutativity.html#292" class="Bound">h</a> <a id="461" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="463" href="Cubical.Categories.Commutativity.html#318" class="Bound">m</a><a id="464" class="Symbol">)</a> <a id="466" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="468" href="Cubical.Categories.Commutativity.html#322" class="Bound">n</a>
<a id="472" href="Cubical.Categories.Commutativity.html#246" class="Function">compSq</a> <a id="479" class="Symbol">{</a><a id="480" class="Argument">f</a> <a id="482" class="Symbol">=</a> <a id="484" href="Cubical.Categories.Commutativity.html#484" class="Bound">f</a><a id="485" class="Symbol">}</a> <a id="487" class="Symbol">{</a><a id="488" href="Cubical.Categories.Commutativity.html#488" class="Bound">g</a><a id="489" class="Symbol">}</a> <a id="491" class="Symbol">{</a><a id="492" href="Cubical.Categories.Commutativity.html#492" class="Bound">h</a><a id="493" class="Symbol">}</a> <a id="495" class="Symbol">{</a><a id="496" href="Cubical.Categories.Commutativity.html#496" class="Bound">k</a><a id="497" class="Symbol">}</a> <a id="499" class="Symbol">{</a><a id="500" href="Cubical.Categories.Commutativity.html#500" class="Bound">l</a><a id="501" class="Symbol">}</a> <a id="503" class="Symbol">{</a><a id="504" href="Cubical.Categories.Commutativity.html#504" class="Bound">m</a><a id="505" class="Symbol">}</a> <a id="507" class="Symbol">{</a><a id="508" href="Cubical.Categories.Commutativity.html#508" class="Bound">n</a><a id="509" class="Symbol">}</a> <a id="511" href="Cubical.Categories.Commutativity.html#511" class="Bound">p</a> <a id="513" href="Cubical.Categories.Commutativity.html#513" class="Bound">q</a>
<a id="519" class="Symbol">=</a> <a id="521" href="Cubical.Categories.Commutativity.html#484" class="Bound">f</a> <a id="523" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="525" class="Symbol">(</a><a id="526" href="Cubical.Categories.Commutativity.html#488" class="Bound">g</a> <a id="528" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="530" href="Cubical.Categories.Commutativity.html#500" class="Bound">l</a><a id="531" class="Symbol">)</a>
<a id="537" href="Cubical.Foundations.Prelude.html#7981" class="Function">≡⟨</a> <a id="540" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="544" class="Symbol">(</a><a id="545" href="Cubical.Categories.Category.Base.html#709" class="Field">⋆Assoc</a> <a id="552" class="Symbol">_</a> <a id="554" class="Symbol">_</a> <a id="556" class="Symbol">_)</a> <a id="559" href="Cubical.Foundations.Prelude.html#7981" class="Function">⟩</a>
<a id="537" href="Cubical.Foundations.Prelude.html#7980" class="Function">≡⟨</a> <a id="540" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="544" class="Symbol">(</a><a id="545" href="Cubical.Categories.Category.Base.html#709" class="Field">⋆Assoc</a> <a id="552" class="Symbol">_</a> <a id="554" class="Symbol">_</a> <a id="556" class="Symbol">_)</a> <a id="559" href="Cubical.Foundations.Prelude.html#7980" class="Function">⟩</a>
<a id="567" class="Symbol">(</a><a id="568" href="Cubical.Categories.Commutativity.html#484" class="Bound">f</a> <a id="570" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="572" href="Cubical.Categories.Commutativity.html#488" class="Bound">g</a><a id="573" class="Symbol">)</a> <a id="575" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="577" href="Cubical.Categories.Commutativity.html#500" class="Bound">l</a>
<a id="583" href="Cubical.Foundations.Prelude.html#7981" class="Function">≡⟨</a> <a id="586" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="591" class="Symbol">(</a><a id="592" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">_⋆</a> <a id="595" href="Cubical.Categories.Commutativity.html#500" class="Bound">l</a><a id="596" class="Symbol">)</a> <a id="598" href="Cubical.Categories.Commutativity.html#511" class="Bound">p</a> <a id="600" href="Cubical.Foundations.Prelude.html#7981" class="Function">⟩</a>
<a id="583" href="Cubical.Foundations.Prelude.html#7980" class="Function">≡⟨</a> <a id="586" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="591" class="Symbol">(</a><a id="592" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">_⋆</a> <a id="595" href="Cubical.Categories.Commutativity.html#500" class="Bound">l</a><a id="596" class="Symbol">)</a> <a id="598" href="Cubical.Categories.Commutativity.html#511" class="Bound">p</a> <a id="600" href="Cubical.Foundations.Prelude.html#7980" class="Function">⟩</a>
<a id="608" class="Symbol">(</a><a id="609" href="Cubical.Categories.Commutativity.html#492" class="Bound">h</a> <a id="611" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="613" href="Cubical.Categories.Commutativity.html#496" class="Bound">k</a><a id="614" class="Symbol">)</a> <a id="616" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="618" href="Cubical.Categories.Commutativity.html#500" class="Bound">l</a>
<a id="624" href="Cubical.Foundations.Prelude.html#7981" class="Function">≡⟨</a> <a id="627" href="Cubical.Categories.Category.Base.html#709" class="Field">⋆Assoc</a> <a id="634" class="Symbol">_</a> <a id="636" class="Symbol">_</a> <a id="638" class="Symbol">_</a> <a id="640" href="Cubical.Foundations.Prelude.html#7981" class="Function">⟩</a>
<a id="624" href="Cubical.Foundations.Prelude.html#7980" class="Function">≡⟨</a> <a id="627" href="Cubical.Categories.Category.Base.html#709" class="Field">⋆Assoc</a> <a id="634" class="Symbol">_</a> <a id="636" class="Symbol">_</a> <a id="638" class="Symbol">_</a> <a id="640" href="Cubical.Foundations.Prelude.html#7980" class="Function">⟩</a>
<a id="648" href="Cubical.Categories.Commutativity.html#492" class="Bound">h</a> <a id="650" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="652" class="Symbol">(</a><a id="653" href="Cubical.Categories.Commutativity.html#496" class="Bound">k</a> <a id="655" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="657" href="Cubical.Categories.Commutativity.html#500" class="Bound">l</a><a id="658" class="Symbol">)</a>
<a id="664" href="Cubical.Foundations.Prelude.html#7981" class="Function">≡⟨</a> <a id="667" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="672" class="Symbol">(</a><a id="673" href="Cubical.Categories.Commutativity.html#492" class="Bound">h</a> <a id="675" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆_</a><a id="677" class="Symbol">)</a> <a id="679" href="Cubical.Categories.Commutativity.html#513" class="Bound">q</a> <a id="681" href="Cubical.Foundations.Prelude.html#7981" class="Function">⟩</a>
<a id="664" href="Cubical.Foundations.Prelude.html#7980" class="Function">≡⟨</a> <a id="667" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="672" class="Symbol">(</a><a id="673" href="Cubical.Categories.Commutativity.html#492" class="Bound">h</a> <a id="675" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆_</a><a id="677" class="Symbol">)</a> <a id="679" href="Cubical.Categories.Commutativity.html#513" class="Bound">q</a> <a id="681" href="Cubical.Foundations.Prelude.html#7980" class="Function">⟩</a>
<a id="689" href="Cubical.Categories.Commutativity.html#492" class="Bound">h</a> <a id="691" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="693" class="Symbol">(</a><a id="694" href="Cubical.Categories.Commutativity.html#504" class="Bound">m</a> <a id="696" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="698" href="Cubical.Categories.Commutativity.html#508" class="Bound">n</a><a id="699" class="Symbol">)</a>
<a id="705" href="Cubical.Foundations.Prelude.html#7981" class="Function">≡⟨</a> <a id="708" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="712" class="Symbol">(</a><a id="713" href="Cubical.Categories.Category.Base.html#709" class="Field">⋆Assoc</a> <a id="720" class="Symbol">_</a> <a id="722" class="Symbol">_</a> <a id="724" class="Symbol">_)</a> <a id="727" href="Cubical.Foundations.Prelude.html#7981" class="Function">⟩</a>
<a id="705" href="Cubical.Foundations.Prelude.html#7980" class="Function">≡⟨</a> <a id="708" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="712" class="Symbol">(</a><a id="713" href="Cubical.Categories.Category.Base.html#709" class="Field">⋆Assoc</a> <a id="720" class="Symbol">_</a> <a id="722" class="Symbol">_</a> <a id="724" class="Symbol">_)</a> <a id="727" href="Cubical.Foundations.Prelude.html#7980" class="Function">⟩</a>
<a id="735" class="Symbol">(</a><a id="736" href="Cubical.Categories.Commutativity.html#492" class="Bound">h</a> <a id="738" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="740" href="Cubical.Categories.Commutativity.html#504" class="Bound">m</a><a id="741" class="Symbol">)</a> <a id="743" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="745" href="Cubical.Categories.Commutativity.html#508" class="Bound">n</a>
<a id="751" href="Cubical.Foundations.Prelude.html#8528" class="Function Operator">∎</a>
<a id="751" href="Cubical.Foundations.Prelude.html#8527" class="Function Operator">∎</a>
</pre></body></html>
Loading

0 comments on commit ba55a8f

Please sign in to comment.