Author Archives: spitters37

In section 10.5 of the HoTT book, the cumulative hierarchy V is defined as a rather non-standard higher inductive type. We can then define a membership relation ∈ on this type, such that (V, ∈) satisfies most of the axioms … Continue reading →