%include poly.fmt
%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}