Skip to content

Commit

Permalink
Add documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahulc29
rahulc29 committed Feb 8, 2024
1 parent 452726a commit 1ceb218
Show file tree
Hide file tree
Showing 13 changed files with 1,628 additions and 1,297 deletions.
20 changes: 20 additions & 0 deletions docs/Cubical.Data.Bool.Properties.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -410,4 +410,24 @@

<a id="separatedBool"></a><a id="12070" href="Cubical.Data.Bool.Properties.html#12070" class="Function">separatedBool</a> <a id="12084" class="Symbol">:</a> <a id="12086" href="Cubical.Relation.Nullary.Base.html#1284" class="Function">Separated</a> <a id="12096" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a>
<a id="12101" href="Cubical.Data.Bool.Properties.html#12070" class="Function">separatedBool</a> <a id="12115" class="Symbol">=</a> <a id="12117" href="Cubical.Relation.Nullary.Properties.html#6859" class="Function">Discrete→Separated</a> <a id="12136" href="Cubical.Data.Bool.Base.html#756" class="Function Operator">_≟_</a>


<a id="Bool→Bool→∙Bool"></a><a id="12142" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12158" class="Symbol">:</a> <a id="12160" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12165" class="Symbol">→</a> <a id="12167" class="Symbol">(</a><a id="12168" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12173" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="12175" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12179" class="Symbol">)</a> <a id="12181" href="Cubical.Foundations.Pointed.Base.html#638" class="Function Operator">→∙</a> <a id="12184" class="Symbol">(</a><a id="12185" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12190" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="12192" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12196" class="Symbol">)</a>
<a id="12198" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12214" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12220" class="Symbol">=</a> <a id="12222" href="Cubical.Foundations.Pointed.Base.html#893" class="Function">idfun∙</a> <a id="12229" class="Symbol">_</a>
<a id="12231" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12247" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12252" class="Symbol">=</a> <a id="12254" href="Cubical.Foundations.Pointed.Properties.html#2394" class="Function">const∙</a> <a id="12261" class="Symbol">_</a> <a id="12263" class="Symbol">_</a>

