Model of the circle without HITs While playing around with HoTT, I came across a type "$C$" which seems a lot like $S^1$:
$$
C \equiv \Pi_{A:U} \Pi_{x:A} (x=x\rightarrow A)
$$
It has values
$$
\begin{align}
\text{base}C &: C   \\
\text{base}C &\equiv \lambda A. \lambda x. \lambda p. x \\
\text{loop}C &: \text{base}C = \text{base}C \\
\text{loop}C &\equiv \text{funext}\,\lambda A. \text{funext}\,\lambda x.  \text{funext}\, \lambda p. p
\end{align}
$$
And I've implemented functions:
$$
\begin{align}
\text{to-}S^1 &: C \rightarrow S^1 \\
\text{from-}S^1 &: S^1 \rightarrow C
\end{align}
$$
such that
$$
\begin{align}
\text{to-}S^1 \, \text{base}C &= \text{base} \\
\text{ap} \, \text{to-}S^1 \, \text{loop}C &= \text{loop} \\
\text{from-}S^1 \, \text{base} &= \text{base}C \\
\text{ap} \, \text{from-}S^1 \, \text{loop} &= \text{loop}C
\end{align}
$$
So far it sure looks like an isomorphism.  However when I try to write an equivalence $C \simeq S^1$ I get hopelessly stuck proving $\text{to-}S^1 \circ \text{from-}S^1 = \text{id}_{S^1}$ and vice versa.  I thought maybe I could write the circle's elimination principle for $C$ to help, but I have no idea how to approach that either.  It seems like I need some sort of parametricity theorem (which is probably not possible).
So I'm asking for guidance.


*

*Is $C$ actually equivalent to $S^1$?


*

*If so, what do I need to prove it?  

*If not, what would a counterexample look like?  And are there any types in MLTT + Univalence (i.e. HoTT without HITs) that are equivalent to $S^1$?


 A: It looks like you've (re)discovered the impredicative encoding of (higher) inductive types.  In general, this produces a type that has the same constructors and non-dependent "recursion" principle as the desired inductive type, but lacks the dependent "induction" principle and hence cannot be proven equivalent to it.
Your intuition about parametricity is basically right: in "classical" models that violate parametricity, your type $C$ is inhabited by wacky things that don't correspond to anything in $S^1$.  Excluded middle allows us to define functions of the sort $\prod_{A:U}$ by saying "if $A$ is equivalent to $X$, do $Y$, otherwise to $Z$" for some fixed type $X$.  So, for instance, under LEM there is an inhabitant of your $C$ that acts like $\mathsf{loop}$ if $A$ is equivalent to $S^1$ but like $\mathsf{loop}^2$ otherwise.
There is sort of a way to fix this: add a "naturality" condition to the definition of $C$, saying that if a map $A\to A'$ preserves the specified loops then it also preserves the induced maps out of $C$.  If there is no restriction on homotopy level of types, then this naturality requires arbitrarily higher coherences as well, which we don't know how to represent in the finite syntax of type theory (the "problem of infinite objects").  But if there is a global restriction on homotopy level, you may be able to make it work.  I'm not sure whether this is written down yet in a HoTT context; I know that Steve Awodey and Andrej Bauer have worked on it in the context of a realizability model, where one has "true" impredicativity that quantifies over $A:U$ but produces an element of $U$, rather than the next higher universe as would happen in ordinary MLTT.  (This universe level-increasing is in general another problem with such impredicative definitions.)
At least if you're willing to admit propositional truncation into your type theory, then there are other ways to define a circle, such as the type of $\mathbb{Z}$-torsors.  I know that that produces an object that's equivalent to the HIT $S^1$ if the latter exists; I don't know whether it is possible to prove that it satisfies the induction principle of $S^1$ if we don't already have an $S^1$.
