cubical icon indicating copy to clipboard operation
cubical copied to clipboard

Published 20 hours ago • verified publisher icon agda

Examples for modalities

Open MatthiasHu opened this issue 2 years ago • 1 comments

This PR provides a few simple examples of modalities (as defined in Cubical.Modalities.Modality). Note that there is already HLevelTruncModality in Cubical.HITs.Truncation.Properties.

MatthiasHu avatar Jun 23 '22 13:06 MatthiasHu

I wonder whether there is a more elegant definition for the open modality. But I can't find one, so I leave it like this for now.

MatthiasHu avatar Aug 12 '22 18:08 MatthiasHu

I don't know a better presentation of the open modality.

felixwellen avatar Aug 23 '22 08:08 felixwellen