We explain Ahman and Uustalu's dependently typed update monad, give an imperfect algebraic presentation, and describe its comodels.