Perhaps I'm just not understanding how the definitions are actually supposed to work. In particular, the definition of $\mathbb{S}^{1}$ confuses me.
So first, we have $\text{base}:\mathbb{S}^{1}$ and $\text{loop}:\text{base}=\text{base}$
We also have $isProp(A):\equiv \prod_{x:A}\prod_{y:A}x=y$ and $isSet(A):\equiv \prod_{x:A}\prod_{y:A}\prod_{p:x=y}\prod_{q:x=y}p=q$
And it is taken for granted that for any $A$, $isProp(A)\rightarrow isSet(A)$, via path induction.
But $\text{base}$ is the only element of $\mathbb{S}^{1}$, so $isProp(\mathbb{S}^{1})$ is clearly inhabited, by either $\lambda x.\lambda y.\text{loop}$ or $\lambda x. \lambda y.\text{refl}_{\text{base}}$ or concatenations thereof. But because we have to assume $\text{loop}=\text{refl}_{\text{base}}$ is uninhabited, it's clear that $isSet(\mathbb{S}^{1})$ is, at best, a partial function, which I don't believe HoTT allows.
And that's only the start of the problems that I'm having trouble with. In general, it seems that the theory sets up rules for paths that are both expected to be adhered to and ignored at the same time. Can someone simplify this? Should I be assuming there are points in $\mathbb{S}^{1}$ that aren't $\text{base}$? Or is there another answer?
If $\mathsf{isProp}(\mathbb S^1)$ is "clearly inhabited", what's the inhabitant?
Let's try to write it. The induction principle for $\mathbb S^1$ is: given $P:\mathbb S^1\to\mathcal U$, $b : P(\mathsf{base})$, and $\ell : \mathsf{transport}^P(\mathsf{loop}, b)=b$ where $\mathsf{transport}^P(p,-):P(x)\to P(y)$ given $p : x=y$ there is a $f:\prod_{x:\mathbb S^1}P(x)$ such that $f(\mathsf{base})=b$ and $\mathsf{apd}_f(\mathsf{loop})=\ell$.
It's pretty clear that we will need to use this induction principle with $P(x):\equiv\prod_{y:\mathbb S^1}(x=y)$ to show $\mathsf{isProp}(\mathbb S^1)$. We need to then produce a value of type $P(\mathsf{base})$, i.e. $\prod_{y:\mathbb S^1}(\mathsf{base}=y)$.
Again, it is pretty clear that we will need to use the induction principle. This time with $P'(y):\equiv(\mathsf{base}=y)$. Again, we need $P'(\mathsf{base})$, i.e. $\mathsf{base}=\mathsf{base}$. Easy enough, we can pick $\mathsf{refl}_{\mathsf{base}}$ or $\mathsf{loop}$ (or $\mathsf{loop}\centerdot\mathsf{loop}$, etc.), call this $p$. But to apply the induction principle, we also need an $\ell:\mathsf{transport}^{P'}(\mathsf{loop},p)=p$. Generally, we have $\mathsf{transport}^{\lambda y.x=y}(p,q) = q\centerdot p$, so $\mathsf{transport}^{P'}(\mathsf{loop},p)=p$ is asking for $p\centerdot\mathsf{loop}=p$. There are no values of this type though. If $p\equiv\mathsf{refl}_{\mathsf{base}}$, then this is just asking for $\mathsf{loop}=\mathsf{refl}_{\mathsf{base}}$ which is explicitly not true, and if $p\equiv\mathsf{loop}$, then we have $\mathsf{loop}\centerdot\mathsf{loop}=\mathsf{loop}$ which also isn't true.
$\mathbb S^1$ is more than just a point. Indeed, it is the $\mathsf{loop}$ part of $\mathbb{S}^1$ that is the important part. $\mathsf{base}$ is only there so we can talk about $\mathsf{loop}$. A value of type $\prod_{x:\mathbb S^1}P(x)$ doesn't just send points to points, it sends paths to paths. This is the homotopical aspect of Homotopy Type Theory. From a logical perspective, $f:\prod_{x:\mathbb S^1}P(x)$ doesn't only need to map points to points, it needs to preserve equivalences between those points (and equivalences between the equivalences and so on).