Skip to content

Conversation

@Alizter
Copy link
Collaborator

@Alizter Alizter commented Jan 16, 2024

This gives a slightly simpler definition of cate_prod_corec_inv.

@Alizter Alizter requested a review from jdchristensen January 16, 2024 21:51
Signed-off-by: Ali Caglayan <[email protected]>
@Alizter Alizter force-pushed the ps/branch/add_prod_0gpd_corec branch from 58fcd0a to 087e0e0 Compare January 16, 2024 21:52
@Alizter Alizter merged commit bd409fb into HoTT:master Jan 16, 2024
@Alizter Alizter deleted the ps/branch/add_prod_0gpd_corec branch January 16, 2024 22:58
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