Deploying to gh-pages from @ 6ce70a4 🚀

agda · Mar 1, 2024 · 837f35f · 837f35f
1 parent e295d05
commit 837f35f
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/Cubical.Foundations.Isomorphism.html b/Cubical.Foundations.Isomorphism.html
@@ -218,4 +218,10 @@
   <a id="7112" href="Cubical.Foundations.Prelude.html#17633" class="Function">isSet→isSet&#39;</a> <a id="7125" href="Cubical.Foundations.Isomorphism.html#7084" class="Bound">hB</a> <a id="7128" class="Symbol">(</a><a id="7129" href="Cubical.Foundations.Isomorphism.html#917" class="Field">rightInv</a> <a id="7138" href="Cubical.Foundations.Isomorphism.html#7087" class="Bound">f</a> <a id="7140" href="Cubical.Foundations.Isomorphism.html#7104" class="Bound">x</a><a id="7141" class="Symbol">)</a> <a id="7143" class="Symbol">(</a><a id="7144" href="Cubical.Foundations.Isomorphism.html#917" class="Field">rightInv</a> <a id="7153" href="Cubical.Foundations.Isomorphism.html#7089" class="Bound">g</a> <a id="7155" href="Cubical.Foundations.Isomorphism.html#7104" class="Bound">x</a><a id="7156" class="Symbol">)</a> <a id="7158" class="Symbol">(λ</a> <a id="7161" href="Cubical.Foundations.Isomorphism.html#7161" class="Bound">i</a> <a id="7163" class="Symbol">→</a> <a id="7165" href="Cubical.Foundations.Isomorphism.html#7091" class="Bound">hfun</a> <a id="7170" class="Symbol">(</a><a id="7171" href="Cubical.Foundations.Isomorphism.html#7096" class="Bound">hinv</a> <a id="7176" href="Cubical.Foundations.Isomorphism.html#7104" class="Bound">x</a> <a id="7178" href="Cubical.Foundations.Isomorphism.html#7161" class="Bound">i</a><a id="7179" class="Symbol">)</a> <a id="7181" href="Cubical.Foundations.Isomorphism.html#7161" class="Bound">i</a><a id="7182" class="Symbol">)</a> <a id="7184" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="7189" href="Cubical.Foundations.Isomorphism.html#7101" class="Bound">i</a> <a id="7191" href="Cubical.Foundations.Isomorphism.html#7106" class="Bound">j</a>
 <a id="7193" href="Cubical.Foundations.Isomorphism.html#948" class="Field">leftInv</a> <a id="7201" class="Symbol">(</a><a id="7202" href="Cubical.Foundations.Isomorphism.html#6819" class="Function">Iso≡Set</a> <a id="7210" href="Cubical.Foundations.Isomorphism.html#7210" class="Bound">hA</a> <a id="7213" href="Cubical.Foundations.Isomorphism.html#7213" class="Bound">hB</a> <a id="7216" href="Cubical.Foundations.Isomorphism.html#7216" class="Bound">f</a> <a id="7218" href="Cubical.Foundations.Isomorphism.html#7218" class="Bound">g</a> <a id="7220" href="Cubical.Foundations.Isomorphism.html#7220" class="Bound">hfun</a> <a id="7225" href="Cubical.Foundations.Isomorphism.html#7225" class="Bound">hinv</a> <a id="7230" href="Cubical.Foundations.Isomorphism.html#7230" class="Bound">i</a><a id="7231" class="Symbol">)</a> <a id="7233" href="Cubical.Foundations.Isomorphism.html#7233" class="Bound">x</a> <a id="7235" href="Cubical.Foundations.Isomorphism.html#7235" class="Bound">j</a> <a id="7237" class="Symbol">=</a>
   <a id="7241" href="Cubical.Foundations.Prelude.html#17633" class="Function">isSet→isSet&#39;</a> <a id="7254" href="Cubical.Foundations.Isomorphism.html#7210" class="Bound">hA</a> <a id="7257" class="Symbol">(</a><a id="7258" href="Cubical.Foundations.Isomorphism.html#948" class="Field">leftInv</a> <a id="7266" href="Cubical.Foundations.Isomorphism.html#7216" class="Bound">f</a> <a id="7268" href="Cubical.Foundations.Isomorphism.html#7233" class="Bound">x</a><a id="7269" class="Symbol">)</a> <a id="7271" class="Symbol">(</a><a id="7272" href="Cubical.Foundations.Isomorphism.html#948" class="Field">leftInv</a> <a id="7280" href="Cubical.Foundations.Isomorphism.html#7218" class="Bound">g</a> <a id="7282" href="Cubical.Foundations.Isomorphism.html#7233" class="Bound">x</a><a id="7283" class="Symbol">)</a> <a id="7285" class="Symbol">(λ</a> <a id="7288" href="Cubical.Foundations.Isomorphism.html#7288" class="Bound">i</a> <a id="7290" class="Symbol">→</a> <a id="7292" href="Cubical.Foundations.Isomorphism.html#7225" class="Bound">hinv</a> <a id="7297" class="Symbol">(</a><a id="7298" href="Cubical.Foundations.Isomorphism.html#7220" class="Bound">hfun</a> <a id="7303" href="Cubical.Foundations.Isomorphism.html#7233" class="Bound">x</a> <a id="7305" href="Cubical.Foundations.Isomorphism.html#7288" class="Bound">i</a><a id="7306" class="Symbol">)</a> <a id="7308" href="Cubical.Foundations.Isomorphism.html#7288" class="Bound">i</a><a id="7309" class="Symbol">)</a> <a id="7311" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a> <a id="7316" href="Cubical.Foundations.Isomorphism.html#7230" class="Bound">i</a> <a id="7318" href="Cubical.Foundations.Isomorphism.html#7235" class="Bound">j</a>
