Translating the induction principle from verbal form into rigorous one According to the HoTT book [6.9], the propositional truncation $||A||$ of a type $A$ can be viewed as a higher inductive type generated by

*

*A map $|-|: A \to ||A||$

*A path in $x = y$ for any $x,y: ||A||.$
Then the recursion principle, it says, gives that with a type $B$ provided with

*

*A map $A \to B$

*A path in $x = y$ for any $x,y: B,$
there is a map $||A|| \to B$ such that [something]. But this is not what I expected. Why would one require that all points of $B$ are equal? For instance, when constructing a map from an interval, one only needs a path between images of its endpoints. But here for some reason 1-dimensional conditions are imposed on $B$ with no regard to how the points of $A$ are mapped to $B$.
The second constructor for $||A||$ seems to be $\prod\limits_{x,y:||A||} x = y.$ Then [waves hands fiercely] the domain already has the type being defined in it, so it is like $\mathbb{N} \to \mathbb{N},$ and $\mathbb{N}$ is initial among $B$ with a map $B \to B.$ Similarly $||A||$ has to be initial among objects with two maps of the form above. However, not only that this is vague, but it is also not entirely clear how to correctly write the case of the interval this way and how should the difference be clear from the verbal descriptions given.
What is the right way to approach this? What is the uniform way to write these definitions rigorously?
 A: There's not just one way to approach this, but here are some ideas that may help.
Informally, the point of $\Vert A \Vert$ is to be something like the proposition freely generated by $A$. The elimination principle you mention is just writing that explicitly. Every map $A → B$ where $B$ is a proposition factors through $\Vert A \Vert$. The condition you kind of don't like is "$B$ is a proposition."
For how to generally formalize this stuff, I think the cubical approach can make some angles a little easier to think about. The syntax in cubical Agda looks like this:
data ∥_∥ (A : Type) : Type where
  |_| : A → ∥ A ∥
  squash : (x y : ∥ A ∥) → x ≡ y

(An underscore between symbols is the prefix name corresponding to a circumfix notation.) However, when you go to write a definition by cases on $\Vert A \Vert$, these are the cases:
f : ∥ A ∥ → B
f | x | = ...
f (squash x y i) = ...

Notice that squash has 3 arguments, the third being a dimension variable. This is because in the cubical formalism, $x \equiv y$ is kind of like $\mathbb I → A$, where $\mathbb I$ is a special not-quite-type, and the function is known to take the value $x$ at $0$ and $y$ at $1$. So, the higher constructors can be explained in this setting as being like normal constructors with additional dimension arguments, and reduce to other constructors for certain values of those dimension arguments. And eliminations require you give values for those formal intermediate points which reduce in a corresponding way to the values given in other cases. Some papers on higher inductive types in cubical type theory actually present the types entirely in terms of 'points' with reduction rules, but Agda uses a notation more like the HoTT book.
Now, you are actually correct that the eliminator you cited doesn't exactly cover all possibilities. You can eliminate into types $B$ that are not propositions. This paper explains the details. The details are not simple, though. Here is the Agda code for eliminating from propositional truncation into a set and a groupoid.
Essentially, the function $A → B$ needs to be constant up to higher dimensional structure in $B$. But, there doesn't appear to be any way to characterize the appropriate notion of constancy in e.g. book HoTT unless $B$ has a finite dimension. Even then, it gets complicated pretty fast. In the case where $B$ is a proposition, every function is constant in the appropriate sense, which makes that the simplest eliminator to give. If $B$ is a set, then it suffices to give a path between values in the image of $f$. If $B$ is a groupoid, then you need to give coherences on those paths. Etc.
If you're wondering why this is more complicated than the interval, say:
data Interval : Type where
  zero one : Interval
  seg : zero ≡ one

The way I'd describe it is that the interval is constructed in a 'smarter' way. There are two base points, and a path is added where there otherwise wouldn't be one, to make the type contractible. This isn't what truncation does, because it cannot do that in general. Note that squash adds paths between all points, including, say, intermediate points in lower dimensional squash paths. So, there is formal structure 'all the way up', but the added formal structure ends up collapsing the topological structure. But this means that we can't actually formally specify an elimination unless we act in a formally uniform way above some dimension (which is what $B$ having finite dimension accomplishes), or extend the theory with a way to essentially give a definition by arbitrarily many cases.
A: To put this a little bit differently: your discussion of the second constructor is exactly the reason for the second requirement on $B$.  The way to make this precise is that a higher inductive type is determined by a certain kind of schema or functor involving a type variable $X$, which in this case is $F(X) = (A\to X) \times (\prod_{x,y:X} x=y)$.  Then the type being defined, here $\Vert A \Vert$ is the initial type equipped with an element of $F(X)$, hence has a universal property with respect to other types $B$ equipped with elements of $F(B)$.
If one defines an "interval" as $\Vert 2\Vert$, then indeed the resulting universal property for it would only map it into other propositions.  It's true that there is a different definition of an "interval", as generated by two points and a single path between them, that has a more general universal property.  However, as Dan points out, it's not immediately clear how that alternative definition of an interval could be generalized to a definition of $\Vert A\Vert$ for arbitrary $A$.
It's not enough to use something like $F(X) = (q:A\to X) \times (\prod_{x,y:A} qx=qy)$ (note the difference in domain of the second constructor), since the HIT generated thereby will not in general even be a proposition itself.  This HIT is the homotopy coequalizer of the two projections $A\times A \rightrightarrows A$, and for instance if $A=1$ this coequalizer is $S^1$.  It is correct if we add an additional set-trucation constructor, but this then only has a universal property for mapping into sets.
Kraus's paper The General Universal Property of the Propositional Truncation cited by Dan is one approach to this problem: he shows that by adding additional constructors one can incrementally increase the assumed truncation level of $B$.  Another approach is Rijke's The join construction, which gives a construction of $\Vert A\Vert$ in terms of pushouts and sequential colimits, thereby giving it a universal property of a sort for mapping into any type (no truncation hypotheses at all).  However, I have not yet seen these universal properties used for $B$ any higher than 1-truncated in practice, as they get increasingly intricate.
