Consider the (putative) higher inductive type $\mathtt{PNest}$, with the constructors:
- $\mathtt{base} : \mathtt{PNest}$
- $\mathtt{nest} : \mathtt{base} = \mathtt{base} \to \mathtt{base} = \mathtt{base}$
Firstly, is this actually a valid HIT? I feel like it should be, but I know that the HoTT book says that path constructors taking other paths as parameters are "somewhat fishy," so I'm not sure if my intuition holds.
Secondly, if it is a valid HIT, what does its path structure look like? I've been trying to figure this out on my own, but I'm no closer to an answer than when I started. How does the path space $\mathtt{base} = \mathtt{base}$ behave? Is $\mathtt{PNest}$ contractible, equivalent to $\mathbb{S}^1$, or something more complicated? Even some pointers on what direction to look would be greatly appreciated!
EDIT: In pursuit of the direction suggested by @ZhenLin's comment about "the free 'group with an endomap,'" is there a way to connect the type $\mathtt{base} = \mathtt{base}$ to a defined type that produces that structure explicitly?