Skip to content

Missed rename of Precat to WildCat #1200

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Missed rename of Precat to WildCat #1200

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
52c12b3
Missed rename of Precat to WildCat
anshwad10 Feb 28, 2025
4e80cd2
Update SmashProducts.agda
anshwad10 Feb 28, 2025
0a4da42
Merge branch 'agda:master' into monoidal-wildcat
anshwad10 May 25, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Cubical/Papers/SmashProducts.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,10 +41,10 @@ open WCat2 using (PointedCat)
open WCat3 using (isMonoidalWildCat)

-- Definition 4 (Symmetric Monoidal wild categories)
open WCat3 using (SymmetricMonoidalPrecat)
open WCat3 using (isSymmetricWildCat)

--- 2.2 Smash Products
-- Definition 5 (Smash products -- note: defined as a coproduct in the
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should leave Axel's formulation as it is - note that he uses a pushout to construct a coproduct in pointed types.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

but calling it a coproduct doesn't make sense - the smash product is a coproduct neither in the (wild) category of types nor in pointed types. I am pretty sure calling it a coproduct was a typo/mistake

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, ok - I didn't read carefully enough. But since it is a collection of results from a paper (and it could be that he wanted to point out that it is a definition where a coproduct is used), let's better check with @aljungstrom.

-- Definition 5 (Smash products -- note: defined as a pushout in the
-- library. E.g. the ⟨ x , y ⟩ constructor here is simply
-- inr(x,y). Also note that pushₗ and pushᵣ are inverted with this
-- definition.)
Expand Down
4 changes: 2 additions & 2 deletions Cubical/WildCat/BraidedSymmetricMonoidal.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,6 @@ module _ (M : WildCat ℓ ℓ') where
hexagon : HexagonType₁ isMonoidal Braid
symBraiding : isSymmetricBraiding isMonoidal Braid

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