Defined container morphisms (natural transformations) and the free monad operation on containers.
Defined the Fin data type.
Copied Paolo's approach to HITs.