Commit 2021-12-28 19:49 8d41552f
View on Github →feat(logic/small): The range of a function from a small type is small (#11029)
That is, you don't actually need an equivalence to build small α, a mere function does the trick.
feat(logic/small): The range of a function from a small type is small (#11029)
That is, you don't actually need an equivalence to build small α, a mere function does the trick.