search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

add proof that Sigma preserves null types #1085

Closed awswan closed 8 months ago

awswan commented 8 months ago

I couldn't find a proof that null types are preserved by Sigma, so here's one, added to Nullification.Properties with some similar proofs.

mortberg commented 8 months ago

Looks good to me so merging. Thanks for the contribution!