Deploying to gh-pages from @ 502b1bb 🚀

agda · May 22, 2024 · bc2ee4f · bc2ee4f
1 parent 13369aa
commit bc2ee4f
Show file tree

Hide file tree

Showing 7 changed files with 332 additions and 265 deletions.
diff --git a/Cubical.Displayed.Function.html b/Cubical.Displayed.Function.html
@@ -77,7 +77,7 @@
       <a id="2081" class="Symbol">(</a><a id="2082" href="Cubical.Foundations.Equiv.html#7639" class="Function">equivImplicitΠCod</a> <a id="2100" class="Symbol">λ</a> <a id="2102" class="Symbol">{</a><a id="2103" href="Cubical.Displayed.Function.html#2103" class="Bound">b</a><a id="2104" class="Symbol">}</a> <a id="2106" class="Symbol">→</a>
         <a id="2116" class="Symbol">(</a><a id="2117" href="Cubical.Foundations.Equiv.html#7639" class="Function">equivImplicitΠCod</a> <a id="2135" class="Symbol">λ</a> <a id="2137" class="Symbol">{</a><a id="2138" href="Cubical.Displayed.Function.html#2138" class="Bound">b&#39;</a><a id="2140" class="Symbol">}</a> <a id="2142" class="Symbol">→</a>
           <a id="2154" class="Symbol">(</a><a id="2155" href="Cubical.Foundations.Equiv.html#9591" class="Function">equivΠ</a> <a id="2162" class="Symbol">(</a><a id="2163" href="Cubical.Displayed.Base.html#1515" class="Function">B.uaᴰ</a> <a id="2169" href="Cubical.Displayed.Function.html#2103" class="Bound">b</a> <a id="2171" href="Cubical.Displayed.Function.html#2054" class="Bound">p</a> <a id="2173" href="Cubical.Displayed.Function.html#2138" class="Bound">b&#39;</a><a id="2175" class="Symbol">)</a> <a id="2177" class="Symbol">(λ</a> <a id="2180" href="Cubical.Displayed.Function.html#2180" class="Bound">q</a> <a id="2182" class="Symbol">→</a> <a id="2184" href="Cubical.Displayed.Base.html#1515" class="Field">C.uaᴰ</a> <a id="2190" class="Symbol">(</a><a id="2191" href="Cubical.Displayed.Function.html#2052" class="Bound">f</a> <a id="2193" href="Cubical.Displayed.Function.html#2103" class="Bound">b</a><a id="2194" class="Symbol">)</a> <a id="2196" class="Symbol">(</a><a id="2197" href="Cubical.Displayed.Function.html#2054" class="Bound">p</a> <a id="2199" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="2201" href="Cubical.Displayed.Function.html#2180" class="Bound">q</a><a id="2202" class="Symbol">)</a> <a id="2204" class="Symbol">(</a><a id="2205" href="Cubical.Displayed.Function.html#2056" class="Bound">f&#39;</a> <a id="2208" href="Cubical.Displayed.Function.html#2138" class="Bound">b&#39;</a><a id="2210" class="Symbol">)))))</a>
-      <a id="2222" href="Cubical.Functions.FunExtEquiv.html#5850" class="Function">funExtDepEquiv</a>
+      <a id="2222" href="Cubical.Functions.FunExtEquiv.html#5754" class="Function">funExtDepEquiv</a>
 
 <a id="_→𝒮ᴰ_"></a><a id="2238" href="Cubical.Displayed.Function.html#2238" class="Function Operator">_→𝒮ᴰ_</a> <a id="2244" class="Symbol">:</a> <a id="2246" class="Symbol">{</a><a id="2247" href="Cubical.Displayed.Function.html#2247" class="Bound">A</a> <a id="2249" class="Symbol">:</a> <a id="2251" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="2256" href="Cubical.Displayed.Function.html#640" class="Generalizable">ℓA</a><a id="2258" class="Symbol">}</a> <a id="2260" class="Symbol">{</a><a id="2261" href="Cubical.Displayed.Function.html#2261" class="Bound">𝒮-A</a> <a id="2265" class="Symbol">:</a> <a id="2267" href="Cubical.Displayed.Base.html#433" class="Record">UARel</a> <a id="2273" href="Cubical.Displayed.Function.html#2247" class="Bound">A</a> <a id="2275" href="Cubical.Displayed.Function.html#643" class="Generalizable">ℓ≅A</a><a id="2278" class="Symbol">}</a>
   <a id="2282" class="Symbol">{</a><a id="2283" href="Cubical.Displayed.Function.html#2283" class="Bound">B</a> <a id="2285" class="Symbol">:</a> <a id="2287" href="Cubical.Displayed.Function.html#2247" class="Bound">A</a> <a id="2289" class="Symbol">→</a> <a id="2291" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="2296" href="Cubical.Displayed.Function.html#647" class="Generalizable">ℓB</a><a id="2298" class="Symbol">}</a> <a id="2300" class="Symbol">(</a><a id="2301" href="Cubical.Displayed.Function.html#2301" class="Bound">𝒮ᴰ-B</a> <a id="2306" class="Symbol">:</a> <a id="2308" href="Cubical.Displayed.Base.html#1242" class="Record">DUARel</a> <a id="2315" href="Cubical.Displayed.Function.html#2261" class="Bound">𝒮-A</a> <a id="2319" href="Cubical.Displayed.Function.html#2283" class="Bound">B</a> <a id="2321" href="Cubical.Displayed.Function.html#650" class="Generalizable">ℓ≅B</a><a id="2324" class="Symbol">)</a>