Cubical Classics

An attempt towards univalent classical mathematics in Cubical Agda.