search

mikeshulman / Coq-HoTT

Homotopy type theory
http://homotopytypetheory.org/
Other
12 stars 4 forks source link

Reflective subcategories #34

Open mikeshulman opened 4 years ago

mikeshulman commented 4 years ago

As Egbert pointed out, a lot of the theory of reflective subuniverses should generalize. But we couldn't get the theory of reflective subuniverses itself as a special case, unless we did away with the modules there.