How to define morphism equivalence

[Lysxia]

Right now eq2 for Basics.Function is defined as extensional equality (pointwise_relation _ eq). However eq2 for ktree is defined as pointwise_relation _ (eutt eq), and that's a bit of a mismatch we need to address to be able to formalize that ktree is a Kleisli category of Basics.Function.Fun. (The same issue arises for Indexed.IFun vs Handler.)

Extensional equality for Fun is definitely too restrictive, and instead the domains and codomains of functions should come equipped with equivalence relations (maybe partial), so Fun is really a category of setoids (or possibly PERs).

A natural answer then is to change the type of objects of Fun to be records { T : Type ; eqT : T -> T -> Prop ; (* eqT is an equivalence relation *) }. But this will make Basics.Function so much more complicated, and I expect it will be a pain to program with.

So far we have also been pretty successful with keeping a separation between programs and proofs. In particular, the program side hardly makes any mention of equivalence (and with a bit of work we should be able to totally remove the rest, we just haven't had a motivation to do so yet). The main benefits are:

• There is a general principle that proofs should be irrelevant (I don't mean the axiom here, just the general idea). They are erased during extraction, but it seems even simpler if they do not appear in programs in the first place.

• This should remove one need for proof irrelevance as an axiom. It can still crop up in other ways when reasoning about dependently typed programs, but that's a different issue. (see #72)

• Once in a while we run into universe inconsistencies; the separation can delay them a bit.

So I've been thinking of ways to add the required structure on objects purely on the proof side. I have this schema to redefine eq2 but haven't gotten to try it yet:

(* Morphism in the category of functions. That's all you need to write programs with. *)
Fun : Type -> Type -> Type := fun a b => (a -> b).

(* But for proofs, we need to make explicit equivalence relations for a and b. *)
EQ : forall a : Type, a -> a -> Prop.
eq2 : forall a b : Type, EQ a -> EQ b -> Fun a b -> Fun a b -> Prop.

[gmalecha]

One thing that will arise is whether you require EQ to be reflexive, or only reflexive on certain "good" elements. This is basically the complexity that got Monad generalized into PMonad in ExtLib.

[Lysxia]

Surprisingly, I can't even make the generalized eq2 an equivalence relation no matter what restrictions I make on EQ. When generalizing from plain functions (with extensional equality) to functions between setoids (or PERs or whatever), we really want to restrict the set of functions to those that preserve relations between their domain and codomain. I can only see two places to add those "respectfulness" constraints, neither seems very promising or even feasible:

1. either in the type of functions, making them sigma types;
2. or add them as assumptions in morphism equivalence lemmas.

The main reason for doing all that is to formalize the result that itree is a monad in the category-theoretical sense, to establish a concrete relation between the category of functions and the category of ktrees. Now it seems that cannot be done without significantly complicating our definition of categories and the usability of the library: we cannot even state the fact that itree is an endofunctor (except if we consider only strong bisimulation with the axiom which identifies it with propositional equality, but we are really using weak bisimulation everywhere).

A more productive avenue is probably to only work in ktree, and reformulate results about monads to not mention monads.

[Lysxia]

We only need this if we are to formalize the categorical definition of monads, which so far we don't.