Skip to content

Conversation

@jdchristensen
Copy link
Collaborator

I should have noticed when reviewing #2291 that the unique tactic is essentially reproving path_contr each time.

@CharlesCNorton I think you'll find path_contr useful in other places. Can you give this PR a quick review?

@CharlesCNorton
Copy link
Contributor

Tested locally - changes work correctly. LGTM.

@jdchristensen jdchristensen merged commit 389fe14 into HoTT:master Jun 25, 2025
21 of 22 checks passed
@jdchristensen jdchristensen deleted the category-objects branch June 25, 2025 17:16
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