Typefified FSM Version of core relies on inductive definitions

[FabrizioRomanoGenovese]

In FSM core, we provide instructions to build a path category for a FSM (call it C), together with a list of edges that we want to verify making a path in C.

At the moment we are doing so by relying on the fact that C, being a path category, has paths as morphisms. As such, we are relying on the inductive definition of path do work things out.

This approach will not generalize to other categories. For instance, in the hypergraph case we won't be able to do anything of this sort since we don't have an inductive data structure representing string diagrams.

So we need to develop a technique to tackle this more general problem:
Given a category C, and a list of morphisms for C, verify if you can lift this list to a valid morphism in C

For instance, if C has objects a, b, c, ... then [f: Mor a b, g: Mor b c] can be lifted to a valid morphism compose C a b c f g, while [f: Mor a b, g: Mor x y] cannot.