<a id="Iso-Bool→∙Bool-Bool"></a><a id="12266" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12286" class="Symbol">:</a> <a id="12288" href="Cubical.Foundations.Isomorphism.html#773" class="Record">Iso</a> <a id="12292" class="Symbol">((</a><a id="12294" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12299" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="12301" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12305" class="Symbol">)</a> <a id="12307" href="Cubical.Foundations.Pointed.Base.html#638" class="Function Operator">→∙</a> <a id="12310" class="Symbol">(</a><a id="12311" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a> <a id="12316" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="12318" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12322" class="Symbol">))</a> <a id="12325" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a>
<a id="12330" href="Cubical.Foundations.Isomorphism.html#885" class="Field">Iso.fun</a> <a id="12338" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12358" href="Cubical.Data.Bool.Properties.html#12358" class="Bound">f</a> <a id="12360" class="Symbol">=</a> <a id="12362" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12366" href="Cubical.Data.Bool.Properties.html#12358" class="Bound">f</a> <a id="12368" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a>
<a id="12374" href="Cubical.Foundations.Isomorphism.html#901" class="Field">Iso.inv</a> <a id="12382" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12402" class="Symbol">=</a> <a id="12404" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a>
<a id="12420" href="Cubical.Foundations.Isomorphism.html#917" class="Field">Iso.rightInv</a> <a id="12433" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12453" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12459" class="Symbol">=</a> <a id="12461" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="12466" href="Cubical.Foundations.Isomorphism.html#917" class="Field">Iso.rightInv</a> <a id="12479" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12499" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12504" class="Symbol">=</a> <a id="12506" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a>
<a id="12511" href="Cubical.Foundations.Isomorphism.html#948" class="Field">Iso.leftInv</a> <a id="12523" href="Cubical.Data.Bool.Properties.html#12266" class="Function">Iso-Bool→∙Bool-Bool</a> <a id="12543" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a> <a id="12545" class="Symbol">=</a> <a id="12547" href="Cubical.Data.Sigma.Properties.html#13744" class="Function">Σ≡Prop</a> <a id="12554" class="Symbol">(λ</a> <a id="12557" href="Cubical.Data.Bool.Properties.html#12557" class="Bound">_</a> <a id="12559" class="Symbol">→</a> <a id="12561" href="Cubical.Data.Bool.Properties.html#1800" class="Function">isSetBool</a> <a id="12571" class="Symbol">_</a> <a id="12573" class="Symbol">_)</a> <a id="12576" class="Symbol">(</a><a id="12577" href="Cubical.Data.Bool.Properties.html#12600" class="Function">help</a> <a id="12582" class="Symbol">_</a> <a id="12584" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a><a id="12588" class="Symbol">)</a>
<a id="12592" class="Keyword">where</a>
<a id="12600" href="Cubical.Data.Bool.Properties.html#12600" class="Function">help</a> <a id="12605" class="Symbol">:</a> <a id="12607" class="Symbol">(</a><a id="12608" href="Cubical.Data.Bool.Properties.html#12608" class="Bound">x</a> <a id="12610" class="Symbol">:</a> <a id="12612" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a><a id="12616" class="Symbol">)</a> <a id="12618" class="Symbol">→</a> <a id="12620" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12624" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a> <a id="12626" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12632" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="12634" href="Cubical.Data.Bool.Properties.html#12608" class="Bound">x</a>
<a id="12640" class="Symbol">→</a> <a id="12642" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12658" class="Symbol">(</a><a id="12659" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12663" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a> <a id="12665" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a><a id="12670" class="Symbol">)</a> <a id="12672" class="Symbol">.</a><a id="12673" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12677" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="12679" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a> <a id="12681" class="Symbol">.</a><a id="12682" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a>
<a id="12688" href="Cubical.Data.Bool.Properties.html#12600" class="Function">help</a> <a id="12693" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12699" href="Cubical.Data.Bool.Properties.html#12699" class="Bound">p</a> <a id="12701" class="Symbol">=</a> <a id="12703" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a>
<a id="12714" class="Symbol">λ</a> <a id="12716" class="Symbol">{</a> <a id="12718" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12724" class="Symbol">→</a> <a id="12726" class="Symbol">(λ</a> <a id="12729" href="Cubical.Data.Bool.Properties.html#12729" class="Bound">j</a> <a id="12731" class="Symbol">→</a> <a id="12733" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12749" class="Symbol">(</a><a id="12750" href="Cubical.Data.Bool.Properties.html#12699" class="Bound">p</a> <a id="12752" href="Cubical.Data.Bool.Properties.html#12729" class="Bound">j</a><a id="12753" class="Symbol">)</a> <a id="12755" class="Symbol">.</a><a id="12756" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12760" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a><a id="12765" class="Symbol">)</a> <a id="12767" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="12769" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12773" href="Cubical.Data.Bool.Properties.html#12699" class="Bound">p</a>
<a id="12781" class="Symbol">;</a> <a id="12783" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12788" class="Symbol">→</a> <a id="12790" class="Symbol">(λ</a> <a id="12793" href="Cubical.Data.Bool.Properties.html#12793" class="Bound">j</a> <a id="12795" class="Symbol">→</a> <a id="12797" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12813" class="Symbol">(</a><a id="12814" href="Cubical.Data.Bool.Properties.html#12699" class="Bound">p</a> <a id="12816" href="Cubical.Data.Bool.Properties.html#12793" class="Bound">j</a><a id="12817" class="Symbol">)</a> <a id="12819" class="Symbol">.</a><a id="12820" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="12824" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="12828" class="Symbol">)</a> <a id="12830" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="12832" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12836" class="Symbol">(</a><a id="12837" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="12841" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a><a id="12842" class="Symbol">)}</a>
<a id="12847" href="Cubical.Data.Bool.Properties.html#12600" class="Function">help</a> <a id="12852" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12857" href="Cubical.Data.Bool.Properties.html#12857" class="Bound">p</a> <a id="12859" class="Symbol">=</a> <a id="12861" class="Symbol">(λ</a> <a id="12864" href="Cubical.Data.Bool.Properties.html#12864" class="Bound">j</a> <a id="12866" class="Symbol">→</a> <a id="12868" href="Cubical.Data.Bool.Properties.html#12142" class="Function">Bool→Bool→∙Bool</a> <a id="12884" class="Symbol">(</a><a id="12885" href="Cubical.Data.Bool.Properties.html#12857" class="Bound">p</a> <a id="12887" href="Cubical.Data.Bool.Properties.html#12864" class="Bound">j</a><a id="12888" class="Symbol">)</a> <a id="12890" class="Symbol">.</a><a id="12891" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a><a id="12894" class="Symbol">)</a>
<a id="12910" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="12912" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="12919" class="Symbol">λ</a> <a id="12921" class="Symbol">{</a> <a id="12923" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="12929" class="Symbol">→</a> <a id="12931" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12935" href="Cubical.Data.Bool.Properties.html#12857" class="Bound">p</a> <a id="12937" class="Symbol">;</a> <a id="12939" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="12944" class="Symbol">→</a> <a id="12946" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12950" class="Symbol">(</a><a id="12951" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="12955" href="Cubical.Data.Bool.Properties.html#12543" class="Bound">f</a><a id="12956" class="Symbol">)}</a>
</pre></body></html>
Loading

0 comments on commit 1ceb218

Please sign in to comment.