On 2011-03-31 09:06, Nicolas Pouillard wrote:
> record Irr {a} (A : Set a) : Set a where
> constructor irr
> field
> .cert : A
What would happen if we replaced the irrelevance machinery with a single
type like Irr? (I think such a type is more commonly called a "squash"
or "bracket" type.) Would we lose anything?
--
/NAD