I'm still trying to figure out things around higher inductive type in the setting of the HoTT Book.
Setting
Given the definition of $\mathbb{S}^1$ as it is stated in the HoTT Book, i.e. $\mathbb{S}^1$ given by
- a base point $\mathsf{base} : \mathbb{S}^1$
- a path $\mathsf{loop} : \mathsf{base} = \mathsf{base}$
I consider path induction in $\mathbb{S}^1$. So, for example let $C : \Pi_{m,n:\mathbb{S}^1} m = n \to \mathcal{U}$ and I want to define a function $$ f : \Pi_{m,n:\mathbb{S}^1}\Pi_{p: m = n} C(m,n,p) $$ This is possible with path induction, i.e. by providing $$ f(m,m,\mathsf{refl}_m) :\equiv c_m : C(m,m,\mathsf{refl}_m) $$
Now, I assume I can define $c_m$ without going into induction on $m$ here. So $\mathsf{loop}$ is not considered anywhere.
Questions
Just to recheck: looking only at $\mathsf{refl}$ here is enough to define such function $f$?
But my central question is: What is $f(\mathsf{base},\mathsf{base},\mathsf{loop})$? Or rather: is there some general principle to claim properties about these functions acting on other paths then $\mathsf{refl}$? (This, not explicitly on $\mathbb{S}^1$.)
Yes, it's enough to deal with the case of $\mathsf{refl}$ to define $f$; that's what path induction says.
As for the value of $f(\sf base,base,loop)$, there's not going to be a very non-tautological answer in the general case. We can say that it's the result of transporting $c_{\sf base}$ along $\sf loop$, but that kind of begs the question because the operation of transport is also defined by path induction.
For specific type families $C$ obtained using the basic type formers, you can "compute" transport in terms of its action on the "pieces". This is described for each type former in chapter 2 of the HoTT Book, e.g. Theorems 2.6.4 and 2.7.4 and equation (2.9.4).
When you know something about the base type (in your case $\mathbb{S}^1$), you can sometimes also use that. For instance, it might be the case that $C:\mathbb{S}^1\to \mathcal{U}$ was defined by using the recursion principle of $\mathbb{S}^1$, giving a type $C(\sf base)$ and an equivalence $g: C({\sf base}) \simeq C(\sf base)$ to be the image of $\sf loop$ (applying univalence). In that case, your $f(\sf base,base,loop)$ will be $g(c_{\sf base})$.