Deploying to gh-pages from @ e78ac78 🚀

agda · Nov 2, 2023 · 85134c8 · 85134c8
1 parent 925081b
commit 85134c8
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Cubical.Foundations.Equiv.html b/Cubical.Foundations.Equiv.html
@@ -317,4 +317,7 @@
 
 <a id="isEquiv≃isEquiv&#39;"></a><a id="11377" href="Cubical.Foundations.Equiv.html#11377" class="Function">isEquiv≃isEquiv&#39;</a> <a id="11394" class="Symbol">:</a> <a id="11396" class="Symbol">(</a><a id="11397" href="Cubical.Foundations.Equiv.html#11397" class="Bound">f</a> <a id="11399" class="Symbol">:</a> <a id="11401" href="Cubical.Foundations.Equiv.html#790" class="Generalizable">A</a> <a id="11403" class="Symbol">→</a> <a id="11405" href="Cubical.Foundations.Equiv.html#792" class="Generalizable">B</a><a id="11406" class="Symbol">)</a> <a id="11408" class="Symbol">→</a> <a id="11410" href="Agda.Builtin.Cubical.Equiv.html#830" class="Record">isEquiv</a> <a id="11418" href="Cubical.Foundations.Equiv.html#11397" class="Bound">f</a> <a id="11420" href="Agda.Builtin.Cubical.Equiv.html#1012" class="Function Operator">≃</a> <a id="11422" href="Cubical.Foundations.Equiv.Base.html#1177" class="Function">isEquiv&#39;</a> <a id="11431" href="Cubical.Foundations.Equiv.html#11397" class="Bound">f</a>
 <a id="11433" href="Cubical.Foundations.Equiv.html#11377" class="Function">isEquiv≃isEquiv&#39;</a> <a id="11450" href="Cubical.Foundations.Equiv.html#11450" class="Bound">f</a> <a id="11452" class="Symbol">=</a> <a id="11454" href="Cubical.Foundations.Isomorphism.html#3127" class="Function">isoToEquiv</a> <a id="11465" class="Symbol">(</a><a id="11466" href="Cubical.Foundations.Equiv.html#11108" class="Function">isEquiv-isEquiv&#39;-Iso</a> <a id="11487" href="Cubical.Foundations.Equiv.html#11450" class="Bound">f</a><a id="11488" class="Symbol">)</a>
+
+<a id="11491" class="Comment">-- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv</a>
+
 </pre></body></html>