I've been playing with double categories. I'm having trouble figuring out appropriate laws for induction squares in a double category.

Assume an object $\mathbb{N}$.

Assume horizontal arrows

- zero $0\colon 1 \rightarrow \mathbb{N}$
- successor $\text{S}\colon\mathbb{N} \rightarrow \mathbb{N}$

Then for all vertical arrows $P\colon\mathbb{N} \nrightarrow \mathbb{N}$ you want an induction principle/relator

$$ \text{u}\colon \begin{split} & 0 & \\ \text{id} & \Rightarrow &P \\ & 0 & \end{split}\rightarrow \begin{split} & \text{S}& \\ P & \Rightarrow &P \\ & \text{S} & \end{split}\rightarrow \begin{split} &\text{id}&\\ \text{id} & \Rightarrow & P\\ &\text{id}& \end{split}$$

But I have trouble with figuring out appropriate laws for how the 2-cells compose.

I think classically you can get away with something similar to the category of relations where squares are just truth values but I think constructively you really want something like the category of spans where squares carry information.

What example(s) are you trying to abstract from?E.g. the question “axiomatise disjoint unions in a category” could lead either to “coproduct” if you’re thinking of them in categories like Set, or “product” if you’re thinking of them in categories like Rel. We usually think of the former, just because our default examples are things like Set and concrete categories over it — but with double categories, it’s less clear what the “default” examples your trying to generalise from would be. $\endgroup$