Setting
Currently I try to formulate the simply typed $\lambda$-calculus in HoTT which results in quite involved inductive type families. Since I'm still new, I'm often unsure if my induction principles are stated correctly.
Important is, since I'm still learning, I need an answer according to the HoTT Book, the stricter the better. Thanks a lot!
Example
Okay, this type might not catch any greater idea, it's just a pile of syntax. Let $A$ be any dummy type here. Then I want to consider the inductive type family $T : A \to \mathcal{U}$ given by
- $e : \Pi_{\Delta : A} T(\Delta)$
- $\_[\_] : \Pi_{\Delta : A} T(\Delta) \to \mathsf{List}(T(\Delta)) \to T(\Delta)$
as point and
- $\mathsf{re} : \Pi_{\Delta : A}\Pi_{\delta : T(\Delta)}\Pi_{l : \mathsf{List}(T(\Delta))} e[(\delta,l)] = \delta$ in $T(\Delta)$
as path constructors where $(\delta,l)$ appends $\delta$ to the list $l$.
The induction principle therefore: To define a function $f : \Pi_{\Delta : A} \Pi_{T(\Delta)} C(\Delta,T(\Delta))$ one needs
- $c_e : \Pi_{\Delta : A} C(\Delta, e)$
- $c_s : \Pi_{\Delta : A} \Pi_{m : T(\Delta)} \Pi_{l : \mathsf{List}(T(\Delta))} C(\Delta, m) \to C(\Delta,m[l])$
as well as a path over $\mathsf{re}$:
- $p : \Pi_{\Delta : A}\Pi_{l:\mathsf{List}(T(\Delta))}\Pi_{\delta:T(\Delta)}\Pi_{c_\delta : C(\Delta,\delta)} \;\;\;c_s(\Delta,e,(\delta,l),c_e(\Delta)) =_{\mathsf{re}}^{C(\Delta)} c_\delta$
which then yields
\begin{align*} f(\Delta,e) &:\equiv c_e(\Delta)\\ f(\Delta,m[l]) &:\equiv c_s(\Delta,m,l,f(\Delta,m))\\ \mathsf{apd}_f(\mathsf{re}) &:= p \end{align*}
Questions
So, the most important question at first: Is this induction principle stated correctly, especially the dependent path?
And as a broader, more subjective question: If you use HoTT in a "working" manner, on paper then type setting it: How do you deal with big inductive definitions while working (in)formally in HoTT? Some of my definitions are made up out of 6 or more paths on 5 or so constructors, making not only the induction principle but especially proofs utilizing these quite a pain (even more so in when typing it in LaTeX).