From 2ecfa0093af5d385ed40f73eb5b27b21065fe7a3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Axel=20Ljungstr=C3=B6m?=
 <49276137+aljungstrom@users.noreply.github.com>
Date: Wed, 31 Jan 2024 11:55:53 +0100
Subject: [PATCH] Placeholder for paper in progress (#1094)

* t

* duplicate

* wups

* rme

* ganea stuff

* w

* w

* w

* placeholder
---
 Cubical/Papers/SmashProducts.agda | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 Cubical/Papers/SmashProducts.agda

diff --git a/Cubical/Papers/SmashProducts.agda b/Cubical/Papers/SmashProducts.agda
new file mode 100644
index 0000000000..0d62346545
--- /dev/null
+++ b/Cubical/Papers/SmashProducts.agda
@@ -0,0 +1,25 @@
+{-
+
+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
+
+-}
+
+-- The "--safe" flag ensures that there are no postulates or unfinished goals
+{-# OPTIONS --safe #-}
+module Cubical.Papers.SmashProducts where
+
+-- 2: Background
+
+-- 3: Associativity
+
+-- 4: The Heuristic
+
+-- 5. The symmetric monoidal structure
+
+-- 6. A formal statement of the heuristic