Skip to content

Commit

Permalink
Commit before major refactor
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahulc29
rahulc29 committed Dec 28, 2023
1 parent d142749 commit 5d8c7d6
Show file tree
Hide file tree
Showing 47 changed files with 4,286 additions and 1,165 deletions.
117 changes: 117 additions & 0 deletions docs/Cubical.Algebra.CommMonoid.Base.html
View file

Large diffs are not rendered by default.

61 changes: 61 additions & 0 deletions docs/Cubical.Algebra.CommMonoid.Properties.html
View file

Large diffs are not rendered by default.

7 changes: 7 additions & 0 deletions docs/Cubical.Algebra.CommMonoid.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Algebra.CommMonoid</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>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Algebra.CommMonoid.html" class="Module">Cubical.Algebra.CommMonoid</a> <a id="58" class="Keyword">where</a>

<a id="65" class="Keyword">open</a> <a id="70" class="Keyword">import</a> <a id="77" href="Cubical.Algebra.CommMonoid.Base.html" class="Module">Cubical.Algebra.CommMonoid.Base</a> <a id="109" class="Keyword">public</a>
<a id="116" class="Keyword">open</a> <a id="121" class="Keyword">import</a> <a id="128" href="Cubical.Algebra.CommMonoid.Properties.html" class="Module">Cubical.Algebra.CommMonoid.Properties</a> <a id="166" class="Keyword">public</a>
</pre></body></html>
237 changes: 237 additions & 0 deletions docs/Cubical.Algebra.Lattice.Base.html
View file

Large diffs are not rendered by default.

133 changes: 133 additions & 0 deletions docs/Cubical.Algebra.Lattice.Properties.html
View file

Large diffs are not rendered by default.

7 changes: 7 additions & 0 deletions docs/Cubical.Algebra.Lattice.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Algebra.Lattice</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>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Algebra.Lattice.html" class="Module">Cubical.Algebra.Lattice</a> <a id="55" class="Keyword">where</a>

<a id="62" class="Keyword">open</a> <a id="67" class="Keyword">import</a> <a id="74" href="Cubical.Algebra.Lattice.Base.html" class="Module">Cubical.Algebra.Lattice.Base</a> <a id="103" class="Keyword">public</a>
<a id="110" class="Keyword">open</a> <a id="115" class="Keyword">import</a> <a id="122" href="Cubical.Algebra.Lattice.Properties.html" class="Module">Cubical.Algebra.Lattice.Properties</a> <a id="157" class="Keyword">public</a>
</pre></body></html>
144 changes: 144 additions & 0 deletions docs/Cubical.Algebra.Monoid.Base.html
View file

Large diffs are not rendered by default.

61 changes: 61 additions & 0 deletions docs/Cubical.Algebra.Monoid.BigOp.html
View file

Large diffs are not rendered by default.

6 changes: 6 additions & 0 deletions docs/Cubical.Algebra.Monoid.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Algebra.Monoid</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>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Algebra.Monoid.html" class="Module">Cubical.Algebra.Monoid</a> <a id="54" class="Keyword">where</a>

<a id="61" class="Keyword">open</a> <a id="66" class="Keyword">import</a> <a id="73" href="Cubical.Algebra.Monoid.Base.html" class="Module">Cubical.Algebra.Monoid.Base</a> <a id="101" class="Keyword">public</a>
</pre></body></html>
101 changes: 101 additions & 0 deletions docs/Cubical.Algebra.Semigroup.Base.html
View file

Large diffs are not rendered by default.

6 changes: 6 additions & 0 deletions docs/Cubical.Algebra.Semigroup.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Algebra.Semigroup</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>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Algebra.Semigroup.html" class="Module">Cubical.Algebra.Semigroup</a> <a id="57" class="Keyword">where</a>

<a id="64" class="Keyword">open</a> <a id="69" class="Keyword">import</a> <a id="76" href="Cubical.Algebra.Semigroup.Base.html" class="Module">Cubical.Algebra.Semigroup.Base</a> <a id="107" class="Keyword">public</a>
</pre></body></html>
265 changes: 265 additions & 0 deletions docs/Cubical.Algebra.Semilattice.Base.html
View file

