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
A type with a nontrivial apartness relation cannot be injective unless WEM holds. #285
Closed
tomdjong closed 4 months ago
@martinescardo I implemented this morning's TODO and left an optional one.