Let me elaborate a bit on my answer. One might naively try to copy Dan and Guillaume's definition and write the following in Cubical Agda:
Omega : (A : Type₀) → A → Type₀
Omega A a = (a ≡ a)
itOmega : ℕ → (A : Type₀) → A → Type₀
itOmega zero A a = Omega A a
itOmega (suc n) A a = itOmega n (Omega A a) refl
data Sn (n : ℕ) : Type₀ where
base : Sn n
surf : itOmega n (Sn n) base
However Agda will complain as surf is not constructing an element of Sn. This might seem a bit funny as Cubical Agda is perfectly happy with
data S³ : Type₀ where
base : S³
surf : Path (Path (base ≡ base) refl refl) refl refl
But what is happening under the hood is that surf is a constructor taking i, j, and k in the interval and returning an element of S^3 with boundary "base" whenever i, j and k are 0 or 1. In cubicaltt we can write this HIT in the following way:
data S3 = base
| surf <i j k> [ (i=0) -> base
, (i=1) -> base
, (j=0) -> base
, (j=1) -> base
, (k=0) -> base
, (k=1) -> base ]
The problem is then clearer: in order to write the surf constructor of Sn we would have to quantify over n interval variables and specify the boundary of the n-cell. This is what that is not supported by any of the cubical schemas for HITs.
--
Anders
On Wednesday, September 18, 2019 at 11:00:22 AM UTC+2, Guillaume Brunerie wrote:
Hi,
We give a definition of S^n with one point and one n-loop by
introduction/elimination/reduction rules in our paper with Dan Licata
(https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf), which can be
implemented in Agda (so Kristina’s question can be formulated and can
presumably be formalized in Agda) but I don’t think we actually proved
it.
Best,
Guillaume
Den ons 18 sep. 2019 kl 10:32 skrev Anders Mortberg <andersm...@gmail.com>:
>
> Hi Kristina,
>
> We have proofs for S^0, S^1, S^2 and S^3 in Cubical Agda:
> https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp/Base.agda
>
> However, I don't think we can even write down the general version of
> S^n as a type with a point and an n-loop with the schema implemented
> in Cubical Agda. As far as I know no other schema for HITs support
> this kind of types either.
>
> --
> Anders
>
> On Tue, Sep 17, 2019 at 9:56 PM Kristina Sojakova
> <sojakova...@gmail.com> wrote:
> >
> > Hello everybody,
> >
> > Is it worked out somewhere that the two definitions of Sn as a
> > suspension on one hand and a HIT with a point and an n-loop on the other
> > hand are equivalent? This is also an exercise in the book. I know
> > Favonia has some Agda code on spheres but I couldn't find this result in
> > there.
> >
> > Thanks,
> >
> > Kristina
> >
> >