Large diffs are not rendered by default.

6 changes: 6 additions & 0 deletions docs/Cubical.Algebra.Semilattice.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Algebra.Semilattice</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>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Algebra.Semilattice.html" class="Module">Cubical.Algebra.Semilattice</a> <a id="59" class="Keyword">where</a>

<a id="66" class="Keyword">open</a> <a id="71" class="Keyword">import</a> <a id="78" href="Cubical.Algebra.Semilattice.Base.html" class="Module">Cubical.Algebra.Semilattice.Base</a> <a id="111" class="Keyword">public</a>
</pre></body></html>
45 changes: 45 additions & 0 deletions docs/Cubical.Categories.Limits.BinCoproduct.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Categories.Limits.BinCoproduct</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Binary coproducts</a>
<a id="22" class="Symbol">{-#</a> <a id="26" class="Keyword">OPTIONS</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Symbol">#-}</a>

<a id="46" class="Keyword">module</a> <a id="53" href="Cubical.Categories.Limits.BinCoproduct.html" class="Module">Cubical.Categories.Limits.BinCoproduct</a> <a id="92" class="Keyword">where</a>

<a id="99" class="Keyword">open</a> <a id="104" class="Keyword">import</a> <a id="111" href="Cubical.Categories.Category.Base.html" class="Module">Cubical.Categories.Category.Base</a>
<a id="144" class="Keyword">open</a> <a id="149" class="Keyword">import</a> <a id="156" href="Cubical.Data.Sigma.Base.html" class="Module">Cubical.Data.Sigma.Base</a>
<a id="180" class="Keyword">open</a> <a id="185" class="Keyword">import</a> <a id="192" href="Cubical.Foundations.HLevels.html" class="Module">Cubical.Foundations.HLevels</a>
<a id="220" class="Keyword">open</a> <a id="225" class="Keyword">import</a> <a id="232" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>
<a id="260" class="Keyword">open</a> <a id="265" class="Keyword">import</a> <a id="272" href="Cubical.HITs.PropositionalTruncation.Base.html" class="Module">Cubical.HITs.PropositionalTruncation.Base</a>

<a id="315" class="Keyword">private</a>
<a id="325" class="Keyword">variable</a>
<a id="338" href="Cubical.Categories.Limits.BinCoproduct.html#338" class="Generalizable">ℓ</a> <a id="340" href="Cubical.Categories.Limits.BinCoproduct.html#340" class="Generalizable">ℓ&#39;</a> <a id="343" class="Symbol">:</a> <a id="345" href="Agda.Primitive.html#742" class="Postulate">Level</a>

<a id="352" class="Keyword">module</a> <a id="359" href="Cubical.Categories.Limits.BinCoproduct.html#359" class="Module">_</a> <a id="361" class="Symbol">(</a><a id="362" href="Cubical.Categories.Limits.BinCoproduct.html#362" class="Bound">C</a> <a id="364" class="Symbol">:</a> <a id="366" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="375" href="Cubical.Categories.Limits.BinCoproduct.html#338" class="Generalizable">ℓ</a> <a id="377" href="Cubical.Categories.Limits.BinCoproduct.html#340" class="Generalizable">ℓ&#39;</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.Categories.Category.Base.html#334" class="Module">Category</a> <a id="403" href="Cubical.Categories.Limits.BinCoproduct.html#362" class="Bound">C</a>

<a id="408" class="Keyword">module</a> <a id="415" href="Cubical.Categories.Limits.BinCoproduct.html#415" class="Module">_</a> <a id="417" class="Symbol">{</a><a id="418" href="Cubical.Categories.Limits.BinCoproduct.html#418" class="Bound">x</a> <a id="420" href="Cubical.Categories.Limits.BinCoproduct.html#420" class="Bound">y</a> <a id="422" href="Cubical.Categories.Limits.BinCoproduct.html#422" class="Bound">x+y</a> <a id="426" class="Symbol">:</a> <a id="428" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a><a id="430" class="Symbol">}</a>
<a id="443" class="Symbol">(</a><a id="444" href="Cubical.Categories.Limits.BinCoproduct.html#444" class="Bound">i₁</a> <a id="447" class="Symbol">:</a> <a id="449" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">Hom[</a> <a id="454" href="Cubical.Categories.Limits.BinCoproduct.html#418" class="Bound">x</a> <a id="456" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">,</a> <a id="458" href="Cubical.Categories.Limits.BinCoproduct.html#422" class="Bound">x+y</a> <a id="462" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">]</a><a id="463" class="Symbol">)</a>
<a id="476" class="Symbol">(</a><a id="477" href="Cubical.Categories.Limits.BinCoproduct.html#477" class="Bound">i₂</a> <a id="480" class="Symbol">:</a> <a id="482" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">Hom[</a> <a id="487" href="Cubical.Categories.Limits.BinCoproduct.html#420" class="Bound">y</a> <a id="489" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">,</a> <a id="491" href="Cubical.Categories.Limits.BinCoproduct.html#422" class="Bound">x+y</a> <a id="495" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">]</a><a id="496" class="Symbol">)</a> <a id="498" class="Keyword">where</a>

<a id="509" href="Cubical.Categories.Limits.BinCoproduct.html#509" class="Function">isBinCoproduct</a> <a id="524" class="Symbol">:</a> <a id="526" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="531" class="Symbol">(</a><a id="532" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="538" href="Cubical.Categories.Limits.BinCoproduct.html#375" class="Bound">ℓ</a> <a id="540" href="Cubical.Categories.Limits.BinCoproduct.html#377" class="Bound">ℓ&#39;</a><a id="542" class="Symbol">)</a>
<a id="548" href="Cubical.Categories.Limits.BinCoproduct.html#509" class="Function">isBinCoproduct</a> <a id="563" class="Symbol">=</a> <a id="565" class="Symbol">∀</a> <a id="567" class="Symbol">{</a><a id="568" href="Cubical.Categories.Limits.BinCoproduct.html#568" class="Bound">z</a> <a id="570" class="Symbol">:</a> <a id="572" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a><a id="574" class="Symbol">}</a> <a id="576" class="Symbol">(</a><a id="577" href="Cubical.Categories.Limits.BinCoproduct.html#577" class="Bound">f₁</a> <a id="580" class="Symbol">:</a> <a id="582" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">Hom[</a> <a id="587" href="Cubical.Categories.Limits.BinCoproduct.html#418" class="Bound">x</a> <a id="589" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">,</a> <a id="591" href="Cubical.Categories.Limits.BinCoproduct.html#568" class="Bound">z</a> <a id="593" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">]</a><a id="594" class="Symbol">)</a> <a id="596" class="Symbol">(</a><a id="597" href="Cubical.Categories.Limits.BinCoproduct.html#597" class="Bound">f₂</a> <a id="600" class="Symbol">:</a> <a id="602" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">Hom[</a> <a id="607" href="Cubical.Categories.Limits.BinCoproduct.html#420" class="Bound">y</a> <a id="609" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">,</a> <a id="611" href="Cubical.Categories.Limits.BinCoproduct.html#568" class="Bound">z</a> <a id="613" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">]</a><a id="614" class="Symbol">)</a> <a id="616" class="Symbol">→</a>
<a id="626" href="Cubical.Data.Sigma.Base.html#943" class="Function">∃![</a> <a id="630" href="Cubical.Categories.Limits.BinCoproduct.html#630" class="Bound">f</a> <a id="632" href="Cubical.Data.Sigma.Base.html#943" class="Function">∈</a> <a id="634" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">Hom[</a> <a id="639" href="Cubical.Categories.Limits.BinCoproduct.html#422" class="Bound">x+y</a> <a id="643" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">,</a> <a id="645" href="Cubical.Categories.Limits.BinCoproduct.html#568" class="Bound">z</a> <a id="647" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">]</a> <a id="649" href="Cubical.Data.Sigma.Base.html#943" class="Function">]</a> <a id="651" class="Symbol">(</a><a id="652" href="Cubical.Categories.Limits.BinCoproduct.html#444" class="Bound">i₁</a> <a id="655" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="657" href="Cubical.Categories.Limits.BinCoproduct.html#630" class="Bound">f</a> <a id="659" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="661" href="Cubical.Categories.Limits.BinCoproduct.html#577" class="Bound">f₁</a><a id="663" class="Symbol">)</a> <a id="665" href="Cubical.Data.Sigma.Base.html#461" class="Function Operator">×</a> <a id="667" class="Symbol">(</a><a id="668" href="Cubical.Categories.Limits.BinCoproduct.html#477" class="Bound">i₂</a> <a id="671" href="Cubical.Categories.Category.Base.html#533" class="Field Operator">⋆</a> <a id="673" href="Cubical.Categories.Limits.BinCoproduct.html#630" class="Bound">f</a> <a id="675" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="677" href="Cubical.Categories.Limits.BinCoproduct.html#597" class="Bound">f₂</a><a id="679" class="Symbol">)</a>

<a id="686" href="Cubical.Categories.Limits.BinCoproduct.html#686" class="Function">isPropIsBinCoproduct</a> <a id="707" class="Symbol">:</a> <a id="709" href="Cubical.Foundations.Prelude.html#14575" class="Function">isProp</a> <a id="716" class="Symbol">(</a><a id="717" href="Cubical.Categories.Limits.BinCoproduct.html#509" class="Function">isBinCoproduct</a><a id="731" class="Symbol">)</a>
<a id="737" href="Cubical.Categories.Limits.BinCoproduct.html#686" class="Function">isPropIsBinCoproduct</a> <a id="758" class="Symbol">=</a> <a id="760" href="Cubical.Foundations.HLevels.html#17512" class="Function">isPropImplicitΠ</a> <a id="776" class="Symbol">(λ</a> <a id="779" href="Cubical.Categories.Limits.BinCoproduct.html#779" class="Bound">_</a> <a id="781" class="Symbol">→</a> <a id="783" href="Cubical.Foundations.HLevels.html#16452" class="Function">isPropΠ2</a> <a id="792" class="Symbol">(λ</a> <a id="795" href="Cubical.Categories.Limits.BinCoproduct.html#795" class="Bound">_</a> <a id="797" href="Cubical.Categories.Limits.BinCoproduct.html#797" class="Bound">_</a> <a id="799" class="Symbol">→</a> <a id="801" href="Cubical.Foundations.Prelude.html#18443" class="Function">isPropIsContr</a><a id="814" class="Symbol">))</a>


<a id="821" class="Keyword">record</a> <a id="828" href="Cubical.Categories.Limits.BinCoproduct.html#828" class="Record">BinCoproduct</a> <a id="841" class="Symbol">(</a><a id="842" href="Cubical.Categories.Limits.BinCoproduct.html#842" class="Bound">x</a> <a id="844" href="Cubical.Categories.Limits.BinCoproduct.html#844" class="Bound">y</a> <a id="846" class="Symbol">:</a> <a id="848" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a><a id="850" class="Symbol">)</a> <a id="852" class="Symbol">:</a> <a id="854" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="859" class="Symbol">(</a><a id="860" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="866" href="Cubical.Categories.Limits.BinCoproduct.html#375" class="Bound">ℓ</a> <a id="868" href="Cubical.Categories.Limits.BinCoproduct.html#377" class="Bound">ℓ&#39;</a><a id="870" class="Symbol">)</a> <a id="872" class="Keyword">where</a>
<a id="882" class="Keyword">field</a>
<a id="894" href="Cubical.Categories.Limits.BinCoproduct.html#894" class="Field">binCoprodOb</a> <a id="906" class="Symbol">:</a> <a id="908" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a>
<a id="917" href="Cubical.Categories.Limits.BinCoproduct.html#917" class="Field">binCoprodInj₁</a> <a id="931" class="Symbol">:</a> <a id="933" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">Hom[</a> <a id="938" href="Cubical.Categories.Limits.BinCoproduct.html#842" class="Bound">x</a> <a id="940" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">,</a> <a id="942" href="Cubical.Categories.Limits.BinCoproduct.html#894" class="Field">binCoprodOb</a> <a id="954" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">]</a>
<a id="962" href="Cubical.Categories.Limits.BinCoproduct.html#962" class="Field">binCoprodInj₂</a> <a id="976" class="Symbol">:</a> <a id="978" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">Hom[</a> <a id="983" href="Cubical.Categories.Limits.BinCoproduct.html#844" class="Bound">y</a> <a id="985" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">,</a> <a id="987" href="Cubical.Categories.Limits.BinCoproduct.html#894" class="Field">binCoprodOb</a> <a id="999" href="Cubical.Categories.Category.Base.html#468" class="Field Operator">]</a>
<a id="1007" href="Cubical.Categories.Limits.BinCoproduct.html#1007" class="Field">univProp</a> <a id="1016" class="Symbol">:</a> <a id="1018" href="Cubical.Categories.Limits.BinCoproduct.html#509" class="Function">isBinCoproduct</a> <a id="1033" href="Cubical.Categories.Limits.BinCoproduct.html#917" class="Field">binCoprodInj₁</a> <a id="1047" href="Cubical.Categories.Limits.BinCoproduct.html#962" class="Field">binCoprodInj₂</a>


<a id="1065" href="Cubical.Categories.Limits.BinCoproduct.html#1065" class="Function">BinCoproducts</a> <a id="1079" class="Symbol">:</a> <a id="1081" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="1086" class="Symbol">(</a><a id="1087" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="1093" href="Cubical.Categories.Limits.BinCoproduct.html#375" class="Bound">ℓ</a> <a id="1095" href="Cubical.Categories.Limits.BinCoproduct.html#377" class="Bound">ℓ&#39;</a><a id="1097" class="Symbol">)</a>
<a id="1101" href="Cubical.Categories.Limits.BinCoproduct.html#1065" class="Function">BinCoproducts</a> <a id="1115" class="Symbol">=</a> <a id="1117" class="Symbol">(</a><a id="1118" href="Cubical.Categories.Limits.BinCoproduct.html#1118" class="Bound">x</a> <a id="1120" href="Cubical.Categories.Limits.BinCoproduct.html#1120" class="Bound">y</a> <a id="1122" class="Symbol">:</a> <a id="1124" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a><a id="1126" class="Symbol">)</a> <a id="1128" class="Symbol">→</a> <a id="1130" href="Cubical.Categories.Limits.BinCoproduct.html#828" class="Record">BinCoproduct</a> <a id="1143" href="Cubical.Categories.Limits.BinCoproduct.html#1118" class="Bound">x</a> <a id="1145" href="Cubical.Categories.Limits.BinCoproduct.html#1120" class="Bound">y</a>

<a id="1150" href="Cubical.Categories.Limits.BinCoproduct.html#1150" class="Function">hasBinCoproducts</a> <a id="1167" class="Symbol">:</a> <a id="1169" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="1174" class="Symbol">(</a><a id="1175" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="1181" href="Cubical.Categories.Limits.BinCoproduct.html#375" class="Bound">ℓ</a> <a id="1183" href="Cubical.Categories.Limits.BinCoproduct.html#377" class="Bound">ℓ&#39;</a><a id="1185" class="Symbol">)</a>
<a id="1189" href="Cubical.Categories.Limits.BinCoproduct.html#1150" class="Function">hasBinCoproducts</a> <a id="1206" class="Symbol">=</a> <a id="1208" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥</a> <a id="1210" href="Cubical.Categories.Limits.BinCoproduct.html#1065" class="Function">BinCoproducts</a> <a id="1224" href="Cubical.HITs.PropositionalTruncation.Base.html#249" class="Datatype Operator">∥₁</a>
</pre></body></html>
Loading

0 comments on commit 5d8c7d6

Please sign in to comment.