Universes in sheafification_hprop #3
Description
There is still a "Universe inconsistency" in sheaf_induction, in Lemma sheafification_hprop, even with type-in-type on.
{{ message }}
There is still a "Universe inconsistency" in sheaf_induction, in Lemma sheafification_hprop, even with type-in-type on.