From 28704e6786a8e7b1edd42c8c35b3cfaebc8a0b9a Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Tue, 20 Feb 2024 19:04:27 +0100 Subject: [PATCH] update refs in Papers --- Cubical/Papers/SmashProducts.agda | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/Cubical/Papers/SmashProducts.agda b/Cubical/Papers/SmashProducts.agda index 3ee0edf037..25aa062464 100644 --- a/Cubical/Papers/SmashProducts.agda +++ b/Cubical/Papers/SmashProducts.agda @@ -14,14 +14,16 @@ Axel Ljungström, 2024 {-# OPTIONS --safe #-} module Cubical.Papers.SmashProducts where -- Section 2 -import Cubical.Categories.Category.Precategory as WCat +import Cubical.WildCat.Base as WCat1 +import Cubical.WildCat.Instances.Pointed as WCat2 +import Cubical.WildCat.BraidedSymmetricMonoidal as WCat3 import Cubical.HITs.SmashProduct.Base as Smash -- Section 3 import Cubical.Foundations.Pointed.Homogeneous as Hom -- Section 5 -import Cubical.HITs.SmashProduct.SymmetricMonoidal as SM +import Cubical.HITs.SmashProduct.SymmetricMonoidalCat as SM -- Section 6 import Cubical.HITs.SmashProduct.Induction as SmashInduction @@ -29,17 +31,17 @@ import Cubical.HITs.SmashProduct.Induction as SmashInduction ---- 2 Background ---- --- 2.1 Symmetric monoidal wild categories --- Definition 1 (Wild categories - note: currently called precategories in the library) -open WCat using (Precategory) +-- Definition 1 (Wild categories) +open WCat1 using (WildCat) -- Proposition 2 (Pointed types form a wild cat) -open WCat using (PointedCat) +open WCat2 using (PointedCat) -- Definition 3 (Monoidal wild categories) -open WCat using (isMonoidalPrecategory) +open WCat3 using (isMonoidalWildCat) -- Definition 4 (Symmetric Monoidal wild categories) -open WCat using (SymmetricMonoidalPrecat) +open WCat3 using (SymmetricMonoidalPrecat) --- 2.2 Smash Products -- Definition 5 (Smash products -- note: defined as a coproduct in the