Lemma [efr-CZUI]

In \mathsf {Set}, the free iterable midpoint algebra on two generators 0,1 is [0,1]. That is, given an iterable midpoint algebra A and two points a_0, a_1, there exists a unique midpoint homomorphism f: [0,1] \to A so that f(0)=a_0, f(1)=a_1.

Context