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

sphere1-to-s1 equivalence #460

Closed ecavallo closed 5 years ago

ecavallo commented 5 years ago

Keeping up with cubical agda (https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp.agda)