search

thehottgame / TheHoTTGame

Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT
125 stars 15 forks source link

compatibility with recent cubical #18

Closed iblech closed 9 months ago

iblech commented 9 months ago

Without this commit, there is a naming collision with the elim of Cubical.HITs.S1.

This issue was brought to my attention by an Agdapad player :-)

Thank you for your work on the HoTT game :-)

Jlh18 commented 9 months ago

Excellent! Thank you to both you and the Agdapad player.