Skip to content

Commit

Permalink
Deploying to gh-pages from @ cb0328e 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@felixwellen
felixwellen committed Apr 22, 2024
1 parent 1bdb65d commit 435d152
Show file tree
Hide file tree
Showing 6 changed files with 516 additions and 444 deletions.
754 changes: 385 additions & 369 deletions Cubical.Categories.Constructions.Slice.Base.html
View file

Large diffs are not rendered by default.

30 changes: 15 additions & 15 deletions Cubical.Categories.Constructions.Slice.Properties.html
View file

Large diffs are not rendered by default.

100 changes: 78 additions & 22 deletions Cubical.Categories.Constructions.SubObject.html
View file

Large diffs are not rendered by default.

64 changes: 32 additions & 32 deletions Cubical.Categories.Presheaf.Properties.html
View file

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions Cubical.Categories.Site.Cover.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
<a id="478" class="Keyword">open</a> <a id="483" href="Cubical.Categories.Category.Base.html#334" class="Module">Category</a>

<a id="495" href="Cubical.Categories.Site.Cover.html#495" class="Function">Cover</a> <a id="501" class="Symbol">:</a> <a id="503" class="Symbol">(</a><a id="504" href="Cubical.Categories.Site.Cover.html#504" class="Bound">ℓpat</a> <a id="509" class="Symbol">:</a> <a id="511" href="Agda.Primitive.html#742" class="Postulate">Level</a><a id="516" class="Symbol">)</a> <a id="518" class="Symbol">→</a> <a id="520" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a> <a id="523" href="Cubical.Categories.Site.Cover.html#448" class="Bound">C</a> <a id="525" class="Symbol">→</a> <a id="527" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="532" class="Symbol">(</a><a id="533" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="539" class="Symbol">(</a><a id="540" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="546" href="Cubical.Categories.Site.Cover.html#431" class="Bound">ℓ</a> <a id="548" href="Cubical.Categories.Site.Cover.html#433" class="Bound">ℓ&#39;</a><a id="550" class="Symbol">)</a> <a id="552" class="Symbol">(</a><a id="553" href="Agda.Primitive.html#931" class="Primitive">ℓ-suc</a> <a id="559" href="Cubical.Categories.Site.Cover.html#504" class="Bound">ℓpat</a><a id="563" class="Symbol">))</a>
<a id="568" href="Cubical.Categories.Site.Cover.html#495" class="Function">Cover</a> <a id="574" href="Cubical.Categories.Site.Cover.html#574" class="Bound">ℓpat</a> <a id="579" href="Cubical.Categories.Site.Cover.html#579" class="Bound">c</a> <a id="581" class="Symbol">=</a> <a id="583" href="Cubical.Foundations.Structure.html#399" class="Function">TypeWithStr</a> <a id="595" href="Cubical.Categories.Site.Cover.html#574" class="Bound">ℓpat</a> <a id="600" class="Symbol">λ</a> <a id="602" href="Cubical.Categories.Site.Cover.html#602" class="Bound">patches</a> <a id="610" class="Symbol">→</a> <a id="612" href="Cubical.Categories.Site.Cover.html#602" class="Bound">patches</a> <a id="620" class="Symbol">→</a> <a id="622" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a> <a id="625" class="Symbol">(</a><a id="626" href="Cubical.Categories.Constructions.Slice.Base.html#3368" class="Function">SliceCat</a> <a id="635" href="Cubical.Categories.Site.Cover.html#448" class="Bound">C</a> <a id="637" href="Cubical.Categories.Site.Cover.html#579" class="Bound">c</a><a id="638" class="Symbol">)</a>
<a id="568" href="Cubical.Categories.Site.Cover.html#495" class="Function">Cover</a> <a id="574" href="Cubical.Categories.Site.Cover.html#574" class="Bound">ℓpat</a> <a id="579" href="Cubical.Categories.Site.Cover.html#579" class="Bound">c</a> <a id="581" class="Symbol">=</a> <a id="583" href="Cubical.Foundations.Structure.html#399" class="Function">TypeWithStr</a> <a id="595" href="Cubical.Categories.Site.Cover.html#574" class="Bound">ℓpat</a> <a id="600" class="Symbol">λ</a> <a id="602" href="Cubical.Categories.Site.Cover.html#602" class="Bound">patches</a> <a id="610" class="Symbol">→</a> <a id="612" href="Cubical.Categories.Site.Cover.html#602" class="Bound">patches</a> <a id="620" class="Symbol">→</a> <a id="622" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a> <a id="625" class="Symbol">(</a><a id="626" href="Cubical.Categories.Constructions.Slice.Base.html#3953" class="Function">SliceCat</a> <a id="635" href="Cubical.Categories.Site.Cover.html#448" class="Bound">C</a> <a id="637" href="Cubical.Categories.Site.Cover.html#579" class="Bound">c</a><a id="638" class="Symbol">)</a>

<a id="641" class="Keyword">module</a> <a id="648" href="Cubical.Categories.Site.Cover.html#648" class="Module">_</a>
<a id="652" class="Symbol">{</a><a id="653" href="Cubical.Categories.Site.Cover.html#653" class="Bound">ℓ</a> <a id="655" href="Cubical.Categories.Site.Cover.html#655" class="Bound">ℓ&#39;</a> <a id="658" class="Symbol">:</a> <a id="660" href="Agda.Primitive.html#742" class="Postulate">Level</a><a id="665" class="Symbol">}</a>
Expand All @@ -39,8 +39,8 @@
<a id="865" class="Keyword">where</a>

<a id="876" href="Cubical.Categories.Site.Cover.html#876" class="Function">patchObj</a> <a id="885" class="Symbol">:</a> <a id="887" href="Cubical.Categories.Category.Base.html#452" class="Field">ob</a> <a id="890" href="Cubical.Categories.Site.Cover.html#670" class="Bound">C</a>
<a id="896" href="Cubical.Categories.Site.Cover.html#876" class="Function">patchObj</a> <a id="905" class="Symbol">=</a> <a id="907" href="Cubical.Categories.Constructions.Slice.Base.html#777" class="Field">S-ob</a> <a id="912" class="Symbol">(</a><a id="913" href="Cubical.Foundations.Structure.html#557" class="Function">str</a> <a id="917" href="Cubical.Categories.Site.Cover.html#817" class="Bound">cov</a> <a id="921" href="Cubical.Categories.Site.Cover.html#844" class="Bound">patch</a><a id="926" class="Symbol">)</a>
<a id="896" href="Cubical.Categories.Site.Cover.html#876" class="Function">patchObj</a> <a id="905" class="Symbol">=</a> <a id="907" href="Cubical.Categories.Constructions.Slice.Base.html#814" class="Field">S-ob</a> <a id="912" class="Symbol">(</a><a id="913" href="Cubical.Foundations.Structure.html#557" class="Function">str</a> <a id="917" href="Cubical.Categories.Site.Cover.html#817" class="Bound">cov</a> <a id="921" href="Cubical.Categories.Site.Cover.html#844" class="Bound">patch</a><a id="926" class="Symbol">)</a>

<a id="933" href="Cubical.Categories.Site.Cover.html#933" class="Function">patchArr</a> <a id="942" class="Symbol">:</a> <a id="944" href="Cubical.Categories.Site.Cover.html#670" class="Bound">C</a> <a id="946" href="Cubical.Categories.Category.Base.html#1083" class="Function Operator">[</a> <a id="948" href="Cubical.Categories.Site.Cover.html#876" class="Function">patchObj</a> <a id="957" href="Cubical.Categories.Category.Base.html#1083" class="Function Operator">,</a> <a id="959" href="Cubical.Categories.Site.Cover.html#802" class="Bound">c</a> <a id="961" href="Cubical.Categories.Category.Base.html#1083" class="Function Operator">]</a>
<a id="967" href="Cubical.Categories.Site.Cover.html#933" class="Function">patchArr</a> <a id="976" class="Symbol">=</a> <a id="978" href="Cubical.Categories.Constructions.Slice.Base.html#795" class="Field">S-arr</a> <a id="984" class="Symbol">(</a><a id="985" href="Cubical.Foundations.Structure.html#557" class="Function">str</a> <a id="989" href="Cubical.Categories.Site.Cover.html#817" class="Bound">cov</a> <a id="993" href="Cubical.Categories.Site.Cover.html#844" class="Bound">patch</a><a id="998" class="Symbol">)</a>
<a id="967" href="Cubical.Categories.Site.Cover.html#933" class="Function">patchArr</a> <a id="976" class="Symbol">=</a> <a id="978" href="Cubical.Categories.Constructions.Slice.Base.html#832" class="Field">S-arr</a> <a id="984" class="Symbol">(</a><a id="985" href="Cubical.Foundations.Structure.html#557" class="Function">str</a> <a id="989" href="Cubical.Categories.Site.Cover.html#817" class="Bound">cov</a> <a id="993" href="Cubical.Categories.Site.Cover.html#844" class="Bound">patch</a><a id="998" class="Symbol">)</a>
</pre></body></html>
6 changes: 3 additions & 3 deletions Cubical.Categories.Site.Instances.ZariskiCommRing.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@
<a id="978" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#978" class="Generalizable">ℓ</a> <a id="980" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#980" class="Generalizable">ℓ&#39;</a> <a id="983" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#983" class="Generalizable">ℓ&#39;&#39;</a> <a id="987" class="Symbol">:</a> <a id="989" href="Agda.Primitive.html#742" class="Postulate">Level</a>

<a id="996" class="Keyword">open</a> <a id="1001" href="Cubical.Categories.Site.Coverage.html#952" class="Module">Coverage</a>
<a id="1010" class="Keyword">open</a> <a id="1015" href="Cubical.Categories.Constructions.Slice.Base.html#720" class="Module">SliceOb</a>
<a id="1010" class="Keyword">open</a> <a id="1015" href="Cubical.Categories.Constructions.Slice.Base.html#757" class="Module">SliceOb</a>

<a id="1024" class="Comment">-- the type of unimodular vectors, i.e. generators of the 1-ideal</a>
<a id="1090" class="Keyword">record</a> <a id="UniModVec"></a><a id="1097" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1097" class="Record">UniModVec</a> <a id="1107" class="Symbol">(</a><a id="1108" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1108" class="Bound">R</a> <a id="1110" class="Symbol">:</a> <a id="1112" href="Cubical.Algebra.CommRing.Base.html#1279" class="Function">CommRing</a> <a id="1121" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#978" class="Generalizable">ℓ</a><a id="1122" class="Symbol">)</a> <a id="1124" class="Symbol">:</a> <a id="1126" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="1131" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1121" class="Bound">ℓ</a> <a id="1133" class="Keyword">where</a>
Expand Down Expand Up @@ -91,11 +91,11 @@
<a id="2669" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="2673" class="Symbol">(</a><a id="2674" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2678" class="Symbol">(</a><a id="2679" href="Cubical.Categories.Site.Coverage.html#1077" class="Field">covers</a> <a id="2686" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2556" class="Function">zariskiCoverage</a> <a id="2702" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2702" class="Bound">R</a><a id="2703" class="Symbol">)</a> <a id="2705" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2705" class="Bound">um</a><a id="2707" class="Symbol">)</a> <a id="2709" class="Symbol">=</a> <a id="2711" href="Cubical.Data.FinData.Base.html#375" class="Datatype">Fin</a> <a id="2715" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1239" class="Field">n</a> <a id="2717" class="Comment">--patches</a>
<a id="2729" class="Keyword">where</a>
<a id="2737" class="Keyword">open</a> <a id="2742" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1097" class="Module">UniModVec</a> <a id="2752" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2705" class="Bound">um</a>
<a id="2755" href="Cubical.Categories.Constructions.Slice.Base.html#777" class="Field">S-ob</a> <a id="2760" class="Symbol">(</a><a id="2761" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2765" class="Symbol">(</a><a id="2766" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2770" class="Symbol">(</a><a id="2771" href="Cubical.Categories.Site.Coverage.html#1077" class="Field">covers</a> <a id="2778" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2556" class="Function">zariskiCoverage</a> <a id="2794" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2794" class="Bound">R</a><a id="2795" class="Symbol">)</a> <a id="2797" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2797" class="Bound">um</a><a id="2799" class="Symbol">)</a> <a id="2801" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2801" class="Bound">i</a><a id="2802" class="Symbol">)</a> <a id="2804" class="Symbol">=</a> <a id="2806" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#3272" class="Function Operator">R[1/</a> <a id="2811" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1249" class="Function">f</a> <a id="2813" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2801" class="Bound">i</a> <a id="2815" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#3272" class="Function Operator">]AsCommRing</a>
<a id="2755" href="Cubical.Categories.Constructions.Slice.Base.html#814" class="Field">S-ob</a> <a id="2760" class="Symbol">(</a><a id="2761" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2765" class="Symbol">(</a><a id="2766" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2770" class="Symbol">(</a><a id="2771" href="Cubical.Categories.Site.Coverage.html#1077" class="Field">covers</a> <a id="2778" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2556" class="Function">zariskiCoverage</a> <a id="2794" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2794" class="Bound">R</a><a id="2795" class="Symbol">)</a> <a id="2797" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2797" class="Bound">um</a><a id="2799" class="Symbol">)</a> <a id="2801" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2801" class="Bound">i</a><a id="2802" class="Symbol">)</a> <a id="2804" class="Symbol">=</a> <a id="2806" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#3272" class="Function Operator">R[1/</a> <a id="2811" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1249" class="Function">f</a> <a id="2813" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2801" class="Bound">i</a> <a id="2815" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#3272" class="Function Operator">]AsCommRing</a>
<a id="2829" class="Keyword">where</a>
<a id="2837" class="Keyword">open</a> <a id="2842" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1097" class="Module">UniModVec</a> <a id="2852" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2797" class="Bound">um</a>
<a id="2857" class="Keyword">open</a> <a id="2862" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#2217" class="Module">InvertingElementsBase</a> <a id="2884" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2794" class="Bound">R</a>
<a id="2886" href="Cubical.Categories.Constructions.Slice.Base.html#795" class="Field">S-arr</a> <a id="2892" class="Symbol">(</a><a id="2893" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2897" class="Symbol">(</a><a id="2898" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2902" class="Symbol">(</a><a id="2903" href="Cubical.Categories.Site.Coverage.html#1077" class="Field">covers</a> <a id="2910" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2556" class="Function">zariskiCoverage</a> <a id="2926" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2926" class="Bound">R</a><a id="2927" class="Symbol">)</a> <a id="2929" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2929" class="Bound">um</a><a id="2931" class="Symbol">)</a> <a id="2933" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2933" class="Bound">i</a><a id="2934" class="Symbol">)</a> <a id="2936" class="Symbol">=</a> <a id="2938" href="Cubical.Algebra.CommRing.Localisation.UniversalProperty.html#2722" class="Function">/1AsCommRingHom</a>
<a id="2886" href="Cubical.Categories.Constructions.Slice.Base.html#832" class="Field">S-arr</a> <a id="2892" class="Symbol">(</a><a id="2893" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2897" class="Symbol">(</a><a id="2898" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="2902" class="Symbol">(</a><a id="2903" href="Cubical.Categories.Site.Coverage.html#1077" class="Field">covers</a> <a id="2910" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2556" class="Function">zariskiCoverage</a> <a id="2926" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2926" class="Bound">R</a><a id="2927" class="Symbol">)</a> <a id="2929" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2929" class="Bound">um</a><a id="2931" class="Symbol">)</a> <a id="2933" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2933" class="Bound">i</a><a id="2934" class="Symbol">)</a> <a id="2936" class="Symbol">=</a> <a id="2938" href="Cubical.Algebra.CommRing.Localisation.UniversalProperty.html#2722" class="Function">/1AsCommRingHom</a>
<a id="2956" class="Keyword">where</a>
<a id="2964" class="Keyword">open</a> <a id="2969" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1097" class="Module">UniModVec</a> <a id="2979" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2929" class="Bound">um</a>
<a id="2984" class="Keyword">open</a> <a id="2989" href="Cubical.Algebra.CommRing.Localisation.InvertingElements.html#10906" class="Module">InvertingElementsBase.UniversalProp</a> <a id="3025" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2926" class="Bound">R</a> <a id="3027" class="Symbol">(</a><a id="3028" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#1249" class="Function">f</a> <a id="3030" href="Cubical.Categories.Site.Instances.ZariskiCommRing.html#2933" class="Bound">i</a><a id="3031" class="Symbol">)</a>
Expand Down

0 comments on commit 435d152

Please sign in to comment.