Deploying to gh-pages from @ b046b02 🚀

Cubical.Categories.Presheaf.Base.html

@@ -23,7 +23,7 @@
 
 <a id="isUnivalentPresheafCategory"></a><a id="644" href="Cubical.Categories.Presheaf.Base.html#644" class="Function">isUnivalentPresheafCategory</a> <a id="672" class="Symbol">:</a> <a id="674" class="Symbol">{</a><a id="675" href="Cubical.Categories.Presheaf.Base.html#675" class="Bound">C</a> <a id="677" class="Symbol">:</a> <a id="679" href="Cubical.Categories.Category.Base.html#334" class="Record">Category</a> <a id="688" href="Cubical.Categories.Presheaf.Base.html#316" class="Generalizable">ℓ</a> <a id="690" href="Cubical.Categories.Presheaf.Base.html#318" class="Generalizable">ℓ&#39;</a><a id="692" class="Symbol">}</a>
                             <a id="722" class="Symbol">→</a> <a id="724" href="Cubical.Categories.Category.Base.html#3545" class="Record">isUnivalent</a> <a id="736" class="Symbol">(</a><a id="737" href="Cubical.Categories.Presheaf.Base.html#454" class="Function">PresheafCategory</a> <a id="754" href="Cubical.Categories.Presheaf.Base.html#675" class="Bound">C</a> <a id="756" href="Cubical.Categories.Presheaf.Base.html#321" class="Generalizable">ℓS</a><a id="758" class="Symbol">)</a>
-<a id="760" href="Cubical.Categories.Presheaf.Base.html#644" class="Function">isUnivalentPresheafCategory</a> <a id="788" class="Symbol">=</a> <a id="790" href="Cubical.Categories.Instances.Functors.html#4321" class="Function">isUnivalentFUNCTOR</a> <a id="809" class="Symbol">_</a> <a id="811" class="Symbol">_</a> <a id="813" href="Cubical.Categories.Instances.Sets.html#3352" class="Function">isUnivalentSET</a>
+<a id="760" href="Cubical.Categories.Presheaf.Base.html#644" class="Function">isUnivalentPresheafCategory</a> <a id="788" class="Symbol">=</a> <a id="790" href="Cubical.Categories.Instances.Functors.html#4321" class="Function">isUnivalentFUNCTOR</a> <a id="809" class="Symbol">_</a> <a id="811" class="Symbol">_</a> <a id="813" href="Cubical.Categories.Instances.Sets.html#3799" class="Function">isUnivalentSET</a>
 
 <a id="829" class="Keyword">open</a> <a id="834" href="Cubical.Categories.Category.Base.html#334" class="Module">Category</a>
 <a id="843" class="Keyword">open</a> <a id="848" href="Cubical.Categories.Functor.Base.html#441" class="Module">Functor</a>

Cubical.Categories.Presheaf.Properties.html

@@ -281,7 +281,7 @@
       <a id="11720" class="Keyword">where</a>
         <a id="11734" href="Cubical.Categories.Presheaf.Properties.html#11734" class="Function">isIsoCf</a> <a id="11742" class="Symbol">:</a> <a id="11744" class="Symbol">∀</a> <a id="11746" class="Symbol">(</a><a id="11747" href="Cubical.Categories.Presheaf.Properties.html#11747" class="Bound">c</a> <a id="11749" class="Symbol">:</a> <a id="11751" href="Cubical.Categories.Presheaf.Properties.html#1106" class="Bound">C</a> <a id="11753" class="Symbol">.</a><a id="11754" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a><a id="11756" class="Symbol">)</a>
                 <a id="11774" class="Symbol">→</a> <a id="11776" href="Cubical.Categories.Presheaf.Properties.html#137" class="Record">isIsoC</a> <a id="11783" class="Symbol">_</a> <a id="11785" class="Symbol">(</a><a id="11786" href="Cubical.Categories.Presheaf.Properties.html#10419" class="Function">ηTrans</a> <a id="11793" class="Symbol">.</a><a id="11794" href="Cubical.Categories.NaturalTransformation.Base.html#1416" class="Field">N-ob</a> <a id="11799" href="Cubical.Categories.Presheaf.Properties.html#11656" class="Bound">sob</a> <a id="11803" class="Symbol">.</a><a id="11804" href="Cubical.Categories.Constructions.Slice.Base.html#960" class="Field">S-hom</a> <a id="11810" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟦</a> <a id="11812" href="Cubical.Categories.Presheaf.Properties.html#11747" class="Bound">c</a> <a id="11814" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟧</a><a id="11815" class="Symbol">)</a>
-        <a id="11825" href="Cubical.Categories.Presheaf.Properties.html#11734" class="Function">isIsoCf</a> <a id="11833" href="Cubical.Categories.Presheaf.Properties.html#11833" class="Bound">c</a> <a id="11835" class="Symbol">=</a> <a id="11837" href="Cubical.Categories.Morphism.html#4756" class="Function">Morphism.CatIso→isIso</a> <a id="11859" class="Symbol">(</a><a id="11860" href="Cubical.Categories.Instances.Sets.html#2310" class="Function">Iso→CatIso</a> <a id="11871" class="Symbol">(</a><a id="11872" href="Cubical.Categories.Presheaf.Properties.html#9895" class="Function">typeSectionIso</a> <a id="11887" class="Symbol">{</a><a id="11888" class="Argument">isSetB</a> <a id="11895" class="Symbol">=</a> <a id="11897" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="11901" class="Symbol">(</a><a id="11902" href="Cubical.Categories.Presheaf.Properties.html#1126" class="Bound">F</a> <a id="11904" href="Cubical.Categories.Functor.Base.html#3706" class="Function Operator">⟅</a> <a id="11906" href="Cubical.Categories.Presheaf.Properties.html#11833" class="Bound">c</a> <a id="11908" href="Cubical.Categories.Functor.Base.html#3706" class="Function Operator">⟆</a><a id="11909" class="Symbol">)}</a> <a id="11912" class="Symbol">(</a><a id="11913" href="Cubical.Categories.Presheaf.Properties.html#11669" class="Bound">ϕ</a> <a id="11915" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟦</a> <a id="11917" href="Cubical.Categories.Presheaf.Properties.html#11833" class="Bound">c</a> <a id="11919" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟧</a><a id="11920" class="Symbol">)))</a>
+        <a id="11825" href="Cubical.Categories.Presheaf.Properties.html#11734" class="Function">isIsoCf</a> <a id="11833" href="Cubical.Categories.Presheaf.Properties.html#11833" class="Bound">c</a> <a id="11835" class="Symbol">=</a> <a id="11837" href="Cubical.Categories.Morphism.html#4756" class="Function">Morphism.CatIso→isIso</a> <a id="11859" class="Symbol">(</a><a id="11860" href="Cubical.Categories.Instances.Sets.html#2757" class="Function">Iso→CatIso</a> <a id="11871" class="Symbol">(</a><a id="11872" href="Cubical.Categories.Presheaf.Properties.html#9895" class="Function">typeSectionIso</a> <a id="11887" class="Symbol">{</a><a id="11888" class="Argument">isSetB</a> <a id="11895" class="Symbol">=</a> <a id="11897" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="11901" class="Symbol">(</a><a id="11902" href="Cubical.Categories.Presheaf.Properties.html#1126" class="Bound">F</a> <a id="11904" href="Cubical.Categories.Functor.Base.html#3706" class="Function Operator">⟅</a> <a id="11906" href="Cubical.Categories.Presheaf.Properties.html#11833" class="Bound">c</a> <a id="11908" href="Cubical.Categories.Functor.Base.html#3706" class="Function Operator">⟆</a><a id="11909" class="Symbol">)}</a> <a id="11912" class="Symbol">(</a><a id="11913" href="Cubical.Categories.Presheaf.Properties.html#11669" class="Bound">ϕ</a> <a id="11915" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟦</a> <a id="11917" href="Cubical.Categories.Presheaf.Properties.html#11833" class="Bound">c</a> <a id="11919" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟧</a><a id="11920" class="Symbol">)))</a>
 
 
   <a id="11928" class="Comment">-- ========================================</a>
@@ -378,7 +378,7 @@
       <a id="16663" class="Keyword">where</a>
         <a id="16677" href="Cubical.Categories.Presheaf.Properties.html#16677" class="Function">isIsoC&#39;</a> <a id="16685" class="Symbol">:</a> <a id="16687" class="Symbol">∀</a> <a id="16689" class="Symbol">(</a><a id="16690" href="Cubical.Categories.Presheaf.Properties.html#16690" class="Bound">cx</a> <a id="16693" class="Symbol">:</a> <a id="16695" class="Symbol">(</a><a id="16696" href="Cubical.Categories.Constructions.Elements.html#3372" class="Function Operator">∫ᴾ</a> <a id="16699" href="Cubical.Categories.Presheaf.Properties.html#1126" class="Bound">F</a><a id="16700" class="Symbol">)</a> <a id="16702" class="Symbol">.</a><a id="16703" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a><a id="16705" class="Symbol">)</a>
                 <a id="16723" class="Symbol">→</a> <a id="16725" href="Cubical.Categories.Presheaf.Properties.html#137" class="Record">isIsoC</a> <a id="16732" class="Symbol">(</a><a id="16733" href="Cubical.Categories.Instances.Sets.html#551" class="Function">SET</a> <a id="16737" class="Symbol">_)</a> <a id="16740" class="Symbol">((</a><a id="16742" href="Cubical.Categories.Presheaf.Properties.html#12802" class="Function">εTrans</a> <a id="16749" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟦</a> <a id="16751" href="Cubical.Categories.Presheaf.Properties.html#16628" class="Bound">P</a> <a id="16753" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟧</a><a id="16754" class="Symbol">)</a> <a id="16756" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟦</a> <a id="16758" href="Cubical.Categories.Presheaf.Properties.html#16690" class="Bound">cx</a> <a id="16761" href="Cubical.Categories.NaturalTransformation.Base.html#2789" class="Function Operator">⟧</a><a id="16762" class="Symbol">)</a>
-        <a id="16772" href="Cubical.Categories.Presheaf.Properties.html#16677" class="Function">isIsoC&#39;</a> <a id="16780" href="Cubical.Categories.Presheaf.Properties.html#16780" class="Bound">cx</a><a id="16782" class="Symbol">@(</a><a id="16784" href="Cubical.Categories.Presheaf.Properties.html#16784" class="Bound">c</a> <a id="16786" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="16788" class="Symbol">_)</a> <a id="16791" class="Symbol">=</a> <a id="16793" href="Cubical.Categories.Morphism.html#4756" class="Function">Morphism.CatIso→isIso</a> <a id="16815" class="Symbol">(</a><a id="16816" href="Cubical.Categories.Instances.Sets.html#2310" class="Function">Iso→CatIso</a> <a id="16827" class="Symbol">(</a><a id="16828" href="Cubical.Foundations.Isomorphism.html#3382" class="Function">invIso</a> <a id="16835" class="Symbol">(</a><a id="16836" href="Cubical.Categories.Presheaf.Properties.html#12210" class="Function">typeFiberIso</a> <a id="16849" class="Symbol">{</a><a id="16850" class="Argument">isSetA</a> <a id="16857" class="Symbol">=</a> <a id="16859" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="16863" class="Symbol">(</a><a id="16864" href="Cubical.Categories.Presheaf.Properties.html#1126" class="Bound">F</a> <a id="16866" href="Cubical.Categories.Functor.Base.html#3706" class="Function Operator">⟅</a> <a id="16868" href="Cubical.Categories.Presheaf.Properties.html#16784" class="Bound">c</a> <a id="16870" href="Cubical.Categories.Functor.Base.html#3706" class="Function Operator">⟆</a><a id="16871" class="Symbol">)}</a> <a id="16874" class="Symbol">_)))</a>
+        <a id="16772" href="Cubical.Categories.Presheaf.Properties.html#16677" class="Function">isIsoC&#39;</a> <a id="16780" href="Cubical.Categories.Presheaf.Properties.html#16780" class="Bound">cx</a><a id="16782" class="Symbol">@(</a><a id="16784" href="Cubical.Categories.Presheaf.Properties.html#16784" class="Bound">c</a> <a id="16786" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="16788" class="Symbol">_)</a> <a id="16791" class="Symbol">=</a> <a id="16793" href="Cubical.Categories.Morphism.html#4756" class="Function">Morphism.CatIso→isIso</a> <a id="16815" class="Symbol">(</a><a id="16816" href="Cubical.Categories.Instances.Sets.html#2757" class="Function">Iso→CatIso</a> <a id="16827" class="Symbol">(</a><a id="16828" href="Cubical.Foundations.Isomorphism.html#3382" class="Function">invIso</a> <a id="16835" class="Symbol">(</a><a id="16836" href="Cubical.Categories.Presheaf.Properties.html#12210" class="Function">typeFiberIso</a> <a id="16849" class="Symbol">{</a><a id="16850" class="Argument">isSetA</a> <a id="16857" class="Symbol">=</a> <a id="16859" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="16863" class="Symbol">(</a><a id="16864" href="Cubical.Categories.Presheaf.Properties.html#1126" class="Bound">F</a> <a id="16866" href="Cubical.Categories.Functor.Base.html#3706" class="Function Operator">⟅</a> <a id="16868" href="Cubical.Categories.Presheaf.Properties.html#16784" class="Bound">c</a> <a id="16870" href="Cubical.Categories.Functor.Base.html#3706" class="Function Operator">⟆</a><a id="16871" class="Symbol">)}</a> <a id="16874" class="Symbol">_)))</a>
 
 
   <a id="16883" class="Comment">-- putting it all together</a>