Partial and copartial functions

[EgbertRijke]

This PR adds partial and copartial functions to the library. Partial functions were needed to define partial sequences, which are ultimately needed for some OEIS entries. Copartial functions are simply the dual of partial functions, which I came up with while formalizing partial functions.

Note that partial functions are defined using the open modalities, so naturally copartial functions are defined using the closed modalities. They specify where a function is prohibited. The terminology in the files about copartial functions is not established in the literature (as far as I know), and should be considered experimental.

[fredrik-bakke]

Neat! Your idea for copartial elements makes a lot of sense.

[EgbertRijke]

Instead of calling copartial elements "prohibited" if the underlying proposition holds, another suggestion would be to call them "erased". That would be more clearly dual to "defined". Reviewers, what do you think?

[fredrik-bakke]

Yeah! I do like "erased" better than "prohibited".

[EgbertRijke]

Then they could be called "wiped functions" 😁

[fredrik-bakke]

What role would P × B play in this context? After all, this corresponds to the only internally definable coreflective subuniverses

[EgbertRijke]

Good question! I thought about that option earlier today, but I don't remember why I dismissed it. Maybe I shouldn't have:)

[VojtechStep]

another suggestion would be to call them "erased"

I like "erased" 👍

[EgbertRijke]

I have addressed all the comments. Furthermore, I have also added some informal text explaining how partial functions can be viewed as composites of polynomial endofunctors, and how copartial functions can be viewed as pushout-products. I have not added the formalizations of these insights yet, but it is starting to look very interesting to pursue these remarks in a future pull request.

[fredrik-bakke]

Looks good to me!