Unit Law Dirichlet Product [00E3]

Define by

Note that is a proposition (TODO: write out why) 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