Lemma. Unit Law Dirichlet Product [00E3]
Define
by
Note that
is a proposition (TODO: explain) so in particular a set.
Note also that this fits the definition of
in the paper quite well.
We prove that
by constructing for each
a map
and showing it has contractible fibers.
Proof. A term of type
is of the form
where
Note that
, so
contractible. We denote its center of contraction by
. We now define an equivalence
by
. Because
is contractible,
, so
is indeed an equivalence.
By univalence
gives us a path
Define
Now we show that the fibers of
are contracible:
Let
. Then the fiber is given by
Define
where
is the right unit equivalence and
is the identity.
Then
Pick
as the center.
We now show that given
, with
holds.
Observe, that using
(from
), we get that
.
this means we get an element
(that we also call
by abuse of notation)
We now use the the characterization of the Identity type of Dirichlet Product, so we only need to give a path
Thus we need
We already have have
. Define
by applying univalence to
. Set
. Note that
, which is contracible,so
It only reamains to construct
. (TODO: copy from Notebook II)