Add instances for rig categories

[ricky136973]

Introduce Sets and PartialFunctions as rig categories.

[JacquesCarette]

Very nice! I want to explore some potential changes. But while I say 'Request changes', what I really mean is "let's discuss the design some more". This is definitely a great contribution.

[JacquesCarette]

we've used very little with in agda-categories up until now. It's fragile. I do realize that for dealing with partial functions, it is a powerful tool.

What I'm wondering is if the "pattern of reasoning" going on here could be abstracted out and used here?

[ricky136973]

I tried to pull the with-clauses out into a where-block, but Agda cannot infer the type of the helper functions if I do not provide the lengthy type signature explicitly.

[JacquesCarette]

here I definitely would like to see this kind of reasoning abstracted out!

[ricky136973]

Similar cases happened to the previous case. The more elegant way could have been like

PM⊗ .unitorˡ-commute-from {f = f} (lift tt , x) =
  maybe {B = λ fx → ?} (erefl ∘ just) refl (f x)

but Agda cannot infer B, and the explicit form of it is just as lengthy as in the previous case.

[TOTBWF]

I'd maybe rename PartialFunctions to something else. In constructive foundations, A -> Maybe B describes partial functions whose domain of definition has decidable membership.

[ricky136973]

I'd maybe rename PartialFunctions to something else. In constructive foundations, A -> Maybe B describes partial functions whose domain of definition has decidable membership.

I know the more general notion of "partial functions" is $\sum_{P:X\to\Omega}(\sum_{x:X}P(x))\to Y$, and that's also the encoding used in 1lab. I still named it as PartialFunctions only because there is already a module Categories.Category.Instance.PartialFunctions defining the maybe-functions as a category, and I believe it is better to maintain some sort of consistency of naming here.

[JacquesCarette]

I agree that consistency is very important. In the absence of other forces, I would always let consistency win.

In this case: I agree with @TOTBWF that this is a bad name. So I would like to find a better name -- and then I will change Categories.Category.Instance.PartialFunctions accordingly.

[ricky136973]

I agree that consistency is very important. In the absence of other forces, I would always let consistency win.

In this case: I agree with @TOTBWF that this is a bad name. So I would like to find a better name -- and then I will change Categories.Category.Instance.PartialFunctions accordingly.

Name suggestion: MaybeFunction. DecidablePartialFunction is too long, Maybe is ambiguous.