Products of FinCats and isomorphism testing of diagrams of C-sets #896
+307
−4
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.
This PR implements uncurrying, where we take a diagram of C-Sets (
J -> C -> Set
) and make it into an instance ofJ x C -> Set
. This allows us to apply various C-Set algorithms, such as isomorphism testing, to morphisms (indexed by the walking arrow category), spans, etc. This is useful for writing robust tests for (co)limits, which produce (co)spans only up to isomorphism (presently, we make assumptions about which isomorph is coming out of the (co)limit machinery whenever testing the output map data).In order to do this, there is an implementation of products of FinCatPresentations, taken from #615 and cleaned up (there many features there which are left behind, such as the inverse operation of currying, and the action of (un)currying on FinTransformations rather than just FinFunctors).
This is only expected to work for C-Sets (no attributes, no variables) though it should be possible to generalize to that setting.