notation

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