Problem 1.2.1 (pg. 38) of Categorical logic from a categorical point of view by Michael Shulman (readable here) asks the following;
Let M be a fixed category; then we have an induced adjunction between Cat/M and Gr/M. Describe a cut-free type theory for presenting the free category-over-M on a directed-graph-over-M, and prove the initiality theorem (the analogue of Theorem 1.2.13). Note that you will have to prove that cut is admissible first. (Hint: index the judgments by arrows in M, so that for instance A ⊢α B represents an arrow lying over a given arrow α in M.)
I've been thinking about this problem for a few days, and I'm not making a lot of progress. I don't imagine that proving initiality or cut-admissibility will be hard, so I'm not asking about that. I just want to know what this type theory is supposed to look like.
This question has several followups in the book, for example Exercise 1.3.9 on pg. 46. This gives enough hints for me to guess what id probably looks like, but it's not clear to me what the composition rule is supposed to look like, and that indexing confuses me.
I've seen over-categories used in type theories before, such as discussions of inductive datatypes, but I haven't seen judgements be indexed by morphisms, and I don't know what "arrow lying over a given arrow" even means.
Any clarification would be helpful. Thank you.
Edit:
I think I may have figured it out.
Given some graph $\mathscr{G}$ with a functor $F : \mathscr{G} \to \mathscr{M}$, we can state the following analog of $id$.
$\cfrac{A \in \mathscr{G}}{x : A \vdash_{id_{F(A)}} x : A}$
Furthermore, given some edge in $\mathscr{G}$, we can derive the following rule for composition;
$\cfrac{x : X \vdash_{g : F(X) \to F(A)} M : A \ \ \ \ \ \ \ \ \ \ \ \ f \in \mathscr{G}(A,B)}{x : X \vdash_{F(f) \circ g : F(X) \to F(B)} f(M) : B}$
To answer part of the original question, I will prove cut-admissibility. We can do this by simple induction. We do an induction on proofs. If the proof is by $id$, then it is already cut-free. If it ends in some edge application, then by the inductive hypothesis the proof preceding the application is cut-free. If our proof ends in the cut-rule then it is of the form;
$\cfrac{A \vdash_{f} C \ \ \ \ \ \ \ \ \ \ \ \ C \vdash_{g} B}{A \vdash_{g \circ f} B}$
in which case, we can replace the cut with an application;
$\cfrac{A \vdash_{f} C}{A \vdash_{g \circ f} B}$
and by the inductive hypothesis, the rest of the proof leading to this end can have cuts removed as well. This proves that cut is admissible.
Looking at followup questions in the book, it seems to me that this answer lines up nicely with what is expected, and the exercise is intended to prepare one for the concept of a fibration. I'm still not 100% confident that this is the right answer, but it seems so.