In Coq a loose approximation to the free monad over a polynomial endofunctor might be.
Polymorphic Cumulative Record Poly := {
pos: Type ;
dir: pos -> Type ;
}.
Inductive free (p: Poly) A :=
| pure (v: A)
| roll x (p: dir p x -> free p A).
A monad in the bicategory of spans in Set is a category. Loosely the free category of an endospan is something like:
Polymorphic Cumulative Record span A B := {
s: Type ;
p1: s -> A ;
p2: s -> B ;
}.
Arguments p1 {A B}.
Arguments p2 {A B}.
Inductive free {Obj} (p: span Obj Obj): Obj -> Obj -> Type :=
| id A: free p A A
| compose {A B C}: free p B C -> free p A B -> free p A C
| op x: free p (p1 p x) (p2 p x)
.
I'm having trouble untangling what the free indexed category of an endospan should be.
An endospan in a slice category $\text{Set}/\Gamma$ indexed over a set kind of makes sense. But maybe there is a more natural definition?
I'm not quite sure how to interpret the equivalent of a slice category for spans. I know comma categories are sort of like pullbacks. A straightforward reinterpretation of a slice as for some object $x$ a map between a constant span and the identity span on $x$ seems very quirky though.
$$ \text{Obj}/\Gamma = \Sigma \, (x: \text{Obj}) , \; \text{id}_x \Rightarrow \, ! \Gamma $$
A more involved idea is to make $\text{Obj}$ a category and then look at the free monad of an indexed two sided discrete fibration $\text{Obj}/\Gamma \rightarrow \text{Obj}/\Gamma^{\text{op}}$. You get this weird profunctor equivalent of a free monad but I find this really confusing.