Wedge of a family of pType #1829
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Defined. | ||
|
|
||
| (** Recursion principle for the wedge of an indexed family of pointed types. *) |
There was a problem hiding this comment.
This should be an equivalence, which means that FamilyWedge X is a coproduct in pType. Does the Wildcat library have coproducts where the summands are indexed by a type?
There was a problem hiding this comment.
I didn't add such coproducts yet, but it should be straightforward.
There was a problem hiding this comment.
I think I'll hold off on making this an equivalence for now and perhaps introduce it when we have that result for coproducts.
Alizter
force-pushed
the
ps/branch/wedge_of_a_family_of_ptype
branch
3 times, most recently
from
ca50dcb to
6e534a2
Compare
jdchristensen
approved these changes
Jan 25, 2024
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
We don't have to convert the indexing type into a pointed type, it already is a type! Signed-off-by: Ali Caglayan <[email protected]>
Alizter
force-pushed
the
ps/branch/wedge_of_a_family_of_ptype
branch
from
6e534a2 to
1d3ee90
Compare
|
LGTM! |
|
Thanks! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We define wedges of families of pTypes.
Interestingly, we have to make some decidability assumptions on the indexing type in order to get the inclusion from wedge to product. This is also true for such colimits in a general pointed category.
I'm not sure if these assumptions are necessary, and in practice most index sets we will choose are decidable.
Once we have free products of abelian groups defined, we should be able to extend the PinSn result to wedges of spheres.