Regular universes and formal spaces Export

@article{citeulike:6067411, abstract = {We present an alternative solution to the problem of inductive generation of covers in formal topology by using a restricted form of type universes. These universes are at the same time constructive analogues of regular cardinals and sets of infinitary formulae. The technique of regular universes is also used to construct canonical positivity predicates for inductively generated covers.}, author = {Palmgren, E.}, citeulike-article-id = {6067411}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.apal.2005.05.025}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S0168007205000758}, doi = {10.1016/j.apal.2005.05.025}, issn = {01680072}, journal = {Annals of Pure and Applied Logic}, keywords = {dependent-types, universe}, month = {January}, number = {1-3}, pages = {299--316}, posted-at = {2009-11-04 11:43:52}, priority = {2}, title = {Regular universes and formal spaces}, url = {http://dx.doi.org/10.1016/j.apal.2005.05.025}, volume = {137}, year = {2006} }

TY - JOUR ID - citeulike:6067411 L3 - citeulike-article-id:6067411 N2 - We present an alternative solution to the problem of inductive generation of covers in formal topology by using a restricted form of type universes. These universes are at the same time constructive analogues of regular cardinals and sets of infinitary formulae. The technique of regular universes is also used to construct canonical positivity predicates for inductively generated covers. IS - 1-3 JF - Annals of Pure and Applied Logic SN - 01680072 EP - 316 TI - Regular universes and formal spaces VL - 137 SP - 299 KW - dependent-types KW - universe AU - Palmgren, E PY - 2006/01// UR - http://dx.doi.org/10.1016/j.apal.2005.05.025 ER -