Nice. I haven't seen this. But I have considered two similar things:
(1) The natural numbers defined by
0
2x+1
2x+2
This is not a HIT - just a normal inductive types.
(2) A HIT for the dyadics numbers D in the interval [0,1] with constructors
data 𝔹 : Type₀ where
L R : 𝔹 -- 0 and 1
l r : 𝔹 → 𝔹 -- x ↦ x/2 and x ↦ (x+1)/2
eqL : L ≡ l L -- 0 = 0/2
eqM : l R ≡ r L -- 1/2 = (0+1)/2
eqR : R ≡ r R -- 1 = (1+1)/2
Then, like your HIT, this is automatically a set without the need of
truncation. But I didn't find an simple proof of this. Together with
Alex Rice, we proved this by showing it to be equivalent to another type
which is easily seen to be a aset:
data 𝔻 : Type₀ where
middle : 𝔻
left : 𝔻 → 𝔻
right : 𝔻 → 𝔻
data 𝔹' : Type₀ where
L' : 𝔹'
R' : 𝔹'
η : 𝔻 → 𝔹'
l' : 𝔹' → 𝔹'
l' L' = L'
l' R' = η middle
l' (η x) = η (left x)
r' : 𝔹' → 𝔹'
r' L' = η middle
r' R' = R'
r' (η x) = η (right x)
eqL' : L' ≡ l' L'
eqM' : l' R' ≡ r' L'
eqR' : R' ≡ r' R'
eqL' = refl
eqM' = refl
eqR' = refl
Then the types 𝔹 and 𝔹' are equivalent, and clearly 𝔹' is a set
because it has decidable equality.
Moreover, the "binary systems" (𝔹,L,R,l,r,eqL,eqM,eqR) and
(𝔹',L',R',l',r',eqL',eqM',eqR') are isomorphic.
(And we implemented in this in Cubical Agda.)
I wonder if your definition of the integers with the HIT is isomorphic
to an inductively defined version without a HIT as above, and this is
how you proved it to be a set.
Martin