Author Archives: spitters37

The cumulative hierarchy of sets (guest post by Jeremy Ledent)

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

Posted in Uncategorized | 2 Comments