Deploying to gh-pages from @ d96372c 🚀

Author: ecavallo

Cubical.Categories.Constructions.Slice.Base.html

@@ -388,7 +388,7 @@
 <a id="sliceIso"></a><a id="14694" href="Cubical.Categories.Constructions.Slice.Base.html#14694" class="Function">sliceIso</a> <a id="14703" class="Symbol">:</a> <a id="14705" class="Symbol">∀</a> <a id="14707" class="Symbol">{</a><a id="14708" href="Cubical.Categories.Constructions.Slice.Base.html#14708" class="Bound">a</a> <a id="14710" href="Cubical.Categories.Constructions.Slice.Base.html#14710" class="Bound">b</a><a id="14711" class="Symbol">}</a> <a id="14713" class="Symbol">(</a><a id="14714" href="Cubical.Categories.Constructions.Slice.Base.html#14714" class="Bound">f</a> <a id="14716" class="Symbol">:</a> <a id="14718" href="Cubical.Categories.Constructions.Slice.Base.html#554" class="Bound">C</a> <a id="14720" href="Cubical.Categories.Category.Base.html#1218" class="Function Operator">[</a> <a id="14722" href="Cubical.Categories.Constructions.Slice.Base.html#14708" class="Bound">a</a> <a id="14724" class="Symbol">.</a><a id="14725" href="Cubical.Categories.Constructions.Slice.Base.html#791" class="Field">S-ob</a> <a id="14730" href="Cubical.Categories.Category.Base.html#1218" class="Function Operator">,</a> <a id="14732" href="Cubical.Categories.Constructions.Slice.Base.html#14710" class="Bound">b</a> <a id="14734" class="Symbol">.</a><a id="14735" href="Cubical.Categories.Constructions.Slice.Base.html#791" class="Field">S-ob</a> <a id="14740" href="Cubical.Categories.Category.Base.html#1218" class="Function Operator">]</a><a id="14741" class="Symbol">)</a> <a id="14743" class="Symbol">(</a><a id="14744" href="Cubical.Categories.Constructions.Slice.Base.html#14744" class="Bound">c</a> <a id="14746" class="Symbol">:</a> <a id="14748" class="Symbol">(</a><a id="14749" href="Cubical.Categories.Constructions.Slice.Base.html#14714" class="Bound">f</a> <a id="14751" href="Cubical.Categories.Category.Base.html#1461" class="Function">⋆⟨</a> <a id="14754" href="Cubical.Categories.Constructions.Slice.Base.html#554" class="Bound">C</a> <a id="14756" href="Cubical.Categories.Category.Base.html#1461" class="Function">⟩</a> <a id="14758" href="Cubical.Categories.Constructions.Slice.Base.html#14710" class="Bound">b</a> <a id="14760" class="Symbol">.</a><a id="14761" href="Cubical.Categories.Constructions.Slice.Base.html#809" class="Field">S-arr</a><a id="14766" class="Symbol">)</a> <a id="14768" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="14770" href="Cubical.Categories.Constructions.Slice.Base.html#14708" class="Bound">a</a> <a id="14772" class="Symbol">.</a><a id="14773" href="Cubical.Categories.Constructions.Slice.Base.html#809" class="Field">S-arr</a><a id="14778" class="Symbol">)</a>
          <a id="14789" class="Symbol">→</a> <a id="14791" href="Cubical.Categories.Constructions.Slice.Base.html#365" class="Record">isIsoC</a> <a id="14798" href="Cubical.Categories.Constructions.Slice.Base.html#554" class="Bound">C</a> <a id="14800" href="Cubical.Categories.Constructions.Slice.Base.html#14714" class="Bound">f</a>
          <a id="14811" class="Symbol">→</a> <a id="14813" href="Cubical.Categories.Constructions.Slice.Base.html#365" class="Record">isIsoC</a> <a id="14820" href="Cubical.Categories.Constructions.Slice.Base.html#3960" class="Function">SliceCat</a> <a id="14829" class="Symbol">(</a><a id="14830" href="Cubical.Categories.Constructions.Slice.Base.html#916" class="InductiveConstructor">slicehom</a> <a id="14839" href="Cubical.Categories.Constructions.Slice.Base.html#14714" class="Bound">f</a> <a id="14841" href="Cubical.Categories.Constructions.Slice.Base.html#14744" class="Bound">c</a><a id="14842" class="Symbol">)</a>