+
+<a id="transportIsoToPath"></a><a id="7321" href="Cubical.Foundations.Isomorphism.html#7321" class="Function">transportIsoToPath</a> <a id="7340" class="Symbol">:</a> <a id="7342" class="Symbol">(</a><a id="7343" href="Cubical.Foundations.Isomorphism.html#7343" class="Bound">f</a> <a id="7345" class="Symbol">:</a> <a id="7347" href="Cubical.Foundations.Isomorphism.html#773" class="Record">Iso</a> <a id="7351" href="Cubical.Foundations.Isomorphism.html#481" class="Generalizable">A</a> <a id="7353" href="Cubical.Foundations.Isomorphism.html#483" class="Generalizable">B</a><a id="7354" class="Symbol">)</a> <a id="7356" class="Symbol">(</a><a id="7357" href="Cubical.Foundations.Isomorphism.html#7357" class="Bound">x</a> <a id="7359" class="Symbol">:</a> <a id="7361" href="Cubical.Foundations.Isomorphism.html#481" class="Generalizable">A</a><a id="7362" class="Symbol">)</a> <a id="7364" class="Symbol">→</a> <a id="7366" href="Cubical.Foundations.Prelude.html#8955" class="Function">transport</a> <a id="7376" class="Symbol">(</a><a id="7377" href="Cubical.Foundations.Isomorphism.html#3223" class="Function">isoToPath</a> <a id="7387" href="Cubical.Foundations.Isomorphism.html#7343" class="Bound">f</a><a id="7388" class="Symbol">)</a> <a id="7390" href="Cubical.Foundations.Isomorphism.html#7357" class="Bound">x</a> <a id="7392" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="7394" href="Cubical.Foundations.Isomorphism.html#7343" class="Bound">f</a> <a id="7396" class="Symbol">.</a><a id="7397" href="Cubical.Foundations.Isomorphism.html#885" class="Field">fun</a> <a id="7401" href="Cubical.Foundations.Isomorphism.html#7357" class="Bound">x</a>
+<a id="7403" href="Cubical.Foundations.Isomorphism.html#7321" class="Function">transportIsoToPath</a> <a id="7422" href="Cubical.Foundations.Isomorphism.html#7422" class="Bound">f</a> <a id="7424" href="Cubical.Foundations.Isomorphism.html#7424" class="Bound">x</a> <a id="7426" class="Symbol">=</a> <a id="7428" href="Cubical.Foundations.Prelude.html#9176" class="Function">transportRefl</a> <a id="7442" class="Symbol">_</a>
+
+<a id="transportIsoToPath⁻"></a><a id="7445" href="Cubical.Foundations.Isomorphism.html#7445" class="Function">transportIsoToPath⁻</a> <a id="7465" class="Symbol">:</a> <a id="7467" class="Symbol">(</a><a id="7468" href="Cubical.Foundations.Isomorphism.html#7468" class="Bound">f</a> <a id="7470" class="Symbol">:</a> <a id="7472" href="Cubical.Foundations.Isomorphism.html#773" class="Record">Iso</a> <a id="7476" href="Cubical.Foundations.Isomorphism.html#481" class="Generalizable">A</a> <a id="7478" href="Cubical.Foundations.Isomorphism.html#483" class="Generalizable">B</a><a id="7479" class="Symbol">)</a> <a id="7481" class="Symbol">(</a><a id="7482" href="Cubical.Foundations.Isomorphism.html#7482" class="Bound">x</a> <a id="7484" class="Symbol">:</a> <a id="7486" href="Cubical.Foundations.Isomorphism.html#483" class="Generalizable">B</a><a id="7487" class="Symbol">)</a> <a id="7489" class="Symbol">→</a> <a id="7491" href="Cubical.Foundations.Prelude.html#8955" class="Function">transport</a> <a id="7501" class="Symbol">(</a><a id="7502" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="7506" class="Symbol">(</a><a id="7507" href="Cubical.Foundations.Isomorphism.html#3223" class="Function">isoToPath</a> <a id="7517" href="Cubical.Foundations.Isomorphism.html#7468" class="Bound">f</a><a id="7518" class="Symbol">))</a> <a id="7521" href="Cubical.Foundations.Isomorphism.html#7482" class="Bound">x</a> <a id="7523" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="7525" href="Cubical.Foundations.Isomorphism.html#7468" class="Bound">f</a> <a id="7527" class="Symbol">.</a><a id="7528" href="Cubical.Foundations.Isomorphism.html#901" class="Field">inv</a> <a id="7532" href="Cubical.Foundations.Isomorphism.html#7482" class="Bound">x</a>
+<a id="7534" href="Cubical.Foundations.Isomorphism.html#7445" class="Function">transportIsoToPath⁻</a> <a id="7554" href="Cubical.Foundations.Isomorphism.html#7554" class="Bound">f</a> <a id="7556" href="Cubical.Foundations.Isomorphism.html#7556" class="Bound">x</a> <a id="7558" class="Symbol">=</a> <a id="7560" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="7565" class="Symbol">(</a><a id="7566" href="Cubical.Foundations.Isomorphism.html#7554" class="Bound">f</a> <a id="7568" class="Symbol">.</a><a id="7569" href="Cubical.Foundations.Isomorphism.html#901" class="Field">inv</a><a id="7572" class="Symbol">)</a> <a id="7574" class="Symbol">(</a><a id="7575" href="Cubical.Foundations.Prelude.html#9176" class="Function">transportRefl</a> <a id="7589" class="Symbol">_)</a>
 </pre></body></html>