WIP: A constructive Cantor–Schröder–Bernstein theorem?

[fredrik-bakke]

No description provided.

[fredrik-bakke]

I see that we usually phrase small decidable predicates in terms of functions into Fin 2, such as for the omniscience principles. However, I'd like to instead use bool because I'd like to introduce is-true := Eq-bool true and is-false := Eq-bool false predicates, and find the fact that one has to pattern match on the elements of Fin 2 twice a bit hassling. Is it okay if I continue using bool over Fin 2 in my developments in logic @EgbertRijke?

[EgbertRijke]

Would it be possible to move existing files in a separate pull request that only moves files, like I did in #1223 to preserve your authorship of some files about globular types?

[fredrik-bakke]

Sure! I'll see about how to solve this

[fredrik-bakke]

Would you mind answering my question above in the PR, btw?

[fredrik-bakke]

Some of the work I need to do to continue this PR depends on #1188. Could we merge that PR soon?

[EgbertRijke]

Some of the work I need to do to continue this PR depends on #1188. Could we merge that PR soon?

Thanks for the heads up! I'll make it a priority.

[fredrik-bakke]

Turns out the approach I had in mind for this PR doesn't quite work and needs to be rethought a little. Since this PR still covers some additions not covered by other PRs I'll leave it open, but ultimately this PR should be closed until a correct approach is found.