-<a id="14844" href="Cubical.Categories.Constructions.Slice.Base.html#14694" class="Function">sliceIso</a> <a id="14853" href="Cubical.Categories.Constructions.Slice.Base.html#14853" class="Bound">f</a> <a id="14855" href="Cubical.Categories.Constructions.Slice.Base.html#14855" class="Bound">c</a> <a id="14857" href="Cubical.Categories.Constructions.Slice.Base.html#14857" class="Bound">isof</a> <a id="14862" class="Symbol">.</a><a id="14863" href="Cubical.Categories.Constructions.Slice.Base.html#14641" class="Field">invC</a> <a id="14868" class="Symbol">=</a> <a id="14870" href="Cubical.Categories.Constructions.Slice.Base.html#916" class="InductiveConstructor">slicehom</a> <a id="14879" class="Symbol">(</a><a id="14880" href="Cubical.Categories.Constructions.Slice.Base.html#14857" class="Bound">isof</a> <a id="14885" class="Symbol">.</a><a id="14886" href="Cubical.Categories.Constructions.Slice.Base.html#14641" class="Field">invC</a><a id="14890" class="Symbol">)</a> <a id="14892" class="Symbol">(</a><a id="14893" href="Cubical.Foundations.Prelude.html#945" class="Function">sym</a> <a id="14897" class="Symbol">(</a><a id="14898" href="Cubical.Categories.Morphism.html#3640" class="Function">invMoveL</a> <a id="14907" class="Symbol">(</a><a id="14908" href="Cubical.Categories.Morphism.html#4914" class="Function">isIso→areInv</a> <a id="14921" href="Cubical.Categories.Constructions.Slice.Base.html#14857" class="Bound">isof</a><a id="14925" class="Symbol">)</a> <a id="14927" href="Cubical.Categories.Constructions.Slice.Base.html#14855" class="Bound">c</a><a id="14928" class="Symbol">))</a>
+<a id="14844" href="Cubical.Categories.Constructions.Slice.Base.html#14694" class="Function">sliceIso</a> <a id="14853" href="Cubical.Categories.Constructions.Slice.Base.html#14853" class="Bound">f</a> <a id="14855" href="Cubical.Categories.Constructions.Slice.Base.html#14855" class="Bound">c</a> <a id="14857" href="Cubical.Categories.Constructions.Slice.Base.html#14857" class="Bound">isof</a> <a id="14862" class="Symbol">.</a><a id="14863" href="Cubical.Categories.Constructions.Slice.Base.html#14641" class="Field">invC</a> <a id="14868" class="Symbol">=</a> <a id="14870" href="Cubical.Categories.Constructions.Slice.Base.html#916" class="InductiveConstructor">slicehom</a> <a id="14879" class="Symbol">(</a><a id="14880" href="Cubical.Categories.Constructions.Slice.Base.html#14857" class="Bound">isof</a> <a id="14885" class="Symbol">.</a><a id="14886" href="Cubical.Categories.Constructions.Slice.Base.html#14641" class="Field">invC</a><a id="14890" class="Symbol">)</a> <a id="14892" class="Symbol">(</a><a id="14893" href="Cubical.Foundations.Prelude.html#945" class="Function">sym</a> <a id="14897" class="Symbol">(</a><a id="14898" href="Cubical.Categories.Morphism.html#3856" class="Function">invMoveL</a> <a id="14907" class="Symbol">(</a><a id="14908" href="Cubical.Categories.Morphism.html#5130" class="Function">isIso→areInv</a> <a id="14921" href="Cubical.Categories.Constructions.Slice.Base.html#14857" class="Bound">isof</a><a id="14925" class="Symbol">)</a> <a id="14927" href="Cubical.Categories.Constructions.Slice.Base.html#14855" class="Bound">c</a><a id="14928" class="Symbol">))</a>
 <a id="14931" href="Cubical.Categories.Constructions.Slice.Base.html#14694" class="Function">sliceIso</a> <a id="14940" href="Cubical.Categories.Constructions.Slice.Base.html#14940" class="Bound">f</a> <a id="14942" href="Cubical.Categories.Constructions.Slice.Base.html#14942" class="Bound">c</a> <a id="14944" href="Cubical.Categories.Constructions.Slice.Base.html#14944" class="Bound">isof</a> <a id="14949" class="Symbol">.</a><a id="14950" href="Cubical.Categories.Category.Base.html#1947" class="Field">sec</a> <a id="14954" class="Symbol">=</a> <a id="14956" href="Cubical.Categories.Constructions.Slice.Base.html#3210" class="Function">SliceHom-≡-intro&#39;</a> <a id="14974" class="Symbol">(</a><a id="14975" href="Cubical.Categories.Constructions.Slice.Base.html#14944" class="Bound">isof</a> <a id="14980" class="Symbol">.</a><a id="14981" href="Cubical.Categories.Category.Base.html#1947" class="Field">sec</a><a id="14984" class="Symbol">)</a>
 <a id="14986" href="Cubical.Categories.Constructions.Slice.Base.html#14694" class="Function">sliceIso</a> <a id="14995" href="Cubical.Categories.Constructions.Slice.Base.html#14995" class="Bound">f</a> <a id="14997" href="Cubical.Categories.Constructions.Slice.Base.html#14997" class="Bound">c</a> <a id="14999" href="Cubical.Categories.Constructions.Slice.Base.html#14999" class="Bound">isof</a> <a id="15004" class="Symbol">.</a><a id="15005" href="Cubical.Categories.Category.Base.html#1978" class="Field">ret</a> <a id="15009" class="Symbol">=</a> <a id="15011" href="Cubical.Categories.Constructions.Slice.Base.html#3210" class="Function">SliceHom-≡-intro&#39;</a> <a id="15029" class="Symbol">(</a><a id="15030" href="Cubical.Categories.Constructions.Slice.Base.html#14999" class="Bound">isof</a> <a id="15035" class="Symbol">.</a><a id="15036" href="Cubical.Categories.Category.Base.html#1978" class="Field">ret</a><a id="15039" class="Symbol">)</a>
 </pre></body></html>