Skip to content

Conversation

@jdchristensen
Copy link
Collaborator

Swap the names of triangle_v and triangle_v', and same for the _h versions. This is the first commit, which can be deselected to get a cleaner view of the next two commits.

Add trijoin_id_sym as a definition for functor_join idmap (join_sym _ _), which turns out to play a central role as it is the permutation (2,3), the other generator of S_3. Prove that it is natural.

Also export a few more things from canonical_names in HSpace/Core, as some other work I'm doing depends on those.

@jdchristensen jdchristensen requested a review from Alizter October 19, 2023 12:36
@jdchristensen jdchristensen merged commit 11efe93 into HoTT:master Oct 19, 2023
@jdchristensen jdchristensen deleted the join-id-sym branch October 19, 2023 17:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants