Ideal completion has all small joins

martinescardo / TypeTopology

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

GNU General Public License v3.0

228 stars 42 forks source link

Closed tomdjong closed 3 months ago

tomdjong commented 3 months ago

This technical result formalises what was previously left as a module assumption.