agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

447 stars 136 forks source link

Modalities #1025

Open JonasHoefer opened 1 year ago

JonasHoefer commented 1 year ago

I started formalizing some of the results about modalities in HoTT by Rijke et al. This pull request formalizes multiple results for reflective subuniverses from the paper.

604 has a similar goal, but wasn't update in a long time.