### Welcome to the JsCoq/JsHoTT Interactive Online System!

Welcome to the JsCoq technology demo! This page requires Chrome
>= 48 or Firefox >= 45.

#### Instructions:

**Alt-Enter** (Cmd should work in Macs too) goes to
the current point; **Alt-N/P** or **Alt-Down/Up** will
move through the proof; **F8** or the power icon toogles
the goal panel.

#### Setting up the environment:

We will first load the HoTT libraries and do a proof from the library.

### Theorems about the circle [S1].

#### Definition of the circle:

We define the circle as the coequalizer of two copies of the
identity map of [Unit]. This is easily equivalent to the naive
definition:

Private Inductive S1 : Type1 :=
| base : S1
| loop : base = base.

but it allows us to apply the flattening lemma directly rather than having
to pass across that equivalence.

But we want to allow the user to forget that we've defined the circle
in that way.

#### The non-dependent eliminator

#### The loop space of the circle is the Integers.

We use encode-decode.

#### Cool!

Once the basic enviroment has been setup, we can write, share,
and run Coq programs and proofs.