Skip to content

Commit

Permalink
Deploying to gh-pages from @ f8d6fcf 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@mortberg
mortberg committed Nov 3, 2023
1 parent 85134c8 commit e60d022
Show file tree
Hide file tree
Showing 100 changed files with 727 additions and 676 deletions.
6 changes: 3 additions & 3 deletions Cubical.Algebra.Algebra.Properties.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -216,9 +216,9 @@

<a id="AlgebraUAFunctoriality.caracAlgebra≡"></a><a id="8322" href="Cubical.Algebra.Algebra.Properties.html#8322" class="Function">caracAlgebra≡</a> <a id="8336" class="Symbol">:</a> <a id="8338" class="Symbol">(</a><a id="8339" href="Cubical.Algebra.Algebra.Properties.html#8339" class="Bound">p</a> <a id="8341" href="Cubical.Algebra.Algebra.Properties.html#8341" class="Bound">q</a> <a id="8343" class="Symbol">:</a> <a id="8345" href="Cubical.Algebra.Algebra.Properties.html#963" class="Generalizable">A</a> <a id="8347" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="8349" href="Cubical.Algebra.Algebra.Properties.html#965" class="Generalizable">B</a><a id="8350" class="Symbol">)</a> <a id="8352" class="Symbol">→</a> <a id="8354" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="8359" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨_⟩</a> <a id="8363" href="Cubical.Algebra.Algebra.Properties.html#8339" class="Bound">p</a> <a id="8365" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="8367" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="8372" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨_⟩</a> <a id="8376" href="Cubical.Algebra.Algebra.Properties.html#8341" class="Bound">q</a> <a id="8378" class="Symbol">→</a> <a id="8380" href="Cubical.Algebra.Algebra.Properties.html#8339" class="Bound">p</a> <a id="8382" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="8384" href="Cubical.Algebra.Algebra.Properties.html#8341" class="Bound">q</a>
<a id="8387" href="Cubical.Algebra.Algebra.Properties.html#8322" class="Function">caracAlgebra≡</a> <a id="8401" class="Symbol">{</a><a id="8402" class="Argument">A</a> <a id="8404" class="Symbol">=</a> <a id="8406" href="Cubical.Algebra.Algebra.Properties.html#8406" class="Bound">A</a><a id="8407" class="Symbol">}</a> <a id="8409" class="Symbol">{</a><a id="8410" class="Argument">B</a> <a id="8412" class="Symbol">=</a> <a id="8414" href="Cubical.Algebra.Algebra.Properties.html#8414" class="Bound">B</a><a id="8415" class="Symbol">}</a> <a id="8417" href="Cubical.Algebra.Algebra.Properties.html#8417" class="Bound">p</a> <a id="8419" href="Cubical.Algebra.Algebra.Properties.html#8419" class="Bound">q</a> <a id="8421" href="Cubical.Algebra.Algebra.Properties.html#8421" class="Bound">P</a> <a id="8423" class="Symbol">=</a>
<a id="8428" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="8432" class="Symbol">(</a><a id="8433" href="Cubical.Foundations.Transport.html#2446" class="Function">transportTransport⁻</a> <a id="8453" class="Symbol">(</a><a id="8454" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="8457" class="Symbol">(</a><a id="8458" href="Cubical.Algebra.Algebra.Properties.html#7193" class="Function">Algebra≡</a> <a id="8467" href="Cubical.Algebra.Algebra.Properties.html#8406" class="Bound">A</a> <a id="8469" href="Cubical.Algebra.Algebra.Properties.html#8414" class="Bound">B</a><a id="8470" class="Symbol">))</a> <a id="8473" href="Cubical.Algebra.Algebra.Properties.html#8417" class="Bound">p</a><a id="8474" class="Symbol">)</a>
<a id="8428" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="8432" class="Symbol">(</a><a id="8433" href="Cubical.Foundations.Transport.html#2476" class="Function">transportTransport⁻</a> <a id="8453" class="Symbol">(</a><a id="8454" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="8457" class="Symbol">(</a><a id="8458" href="Cubical.Algebra.Algebra.Properties.html#7193" class="Function">Algebra≡</a> <a id="8467" href="Cubical.Algebra.Algebra.Properties.html#8406" class="Bound">A</a> <a id="8469" href="Cubical.Algebra.Algebra.Properties.html#8414" class="Bound">B</a><a id="8470" class="Symbol">))</a> <a id="8473" href="Cubical.Algebra.Algebra.Properties.html#8417" class="Bound">p</a><a id="8474" class="Symbol">)</a>
<a id="8512" href="Cubical.Foundations.Prelude.html#3576" class="Function Operator">∙∙</a> <a id="8515" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="8520" class="Symbol">(</a><a id="8521" href="Cubical.Foundations.Prelude.html#8955" class="Function">transport</a> <a id="8531" class="Symbol">(</a><a id="8532" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="8535" class="Symbol">(</a><a id="8536" href="Cubical.Algebra.Algebra.Properties.html#7193" class="Function">Algebra≡</a> <a id="8545" href="Cubical.Algebra.Algebra.Properties.html#8406" class="Bound">A</a> <a id="8547" href="Cubical.Algebra.Algebra.Properties.html#8414" class="Bound">B</a><a id="8548" class="Symbol">)))</a> <a id="8552" href="Cubical.Algebra.Algebra.Properties.html#8656" class="Function">helper</a>
<a id="8595" href="Cubical.Foundations.Prelude.html#3576" class="Function Operator">∙∙</a> <a id="8598" href="Cubical.Foundations.Transport.html#2446" class="Function">transportTransport⁻</a> <a id="8618" class="Symbol">(</a><a id="8619" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="8622" class="Symbol">(</a><a id="8623" href="Cubical.Algebra.Algebra.Properties.html#7193" class="Function">Algebra≡</a> <a id="8632" href="Cubical.Algebra.Algebra.Properties.html#8406" class="Bound">A</a> <a id="8634" href="Cubical.Algebra.Algebra.Properties.html#8414" class="Bound">B</a><a id="8635" class="Symbol">))</a> <a id="8638" href="Cubical.Algebra.Algebra.Properties.html#8419" class="Bound">q</a>
<a id="8595" href="Cubical.Foundations.Prelude.html#3576" class="Function Operator">∙∙</a> <a id="8598" href="Cubical.Foundations.Transport.html#2476" class="Function">transportTransport⁻</a> <a id="8618" class="Symbol">(</a><a id="8619" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="8622" class="Symbol">(</a><a id="8623" href="Cubical.Algebra.Algebra.Properties.html#7193" class="Function">Algebra≡</a> <a id="8632" href="Cubical.Algebra.Algebra.Properties.html#8406" class="Bound">A</a> <a id="8634" href="Cubical.Algebra.Algebra.Properties.html#8414" class="Bound">B</a><a id="8635" class="Symbol">))</a> <a id="8638" href="Cubical.Algebra.Algebra.Properties.html#8419" class="Bound">q</a>
<a id="8645" class="Keyword">where</a>
<a id="8656" href="Cubical.Algebra.Algebra.Properties.html#8656" class="Function">helper</a> <a id="8663" class="Symbol">:</a> <a id="8665" href="Cubical.Foundations.Prelude.html#8955" class="Function">transport</a> <a id="8675" class="Symbol">(</a><a id="8676" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="8680" class="Symbol">(</a><a id="8681" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="8684" class="Symbol">(</a><a id="8685" href="Cubical.Algebra.Algebra.Properties.html#7193" class="Function">Algebra≡</a> <a id="8694" href="Cubical.Algebra.Algebra.Properties.html#8406" class="Bound">A</a> <a id="8696" href="Cubical.Algebra.Algebra.Properties.html#8414" class="Bound">B</a><a id="8697" class="Symbol">)))</a> <a id="8701" href="Cubical.Algebra.Algebra.Properties.html#8417" class="Bound">p</a> <a id="8703" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="8705" href="Cubical.Foundations.Prelude.html#8955" class="Function">transport</a> <a id="8715" class="Symbol">(</a><a id="8716" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="8720" class="Symbol">(</a><a id="8721" href="Cubical.Foundations.Univalence.html#928" class="Function">ua</a> <a id="8724" class="Symbol">(</a><a id="8725" href="Cubical.Algebra.Algebra.Properties.html#7193" class="Function">Algebra≡</a> <a id="8734" href="Cubical.Algebra.Algebra.Properties.html#8406" class="Bound">A</a> <a id="8736" href="Cubical.Algebra.Algebra.Properties.html#8414" class="Bound">B</a><a id="8737" class="Symbol">)))</a> <a id="8741" href="Cubical.Algebra.Algebra.Properties.html#8419" class="Bound">q</a>
<a id="8748" href="Cubical.Algebra.Algebra.Properties.html#8656" class="Function">helper</a> <a id="8755" class="Symbol">=</a> <a id="8757" href="Cubical.Data.Sigma.Properties.html#13329" class="Function">Σ≡Prop</a>
Expand All @@ -236,7 +236,7 @@
<a id="9591" class="Symbol">→</a> <a id="9593" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9603" class="Symbol">(</a><a id="9604" href="Cubical.Algebra.Algebra.Properties.html#5987" class="Function">compAlgebraEquiv</a> <a id="9621" href="Cubical.Algebra.Algebra.Properties.html#9528" class="Bound">f</a> <a id="9623" href="Cubical.Algebra.Algebra.Properties.html#9551" class="Bound">g</a><a id="9624" class="Symbol">)</a> <a id="9626" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="9628" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9638" href="Cubical.Algebra.Algebra.Properties.html#9528" class="Bound">f</a> <a id="9640" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="9642" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9652" href="Cubical.Algebra.Algebra.Properties.html#9551" class="Bound">g</a>
<a id="9655" href="Cubical.Algebra.Algebra.Properties.html#9506" class="Function">uaCompAlgebraEquiv</a> <a id="9674" href="Cubical.Algebra.Algebra.Properties.html#9674" class="Bound">f</a> <a id="9676" href="Cubical.Algebra.Algebra.Properties.html#9676" class="Bound">g</a> <a id="9678" class="Symbol">=</a> <a id="9680" href="Cubical.Algebra.Algebra.Properties.html#8322" class="Function">caracAlgebra≡</a> <a id="9694" class="Symbol">_</a> <a id="9696" class="Symbol">_</a> <a id="9698" class="Symbol">(</a>
<a id="9703" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="9708" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨_⟩</a> <a id="9712" class="Symbol">(</a><a id="9713" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9723" class="Symbol">(</a><a id="9724" href="Cubical.Algebra.Algebra.Properties.html#5987" class="Function">compAlgebraEquiv</a> <a id="9741" href="Cubical.Algebra.Algebra.Properties.html#9674" class="Bound">f</a> <a id="9743" href="Cubical.Algebra.Algebra.Properties.html#9676" class="Bound">g</a><a id="9744" class="Symbol">))</a>
<a id="9752" href="Cubical.Foundations.Prelude.html#8310" class="Function">≡⟨</a> <a id="9755" href="Cubical.Foundations.Univalence.html#12966" class="Function">uaCompEquiv</a> <a id="9767" class="Symbol">_</a> <a id="9769" class="Symbol">_</a> <a id="9771" href="Cubical.Foundations.Prelude.html#8310" class="Function">⟩</a>
<a id="9752" href="Cubical.Foundations.Prelude.html#8310" class="Function">≡⟨</a> <a id="9755" href="Cubical.Foundations.Univalence.html#13526" class="Function">uaCompEquiv</a> <a id="9767" class="Symbol">_</a> <a id="9769" class="Symbol">_</a> <a id="9771" href="Cubical.Foundations.Prelude.html#8310" class="Function">⟩</a>
<a id="9776" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="9781" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨_⟩</a> <a id="9785" class="Symbol">(</a><a id="9786" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9796" href="Cubical.Algebra.Algebra.Properties.html#9674" class="Bound">f</a><a id="9797" class="Symbol">)</a> <a id="9799" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="9801" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="9806" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨_⟩</a> <a id="9810" class="Symbol">(</a><a id="9811" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9821" href="Cubical.Algebra.Algebra.Properties.html#9676" class="Bound">g</a><a id="9822" class="Symbol">)</a>
<a id="9829" href="Cubical.Foundations.Prelude.html#8310" class="Function">≡⟨</a> <a id="9832" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="9836" class="Symbol">(</a><a id="9837" href="Cubical.Foundations.GroupoidLaws.html#7916" class="Function">cong-∙</a> <a id="9844" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨_⟩</a> <a id="9848" class="Symbol">(</a><a id="9849" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9859" href="Cubical.Algebra.Algebra.Properties.html#9674" class="Bound">f</a><a id="9860" class="Symbol">)</a> <a id="9862" class="Symbol">(</a><a id="9863" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9873" href="Cubical.Algebra.Algebra.Properties.html#9676" class="Bound">g</a><a id="9874" class="Symbol">))</a> <a id="9877" href="Cubical.Foundations.Prelude.html#8310" class="Function">⟩</a>
<a id="9882" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="9887" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨_⟩</a> <a id="9891" class="Symbol">(</a><a id="9892" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9902" href="Cubical.Algebra.Algebra.Properties.html#9674" class="Bound">f</a> <a id="9904" href="Cubical.Foundations.Prelude.html#4776" class="Function Operator">∙</a> <a id="9906" href="Cubical.Algebra.Algebra.Base.html#9322" class="Function">uaAlgebra</a> <a id="9916" href="Cubical.Algebra.Algebra.Properties.html#9676" class="Bound">g</a><a id="9917" class="Symbol">)</a> <a id="9919" href="Cubical.Foundations.Prelude.html#8857" class="Function Operator">∎</a><a id="9920" class="Symbol">)</a>
Expand Down
Loading

0 comments on commit e60d022

Please sign in to comment.