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.

  • 1
    $\begingroup$ 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$ May 14 at 15:15
  • $\begingroup$ @PeterLeFanuLumsdaine I'm interested in using double categories for first order logical theories. Induction for natural numbers is a simple case compared to the axiom of induction for sets. But yeah the natural numbers object should be set like definitely. $\endgroup$ May 14 at 15:27
  • 2
    $\begingroup$ Right, but what are specific examples of double categories+NNO you have in mind, that you want the general definition to capture? E.g. am I understanding right that you’re thinking of $\mathbb{N}$ in the double category of sets with functions as horizontal arrows and relations/spans as vertical arrows? $\endgroup$ May 14 at 15:57
  • 1
    $\begingroup$ @PeterLeFanuLumsdaine yeah that's the kind of double category I'm most interested in. I'm slightly interested in Prof like categories for other reasons but rn I just want to understand the simple cases of Rel and Span like categories. There's some nonsense with categories of displayed categories I want to mess around with as well but again simple things first. $\endgroup$ May 14 at 18:50


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.