Skip to content

Commit 02c996f

Browse files
authored
Missed rename of Precat to WildCat (#1200)
* Missed rename of Precat to WildCat * Update SmashProducts.agda also fixed what I think was a typo: the smash product is defined as a pushout, not a coproduct.
1 parent d96372c commit 02c996f

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

Cubical/Papers/SmashProducts.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -40,10 +40,10 @@ open WCat2 using (PointedCat)
4040
open WCat3 using (isMonoidalWildCat)
4141

4242
-- Definition 4 (Symmetric Monoidal wild categories)
43-
open WCat3 using (SymmetricMonoidalPrecat)
43+
open WCat3 using (isSymmetricWildCat)
4444

4545
--- 2.2 Smash Products
46-
-- Definition 5 (Smash products -- note: defined as a coproduct in the
46+
-- Definition 5 (Smash products -- note: defined as a pushout in the
4747
-- library. E.g. the ⟨ x , y ⟩ constructor here is simply
4848
-- inr(x,y). Also note that pushₗ and pushᵣ are inverted with this
4949
-- definition.)

Cubical/WildCat/BraidedSymmetricMonoidal.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,6 @@ module _ (M : WildCat ℓ ℓ') where
103103
hexagon : HexagonType₁ isMonoidal Braid
104104
symBraiding : isSymmetricBraiding isMonoidal Braid
105105

106-
SymmetricMonoidalPrecat : (ℓ ℓ' : Level) Type (ℓ-suc (ℓ-max ℓ ℓ'))
107-
SymmetricMonoidalPrecat ℓ ℓ' =
106+
SymmetricMonoidalWildCat : (ℓ ℓ' : Level) Type (ℓ-suc (ℓ-max ℓ ℓ'))
107+
SymmetricMonoidalWildCat ℓ ℓ' =
108108
Σ[ C ∈ WildCat ℓ ℓ' ] isSymmetricWildCat C

0 commit comments

Comments
 (0)