notation

[Thierry Coquand]

I was told that the notation in my previous message may be confusing: I write

m_c : X -> D_c(X)

with X implicit argument.

With X explicit argument, the notation would be

m_c X : X -> D_c(X)

and condition of being idempotent is that D_c(m_c X) and m_c (D_c X) are
path equal.

Since D_c(X) = X^{F(c)} this can also be expressed as the fact that

X^{pi_1} and X^{pi_2} : X^{F(c)} -> X^{F(c) x F(c)}

are path equal (note that F(c) is not required to be fibrant).

Another way to state it as a proposition is that the multiplication of the monad

X^{diagonal} : X^{F(c) x F(c)} -> X^{F(c)}

is an equivalence.

Thierry