Deploying to gh-pages from @ 2ecfa00 🚀

agda · Jan 31, 2024 · cdca427 · cdca427
1 parent 9d1e735
commit cdca427
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 2 deletions.
diff --git a/Cubical.Papers.Everything.html b/Cubical.Papers.Everything.html
@@ -7,6 +7,7 @@
 <a id="138" class="Keyword">import</a> <a id="145" href="Cubical.Papers.ComputationalSyntheticCohomology.html" class="Module">Cubical.Papers.ComputationalSyntheticCohomology</a>
 <a id="193" class="Keyword">import</a> <a id="200" href="Cubical.Papers.Pi4S3.html" class="Module">Cubical.Papers.Pi4S3</a>
 <a id="221" class="Keyword">import</a> <a id="228" href="Cubical.Papers.RepresentationIndependence.html" class="Module">Cubical.Papers.RepresentationIndependence</a>
-<a id="270" class="Keyword">import</a> <a id="277" href="Cubical.Papers.Synthetic.html" class="Module">Cubical.Papers.Synthetic</a>
-<a id="302" class="Keyword">import</a> <a id="309" href="Cubical.Papers.ZCohomology.html" class="Module">Cubical.Papers.ZCohomology</a>
+<a id="270" class="Keyword">import</a> <a id="277" href="Cubical.Papers.SmashProducts.html" class="Module">Cubical.Papers.SmashProducts</a>
+<a id="306" class="Keyword">import</a> <a id="313" href="Cubical.Papers.Synthetic.html" class="Module">Cubical.Papers.Synthetic</a>
+<a id="338" class="Keyword">import</a> <a id="345" href="Cubical.Papers.ZCohomology.html" class="Module">Cubical.Papers.ZCohomology</a>
 </pre></body></html>
diff --git a/Cubical.Papers.SmashProducts.html b/Cubical.Papers.SmashProducts.html
@@ -0,0 +1,27 @@
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Cubical.Papers.SmashProducts</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">{-
+
+Please do not move this file. Changes should only be made if necessary.
+
+This file contains pointers to the code examples and main results from
+the paper:
+
+Symmetric Monoidal Smash Products in Homotopy Type Theory,
+Axel Ljungström
+
+-}</a>
+
+<a id="241" class="Comment">-- The &quot;--safe&quot; flag ensures that there are no postulates or unfinished goals</a>
+<a id="319" class="Symbol">{-#</a> <a id="323" class="Keyword">OPTIONS</a> <a id="331" class="Pragma">--safe</a> <a id="338" class="Symbol">#-}</a>
+<a id="342" class="Keyword">module</a> <a id="349" href="Cubical.Papers.SmashProducts.html" class="Module">Cubical.Papers.SmashProducts</a> <a id="378" class="Keyword">where</a>
+
+<a id="385" class="Comment">-- 2: Background</a>
+
+<a id="403" class="Comment">-- 3: Associativity</a>
+
+<a id="424" class="Comment">-- 4: The Heuristic</a>
+
+<a id="445" class="Comment">-- 5. The symmetric monoidal structure</a>
+
+<a id="485" class="Comment">-- 6. A formal statement of the heuristic</a>
+</pre></body></html>