Initial algebra
$%S E$-algebra -- $|M = ( T_{%S}/=, %S/=)$
Properties
no junk
-- $ \A a : T_{%S}/= \E t \dot eval_{|M}(t) = a $
no confusion
-- $ |M |= t_1 = t_2 <=> E |- t_1 = t_2 $
slide
:
Initial models
