Skip to content

rename cat_coprod_prod_incl -> cat_coprod_prod#1946

Merged
Alizter merged 1 commit intoHoTT:masterfrom Alizter:ps/rr/rename_cat_coprod_prod_incl____cat_coprod_prodMay 3, 2024

Commits

Commits on May 2, 2024