Deploying to gh-pages from @ 598dfa5 🚀

agda · Apr 16, 2024 · 1bdb65d · 1bdb65d
1 parent b824e78
commit 1bdb65d
Show file tree

Hide file tree

Showing 20 changed files with 2,913 additions and 2,754 deletions.
diff --git a/Cubical.Algebra.Everything.html b/Cubical.Algebra.Everything.html
@@ -164,9 +164,4 @@
 <a id="7823" class="Keyword">import</a> <a id="7830" href="Cubical.Algebra.Semiring.html" class="Module">Cubical.Algebra.Semiring</a>
 <a id="7855" class="Keyword">import</a> <a id="7862" href="Cubical.Algebra.Semiring.BigOps.html" class="Module">Cubical.Algebra.Semiring.BigOps</a>
 <a id="7894" class="Keyword">import</a> <a id="7901" href="Cubical.Algebra.SymmetricGroup.html" class="Module">Cubical.Algebra.SymmetricGroup</a>
-<a id="7932" class="Keyword">import</a> <a id="7939" href="Cubical.Algebra.ZariskiLattice.Base.html" class="Module">Cubical.Algebra.ZariskiLattice.Base</a>
-<a id="7975" class="Keyword">import</a> <a id="7982" href="Cubical.Algebra.ZariskiLattice.Properties.html" class="Module">Cubical.Algebra.ZariskiLattice.Properties</a>
-<a id="8024" class="Keyword">import</a> <a id="8031" href="Cubical.Algebra.ZariskiLattice.StructureSheaf.html" class="Module">Cubical.Algebra.ZariskiLattice.StructureSheaf</a>
-<a id="8077" class="Keyword">import</a> <a id="8084" href="Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html" class="Module">Cubical.Algebra.ZariskiLattice.StructureSheafPullback</a>
-<a id="8138" class="Keyword">import</a> <a id="8145" href="Cubical.Algebra.ZariskiLattice.UniversalProperty.html" class="Module">Cubical.Algebra.ZariskiLattice.UniversalProperty</a>
 </pre></body></html>
diff --git a/Cubical.Algebra.ZariskiLattice.Base.html b/Cubical.Algebra.ZariskiLattice.Base.html
diff --git a/Cubical.Algebra.ZariskiLattice.Properties.html b/Cubical.Algebra.ZariskiLattice.Properties.html
diff --git a/Cubical.Algebra.ZariskiLattice.StructureSheaf.html b/Cubical.Algebra.ZariskiLattice.StructureSheaf.html
diff --git a/Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html b/Cubical.Algebra.ZariskiLattice.StructureSheafPullback.html
diff --git a/Cubical.Algebra.ZariskiLattice.UniversalProperty.html b/Cubical.Algebra.ZariskiLattice.UniversalProperty.html
diff --git a/Cubical.AlgebraicGeometry.Everything.html b/Cubical.AlgebraicGeometry.Everything.html
@@ -0,0 +1,14 @@
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Cubical.AlgebraicGeometry.Everything</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Symbol">#-}</a>
+<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.AlgebraicGeometry.Everything.html" class="Module">Cubical.AlgebraicGeometry.Everything</a> <a id="68" class="Keyword">where</a>
+
+<a id="75" class="Keyword">import</a> <a id="82" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html" class="Module">Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base</a>
+<a id="134" class="Keyword">import</a> <a id="141" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen.html" class="Module">Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen</a>
+<a id="200" class="Keyword">import</a> <a id="207" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme.html" class="Module">Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme</a>
+<a id="268" class="Keyword">import</a> <a id="275" href="Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme.html" class="Module">Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme</a>
+<a id="333" class="Keyword">import</a> <a id="340" href="Cubical.AlgebraicGeometry.ZariskiLattice.Base.html" class="Module">Cubical.AlgebraicGeometry.ZariskiLattice.Base</a>
+<a id="386" class="Keyword">import</a> <a id="393" href="Cubical.AlgebraicGeometry.ZariskiLattice.Properties.html" class="Module">Cubical.AlgebraicGeometry.ZariskiLattice.Properties</a>
+<a id="445" class="Keyword">import</a> <a id="452" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf.html" class="Module">Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf</a>
+<a id="508" class="Keyword">import</a> <a id="515" href="Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html" class="Module">Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback</a>
+<a id="579" class="Keyword">import</a> <a id="586" href="Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty.html" class="Module">Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty</a>
+</pre></body></html>
diff --git a/Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html b/Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base.html
diff --git a/Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen.html b/Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen.html
diff --git a/Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme.html b/Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme.html
diff --git a/Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme.html b/Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme.html
diff --git a/Cubical.AlgebraicGeometry.ZariskiLattice.Base.html b/Cubical.AlgebraicGeometry.ZariskiLattice.Base.html
diff --git a/Cubical.AlgebraicGeometry.ZariskiLattice.Properties.html b/Cubical.AlgebraicGeometry.ZariskiLattice.Properties.html
diff --git a/Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf.html b/Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf.html
diff --git a/Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html b/Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback.html
diff --git a/Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty.html b/Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty.html
diff --git a/Cubical.Categories.Instances.ZFunctors.html b/Cubical.Categories.Instances.ZFunctors.html
diff --git a/Cubical.Papers.AffineSchemes.html b/Cubical.Papers.AffineSchemes.html
diff --git a/Cubical.Papers.FunctorialQcQsSchemes.html b/Cubical.Papers.FunctorialQcQsSchemes.html
diff --git a/Cubical.README.html b/Cubical.README.html
@@ -69,18 +69,21 @@
 <a id="1788" class="Comment">-- Algebra library (in development)</a>
 <a id="1824" class="Keyword">import</a> <a id="1831" href="Cubical.Algebra.Everything.html" class="Module">Cubical.Algebra.Everything</a>
 
