%include verbatim.fmt
\begingroup
\let\origtt=\ttfamily
\let\small\scriptsize
\def\ttfamily#1#2{\origtt\makebox[0pt]{\phantom{X}}}

>%if style == newcode
>%format ^
>%format ^^    = " "
>%format ti(a) = "{|" a "|}"
>%format ki(a) = "{[" a "]}"
>%else
>%format ^     = " "
>%format ^^    = "\;"
>%format ti(a) = "\lty " a "\rty "
>%format ki(a) = "\lki " a "\rki "
>\newcommand{\lty}{\mathopen{\{\mskip-3.4mu||}}
>\newcommand{\rty}{\mathclose{||\mskip-3.4mu\}}}
>\newcommand{\lki}{\mathopen{\{\mskip-3.5mu[}}
>\newcommand{\rki}{\mathclose{]\mskip-3.5mu\}}}
>%format t1
>%format t2
>%format a1
>%format a2
>%format r_    = "\rho "
>%format s_    = "\sigma "
>%format k_    = "\kappa "
>%format forall a = "\forall " a
>%format .     = "."
>%format mapa  = map "_{" a "}"
>%format mapb  = map "_{" b "}"
>%format :*:   = "\times "
>%endif
>\begin{code}
>type Map^ki(*)         t1  t2       =   t1 -> t2
>type Map^ki(r_ -> s_)  t1  t2       =   forall a1 a2. Map^ki(r_) a1 a2 
>                                          -> Map^ki(s_) (t1 a1) (t2 a2)
>
>map^ti(t :: k_)                     ::  Map^ki(k_) t t
>map^ti(Unit)             Unit       =   Unit
>map^ti(Int)              i          =   i
>map^ti(Sum)   mapa mapb  (Inl  a)   =   Inl  (mapa a)
>map^ti(Sum)   mapa mapb  (Inr  b)   =   Inr  (mapb b)
>map^ti(Prod)  mapa mapb  (a :*: b)  =   mapa a :*: mapb b
>\end{code}

\endgroup