search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

define inverse(??) to associator? #466

Closed jonsterling closed 5 years ago

jonsterling commented 5 years ago

was just playing around. looks like it will be almost impossible to prove this is an equivalence, LOL