-<a id="1859" class="Comment">-- Various talks</a>
-<a id="1876" class="Keyword">import</a> <a id="1883" href="Cubical.Talks.Everything.html" class="Module">Cubical.Talks.Everything</a>
+<a id="1859" class="Comment">-- Algebraic geometry</a>
+<a id="1881" class="Keyword">import</a> <a id="1888" href="Cubical.AlgebraicGeometry.Everything.html" class="Module">Cubical.AlgebraicGeometry.Everything</a>
 
-<a id="1909" class="Comment">-- Reflection</a>
-<a id="1923" class="Keyword">import</a> <a id="1930" href="Cubical.Reflection.Everything.html" class="Module">Cubical.Reflection.Everything</a>
+<a id="1926" class="Comment">-- Various talks</a>
+<a id="1943" class="Keyword">import</a> <a id="1950" href="Cubical.Talks.Everything.html" class="Module">Cubical.Talks.Everything</a>
 
-<a id="1961" class="Comment">-- Displayed univalent graphs</a>
-<a id="1991" class="Keyword">import</a> <a id="1998" href="Cubical.Displayed.Everything.html" class="Module">Cubical.Displayed.Everything</a>
+<a id="1976" class="Comment">-- Reflection</a>
+<a id="1990" class="Keyword">import</a> <a id="1997" href="Cubical.Reflection.Everything.html" class="Module">Cubical.Reflection.Everything</a>
 
-<a id="2028" class="Comment">-- Various axioms and consequences</a>
-<a id="2063" class="Keyword">import</a> <a id="2070" href="Cubical.Axiom.Everything.html" class="Module">Cubical.Axiom.Everything</a>
+<a id="2028" class="Comment">-- Displayed univalent graphs</a>
+<a id="2058" class="Keyword">import</a> <a id="2065" href="Cubical.Displayed.Everything.html" class="Module">Cubical.Displayed.Everything</a>
 
-<a id="2096" class="Comment">-- Automatic proving, solvers</a>
-<a id="2126" class="Keyword">import</a> <a id="2133" href="Cubical.Tactics.Everything.html" class="Module">Cubical.Tactics.Everything</a>
+<a id="2095" class="Comment">-- Various axioms and consequences</a>
+<a id="2130" class="Keyword">import</a> <a id="2137" href="Cubical.Axiom.Everything.html" class="Module">Cubical.Axiom.Everything</a>
+
+<a id="2163" class="Comment">-- Automatic proving, solvers</a>
+<a id="2193" class="Keyword">import</a> <a id="2200" href="Cubical.Tactics.Everything.html" class="Module">Cubical.Tactics.Everything</a>
 </pre></body></html>