ITT.tex

\documentclass{article}
\usepackage[utf8x]{inputenc}
\usepackage{t1enc}

\usepackage{fullpage}
\usepackage{amssymb}
\usepackage{url}
\usepackage{color}
\usepackage{amsmath}

\newcommand{\seqr}[3]
  {\shortstack{$#2$ \\ \mbox{}\\
                   \mbox{}\hrulefill\mbox{}\\ \mbox{}\\ $#3$} \; \raisebox{2.5ex}{$\;\mbox{$#1$}$}}
\newcommand{\Sub}[3]{#1[#3/#2]}
\newcommand{\defeq}{\triangleq}

\newcommand{\Type}{\mathsf{Type}}
\newcommand{\Set}{\mathsf{Set}}
\newcommand{\Prop}{\mathsf{Prop}}

\newcommand{\refl}[1]{\mathsf{refl}\,{#1}}
\newcommand{\subst}[2]{\mathsf{subst}\,{#1}\,\mathsf{in}\,{#2}}
\newcommand{\mkeq}[3]{{#1} =_{#2} {#3}}

\newcommand{\mkprod}[3]{\Pi {#1}\!:\!{#2}.\,{#3}}
\newcommand{\mkimp}[2]{{#1}\rightarrow{#2}}
\newcommand{\mklam}[3]{\lambda {#1}\!:\!{#2}.\,{#3}}
\newcommand{\mkapp}[2]{{#1}\,{#2}}
\newcommand{\prodsort}[2]{\Pi ({#1},{#2})}

\newcommand{\mksig}[3]{\Sigma {#1}\!:\!{#2}.\,{#3}}
\newcommand{\mkpair}[2]{\langle{#1},{#2}\rangle}
\newcommand{\mkfst}[1]{{#1}.1}
\newcommand{\mksnd}[1]{{#1}.2}
\newcommand{\sigsort}[2]{\Sigma ({#1},{#2})}

\newcommand{\sortsort}[1]{{\cal S}_{#1}}

\newcommand{\zero}{0}
\newcommand{\natsucc}[1]{\mathsf{succ}\,{#1}}
\newcommand{\rec}[5]{\mathsf{rec}\,[\zero\, \mapsto\, #1\,|\,\natsucc{#2}\, \mapsto_{#3}\, {#4}]\,{#5}}
\newcommand{\nat}{\mathbb{N}}
\newcommand{\natsort}{l_{\nat}}

\newcommand{\headname}{\mathsf{hd}}
\newcommand{\tailname}{\mathsf{tl}}
\newcommand{\streamname}{\mathsf{Stream}}
\newcommand{\head}[1]{\headname\,{#1}}
\newcommand{\tail}[1]{\tailname\,{#1}}
\newcommand{\mkstream}[5]{\{\headname \mapsto {#2}; \tailname \mapsto_{#3} {#4}\}_{#1}{#5}}
\newcommand{\stream}[1]{\streamname\,{#1}}

\newcommand{\Sone}{\mathbb{S}^1}
\newcommand{\casesone}[5]
  {\mathsf{case}\;{#1}\;\mathsf{of}\;{#2}\;\Rightarrow\;{#3}\;|\;{#4}\;\Rightarrow\;{#5}\;\mathsf{end}}
\newcommand{\base}{\mathsf{base}}
\newcommand{\loopsone}{\mathsf{loop}}
\newcommand{\Sonesort}{l_{\mathbb{S}^1}}

\newcommand{\case}[2]{\mathsf{case}\;{#1}\;\mathsf{of}\;{#2}}

\newcommand{\sort}[1]{\mathsf{U}_{#1}}

\newcommand{\reduce}{\;\triangleright\;}

\newcommand{\emptyctx}{\Box}
\newcommand{\wfctx}[1]{{#1}~\mathsf{wf}}

\newcommand{\sortrule}{\sort{}}
\newcommand{\axrule}{\mathsf{Ax}}
\newcommand{\ctxemptyrule}{\mathsf{Ctx}_{\emptyctx}}
\newcommand{\ctxconsrule}{\mathsf{Ctx}_{\mathsf{cons}}}
\newcommand{\convrule}{\mathsf{Conv}}
\newcommand{\redconvrule}{\mathsf{Conv}_{\reduce}}
\newcommand{\reflconvrule}{\mathsf{Refl}_{\equiv}}
\newcommand{\symconvrule}{\mathsf{Sym}_{\equiv}}
\newcommand{\transconvrule}{\mathsf{Trans}_{\equiv}}

\newcommand{\sigeta}{\eta_{\Sigma}}
\newcommand{\sigbeta}{\beta_{\Sigma}}
\newcommand{\prodeta}{\eta_{\Pi}}
\newcommand{\prodbeta}{\beta_{\Pi}}
\newcommand{\nateta}{\eta_{\nat}}
\newcommand{\natbeta}{\beta_{\nat}}
\newcommand{\streambeta}{\beta_{\streamname}}
\newcommand{\streameta}{\eta_{\streamname}}
\newcommand{\poseta}{\eta_{\mathit{pos}}}
\newcommand{\posbeta}{\beta_{\mathit{pos}}}
\newcommand{\negeta}{\eta_{\mathit{neg}}}
\newcommand{\negbeta}{\beta_{\mathit{neg}}}
\newcommand{\receta}{\eta_{\mathit{\mu}}}
\newcommand{\recbeta}{\beta_{\mathit{\mu}}}
\newcommand{\coreceta}{\eta_{\mathit{\nu}}}
\newcommand{\corecbeta}{\beta_{\mathit{\nu}}}

\begin{document}

\title{Martin-Löf's type theory}

\author{Hugo Herbelin and Nicolas Tabareau}

\maketitle

\section{Core type theory}

The core infrastructure of type theory is presented on Figure~\ref{fig:coretypetheory}.

\begin{figure*}
\centerline{\framebox{$
\begin{array}{c}
  \begin{array}{ccc}
\mbox{\em syntax of contexts} & & \mbox{\em syntax of expressions}
\\
\\
  \begin{array}{ccc}
\Gamma & ::= & \emptyctx ~|~ \Gamma, a:A
  \end{array}
&&
  \begin{array}{cccl}
t, u, A, B & ::= & a ~|~ \sort{l}\\
  \end{array}
\\
\\
&& \mbox{where $a$ ranges over a set of variables}\\
&& \mbox{and $l$ ranges over a set of universe levels}\\
\\
\mbox{\em context formers} & \qquad & \mbox{\em axiom}\\
&& \\
&& \\
\seqr{\ctxemptyrule}
     {}
     {\wfctx{\emptyctx}}
\qquad
\seqr{\ctxconsrule}
     {\Gamma \vdash A : \sort{l}}
     {\wfctx{\Gamma, a : A}}
&& \seqr{\axrule}
     {\wfctx{\Gamma, a:A, \Gamma'}}
     {\Gamma, a:A, \Gamma' \vdash a : A}
  \end{array}
\\
\\
\mbox{\em conversion rule}
\\
\\
\seqr{\convrule}
     {\Gamma \vdash t : A \qquad \Gamma \vdash A \equiv B : \sort{l}}
     {\Gamma \vdash t : B}
\\
\\
\mbox{\em definitional equality}
\\
\\
\seqr{\redconvrule}
     {\Gamma \vdash t \reduce u : A}
     {\Gamma \vdash t \equiv u : A}
\\
\\
\seqr{\reflconvrule}
     {\Gamma \vdash t : A}
     {\Gamma \vdash t \equiv t : A}
\qquad
\seqr{\symconvrule}
     {\Gamma \vdash t \equiv u : A}
     {\Gamma \vdash u \equiv t : A}
\qquad
\seqr{\transconvrule}
     {\Gamma \vdash t \equiv u : A \qquad \Gamma \vdash u \equiv v : A}
     {\Gamma \vdash t \equiv v : A}
\end{array}
$
}}
\caption{Core structure of type theory}
\label{fig:coretypetheory}
\end{figure*}

\section{Universes}

Extension with a hierarchy of universe is obtained with the rules on Figure~\ref{fig:univtypetheory}.

\begin{figure*}
\centerline{ \framebox{$
\begin{array}{c}
\mbox{\em type former}
\\
\\
\seqr{\sortrule}
     {}
     {\Gamma \vdash \sort{l} : \sort{\sortsort{l}}}
\end{array}
$
}}
\caption{Universes in type theory}
\label{fig:univtypetheory}
\end{figure*}

\section{Identity type}

Extension with an identity type is obtained with the rules on Figure~\ref{fig:idtypetheory}.

\begin{figure*}
\centerline{\framebox{$
\begin{array}{c}
\mbox{\em extended syntax of expressions}
\\
\\
  \begin{array}{cccl}
t, u, v, A, B, p, q & ::= & \ldots ~|~ \mkeq{t}{A}{u} ~|~ \refl{t} ~|~ \subst{p}{v}
  \end{array}
\\
\\
\mbox{\em type former}
\\
\\
\seqr{}
     {\Gamma \vdash t : A \qquad \Gamma \vdash u : A}
     {\Gamma \vdash \mkeq{t}{A}{u} : \sort{l}}
\\
\\
  \begin{array}{ccc}
\mbox{\em introduction rule} &\qquad& \mbox{\em elimination rule}\\
\\
\\
\seqr{}
     {\Gamma \vdash t : A}
     {\Gamma \vdash \refl{t} : \mkeq{t}{A}{t}}
&&
\seqr{}
     {\Gamma \vdash p : \mkeq{t}{A}{u} \qquad \Gamma, a : A, b : \mkeq{t}{A}{a} \vdash P : \sort{l} \qquad \Gamma \vdash v : \Sub{\Sub{P}{a}{t}}{b}{\refl{t}}}
     {\Gamma \vdash \subst{p}{v} : \Sub{\Sub{P}{a}{u}}{b}{p}}
  \end{array}
\\
\\
\mbox{\em reduction rule}
\\
\\
\seqr{}
     {\Gamma \vdash t : A \qquad \Gamma, a : A, b : \mkeq{t}{A}{a} \vdash B : \sort{l} \qquad \Gamma \vdash v : \Sub{\Sub{B}{a}{t}}{b}{\refl{t}}}
     {\Gamma \vdash \subst{\refl{t}}{v} \reduce v : \Sub{\Sub{B}{a}{t}}{b}{\refl{t}}}
\\
\\
\mbox{\em congruence rules}
\\
\\
\seqr{}
     {\Gamma \vdash A \equiv A' \qquad \Gamma \vdash t \equiv t' : A \qquad \Gamma \vdash u \equiv u' : A}
     {\Gamma \vdash (\mkeq{t}{A}{u}) \equiv (\mkeq{t'}{A'}{u'}) : \sort{l}}
\\
\\
\seqr{}
     {\Gamma \vdash t \equiv t' : A}
     {\Gamma \vdash \refl{t} \equiv \refl{t'} : \mkeq{t}{A}{t}}
\qquad
\seqr{}
     {\Gamma \vdash p \equiv p' : \mkeq{t}{A}{u} \qquad \Gamma, a : A, q : \mkeq{t}{A}{a} \vdash B : \sort{l} \qquad \Gamma \vdash v \equiv v' : \Sub{\Sub{B}{a}{t}}{q}{\refl{t}}}
     {\Gamma \vdash \subst{p}{v} \equiv \subst{p'}{v'} : \Sub{\Sub{B}{a}{u}}{q}{p}}
\end{array}
$
}}
\caption{Identity type}
\label{fig:idtypetheory}
\end{figure*}

\section{Dependent function type}

Extension with a dependent function type is obtained with the rules on
Figure~\ref{fig:prodtypetheory}. One assumes given a function
$\prodsort{l_1}{l_2}$ on universe levels. We shall occasionally use the following syntactic abbreviations:
$$
\begin{array}{lcll}
A \rightarrow B & \defeq & \mkprod{a}{A}{B} & \mbox{for $a$ fresh variable}\\
A \Rightarrow B & \defeq & \mkprod{a}{A}{B} & \mbox{for $a$ fresh variable}\\
\forall a:A. B & \defeq & \mkprod{a}{A}{B}\\
\end{array}
$$

\begin{figure*}
\centerline{ \framebox{$
\begin{array}{c}
\mbox{\em extended syntax of expressions}
\\
\\
  \begin{array}{cccl}
t, u, v, A, B, p, q & ::= & \ldots ~|~ \mkprod{a}{A}{B} ~|~ \mklam{a}{A}{u} ~|~ \mkapp{v}{t}\\
  \end{array}
\\
\\
\mbox{\em type former}
\\
\\
\seqr{}
     {\Gamma \vdash A : \sort{l_1} \qquad \Gamma, a : A \vdash B : \sort{l_2}}
     {\Gamma \vdash \mkprod{a}{A}{B} : \sort{\prodsort{l_1}{l_2}}}
\\
\\
  \begin{array}{ccc}
\mbox{\em introduction rule} &\qquad& \mbox{\em elimination rule}
\\
\\
\seqr{}
     {\Gamma, a : A \vdash u : B}
     {\Gamma \vdash \mklam{a}{A}{u} : \mkprod{a}{A}{B}}
&&
\seqr{}
     {\Gamma \vdash v : \mkprod{a}{A}{B} \qquad \Gamma \vdash t : A}
     {\Gamma \vdash \mkapp{v}{t} : \Sub{B}{a}{t}}
\\
\\
\mbox{\em reduction rule} &\qquad& \mbox{\em observational rule}
\\
\\
\seqr{\prodbeta}
     {\Gamma, a : A \vdash u : B \qquad \Gamma \vdash t : A}
     {\Gamma \vdash \mkapp{(\mklam{a}{A}{u})}{t} \reduce \Sub{u}{a}{t} : \Sub{B}{a}{t}}
&&
\seqr{\prodeta}
     {\Gamma \vdash v : \mkprod{a}{A}{B}}
     {\Gamma \vdash \mklam{a}{A}{\mkapp{v}{a}} \reduce v : \mkprod{a}{A}{B}}
  \end{array}
\\
\\
\mbox{\em congruence rules}
\\
\\
\seqr{}
     {\Gamma \vdash A \equiv A' : \sort{l_1} \qquad \Gamma, a : A \vdash B \equiv B' : \sort{l_2}}
     {\Gamma \vdash \mkprod{a}{A}{B} \equiv \mkprod{a}{A'}{B'} : \sort{\prodsort{l_1}{l_2}}}
\\
\\
\seqr{}
     {\Gamma \vdash A \equiv A' : \sort{l} \qquad \Gamma, a : A \vdash u \equiv u' : B}
     {\Gamma \vdash \mklam{a}{A}{u} \equiv \mklam{a}{A'}{u'} : \mkprod{a}{A}{B}}
\\
\\
\seqr{}
     {\Gamma \vdash v \equiv v' : \mkprod{a}{A}{B} \qquad \Gamma \vdash t \equiv t' : A}
     {\Gamma \vdash \mkapp{v}{t} \equiv \mkapp{v'}{t'} : \Sub{B}{a}{t}}
\end{array}
$
}}
\caption{Typing and computational rules for $\Pi$}
\label{fig:prodtypetheory}
\end{figure*}

\section{Dependent sum type}

Extension with a dependent sum type is obtained with the rules on
Figure~\ref{fig:sigmatypetheory}. One assumes given a function
$\sigsort{l_1}{l_2}$ on universe levels. We shall occasionally use
the following syntactic abbreviations:
$$
\begin{array}{lcll}
A \times B & \defeq & \mksig{a}{A}{B} & \mbox{for $a$ fresh variable}\\
A \wedge B & \defeq & \mksig{a}{A}{B} & \mbox{for $a$ fresh variable}\\
\exists a:A. B & \defeq & \mksig{a}{A}{B}\\
\end{array}
$$

\begin{figure*}
\centerline{\framebox{$
\begin{array}{c}
\mbox{\em extended syntax of expressions}
\\
\\
  \begin{array}{cccl}
t, u, v, A, B, p, q & ::= & \ldots ~|~ \mksig{a}{A}{B} ~|~ \mkpair{t}{u} ~|~ \mkfst{v} ~|~ \mksnd{v}\\
  \end{array}
\\
\\
\mbox{\em type former}
\\
\\
\seqr{}
     {\Gamma \vdash A : \sort{l_1} \qquad \Gamma, a : A \vdash B : \sort{l_2}}
     {\Gamma \vdash \mksig{a}{A}{B} : \sort{\sigsort{l_1}{l_2}}}
\\
\\
  \begin{array}{ccc}
\mbox{\em introduction rule} &\qquad& \mbox{\em elimination rules}
\\
\\
\seqr{}
     {\Gamma \vdash t : A \qquad \Gamma \vdash u : \Sub{B}{a}{t}}
     {\Gamma \vdash \mkpair{t}{u} : \mksig{a}{A}{B}}
&&
\seqr{}
     {\Gamma \vdash v : \mksig{a}{A}{B}}
     {\Gamma \vdash \mkfst{v} : A}
\qquad
\seqr{}
     {\Gamma \vdash v : \mksig{a}{A}{B}}
     {\Gamma \vdash \mksnd{v} : \Sub{B}{a}{\mkfst{v}}}
\\
\\
\mbox{\em reduction rules} &\qquad& \mbox{\em observational rule}
\\
\\
\seqr{\sigbeta^1}
     {\Gamma \vdash t : A \qquad \Gamma \vdash u : \Sub{B}{a}{t}}
     {\Gamma \vdash \mkfst{(\mkpair{t}{u})} \reduce t : A}
\qquad
\seqr{\sigbeta^2}
     {\Gamma \vdash t : A \qquad \Gamma \vdash u : \Sub{B}{a}{t}}
     {\Gamma \vdash \mksnd{(\mkpair{t}{u})} \reduce u : \Sub{B}{a}{t}}
&&
\seqr{\sigeta}
     {\Gamma \vdash v : \mksig{a}{A}{B}}
     {\Gamma \vdash \mkpair{\mkfst{v}}{\mksnd{v}} \reduce v : \mksig{a}{A}{B}}
  \end{array}
\\
\\
\mbox{\em congruence rules}
\\
\\
\seqr{}
     {\Gamma \vdash A \equiv A' : \sort{l_1} \qquad \Gamma, a : A \vdash B \equiv B' : \sort{l_2}}
     {\Gamma \vdash \mksig{a}{A}{B} \equiv \mksig{a}{A'}{B'} : \sort{\sigsort{l_1}{l_2}}}
\\
\\
\seqr{}
     {\Gamma \vdash t \equiv t' : A \qquad \Gamma, a : A \vdash u \equiv u' : B}
     {\Gamma \vdash \mkpair{t}{u} \equiv \mkpair{t'}{u'} : \mksig{a}{A}{B}}
\\
\\
\seqr{}
     {\Gamma \vdash v \equiv v' : \mksig{a}{A}{B}}
     {\Gamma \vdash \mkfst{v} \equiv \mkfst{v'} : A}
\qquad
\seqr{}
     {\Gamma \vdash v \equiv v' : \mksig{a}{A}{B}}
     {\Gamma \vdash \mksnd{v} \equiv \mksnd{v'} : \Sub{B}{a}{\mkfst{v}}}
\end{array}
$
}}
\caption{Typing and computational rules for $\Sigma$}
\label{fig:sigmatypetheory}
\end{figure*}

\section{Natural numbers}

Extension with Peano natural numbers is obtained with the rules on
Figure~\ref{fig:nattypetheory}.  One assumes given a universe level
$\natsort$ where $\nat$ lives.

\begin{figure*}
\centerline{\framebox{$
\begin{array}{c}
\mbox{\em extended syntax of expressions}
\\
\\
  \begin{array}{cccl}
t, u, v, A, B, p, q & ::= & \ldots ~|~ \nat ~|~ \zero ~|~ \natsucc{t} ~|~ \rec{t}{a}{b}{u}{v} \\
  \end{array}
\\
\\
\mbox{\em type former}
\\
\\
\seqr{}
     {}
     {\Gamma \vdash \nat : \sort{\natsort}}
\\
\\
\mbox{\em introduction rules}
\\
\\
\seqr{}
     {}
     {\Gamma \vdash \zero : \nat}
\qquad
\seqr{}
     {\Gamma \vdash t : \nat}
     {\Gamma \vdash \natsucc{t} : \nat}
\\
\\
\mbox{\em elimination rule}
\\
\\
\seqr{}
     {\Gamma, a : \nat \vdash B : \sort{l} \qquad \Gamma \vdash t : \Sub{B}{a}{\zero} \qquad \Gamma, a : \nat, b : \Sub{B}{a}{n} \vdash u : \Sub{B}{a}{\natsucc{n}} \qquad \Gamma \vdash v : \nat}
     {\Gamma \vdash \rec{t}{a}{b}{u}{v} : \Sub{B}{a}{v}}
\\
\\
\mbox{\em reduction rules}
\\
\\
\seqr{\natbeta^{\zero}}
     {\Gamma, a : \nat \vdash B : \sort{l} \qquad \Gamma \vdash t : \Sub{B}{a}{\zero} \qquad \Gamma, a : \nat, b : \Sub{B}{a}{n} \vdash u : \Sub{B}{a}{\natsucc{n}}}
     {\Gamma \vdash \rec{t}{a}{b}{u}{\zero} \reduce t : \Sub{B}{a}{\zero}}
\\
\\
\seqr{\natbeta^{\natsucc{}}}
     {\Gamma, a : \nat \vdash B : \sort{l} \qquad \Gamma \vdash t : \Sub{B}{a}{\zero} \qquad \Gamma, a : \nat, b : \Sub{B}{a}{n} \vdash u : \Sub{B}{a}{\natsucc{n}} \qquad \Gamma \vdash v : \nat}
     {\Gamma \vdash \rec{t}{a}{b}{u}{\natsucc{v}} \reduce \Sub{\Sub{u}{a}{v}}{b}{\rec{t}{a}{b}{u}{v}} : \Sub{B}{a}{\natsucc{v}}}
\\
\\
\mbox{\em observational rule}
\\
\\
\seqr{\nateta}
     {\Gamma, a : \nat \vdash E[a] : A \qquad \Gamma \vdash v : \nat}
     {\Gamma \vdash \rec{E[\zero]}{a}{b}{E[\natsucc{a}]}{v} \reduce E[v] : A}
\\
\\
\mbox{where $E[a]$ is made only from elimination rules applied to $a$}
\\
\\
\mbox{\em congruence rules}
\\
\\
\seqr{}
     {\Gamma \vdash t \equiv t' : \nat}
     {\Gamma \vdash \natsucc{t} \equiv \natsucc{t'} : \nat}
\\
\\
\seqr{}
     {\Gamma \vdash t \equiv t' : \Sub{B}{a}{\zero} \qquad \Gamma, a : \nat, b : \Sub{B}{a}{n} \vdash u \equiv u' : \Sub{B}{a}{\natsucc{n}} \qquad \Gamma \vdash v \equiv v' : \nat}
     {\Gamma \vdash \rec{t}{a}{b}{u}{v} \equiv \rec{t'}{a}{b}{u'}{v'} : \Sub{B}{a}{v}}
\end{array}
$
}}
\caption{Typing and computational rules for $\nat$}
\label{fig:nattypetheory}
\end{figure*}

\section{Streams}

Extension with streams (infinite lists) is obtained with the rules on
Figure~\ref{fig:streamtypetheory}.

\begin{figure*}
\centerline{\framebox{$
\begin{array}{c}
\mbox{\em extended syntax of expressions}
\\
\\
  \begin{array}{cccl}
t, u, v, A, B, p, q & ::= & \ldots ~|~ \stream{A} ~|~ \head{t} ~|~ \tail{t} ~|~ \mkstream{c}{t}{s}{u}{v} \\
  \end{array}
\\
\\
\mbox{\em type former}
\\
\\
\seqr{}
     {\Gamma \vdash A : \sort{l}}
     {\Gamma \vdash \stream{A} : \sort{l}}
\\
\\
\mbox{\em introduction rule}
\\
\\
\seqr{}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma, c : C \vdash t : A \qquad \Gamma, s : \mkimp{C}{\stream{A}}, c : C \vdash u : \stream{A} \qquad \Gamma \vdash v : C}
     {\Gamma \vdash \mkstream{c}{t}{s}{u}{v} : \stream{\Sub{A}{c}{v}}}
\\
\\
\mbox{\em elimination rules}
\\
\\
\seqr{}
     {\Gamma \vdash A : \sort{l} \qquad \Gamma \vdash t : \stream{A}}
     {\Gamma \vdash \head{t} : A}
\qquad
\seqr{}
     {\Gamma \vdash A : \sort{l} \qquad \Gamma \vdash t : \stream{A}}
     {\Gamma \vdash \tail{t} : \stream{}}
\\
\\
\mbox{\em reduction rules}
\\
\\
\seqr{\streambeta^{\headname}}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma, c : C \vdash t : A \qquad \Gamma, s : \mkimp{C}{\stream{A}}, c : C \vdash u : \stream{A} \qquad \Gamma \vdash v : C}
     {\Gamma \vdash \head{\mkstream{c}{t}{s}{u}{v}} \reduce \Sub{t}{c}{v} : \Sub{A}{c}{v}}
\\
\\
\seqr{\streambeta^{\tailname}}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma, c : C \vdash t : A \qquad \Gamma, s : \mkimp{C}{\stream{A}}, c : C \vdash u : \stream{A} \qquad \Gamma \vdash v : C}
     {\Gamma \vdash \tail{\mkstream{c}{t}{s}{u}{v}} \reduce \Sub{\Sub{u}{c}{v}}{s\,x}{\mkstream{c}{t}{s}{u}{x}} : \stream{A}}
\\
\\
\mbox{\em observational rule}
\\
\\
\seqr{\streameta}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma, a : C \vdash t : \stream{A}}
     {\Gamma \vdash \mkstream{a}{\head{t}}{s}{\tail{t}}{a} \equiv t : \stream{A}}
\\
\\
\mbox{\em congruence rules}
\\
\\
\seqr{}
     {\Gamma \vdash A \equiv A' : \sort{l}}
     {\Gamma \vdash \stream{A} \equiv \stream{A'} : \sort{l}}
\qquad
\seqr{}
     {\Gamma \vdash t \equiv t' : \stream{A}}
     {\Gamma \vdash \head{t} \equiv \head{t'} : A}
\qquad
\seqr{}
     {\Gamma \vdash t \equiv t' : \stream{A}}
     {\Gamma \vdash \tail{t} \equiv \tail{t'} : A}
\\
\\
\seqr{}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma \vdash t \equiv t' : A \qquad \Gamma, s : \mkimp{C}{\stream{A}}, c : C \vdash u \equiv u' : \stream{A} \qquad \Gamma \vdash v \equiv v' : C}
     {\Gamma \vdash \mkstream{c}{t}{s}{u}{v} \equiv \mkstream{c}{t'}{s}{u'}{v'} : \stream{A}}
\end{array}
$
}}
\caption{Typing and computational rules for streams}
\label{fig:streamtypetheory}
\end{figure*}

\section{Generic positive types}

\newcommand{\mkpostype}[4]{#1^{#3}_{#2:#4}}
\newcommand{\vdashpos}{\vdash_{\mathit P}}
\newcommand{\vdashposinh}{\vdash_{\mathit p}}
\newcommand{\vdashpospat}{\vdash_{\mathit pat}}

We give a syntax for arbitrary forms of (non-recursive) positive type,
as a (non-recursive) generalization of the type $\nat$. For that
purpose, we introduce a couple of auxiliary structures.

We introduce a class of positive types,
denoted by the letter $P$ and we reuse for that purpose the notation
$\otimes$ of linear logic, but this time in a dependent form (i.e. the
type on the right can depend on the inhabitant of the type of the
left), and in an intuitionistic setting (i.e. with contraction and
weakening allowed).

We introduce a class $w$ of inhabitants of such positive types and a
class $\rho$ of patterns for matching inhabitants of such positive
types. These patterns can be declared in the context.

A positive type has the form $\mkpostype{(c_1 : P_1 \oplus ... \oplus c_n :
P_n)}{\rho}{w}{P}$ where $w$ are the parameters of the type and the $c_i$ are
the names of constructors (assumed all distinct).

A constructor of this type has the form $c_i\,w$. A destructor has the
form $\case{t}{[ c_1 \rho \mapsto t | ... | c_n \rho \mapsto t ]}$.

Substitution of $\rho$ by $w$ is as expected. Note that the axiom rule
needs to be generalized so as to extract variables of a pattern.

\begin{figure*}
\vspace{-2cm}
\centerline{\framebox{$
\begin{array}{c}
\mbox{\em extended syntax of expressions}
\\
\\
  \begin{array}{lcll}
t, u, v, A, B, p, q & ::= & \ldots  ~|~ \mkpostype{(c_1 : P \oplus ... \oplus c_n : P)}{\rho}{w}{P} ~|~ \case{t}{[ c_1 \rho \mapsto t | ... | c_n \rho \mapsto t ]} ~|~ c_i w\\
P & ::= & 1 ~|~ (a:A) \otimes P\\
w & ::= & () ~|~ (t,w)\\
\rho & ::= & () ~|~ (a,\rho)\\
\Gamma & ::= & ... ~|~ \rho : P\\
  \end{array}
\\
\\
\mbox{\em type formers}
\\
\\
\seqr{}
     {}
     {\Gamma \vdashpos 1 : \sort{l}}
\qquad
\seqr{}
     {\Gamma \vdash A : \sort{l} \qquad \Gamma, a : A \vdashpos P : \sort{l}}
     {\Gamma \vdashpos (a : A) \otimes P : \sort{l}}
\qquad
\seqr{}
     {\Gamma \vdashpos P : \sort{l} \qquad \Gamma, \rho : P \vdashpos P_i : \sort{l} \quad (1 \leq i \leq n) \qquad \Gamma \vdash w : P \qquad \mbox{names $d_i$ disjoint}}
     {\Gamma \vdash \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho}{w}{P} : \sort{l}}
\\
\\
\begin{array}{ccc}
\mbox{\em typing rules for instances} & & \mbox{\em typing rules for patterns}
\\
\\
\seqr{}
     {}
     {\Gamma \vdashposinh () : 1}
\qquad
\seqr{}
     {\Gamma \vdash t : A \qquad \Gamma \vdashposinh w : \Sub{P}{a}{t}}
     {\Gamma \vdashposinh (t,w) : (a:A) \otimes P}
&\qquad&
\seqr{}
     {}
     {\Gamma \vdashpospat () : 1}
\qquad
\seqr{}
     {\Gamma \vdash A : \sort{l} \qquad \Gamma, a : A \vdashpospat \rho : P}
     {\Gamma \vdashpospat (a,\rho) : (a:A) \otimes P}
\qquad
\seqr{}
     {\wfctx{\Gamma} \qquad \Gamma \vdashpospat \rho : P}
     {\wfctx{\Gamma, \rho : P}}
\end{array}
\\
\\
\mbox{\em introduction rules}
\\
\\
\seqr{(1 \leq i \leq n)}
     {\Gamma \vdash w' : P \qquad \Gamma, \rho : P \vdash P_j : \sort{l} \quad (1 \leq j \leq n) \qquad \Gamma \vdash w : \Sub{P_i}{\rho}{w'}}
     {\Gamma \vdash c_i w : \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho}{w'}{P}}
\\
\\
\mbox{\em elimination rule}
\\
\\
\seqr{}
     {\Gamma \vdash v : \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho}{w}{P} \qquad \Gamma, a : \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho}{w}{P} \vdash B : \sort{l} \qquad \Gamma, \rho : \Sub{P_i}{\rho}{w} \vdash t_i : \Sub{B}{a}{c_i\,\rho} \quad (1 \leq i \leq n)}
     {\Gamma \vdash \case{v}{[ c_1 \rho \mapsto t_1 | ... | c_n \rho \mapsto t_n ]} : \Sub{B}{a}{v}}
\\
\\
\mbox{\em reduction rules}
\\
\\
\seqr{\posbeta^{i}}
     {\begin{array}{l}
      \Gamma \vdashpos P : \sort{l} \qquad \Gamma, \rho' : P \vdashpos P_i : \sort{l} \quad (1 \leq i \leq n) \qquad \Gamma \vdash w' : P \qquad \mbox{$d_i$ disjoint}\\
      \Gamma, a : \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho}{w'}{P'} \vdash B : \sort{l} \qquad \Gamma, \rho : \Sub{P_i}{\rho'}{w'} \vdash t_i : \Sub{B}{a}{c_i\,\rho} \quad (1 \leq i \leq n) \qquad \Gamma \vdashposinh w : \Sub{P_i}{\rho'}{w'}\\
      \end{array}}
     {\Gamma \vdash \case{c_i\,w}{[ c_1 \rho \mapsto t_1 | ... | c_n \rho \mapsto t_n ]} \reduce \Sub{t_i}{\rho}{w} : \Sub{B}{a}{c_i\,w}}
\\
\\
\mbox{\em observational rule}
\\
\\
\seqr{\poseta}
     {\Gamma \vdash v : \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho}{w}{P} \qquad \Gamma, a : \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho}{w}{P} \vdash E[a] : A}
     {\Gamma \vdash \case{v}{[ c_1 \rho \mapsto E[c_1\,\rho] | ... | c_n \rho \mapsto E[c_n\,\rho] ]} \reduce E[v] : \Sub{B}{a}{v}}
\\
\\
\mbox{where $E[a]$ is made only from elimination rules applied to $a$}
\\
\\
\mbox{\em congruence rules}
\\
\\
\seqr{}
     {\Gamma \vdash P \equiv P' : \sort{l} \qquad \Gamma, \rho : P \vdash P_i \equiv P_i' : \sort{l} \quad (1 \leq i \leq n) \qquad \Gamma \vdash w \equiv w' : P}
     {\Gamma \vdash \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho}{w}{P} \equiv \mkpostype{(c_1 : P'_1 \oplus ... \oplus c_n : P'_n)}{\rho}{w'}{P'} : \sort{l}}
\\
\\
\seqr{}
     {\Gamma \vdash P : \sort{l} \qquad \Gamma, \rho : P \vdash P_i : \sort{l} \quad (1 \leq i \leq n) \qquad \Gamma \vdash w'' : P \qquad \Gamma \vdash w \equiv w' : \Sub{P_i}{\rho}{w''}}
     {\Gamma \vdash c_i\,w \equiv c_i\,w' : \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho}{w''}{P}}
\\
\\
\seqr{}
     {\Gamma \vdash v \equiv v' : \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho'}{w}{P} \qquad \Gamma, a : \mkpostype{(c_1 : P_1 \oplus ... \oplus c_n : P_n)}{\rho'}{w}{P} \vdash B : \sort{l} \qquad \Gamma, \rho : \Sub{P_i}{\rho'}{w} \vdash t_i \equiv t'_i : \Sub{B}{a}{c_i\,\rho} \quad (1 \leq i \leq n)}
     {\Gamma \vdash \case{v}{[ c_1 \rho \mapsto t_1 | ... | c_n \rho \mapsto t_n ]} \equiv \case{v'}{[ c_1 \rho \mapsto t'_1 | ... | c_n \rho \mapsto t'_n ]} : \Sub{B}{a}{v}}
\\
\\
\mbox{+ judgemental equality and congruence rules for $\Gamma \vdash w : P$}
\end{array}
$
}}
\caption{General typing and computational rules for positive types}
\label{fig:positivetypetheory}
\end{figure*}

\section{Generic negative types}

\newcommand{\mknegtype}[4]{\{ #1 \}^{#3}_{#2:#4}}
\newcommand{\mkneg}[3]{\{ #1 \}_{#2}^{#3}}
\newcommand{\destructor}[2]{#1\,#2}
\newcommand{\vdashneg}{\vdash_{\mathit N}}

We give a syntax for arbitrary forms of (non-recursive) negative type,
as a (non-recursive) generalization of the type $\stream{A}$.

A negative type has the form $\mknegtype{d_1 : A \,\&\, ... \,\&\, d_n :
  A}{\rho}{w}{P}$ where $w$ are the parameters of the type and the
$d_i$ are the names of destructors (assumed all distinct). A
constructor of this type has the form $\mkneg{d_1 \mapsto t ; ... ;
  d_n \mapsto t}{c}{v}$. A destructor has the form $\destructor{t}$.

\begin{figure*}
\centerline{\framebox{$
\begin{array}{c}
\mbox{\em extended syntax of expressions}
\\
\\
  \begin{array}{lcll}
t, u, v, A, B, p, q & ::= & \ldots ~|~ \mknegtype{d_1 : N \,\&\, ... \,\&\, d_n : N}{\rho}{w}{P} ~|~ \mkneg{d_1 \mapsto t ; ... ; d_n \mapsto t}{c}{v} ~|~ \destructor{d_i}{t}\\
N & ::= & A ~|~ \mkprod{a}{A}{N} \qquad \mbox{(i.e. a distinguished subset of the grammar of terms)}\\
  \end{array}
\\
\\
\mbox{\em type formers}
\\
\\
\seqr{}
     {\Gamma \vdashposinh w : P \qquad \Gamma, \rho : P \vdash N_i : \sort{l} \quad (1 \leq i \leq n) \qquad \mbox{names $d_i$ disjoint}}
     {\Gamma \vdash \mknegtype{d_1 : N_1 \,\&\, ... \,\&\, d_n : N_n}{\rho}{w}{P}}
\\
\\
\mbox{\em introduction rule}
\\
\\
\seqr{}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma \vdashposinh w : P \qquad \Gamma, \rho : P \vdash N_i : \sort{l} \quad (1 \leq i \leq n) \qquad \Gamma, c : C \vdash t_i : \Sub{N_i}{\rho}{w} \quad (1 \leq i \leq n) \qquad \Gamma \vdash v : C}
     {\Gamma \vdash \mkneg{d_1 \mapsto t_1 ; ... ; d_n \mapsto t_n}{c}{v} : \mknegtype{d_1 : N_1 \,\&\, ... \,\&\, d_n : N_n}{\rho}{w}{P}}
\\
\\
\mbox{\em elimination rules}
\\
\\
\seqr{(1 \leq i \leq n)}
     {\Gamma \vdash t : \mknegtype{d_1 : N_1 \,\&\, ... \,\&\, d_n : N_n}{\rho}{w}{P}}
     {\Gamma \vdash \destructor{d_i}{t} : \Sub{N_i}{\rho}{w}}
\\
\\
\mbox{\em reduction rules}
\\
\\
\seqr{\negbeta^{i}}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma \vdashposinh w : P \qquad \Gamma, \rho : P \vdash N_i : \sort{l} \quad (1 \leq i \leq n) \qquad \Gamma, c : C \vdash t_i : \Sub{N_i}{\rho}{w} \quad (1 \leq i \leq n) \qquad \Gamma \vdash v : C}
     {\Gamma \vdash \destructor{d_i}{\mkneg{d_1 \mapsto t_1 ; ... ; d_n \mapsto t_n}{c}{v}} \reduce \Sub{t_i}{c}{v} : \Sub{N_i}{\rho}{w}}
\\
\\
\mbox{\em observational rule}
\\
\\
\seqr{\negeta}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma, c : C \vdash t : \mknegtype{d_1 : N_1 \,\&\, ... \,\&\, d_n : N_n}{\rho}{w}{P}}
     {\Gamma \vdash \mkneg{d_1 \mapsto \destructor{d_i}{t}; ... ; d_n \mapsto \destructor{d_n}{t}}{c}{c} \reduce t : \mknegtype{d_1 : N_1 \,\&\, ... \,\&\, d_n : N_n}{\rho}{w}{P}}
\\
\\
\mbox{\em congruence rules}
\\
\\
\seqr{}
     {\Gamma \vdashposinh w \equiv w' : P \qquad \Gamma, \rho : P \vdash N_i \equiv N_i' : \sort{l} \quad (1 \leq i \leq n) \qquad \Gamma \vdash P \equiv P' : \sort{l}}
     {\Gamma \vdash \mknegtype{d_1 : N_1 \,\&\, ... \,\&\, d_n : N_n}{\rho}{w}{P} \equiv \mknegtype{d_1 : N'_1 \,\&\, ... \,\&\, d_n : N'_n}{w'}{P'} : \sort{l}}
\\
\\
\seqr{}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma \vdashposinh w : P \qquad \Gamma, \rho : P \vdash N_i : \sort{l} \quad (1 \leq i \leq n) \qquad \Gamma, c : C \vdash t_i \equiv t_i' : \Sub{N_i}{\rho}{w} \quad (1 \leq i \leq n) \qquad \Gamma \vdash v \equiv v' : C}
     {\Gamma \vdash \mkneg{d_1 \mapsto t_1; ... ; d_n \mapsto t_n}{c}{v} \equiv \mkneg{d_1 \mapsto t'_1; ... ; d_n \mapsto t'_n}{c}{v'} : \mknegtype{d_1 : N_1 \,\&\, ... \,\&\, d_n : N_n}{\rho}{w}{P}}
\\
\\
\seqr{}
     {\Gamma \vdash t \equiv t' : \mknegtype{d_1 : N_1 \,\&\, ... \,\&\, d_n : N_n}{\rho}{w}{P}}
     {\Gamma \vdash \destructor{d_i}{t} \equiv \destructor{d_i}{t'} : \Sub{N_i}{\rho}{w}}
\end{array}
$
}}
\caption{General typing and computational rules for negative types}
\label{fig:negativetypetheory}
\end{figure*}

\section{Recursive types}

\newcommand{\inmu}[1]{\mathsf{enter}\,#1}
\newcommand{\appmu}[4]{\mathsf{fix\,}{#1}\,[\mathsf{enter}\,{#3}\,\mapsto\,{#2}]\,\mathsf{in}\,{#1}\,{#4}}

We give a syntax for recursive types, i.e. for types defined as
smallest type generated by its constructors. Recursion is expected to
occur only in {\em strictly positive} position, as e.g. in $\mu X.(1
\oplus X)$ (which is isomorphic to $\nat$) or $\mu X.(1 \oplus A
\otimes X)_{A:=\nat}$ (which denotes the type of lists of natural
numbers), or $\mu X.\{\headname : \nat \,\&\, \tailname : (1 \oplus X)\}$ (which
denotes the negative presentation of lists).

We restricted the rules to the case of recursion on a variable
$X:\sort{l}$. This could be extended to mutual recursion on a tuple of
type variable. This could be extended as well to a recursion on
arities, i.e. on variables $X$ of type
$\mkprod{a_1}{A_1}{...\mkprod{a_n}{A_n}{\sort{l}}}$ (in which case,
one would also provide an instance for the arity).

The property of $x$ guarded from $a$ in $t$ informally means that the
recursive call $x$ can be applied to an element of $\mu X. A$ which
comes by steps of destruction of $a$ without ever using $\inmu{}$.

Note that the observational rule is one among other variants.

\begin{figure*}
\centerline{\framebox{$
\begin{array}{c}
\mbox{\em extended syntax of expressions}
\\
\\
  \begin{array}{lcll}
t, u, v, A, B, p, q & ::= & \ldots ~|~ \mu X.A ~|~ \inmu{t} ~|~ \appmu{f}{t}{a}{t}\\
P & ::= & \ldots ~|~ (a:X) \otimes P\\
N & ::= & \ldots ~|~ X\\
  \end{array}
\\
\\
\mbox{\em type former}
\\
\\
\seqr{}
     {\Gamma, X : \sort{l} \vdash A : \sort{l} \qquad \mbox{$A$ is a $( ... \oplus ...)$ or $\{ ... \,\&\, ...\}$ type}}
     {\Gamma \vdash \mu X. A : \sort{l}}
\\
\\
\mbox{\em introduction rule}
\\
\\
\seqr{}
     {\Gamma \vdash t : \Sub{A}{X}{\mu X. A}} 
     {\Gamma \vdash \inmu{t} : \mu X.A}
\\
\\
\mbox{\em elimination rule}
\\
\\
\seqr{}
     {\Gamma, X : \sort{l} \vdash A : \sort{l} \qquad \Gamma, b : \mu X. A \vdash P : \sort{l} \qquad \Gamma \vdash v : \mu X. A \qquad \Gamma, f : \mkprod{b}{\mu X. A}{P}, a : \Sub{A}{X}{\mu X. A} \vdash t : \Sub{P}{b}{\inmu{a}} \qquad \mbox{$x$ guarded from $a$ in $t$}}
     {\Gamma \vdash \appmu{f}{t}{a}{v} : \Sub{P}{b}{v}}
\\
\\
\mbox{\em reduction rule}
\\
\\
\seqr{\recbeta}
     {\Gamma, X : \sort{l} \vdash A : \sort{l} \qquad \Gamma, b : \mu X. A \vdash P : \sort{l} \qquad \Gamma \vdash v : \Sub{A}{X}{\mu X. A} \qquad \Gamma, f : \mkprod{b}{\mu X. A}{P}, a : \Sub{A}{X}{\mu X. A} \vdash t : \Sub{P}{b}{\inmu{a}} \qquad \mbox{$x$ guarded from $a$ in $t$}}
     {\Gamma \vdash \appmu{f}{t}{a}{(\inmu{v})} \reduce \Sub{\Sub{t}{a}{v}}{f a}{\appmu{f}{t}{a}{a}} : \Sub{P}{b}{\inmu{v}}}
\\
\\
\mbox{\em observational rule}
\\
\\
\seqr{}
     {\Gamma \vdash t : \mu X.A \qquad \Gamma, a : \mu X.A \vdash E[a] : B}
     {\Gamma \vdash \appmu{f}{E[\inmu{a}]}{a}{t} \reduce E[t] : \Sub{B}{a}{t}}
\\
\\
\mbox{\em congruence rules}
\\
\\
\seqr{}
     {\Gamma, X : \sort{l} \vdash A \equiv A' : \sort{l}}
     {\Gamma \vdash \mu X. A \equiv \mu X. A' : \sort{l}}
\\
\\
\seqr{}
     {\Gamma, X : \sort{l} \vdash A : \sort{l} \qquad \Gamma, a : \mu X. A \vdash P : \sort{l} \qquad \Gamma \vdash v : \mu X. A \qquad \Gamma, f : \mkprod{a}{\mu X. A}{P}, a : \Sub{A}{X}{\mu X. A} \vdash t : P \qquad \mbox{$x$ guarded from $a$ in $t$}}
     {\Gamma \vdash \appmu{f}{t}{a}{v} \equiv \appmu{f}{t'}{a}{v'} : \Sub{P}{a}{v}}
\end{array}
$
}}
\caption{General typing and computational rules for recursive types}
\label{fig:recursivetypetheory}
\end{figure*}

\section{Co-recursive types}

\newcommand{\outnu}[1]{\mathsf{out}\,#1}
\newcommand{\appnu}[4]{\mathsf{cofix\,}{#1}\,{#3}\,=\,\{\mathsf{out}\mapsto{#2}\}\,\mathsf{in}\,{#1}\,{#4}}

We give a syntax for co-recursive types, i.e. for types defined as
greatest type generated by its constructors.

The property of $x$ guarded in $t$ informally means that the path to
the occurrences of $x$ in $t$ never meet an $\outnu{}$.

Note that the observational rule is one among other variants.

\begin{figure*}
\centerline{\framebox{$
\begin{array}{c}
\mbox{\em extended syntax of expressions}
\\
\\
  \begin{array}{lcll}
t, u, v, A, B, p, q & ::= & \ldots ~|~ \nu X.A ~|~ \outnu{t} ~|~ \appnu{f}{t}{c}{v}\\
  \end{array}
\\
\\
\mbox{\em type formers}
\\
\\
\seqr{}
     {\Gamma, X : \sort{l} \vdash A : \sort{l} \qquad \mbox{$A$ is a $( ... \oplus ...)$ or $\{ ... \,\&\, ...\}$ type}}
     {\Gamma \vdash \nu X. A : \sort{l}}
\\
\\
\mbox{\em introduction rule}
\\
\\
\seqr{}
     {\Gamma, X : \sort{l} \vdash A : \sort{l} \qquad \Gamma \vdash C : \sort{l} \qquad \Gamma, f : \mkimp{C}{\nu X. A}, c : C \vdash t : \Sub{A}{X}{\nu X. A} \qquad \Gamma \vdash v : C \qquad \mbox{$x$ guarded in $t$}}
     {\Gamma \vdash \appnu{f}{t}{c}{v} : \nu X.A}
\\
\\
\mbox{\em elimination rule}
\\
\\
\seqr{}
     {\Gamma \vdash t : \nu X.A}
     {\Gamma \vdash \outnu{t} : \Sub{A}{X}{\nu X.A}}
\\
\\
\mbox{\em reduction rule}
\\
\\
\seqr{\corecbeta}
     {\Gamma, X : \sort{l} \vdash A : \sort{l} \qquad \Gamma \vdash C : \sort{l} \qquad \Gamma, f : \mkimp{C}{\nu X. A}, c : C \vdash t : \Sub{A}{X}{\nu X. A} \qquad \Gamma \vdash v : C \qquad \mbox{$x$ guarded in $t$}}
     {\Gamma \vdash \outnu{(\appnu{f}{t}{c}{v})} \reduce \Sub{\Sub{t}{c}{v}}{f\,c}{\appnu{f}{t}{c}{c}} : \Sub{A}{X}{\nu X. A}}
\\
\\
\mbox{\em observational rule}
\\
\\
\seqr{\negeta}
     {\Gamma \vdash C : \sort{l} \qquad \Gamma, c : C \vdash t : \nu X. A \qquad \Gamma \vdash v : C}
     {\Gamma \vdash \appnu{f}{\outnu{t}}{c}{v} \reduce \Sub{t}{c}{v} : \nu X. A}
\\
\\
\mbox{\em congruence rules}
\\
\\
\seqr{}
     {\Gamma, X : \sort{l} \vdash A \equiv A' : \sort{l}}
     {\Gamma \vdash \nu X. A \equiv \nu X. A' : \sort{l}}
\\
\\
\seqr{}
     {\Gamma, X : \sort{l} \vdash A : \sort{l} \qquad \Gamma \vdash C : \sort{l} \qquad \Gamma, f : \mkimp{C}{\nu X. A}, c : C \vdash t \equiv t' : \Sub{A}{X}{\nu X. A} \qquad \Gamma \vdash v \equiv v' : C \qquad \mbox{$x$ guarded in $t$}}
     {\Gamma \vdash \appnu{f}{t}{c}{v} \equiv \appnu{f}{t'}{c}{v'} : \nu X. A}
\end{array}
$
}}
\caption{General typing and computational rules for co-recursive types}
\label{fig:corecursivetypetheory}
\end{figure*}

\end{document}