Skip to content

Construct the initial P algebra, called V⁰

Håkon Gylterud requested to merge hott/hott-set-theory:initiality-merge into master

This constructs the initial algebra of the powerset functor and proves its initiality.

Merge request reports