A -pretopos is a Π-pretopos with all W-types.
In homotopy type theory the h-sets form a ΠW-pretopos (Rijke-Spitter 13). See also at structural set theory.
The inequality spaces and strongly extensional functions form a ΠW-pretopos.
See also at predicative topos.
That the h-sets in homotopy type theory form a ΠW-pretopos is discussed in
which became one chapter in
Last revised on January 9, 2023 at 07:15:51. See the history of this page for a list of all contributions to it.