Missed rename of Precat to WildCat #1200
Conversation
|
@felixwellen missed renaming |
also fixed what I think was a typo: the smash product is defined as a pushout, not a coproduct.
| open WCat3 using (isSymmetricWildCat) | ||
|
|
||
| --- 2.2 Smash Products | ||
| -- Definition 5 (Smash products -- note: defined as a coproduct in the |
There was a problem hiding this comment.
We should leave Axel's formulation as it is - note that he uses a pushout to construct a coproduct in pointed types.
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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.
No description provided.