The lifting of a large proposition as an algebraic dcpo

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.

GNU General Public License v3.0

220 stars 40 forks source link

Closed tomdjong closed 1 month ago

tomdjong commented 1 month ago

...has a small compact basis iff the proposition can be resized.

cc @ayberkt

martinescardo commented 1 month ago

Wonderful! I don't have anything to suggest.