Deploying to gh-pages from @ 904aa21 🚀

Author: mortberg

Cubical.Algebra.CommRing.Localisation.Limit.html

@@ -62,7 +62,7 @@
 <a id="2717" class="Keyword">open</a> <a id="2722" class="Keyword">import</a> <a id="2729" href="Cubical.AlgebraicGeometry.ZariskiLattice.Base.html" class="Module">Cubical.AlgebraicGeometry.ZariskiLattice.Base</a>
 <a id="2775" class="Keyword">open</a> <a id="2780" class="Keyword">import</a> <a id="2787" href="Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty.html" class="Module">Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty</a>
 
-<a id="2847" class="Keyword">open</a> <a id="2852" class="Keyword">import</a> <a id="2859" href="Cubical.Categories.Category.Base.html" class="Module">Cubical.Categories.Category.Base</a> <a id="2892" class="Keyword">hiding</a> <a id="2899" class="Symbol">(</a><a id="2900" href="Cubical.Categories.Category.Base.html#1210" class="Function Operator">_[_,_]</a><a id="2906" class="Symbol">)</a>
+<a id="2847" class="Keyword">open</a> <a id="2852" class="Keyword">import</a> <a id="2859" href="Cubical.Categories.Category.Base.html" class="Module">Cubical.Categories.Category.Base</a> <a id="2892" class="Keyword">hiding</a> <a id="2899" class="Symbol">(</a><a id="2900" href="Cubical.Categories.Category.Base.html#1218" class="Function Operator">_[_,_]</a><a id="2906" class="Symbol">)</a>
 <a id="2908" class="Keyword">open</a> <a id="2913" class="Keyword">import</a> <a id="2920" href="Cubical.Categories.Functor.html" class="Module">Cubical.Categories.Functor</a>
 <a id="2947" class="Keyword">open</a> <a id="2952" class="Keyword">import</a> <a id="2959" href="Cubical.Categories.Limits.Terminal.html" class="Module">Cubical.Categories.Limits.Terminal</a>
 <a id="2994" class="Keyword">open</a> <a id="2999" class="Keyword">import</a> <a id="3006" href="Cubical.Categories.Limits.Pullback.html" class="Module">Cubical.Categories.Limits.Pullback</a>
@@ -132,7 +132,7 @@
  <a id="4768" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4768" class="Function">ZariskiCat</a> <a id="4779" class="Symbol">=</a> <a id="4781" href="Cubical.Categories.Instances.DistLattice.html#243" class="Function">DistLatticeCategory</a> <a id="4801" href="Cubical.AlgebraicGeometry.ZariskiLattice.Base.html#8331" class="Function">ZariskiLattice</a>
 
  <a id="4818" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4818" class="Function">BOCat</a> <a id="4824" class="Symbol">:</a> <a id="4826" href="Cubical.Categories.Category.Base.html#311" class="Record">Category</a> <a id="4835" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#3464" class="Bound">ℓ</a> <a id="4837" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#3464" class="Bound">ℓ</a>
- <a id="4840" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4818" class="Function">BOCat</a> <a id="4846" class="Symbol">=</a> <a id="4848" href="Cubical.Categories.Category.Base.html#4774" class="Function">ΣPropCat</a> <a id="4857" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4768" class="Function">ZariskiCat</a> <a id="4868" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#3986" class="Function">BasicOpens</a>
+ <a id="4840" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4818" class="Function">BOCat</a> <a id="4846" class="Symbol">=</a> <a id="4848" href="Cubical.Categories.Category.Base.html#4835" class="Function">ΣPropCat</a> <a id="4857" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4768" class="Function">ZariskiCat</a> <a id="4868" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#3986" class="Function">BasicOpens</a>
 
  <a id="4881" class="Keyword">private</a>
   <a id="4891" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4891" class="Function">P</a> <a id="4893" class="Symbol">:</a> <a id="4895" href="Cubical.AlgebraicGeometry.ZariskiLattice.Base.html#3369" class="Function">ZL</a> <a id="4898" class="Symbol">→</a> <a id="4900" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="4905" class="Symbol">_</a>
@@ -169,7 +169,7 @@
 
 
  <a id="6199" class="Keyword">open</a> <a id="6204" href="Cubical.Categories.Instances.CommAlgebras.html#24158" class="Module">PreSheafFromUniversalProp</a> <a id="6230" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4768" class="Function">ZariskiCat</a> <a id="6241" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4891" class="Function">P</a> <a id="6243" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4976" class="Function">𝓕</a> <a id="6245" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#5066" class="Function">uniqueHom</a>
- <a id="6256" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#6256" class="Function">BasisStructurePShf</a> <a id="6275" class="Symbol">:</a> <a id="6277" href="Cubical.Categories.Functor.Base.html#418" class="Record">Functor</a> <a id="6285" class="Symbol">(</a><a id="6286" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4818" class="Function">BOCat</a> <a id="6292" href="Cubical.Categories.Category.Base.html#4469" class="Function Operator">^op</a><a id="6295" class="Symbol">)</a> <a id="6297" class="Symbol">(</a><a id="6298" href="Cubical.Categories.Instances.CommAlgebras.html#1156" class="Function">CommAlgebrasCategory</a> <a id="6319" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#3450" class="Bound">R&#39;</a><a id="6321" class="Symbol">)</a>
+ <a id="6256" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#6256" class="Function">BasisStructurePShf</a> <a id="6275" class="Symbol">:</a> <a id="6277" href="Cubical.Categories.Functor.Base.html#418" class="Record">Functor</a> <a id="6285" class="Symbol">(</a><a id="6286" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#4818" class="Function">BOCat</a> <a id="6292" href="Cubical.Categories.Category.Base.html#4530" class="Function Operator">^op</a><a id="6295" class="Symbol">)</a> <a id="6297" class="Symbol">(</a><a id="6298" href="Cubical.Categories.Instances.CommAlgebras.html#1156" class="Function">CommAlgebrasCategory</a> <a id="6319" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#3450" class="Bound">R&#39;</a><a id="6321" class="Symbol">)</a>
  <a id="6324" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html#6256" class="Function">BasisStructurePShf</a> <a id="6343" class="Symbol">=</a> <a id="6345" href="Cubical.Categories.Instances.CommAlgebras.html#25172" class="Function">universalPShf</a>