content: \documentclass{llncs}
  
  %include lhs2TeX.fmt
  %include lhs2TeX.sty
  
  %if anyMath
  
  %format ~ = "~"
  
  %format ! = "{}"
  
  %format .   = ".~"
  %format Set = "\Set"
  %format Type = "\Type"
  %format ==  = "=="
  %format **  = "×"
  %format :   = "\mathrel{:}"
  
  \newcommand \zero {\mathsf{z}}
  \newcommand \suc  {\mathsf{s}}
  %format zero = "\zero"
  %format suc  = "\suc"
  
  %format refl = "\mathsf{refl}"
  
  %format === = "\equiv"
  
  %format of_  = "\mathit{of}"
  
  %format iota    = "ι"
  %format sigma   = "σ"
  %format delta   = "δ"
  %format gamma   = "γ"
  %format eps     = "ε"
  %format beta    = "β"
  %format eta     = "η"
  
  %format eps_I   = "ε_I"
  
  %format inl     = "\mathsf{inl}"
  %format inr     = "\mathsf{inr}"
  
  %format Even'   = "\mathit{Even}^{*}"
  %format evenZ   = "\mathsf{evenZ}"
  %format evenSS  = "\mathsf{evenSS}"
  %format evenZ'  = "\mathsf{evenZ}^{*}"
  %format evenSS' = "\mathsf{evenSS}^{*}"
  %format elim_Even = "\mathit{elim}_{\Even}"
  %format elim_Even' = "\mathit{elim}_{\Even^{*}}"
  \newcommand \Even {\mathit{Even}}
  
  %format pi0 = "π_0"
  %format pi1 = "π_1"
  
  %format elim0 = "\mathit{case}_0"
  %format elim2 = "\elimBool"
  %format Elim2 = "\ElimBool"
  \newcommand \elimBool {\mathit{case}_2}
  \newcommand \ElimBool {\mathit{case}^{\mathit{type}}_2}
  
  %format OP  = "\mathit{OP}"
  %format OPg = "\mathit{OP}^g"
  %format OPr = "\mathit{OP}^r"
  
  %format Fin_n       = "\mathit{Fin}_n"
  %format Args_IE     = "\mathit{Args}_{I,E}"
  %format index_IE    = "\mathit{index}_{I,E}"
  %format IndArg_IE   = "\mathit{IndArg}_{I,E}"
  %format IndIndex_IE = "\mathit{indIndex}_{I,E}"
  %format Ind_IE      = "\mathit{ind}_{I,E}"
  %format IndHyp_IE   = "\mathit{IndHyp}_{I,E}"
  %format indHyp_IE   = "\mathit{indHyp}_{I,E}"
  
  %format elimUrg     = "\mathit{elim}{-}U^r_γ"
  %format elimUreg    = "\mathit{elim}{-}U^r_{εγ}"
  %format elimUgg     = "\mathit{elim}{-}U^g_γ"
  
  %format elimId  = "\mathit{elim}_{==}"
  %format elim_P  = "\mathit{elim}_{==,PM}"
  %format elim_ML = "\mathit{elim}_{==,ML}"
  %format elim_K  = "\mathit{elim}_{==,K}"
  
  %format 0 = "\mathbf{0}"
  %format 1 = "\mathbf{1}"
  %format 2 = "\mathbf{2}"
  %format star = "\star"
  %format star0 = "\star_0"
  %format star1 = "\star_1"
  
  %format < = "\left\langle"
  %format > = "\right\rangle"
  
  %format << = "<"
  %format =~= = "\cong"
  
  %format Urg     = "U^r_γ"
  %format introrg = "\mathrm{intro}^r_γ"
  
  %format Ugg     = "U^g_γ"
  %format introgg = "\mathrm{intro}^g_γ"
  
  %format Ureg     = "U^r_{εγ}"
  %format introreg = "\mathrm{intro}^r_{εγ}"
  
  %format grArgs = "g{\to}rArgs"
  %format grArgs_I = "g{\to}rArgs_I"
  
  %format rgArgs = "r{\to}gArgs"
  %format rgArgs_I = "r{\to}gArgs_I"
  
  %format rgArgssubst = "rgArgs{-}subst"
  
  %format ar   = "a_r"
  %format arg  = "a_{rg}"
  %format stepr = "\mathit{step}_r"
  
  %format IdA   = "\mathrel{{==}_A}"
  
  %endif
  
  \usepackage{ucs}
  \usepackage[utf8x]{inputenc}
  \usepackage{autofe}
  \usepackage{color}
  
  \newcommand \infer[2] {
    \frac
      {\begin{array}{c}\displaystyle #1\end{array}}
      {\begin{array}{c}\displaystyle #2\end{array}}
  }
  
  % Enables greek letters in math environment
  \everymath{\SetUnicodeOption{mathletters}}
  \everydisplay{\SetUnicodeOption{mathletters}}
  
  % This makes sure that local glyph overrides below are
  % chosen.
  \DeclareUnicodeOption{localDefs}
  \SetUnicodeOption{localDefs}
  
  % For some reason these macros need to be defined.
  \newcommand \textmu     {$μ$}
  \newcommand \textnu     {$ν$}
  \newcommand \texteta    {$η$}
  \newcommand \textbeta   {$β$}
  \newcommand \textlambda {$λ$}
  
  % This character doesn't seem to be defined by ucs.sty.
  \DeclareUnicodeCharacter{"21A6}{\ensuremath{\mapsto}}
  
  \input{macros}
  
  \title{Encoding indexed inductive definitions using the intensional identity type}
  \author{Ulf Norell}
  \institute{Chalmers University of Technology \\
    \email{ulfn@@cs.chalmers.se}
  }
  
  \begin{document}
  \maketitle
  \begin{abstract}
    It is well-known how to represent indexed inductive definitions, or inductive
    families, using extensional equality. We show that this encoding also works
    in intensional type theory and that the computation rules associated with an
    inductive family are preserved. The proof has been formalised in Agda.
  \end{abstract}
  
  \section{Introduction}
  
  % Describe the current state of affairs (and sell inductive families)
  
  Indexed inductive definitions (IID), or inductive families, are inductively
  defined families of sets. As such they have a wide range of applications in
  both mathematics and programming. Examples include the transitive closure of a
  relation, the typing relation of simply typed $λ$-calculus, and vectors of a
  fixed length.
  
  Indexed inductive definitions have been studied extensively in various
  theories, such as Martin-Löf type
  theory~\cite{dybjer:sophia,dybjer:bastadfacs}, Calculus of Inductive
  Constructions~\cite{paulin:thesis,coquand:bastad}, and Luo's
  UTT~\cite{luo:typetheory}, and they are supported by tools building on these
  theories. For instance, ALF~\cite{magnussonnordstrom:alf},
  Coq~\cite{mohring:inductivedefsincoq}, LEGO~\cite{luo:lego}, and
  Epigram~\cite{mcbride:left}. They have even made it into languages such as
  Haskell~\cite{pj:gadt}.
  
  % Representing inductive families using equality is well-known
  
  An example of an IID is the predicate |Even| over natural numbers inductively
  defined by the rules
  \[\begin{array}{ccc}
      \infer{}{\Even \, \zero}
  &&  \infer{\Even \, n}{\Even \, (\suc \, (\suc \, n))}
  \end{array}\]
  We distinguish between generalised IID, such as |Even| above, and restricted
  IID where the conclusions must all be of the form $P\,\bar
  x$~\cite{dybjer:indexed-ir}.
  
  It is well-known~\cite{feferman94finitary} how to reduce generalised IID to
  restricted IID using equality. For instance, the |Even| predicate can be
  represented by the restricted IID
  \[\begin{array}{ccc}
      \infer{n = \zero}{\Even \, n}
  &&  \infer{\Even \, m \quad n = \suc \, (\suc \, m)}{\Even \, n}
  \end{array}\]
  There are several reasons, both practical and theoretical, why restricted IID
  are simpler to work with than generalised IID. A practical advantage is that
  the elimination rule for a restricted IID can be presented nicely as pattern
  matching~\cite{coquand:patternmatching}. From a theoretical standpoint a
  restricted IID has the property that it can be expressed as a fixed-point of an
  equation. In the example of |Even|:
  \[\Even \, n \Leftrightarrow n = \zero \vee \exists m. \, \Even \, m \wedge n = \suc \, (\suc \, m) \]
  
  From a set theoretic point of view it is clear that the formulation of the
  generalised IID as a restricted IID is equivalent to the original formulation,
  but in a type theoretic setting it is not so obvious. The reason for this is
  that in type theory we are not only interested in provability but also in the
  proof terms. In the first formulation of the |Even| predicate we have proof
  terms |evenZ| and |evenSS m p|, for a number |m| and a proof |p| that |m| is
  even, corresponding to the two rules. We also have a dependent elimination rule
  |elim_Even|:
  \begin{code}
  elim_Even :  (C : (n : Nat) -> Even n -> Set) ->
               C zero evenZ ->
               (  (n : Nat)(e : Even n) -> C n e ->
                  C (suc (suc n)) (evenSS n e)) ->
               (n : Nat)(e : Even n) -> C n e
  \end{code}
  Note that the predicate |C| that we are eliminating over, depends not only on a
  natural number, but also on the actual proof term that proves it is even.  The
  elimination rule is equipped with two computation rules stating that
  > elim_Even C cz css zero           evenZ         = cz
  > elim_Even C cz css (suc (suc m))  (evenSS m p)  =
  >   css m p (elim_Even C cz css m p)
  Now it is not at all clear that the second formulation of |Even| enjoys the
  same elimination and computation rules, since the proof terms are quite
  different.
  
  Dybjer and Setzer~\cite{dybjer:indexed-ir} show that in extensional type theory
  generalised IID can be reduced to restricted IID, and the main result of the
  present paper is to show that this can be done also in intensional type theory.
  The difference between extensional and intensional type theory is that in
  intensional type theory one distinguishes between provable equality and
  definitional equality.  The advantage of this is that proof checking becomes
  decidable, but a disadvantage is that the proof checker can only decide
  definitional equality, so substituting equals for equals for provable equality
  is more cumbersome. The main challenge in relating the two formulations of
  indexed inductive definitions in intensional type theory is proving that the
  computation rules hold definitionally.
  
  % Fill gap
  
  The main contribution of this paper is a proof that, in intensional type
  theory, we can faithfully represent generalised IID in terms of restricted IID
  and an intensional equality type.  The proof has been formally verified by the
  Agda proof checker~\cite{coquand:stt-lfm99}. The formal proof has been carried
  out for the fully general case of indexed inductive-recursive
  definitions~\cite{dybjer:indexed-ir}, but for presentation reasons we restrict
  ourselves to indexed inductive definitions. Adding a recursive component adds
  no difficulties to the proof.
  
  For systems such as Agda, which only support restricted indexed inductive
  definitions, our result provides a way to get the power of generalised
  inductive families without having to extend the meta-theory.
  
  The rest of this paper is organised as follows. Section~\ref{sec-lf} introduces
  the logical framework, Section~\ref{sec-id} gives a brief introduction to the
  intensional identity type, Section~\ref{sec-IID} gives a formalisation of
  indexed inductive definitions, Section~\ref{sec-Encoding} contains the proof
  that generalised IID can be reduced to restricted IID, Section~\ref{sec-formal}
  comments on the formal proof, and Section~\ref{sec-concl} concludes.
  
  \section{The logical framework} \label{sec-lf}
  
  We use  Martin-Löf's logical framework~\cite{nordstrom:book} extended with
  sigma types |(x : A) ** B|, |0|, |1|, and |2|. This is the same framework as is
  used by Dybjer and Setzer and the complete rules can be found
  in~\cite{dybjer:indexed-ir}. In contrast to Dybjer and Setzer, however, we work
  entirely in intensional type theory.
  
  The type of sets |Set| is closed under dependent sums and products, and if |A :
  Set| then |A| is a type.
  
  Dependent function types are written |(x : A) -> B| and have elements |\ x. a|,
  where |a : B| provided |x : A|.  Application of |f| to |a| is written |f a|. If
  |x| does not occur free in |B| we write |A -> B| for |(x : A) -> B| and when
  the result type is itself a function type we write |(x : A)(y : B) -> C| for
  |(x : A) -> (y : B) -> C|.
  
  The elements of a sigma type |(x : A) ** B| are pairs |<a, b>| where |a : A|
  and $b : B[a/x]$ (|B| with |a| substituted for |x|). We have projections |pi0|
  and |pi1| with the |beta|-rules |pi0 <a, b> = a| and |pi1 <a, b> = b| and the
  |eta|-rule |<pi0 p, pi1 p> = p|.
  
  The empty type |0| has no elements and elimination rule |elim0 : 0 -> A|, for
  any |A : Set|. The element of the singleton type is |star : 1| and if |a : 1|
  then |a = star| (|eta|-rule). The two element type |2| has elements |star0| and
  |star1|, and elimination rule $\elimBool : (i : \mathbf{2}) \to A[\star_0] \to
  A[\star_1] \to A[i]$, where $A[i]$ is a type for |i : 2|. We also have large
  elimination for |2|: |Elim2 : 2 -> Set -> Set -> Set|. Using the large
  elimination we can define the disjoint union of two types
  > A + B = (i : 2) ** Elim2 i A B.
  
  \section{The identity type} \label{sec-id}
  
  In this paper we show that the logical framework extended with restricted IID
  and an intensional identity type can express generalised IID. In order to do
  this we first have to chose the identity type to use. Let us review our
  choices. We want a type
  \begin{code}
    ! IdA ! : A -> A -> Set
  \end{code}
  with introduction rule
  \begin{code}
    refl : (x : A) -> x == x
  \end{code}
  
  The choice lies in the elimination rule, where we have two principal
  candidates. The Martin-Löf elimination rule, introduced in
  1973~\cite{martin-lof:predicative} is defined as follows.
  
  \begin{definition}[Martin-Löf elimination]
  
  The Martin-Löf elimination rule (sometimes called $J$) has the type
  \begin{code}
  elim_ML :  (C : (x, y : A) -> x == y -> Set) ->
             ((x : A) -> C x x (refl x)) ->
             (x, y : A)(p : x == y) -> C x y p
  \end{code}
  and computation rule
  > elim_ML C h x x (refl x) = h x
  \end{definition}
  
  A different elimination rule was introduced by
  Paulin-Mohring~\cite{pfenning-paulin:inductive-coc}:
  
  \begin{definition}[Paulin-Mohring elimination]
  The Paulin-Mohring elimination rule has type
  \begin{code}
  elim_P :  (x : A)(C : (y : A) -> x == y -> Set) ->
            C x (refl x) -> (y : A)(p : x == y) -> C y p
  \end{code}
  and computation rule
  > elim_P x C h x (refl x) = h
  
  \end{definition}
  
  The difference between Martin-Löf elimination and Paulin-Mohring elimination is
  that in Martin-Löf elimination the predicate |C| abstracts over both |x| and
  |y|, whereas in Paulin-Mohring elimination the predicate need only abstract
  over |y|.
  
  At first glance, Paulin-Mohring elimination looks stronger than Martin-Löf
  elimination, and indeed it is easy to define |elim_ML| in terms of |elim_P|.
  
  \begin{lemma}
      Martin-Löf elimination can be defined in terms of Paulin-Mohring
      elimination.
  \end{lemma}
  
  \begin{proof}
  > elim_ML C h x y p = elim_P x (\ z q. C x z q) (h x) y p
  \end{proof}
  %
  However, it turns out that Paulin-Mohring elimination is also definable in
  terms of Martin-Löf elimination~\cite{paulin:mail}. The proof of this is
  slightly more involved.
  %
  \begin{lemma}
      Paulin-Mohring elimination can be defined in terms of Martin-Löf
      elimination.
  \end{lemma}
  
  \begin{proof}
      We first define the substitution rule
  \begin{code}
      subst :  (C : A -> Set)(x, y : A)
               x == y -> C x -> C y
      subst C x y p Cx = elim_ML  (\ a b q. C a -> C b)
                                  (\ a Ca. Ca) x y p Cx
  \end{code}
      Now define |E x = (y : A) ** (x == y)|.  We can prove that any element of
      |E x| is equal to |<x, refl x>|.
  \begin{code}
      uniqE : (x, y : A)(p : x == y) -> <x, refl x> == <y, p>
      uniqE = elim_ML (\ x y p. <x, refl x> == <y, p>) refl
  \end{code}
  Finally
  \begin{code}
      elim_P x C h y p = subst  (\ z. C (pi0 z) (pi1 z))
                                <x, refl x> <y, p> (uniqE x y p) h
  \end{code}
  \end{proof}
  
  In an impredicative setting there is a simpler proof due to
  Streicher~\cite{streicher:habilitation}. Yet another elimination rule is
  Streicher's axiom K~\cite{HofmannM:gromru}, given by
  > elim_K :  (x : A)(C : x == x -> Set) ->
  >           C refl -> (p : x == x) -> C p
  which he shows cannot be defined in terms of the previous elimination rules.
  
  Seeing as Martin-Löf elimination and Paulin-Mohring elimination are equivalent
  we choose Paulin-Mohring elimination which is easier to work with. So we extend
  our logical framework with
  \begin{code}
  ! IdA !  :  A -> A -> Set
  refl     :  (x : A) -> x == x
  elimId   :  (x : A)(C : (y : A) -> x == y -> Set) ->
              C x (refl x) -> (y : A)(p : x == y) -> C y p
  elimId x C h x (refl x) = h
  \end{code}
  
  \section{Indexed Inductive Definitions} \label{sec-IID}
  
  An indexed inductive definition (IID) defines a family of types. We distinguish
  between generalised IID, which can be seen as an inductively defined family of
  types, and restricted IID, which can be seen as a family of inductive types.
  Non-indexed types are a special case of restricted IID, indexed over |1|. For
  instance, the type of natural numbers can be seen as the restricted IID
  \begin{code}
    Nat   : 1 -> Set
    zero  : (x : 1) -> Nat x
    suc   : (x : 1) -> Nat x -> Nat x
  \end{code}
  In these cases we omit the index and simply write
  \begin{code}
    Nat   : Set
    zero  : Nat
    suc   : Nat -> Nat
  \end{code}
  An example of a restricted IID indexed by a natural number |n| is the type of
  ordered lists of natural numbers greater than or equal to |n|:
  \begin{code}
    OrdList  : Nat -> Set
    nil      : (n : Nat) -> OrdList n
    cons     : (n : Nat) -> (m : Nat) -> (m >= n) -> OrdList m -> OrdList n
  \end{code}
  Note that the introduction rules (constructors) |nil| and |cons|, constructs
  elements in |OrdList n| for an arbitrary |n|. Note also that the types at
  different indices can depend on each other. In this case the inductive argument
  of the |cons| constructor is |OrdList m| for an arbitrary |m >= n|.
  
  In a generalised IID, however, the constructors can target different parts of
  the inductive family. In the case of lists of a certain length we have
  \begin{code}
    Vec   : Nat -> Set
    nil   : Vec zero
    cons  : (n : Nat) -> Nat -> Vec n -> Vec (suc n)
  \end{code}
  
  In the rest of this section we present the formalisation of indexed inductive
  types. We follow the formalisation of indexed induction-recursion of Dybjer and
  Setzer~\cite{dybjer:indexed-ir} but leave out the recursion to simplify the
  presentation.
  
  \subsection{Codes for IID} \label{sec-IID-Codes}
  
  Like Dybjer and Setzer we introduce a common type of codes which will serve
  both as codes for general IID and restricted IID.
  
  \begin{code}
  OP I E  : Set
  iota    : E -> OP I E
  sigma   : (A : Set) -> (A -> OP I E) -> OP I E
  delta   : (A : Set) -> (A -> I) -> OP I E -> OP I E
  \end{code}
  
  Now the codes for general indexed inductive types are defined by |OPg I = OP I
  I|, and the codes for restricted types are |OPr I = I -> OP I 1|. The intuition
  is that for general IID the index is computed from the shape of the value,
  whereas the index of a restricted IID is given beforehand. With these
  definitions in mind, let us study the type of codes in more detail. We have
  three constructors:
  \begin{itemize}
      \item
          Base case: |iota e|. This corresponds to an IID with no arguments to the
          constructor. In the case of a general IID we have to give the index for
          the constructor. For instance the code for the singleton type of true
          booleans given by the formation rule |IsTrue : Bool -> Set| and
          introduction rule |IsTrue true| is |iota true : OPg Bool|
      \item
          Non-inductive argument: |sigma A gamma|. In this case the constructor
          has a non-inductive argument |a : A|. The remaining arguments may depend
          on |a| and are coded by |gamma a|. A datatype with
          multiple constructors can be coded by |sigma C gamma| where |C| is a
          type representing the constructors and |gamma c| is the code for the
          constructor corresponding to |c|. For instance, the code for the
          datatype |Bool| with two nullary constructors is
          \begin{code}
          \i . sigma 2 (\c. elim2 c (iota star) (iota star))
          \end{code}
  
          Another example is the type of pairs over |A| and |B|
          \begin{code}
          \ i. sigma A (\ a. sigma B (\ b. iota star)) : OPr 1
          \end{code}
          In this case the following arguments do not depend on the value of the
          non-inductive arguments.
      \item
          Inductive argument: |delta A i gamma|. For an inductive argument we
          need to know the index of the argument. Note that the following
          arguments cannot depend on the value of the inductive argument. The
          inductive argument may occur under some assumptions |A|. For example
          consider the accessible part of a relation |<<| over |A|, |Acc : A ->
          Set| with introduction rule that for any |x|, if |((y : A) -> y << x
          -> Acc y)| then |Acc x|. Here the inductive argument |Acc y| occurs
          under the assumptions |(y : A)| and |y << x|. The code for this type is
          \begin{code}
              \ x. delta ((y : A) ** (y << x)) pi0 (iota star) : OPr A
          \end{code}
          The index of the inductive argument is |y| which is the first projection
          of the assumptions.
  \end{itemize}
  See Section~\ref{sec-IID-Examples} for more examples.
  
  \subsection{From codes to types} \label{sec-IID-Types}
  
  Now that we have defined the codes for IID the next step is to describe their
  semantics, i.e. what the elements of an IID with a given code are. First we
  define the type of arguments to the constructor parameterised by the type of
  inductive arguments\footnote{Analogous to when you for simple inductive types
  define an inductive type as the fixed point of some functor.}.
  \begin{code}
  Args_IE : (gamma : OP I E)(U : I -> Set) -> Set
  Args (iota e)           U  = 1
  Args (sigma A gamma)    U  = A ** \ a. Args (gamma a) U
  Args (delta A i gamma)  U  = ((a : A) -> U (i a)) ** \ d. Args gamma U
  \end{code}
  There are no surprises here, in the base case there are no arguments, in the
  non-inductive case there is one argument |a : A| followed by the rest of the
  arguments (which may depend on |a|). In the inductive case we have a function
  from the assumptions |A| to a value of the inductive type at the specified
  index.
  
  For generalised IID we also need to be able to compute the index of a given
  constructor argument.
  \begin{code}
  index_IE : (gamma : OP I E)(U : I -> Set)(a : Args gamma U) -> E
  index (iota e)           U  star    = e
  index (sigma A gamma)    U  <x, a>  = index (gamma x) U a
  index (delta A i gamma)  U  <_, a>  = index gamma U a
  \end{code}
  Note that only the non-inductive arguments are used when computing the index.
  
  This is all the machinery needed to introduce the types of generalised and
  restricted IID. For restricted IID we introduce, given |gamma : OPr I| and |i :
  I|
  \begin{code}
      Urg : I -> Set
      introrg i : Args (gamma i) Urg -> Urg i
  \end{code}
  For generalised IID, given |gamma : OPg I| we want
  \begin{code}
      Ugg : I -> Set
      introgg : (a : Args gamma Ugg) -> Ugg (index gamma Ugg a)
  \end{code}
  In Section~\ref{sec-Encoding} we show how to define |Ugg| in terms of |Urg|.
  
  As an example take the type of pairs over |A| and |B|:
  \begin{code}
      gamma = \ i. sigma A (\ a. sigma B (\ b. iota star)) : OPr 1
      Pair A B = Urg : 1 -> Set
      introrg star : A ** (\ a. B ** (\ b. 1)) -> Pair A B star
  \end{code}
  
  Note that while the index of a restricted IID is determined from the outside,
  it is still possible to have a different index on the inductive occurrences.
  An example of this is the accessibility predicate given in
  Section~\ref{sec-IID-Codes}. This is crucial when interpreting general IID by
  restricted IID (see Section~\ref{sec-Encoding}).
  
  \subsection{Elimination rules} \label{sec-IID-Elimination}
  
  To complete the formalisation of IID we have to give the elimination rules.  We
  start by defining the set of assumptions of the inductive occurrences in a
  given constructor argument.
  \begin{code}
  IndArg_IE : (gamma : OP I E)(U : I -> Set) -> Args gamma U -> Set
  IndArg (iota e)           U star      = 0
  IndArg (sigma A gamma)    U < a, b >  = IndArg (gamma a) U b
  IndArg (delta A i gamma)  U < g, b >  = A + IndArg gamma U b
  \end{code}
  Simply put |IndArg gamma U a| is the disjoint union of the assumptions of the
  inductive occurrences in |a|.
  
  Now, given the assumptions of one inductive occurrence we can compute the index
  of that occurrence.
  \begin{code}
  IndIndex_IE :  (gamma : OP I E)(U : I -> Set)
                 (a : Args gamma U) -> IndArg gamma U a -> I
  indIndex (iota e)           U  star      z        = elim0 z
  indIndex (sigma A gamma)    U  < a, b >  c        = indIndex (gamma a) U b c
  indIndex (delta A i gamma)  U  < g, b >  (inl a)  = i a
  indIndex (delta A i gamma)  U  < g, b >  (inr a)  = indIndex gamma U b a
  \end{code}
  The code |gamma| contains the values of the indices for the inductive
  occurrences so we just have to find the right inductive occurrence.
  
  We can now define a function to extract a particular inductive occurrence from
  a constructor argument.
  \begin{code}
  Ind_IE :  (gamma : OP I E)(U : I -> Set)
            (a : Args gamma U)(v : IndArg gamma U a) -> U (indIndex gamma U a v)
  ind (iota e)           U  star      z        = elim0 z
  ind (sigma A gamma)    U  < a, b >  c        = ind (gamma a) U b c
  ind (delta A i gamma)  U  < g, b >  (inl a)  = g a
  ind (delta A i gamma)  U  < g, b >  (inr a)  = ind gamma U b a
  \end{code}
  Again the definition is very simple.
  
  Next we define the notion of an induction hypothesis. Given a predicate |C|
  over elements in a datatype, an induction hypothesis for a constructor argument
  |a| is a function that proves the predicate for all inductive occurrences in
  |a|.
  \begin{code}
  IndHyp_IE :  (gamma : OP I E)(U : I -> Set) ->
               (C : (i : I) -> U i -> Set)(a : Args gamma U) -> Set
  IndHyp gamma U C a =  (v : IndArg gamma U a) ->
                        C (indIndex gamma U a v) (ind gamma U a v)
  \end{code}
  
  Given a function |g| that proves |C i u| for all |i| and |u| we can construct an
  induction hypothesis for |a| by applying |g| to all inductive occurrences in
  |a|.
  \begin{code}
  indHyp_IE :
    (gamma : OP I E)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (g : (i : I)(u : U i) -> C i u)
    (a : Args gamma U) -> IndHyp gamma U C a
  indHyp gamma U C g a = \ v. g (indIndex gamma U a v) (ind gamma U a v)
  \end{code}
  
  We are now ready to introduce the elimination rules. Given |I : Set| and |gamma
  : OPr I| the elimination rule for the restricted IID |Urg| is given by the
  following type and computation rule:
  \begin{code}
  elimUrg :
    (C : (i : I) -> Urg i -> Set) ->
    ((i : I)(a : Args (γ i) Urg) -> IndHyp (γ i) Urg C a -> C i (introrg i a))
    -> (i : I)(u : Urg i) -> C i u
  elimUrg C step i (introrg a) =
    step i a (indHyp (γ i) Urg C (elimUrg C step) a)
  \end{code}
  That is, for any predicate |C| over |Urg|, if given that |C| holds for all
  inductive occurrences in some arbitrary constructor argument |a| then |C| holds
  for |introrg a|, then |C| holds for all elements of |Urg|. The computation rule
  states that eliminating an element built by the introduction rule is the same
  as first eliminating all inductive occurrences and then applying the induction
  step.
  
  The elimination rule for a general IID is similar. The difference is that the
  index of a constructor argument is computed from the value of the argument.
  \begin{code}
  elimUgg :
    (C : (i : I) -> Ugg i -> Set) ->
    (  (a : Args γ Ugg) -> IndHyp γ Ugg C a -> C (index γ Ugg a) (introgg a)) ->
    (i : I)(u : Ugg i) -> C i u
  elimUgg C step (index γ Ugg a) (introgg a) =
    step a (indHyp γ Ugg C (elimUgg C m) a)
  \end{code}
  
  \subsection{Examples} \label{sec-IID-Examples}
  
  %format gammaNat = "γ_{\mathit{Nat}}"
  %format introrgn = "\mathit{intro}^r_{γ_{\mathit{Nat}}}"
  
  %format gammaEven = "γ_{\mathit{Even}}"
  %format gammaId   = "γ_{{==}}"
  
  As we have seen, datatypes with more than one constructor can be encoded by
  having the first argument be a representation of the constructor.  For
  instance, the code for natural numbers is
  > gammaNat : OPr 1 = \i. sigma 2 (\ c. elim2 c (iota star) (delta 1 (\ x. star) (iota star)))
  Here, the first argument is an element of |2| encoding whether the number is
  built by |zero| or |suc|. We can recover the familiar introduction rules |zero|
  and |suc| by
  \begin{code}
  zero   = introrgn star ! <star0, star>
  suc n  = introrgn star ! <star1, < \ x. n, star> >
  \end{code}
  Another example is the generalised IID of proofs that a natural numbers are
  even given introduction rules
  \begin{code}
  evenZ  : Even zero
  evenSS : (n : Nat) -> Even n -> Even (suc (suc n))
  \end{code}
  The code for |Even| is
  \begin{code}
  gammaEven  :  OPg Nat
             =  sigma 2 (\ c. elim2 c (iota zero) (sigma Nat (\ n. delta 1 (\ x. n) (iota (suc (suc n))))))
  \end{code}
  Again an argument of type |2| is used to distinguish the two constructors. In
  the |evenZ| case there are no arguments and the index is |zero|. In the
  |evenSS| case there is one non-inductive argument |n| of type |Nat| and one
  inductive argument with no assumptions and index |n|. The index of the result
  is |suc (suc n)|.
  
  The Paulin-Mohring intensional identity type also has a code. Given a set |A|
  and an |x : A| code for the family |x == y| indexed by |y : A| is
  \begin{code}
    gammaId : OPg A = iota x
  \end{code}
  That is, there is a single constructor with no arguments, whose index is |x|.
  This corresponds to the introduction rule
  > refl : x == x
  The elimination rule for this type is exactly the Paulin-Mohring elimination rule.
  
  \section{Encoding generalised IID as restricted IID} \label{sec-Encoding}
  
  In this section we show that generalised IID are expressible in the logical
  framework extended with restricted IID and the intensional identity type. We do
  this by defining the formation, introduction, and elimination rules of a
  generalised IID and subsequently proving that the computation rules hold
  intensionally.
  
  \subsection{Formation rule}
  
  We first show how to transform the code for a generalised IID into the code for
  its encoding as a restricted IID.  The basic idea, as we have seen, is to add a
  proof that the index of the restricted IID is equal to the index computed for
  the generalised IID. Concretely:
  \begin{code}
  eps_I : OPg I -> OPr I
  eps (iota i)           j = sigma (i == j) (\ p. iota star)
  eps (sigma A gamma)    j = sigma A (\ a. eps (gamma a) j)
  eps (delta H i gamma)  j = delta H i (eps gamma j)
  \end{code}
  Now a generalised IID for a code |gamma| can be defined as the restricted IID
  of |eps gamma|.
  \begin{code}
  Ugg : I -> Set
  Ugg i = Ureg i
  \end{code}
  For example, the generalised IID of the proofs that a number is even, given by
  \begin{code}
  Even    : Nat -> Set
  evenZ   : Even zero
  evenSS  : (n : Nat) -> Even n -> Even (suc (suc n))
  \end{code}
  is encoded by the following restricted IID:
  \begin{code}
  Even'    : Nat -> Set
  evenZ'   : (n : Nat) -> zero == n -> Even' n
  evenSS'  : (n : Nat)(m : Nat) -> Even' m -> suc (suc m) == n -> Even' n
  \end{code}
  
  \subsection{Introduction rule}
  
  We need an introduction rule
  \begin{code}
  introgg : (a : Args gamma Ugg) -> Ugg (index gamma Ugg a)
  \end{code}
  and we have the introduction rule for the restricted IID:
  \begin{code}
  introreg i  :  Args (eps gamma i) Ureg  -> Ureg i
              =  Args (eps gamma i) Ugg   -> Ugg i
  \end{code}
  So, what we need is a function |grArgs| to convert a constructor argument for a
  generalised IID, |a : Args gamma Ugg|, to a constructor argument for its
  representation, |Args (eps gamma (index gamma Ugg a)) Ugg|. This function
  simply adds a reflexivity proof to |a|:
  \begin{code}
  grArgs_I :  (gamma : OPg I)(U : I -> Set)
              (a : Args gamma U) -> Args (eps gamma (index gamma U a)) U
  grArgs (iota e)           U a         = < refl, star >
  grArgs (sigma A gamma)    U < a, b >  = < a, grArgs (gamma a) U b >
  grArgs (delta H i gamma)  U < g, b >  = < g, grArgs gamma U b >
  \end{code}
  As usual we abstract over the type of inductive occurrences. Now the
  introduction rule is simply defined by
  \begin{code}
  introgg a = introreg (index gamma Ugg a) (grArgs gamma Ugg a)
  \end{code}
  In our example:
  \begin{code}
  evenZ : Even' zero
  evenZ = evenZ' refl
  
  evenSS : (n : Nat) -> Even' n -> Even' (suc (suc n))
  evenSS n e = evenSS' n e refl
  \end{code}
  
  \subsection{Elimination rule}
  
  Now we turn our attention towards the elimination rule.
  
  \begin{theorem}
  The elimination rule for a generalised IID is provable for the representation
  of generalised IID given above. More precisely, we can prove the following rule
  in the logical framework with restricted IID and the identity type.
  \begin{code}
  elimUgg :  (C : (i : I) -> Ugg i -> Set) ->
             (  (a : Args γ Ugg) -> IndHyp γ Ugg C a ->
                C (index γ Ugg a) (introgg a)) ->
             (i : I)(u : Ugg i) -> C i u
  \end{code}
  \end{theorem}
  
  \begin{proof}
  We can use the elimination for the restricted IID
  \begin{code}
  elimUreg :  (C : (i : I) -> Ugg i -> Set) ->
              (  (i : I)(a : Args (eps gamma i) Ugg) ->
                 IndHyp (eps gamma i) Ugg C a -> C i (introreg i a)) ->
              (i : I)(u : Ugg i) -> C i u
  \end{code}
  Now we face the opposite problem from what we encountered when defining the
  introduction rule. In order to apply the induction step we have to convert a
  constructor argument to the restricted IID to a generalised argument, and
  likewise for the induction hypothesis. To convert a restricted constructor
  argument we simply remove the equality proof.
  
  \begin{code}
  rgArgs_I :  (gamma : OPg I)(U : I -> Set)
              (i : I)(a : Args (eps gamma i) U) -> Args gamma U
  rgArgs (iota i)           U j _         = star
  rgArgs (sigma A gamma)    U j < a, b >  = < a, rgArgs (gamma a) U j b >
  rgArgs (delta H i gamma)  U j < g, b >  = < g, rgArgs gamma U j b >
  \end{code}
  
  Converting induction hypotheses requires a little more work. This work,
  however, is pure book-keeping, as we will see.  We have an induction hypothesis
  for the restricted IID. Namely, for |a : Args (eps gamma i) Ugg| we have
  \begin{code}
  ih  :  IndHyp (eps gamma i) Ugg C a
      =  (v : IndArg (eps gamma i) U a -> C  (indIndex (eps gamma i) U a v)
                                             (ind (eps gamma i) U a v)
  \end{code}
  We need, for |a' = rgArgs gamma Ugg i a|
  \begin{code}
  ih  :  IndHyp gamma Ugg C a'
      =  (v : IndArg gamma U a') -> C (indIndex gamma U a' v) (ind gamma U a' v)
  \end{code}
  Our intuition is that |eps| does not change the inductive occurrences in any
  way, and indeed we can prove the following lemma:
  
  \begin{lemma} \label{lem-eps-ind}
  For any closed |gamma|, and |a : Args (eps gamma i) U| and |v : IndArg (eps
  gamma i) U a| the following equalities hold definitionally.
  \begin{code}
  IndArg    gamma U      (rgArgs gamma U i a)    = IndArg    (eps gamma i) U a
  indIndex  gamma U      (rgArgs gamma U i a) v  = indIndex  (eps gamma i) U a v
  ind       gamma U      (rgArgs gamma U i a) v  = ind       (eps gamma i) U a v
  IndHyp    gamma U C    (rgArgs gamma U i a)    = IndHyp    (eps gamma i) U C a
  indHyp    gamma U C g  (rgArgs gamma U i a)    = indHyp    (eps gamma i) U C g a
  \end{code}
  \end{lemma}
  %format lem_epsInd = "\ref{lem-eps-ind}"
  \begin{proof}
    The first three are proven by induction on |gamma|. The last two follows from the first three.
  \end{proof}
  
  That is, we can use the induction hypothesis we have as it is. Let us now try
  to define the elimination rule. We are given
  \begin{code}
  C     :  (i : I) -> Ugg i -> Set
  step  :  (a : Args gamma Ugg) -> IndHyp gamma Ugg C a ->
           C (index gamma Ugg a) (introgg a)
  i     :  I
  u     :  Ugg i
  \end{code}
  and we have to prove |C i u|. To apply the restricted elimination rule
  (|elimUreg|) we need an induction step |stepr| of type
  \begin{code}
  (i : I)(a : Args (eps gamma i) Ugg) -> IndHyp (eps gamma i) Ugg C a -> C i (intror i a)
  \end{code}
  As we have observed the induction hypothesis already has the right type, so we attempt to
  define
  \begin{code}
  stepr i a ih = step (rgArgs gamma Ugg i a) ih
  \end{code}
  The type of |stepr i a ih| is |C (index gamma U ar) (intror (grArgs gamma U
  ar))|, where |ar = rgArgs gamma Ugg i a|. Here, we would like the conversion of
  a constructor argument from the restricted representation to a generalised
  argument and back to be the definitional identity. It is easy to see that
  this is not the case.  For instance, in our |Even| example the argument to the
  |evenZ'| constructor is a proof |p : zero == zero|. Converting to a generalised
  argument we throw away the proof, and converting back we add a proof by
  reflexivity. But |p| and |refl| are not definitionally equal. Fortunately they
  are provably equal, so we can define the following substitution function:
  
  \begin{code}
  rgArgssubst :  (gamma : OPg I)(U : I -> Set)
                 (C : (i : I) -> rArgs (eps gamma) U i -> Set)
                 (i : I)(a : rArgs (eps gamma) U i) ->
                 (C  (index gamma U (rgArgs gamma U i a))
                     (grArgs gamma U (rgArgs gamma U i a))
                 ) -> C i a
  
  rgArgssubst (iota i) U C j < p, star > m =
    elimId i (\ k q. C k < q, star >) m j p
  
  rgArgssubst (delta A gamma)   U C j < a, b > m =
    rgArgssubst (gamma a) U (\ i c. C i < a, c >) j b m
  
  rgArgssubst (delta H i gamma) U C j < g, b > m =
    rgArgssubst gamma U (\ i c. C i < g, c >) j b m
  \end{code}
  The interesting case is the |iota|-case where we have to prove |C j <p, star>|
  given |C i <refl, star>| and |p : i == j|. This is proven using the elimination
  rule, |elimId|, for the identity type. Armed with this substitution rule we can
  define the elimination rule for a generalised IID:
  \begin{code}
  elimUgg C step i u = elimUreg C stepr i u
    where
      stepr i a ih = rgArgssubst  gamma Ugg (\ i a. C i (intror i a))
                                  i a (step (rgArgs gamma Ugg i a) ih)
  \end{code}
  \end{proof}
  
  In our example the definition of the elimination rule is
  \begin{code}
  elim_Even :  (C : (n : Nat) -> Even n -> Set) ->
               C zero evenZ ->
               (  (n : Nat)(e : Even n) -> C n e ->
                  C (suc (suc n)) (evenSS n e)) ->
               (n : Nat)(e : Even n) -> C n e
  elim_Even C cz css n (evenZ' p)       =
    elimId zero (\ m q. C m (evenZ' q)) cz n p
  elim_Even C cz css n (evenSS' m e p)  =
    elimId  (suc (suc m)) (\ z q. C z (evenSS' m e q))
            (css m e (elim_Even C cz css m e)) n p
  \end{code}
  To improve readability we present the rule using pattern matching and explicit
  recursion rather than calling |elim_Even'|.  The call to |rgArgssubst| is has
  been reduced to identity proof eliminations.
  
  \subsection{Computation rule}
  
  So far we have shown that we can represent generalised IID as a restricted IID
  and that the elimination rule is still valid. The only thing remaining is to
  show that the computation rule is also valid. That is, that we get the same
  definitional equalities for our representation as we would if we extended our
  system with generalised IID.
  
  \begin{theorem}
    For the representation of generalised IID given above, and the encoding of
    the elimination rule |elimUgg| the following computation rule holds
    definitionally for closed |gamma|:
  \begin{code}
  elimUgg C step (index γ Ugg a) (introgg a) =
    step a (indHyp γ Ugg C (elimUgg C step) a)
  \end{code}
  \end{theorem}
  
  \begin{proof}
  The key insight here is that the computation rule does not talk about arbitrary
  elements of |Ugg|, but only those that have been constructed using the
  introduction rule. This means that we do not have to satisfy any definitional
  equalities for elements where the equality proof is not definitionally equal to
  |refl|. So, the main step in the proof is to prove that |rgArgssubst| is the
  definitional identity when the equality proof is |refl|, i.e. when the argument
  is build using the |grArgs| function.
  
  \begin{lemma} \label{lem-rgArgsubst}
    For all closed |gamma|, and all |U|, |C|, |a : Args gamma U|, and
    \begin{code}
      h : C (index gamma U arg) (grArgs gamma U arg)
    \end{code}
    where
    \begin{code}
      ar    = grArgs gamma U a
      i     = index gamma U a
      arg   = rgArgs gamma U i ar
    \end{code}
    it holds definitionally that
    \begin{code}
      rgArgssubst gamma U C i ar h = h
    \end{code}
  \end{lemma}
  
  %format lem_rgArgsubst = "\ref{lem-rgArgsubst}"
  
  \begin{proof}
    By induction on |gamma|. In the |iota|-case we have to prove that
    \begin{code}
      elimId i C' h i refl = h
    \end{code}
    which is exactly the computation rule for the identity type.
  \end{proof}
  
  The final lemma we need before proving the computation rule is that starting with
  a generalised constructor argument, converting it to a restricted one, and then
  back is the definitional identity. This amounts to adding a reflexivity proof
  and then removing it, so it is easy to see that this should be true.
  
  \begin{lemma} \label{lem-arg-is-a}
    For all closed |gamma|, and all |a : Args gamma U| it holds definitionally that
  > rgArgs gamma U (index gamma U a) (grArgs gamma U a) = a
  \end{lemma}
  %format lem_argIsa = "\ref{lem-arg-is-a}"
  \begin{proof}
    By induction on |gamma|.
  \end{proof}
  
  Now we are ready to prove the computation rule. Take |a : Args gamma Ugg| and let
  \begin{code}
    i   = index gamma Ugg a
    ar  = grArgs gamma Ugg a
    arg = rgArgs gamma Ugg i ar
  \end{code}
  we have
  \begin{code}
  elimUgg C step (index gamma Ugg a) (introgg a)
  =  elimUgg C step i (introgg a)
  =  {definition of_ elimUgg and introrg}
     elimUreg C stepr i (introreg i ar)
  =  {computation rule for Ureg}
     stepr i ar (indHyp (eps gamma i) Ugg C (elimUgg C step) ar)
  =  {definition of_ stepr}
     rgArgssubst gamma Ugg (\ i a. C i (intror i ar)) i ar
        (step arg (indHyp (eps gamma i) Ugg C (elimUgg C step) ar))
  =  {Lemma lem_rgArgsubst}
     step arg (indHyp (eps gamma i) Ugg C (elimUgg C step) ar)
  =  {Lemma lem_epsInd}
     step arg (indHyp gamma Ugg C (elimUgg C step) arg)
  =  {Lemma lem_argIsa}
     step a (indHyp gamma Ugg C (elimUgg C step) a)
  \end{code}
  \end{proof}
  
  In the example of |Even| the proofs of the computation rules are
  \begin{code}
  elim_Even C cz css zero evenZ
  = elim_Even C cz css zero (evenZ' refl)
  = elimId zero (\ m q. C m (evenZ' q)) cz zero refl
  = cz
  
  elim_Even C cz css (suc (suc m)) (evenSS m p)
  = elim_Even C cz css (suc (suc m)) (evenSS' m p refl)
  = elimId  (suc (suc m)) (\ z q. C z (evenSS' m e q))
            (css m e (elim_Even C cz css m e)) (suc (suc m)) refl
  = css m e (elim_Even C cz css m e)
  \end{code}
  The important steps are the appeals to the computation rule for the identity
  type.
  
  This concludes the proof that we can faithfully represent generalised IID in
  the theory of restricted IID and the intensional identity type.
  
  \section{Notes on the formal proof} \label{sec-formal}
  
  One approach to formalise our result would be to do a deep embedding,
  formalising the logical framework and the theory of restricted IID in Agda, and
  prove our theorems for this formalisation. This would be a big undertaking,
  however, so we chose a more light-weight approach. In Agda we can define the
  rules for restricted IID directly, that is, we can define restricted IID as a
  datatype in Agda and get the introduction, elimination, and computation rules
  for free. Using this definition of restricted IID we can then prove the
  formation, introduction, and elimination rules for the representation of
  generalised IID.
  
  When we want to prove the computation rule, however, there is a problem. The
  computation rule talks about definitional equality and in Agda we cannot reason
  about the internal definitional equality. To solve this problem we axiomatised
  the definitional equality of the logical framework. That is, for each |A, B :
  Set| we introduce a constant
  \begin{code}
    ! = ! : A -> B -> Set
  \end{code}
  and axioms corresponding to the conversion rules of the logical framework. For
  instance, for all |f|, |g|, |x|, and |y|
  \begin{code}
    app : (f = g) -> (x = y) -> (f x = g y)
  \end{code}
  In this axiom, we can see why the definitional equality has type |A -> B ->
  Set|: since |f| and |g| can be dependent functions, |f x| and |g y| can have
  different types.
  
  With this approach one has to be careful with induction.  For instance, if one
  proves by induction on |n| that |n + zero = n|, this only holds definitionally
  for closed |n|.  In our case the only induction is over codes |gamma| and we
  always assume |gamma| to be closed. The formalisation can be downloaded from
  the author's webpage~\cite{norell:iird-formal}.
  
  \section{Conclusions} \label{sec-concl}
  
  We have shown that the theory of generalised indexed inductive definitions can
  be interpreted in the theory of restricted indexed inductive definitions
  extended with an intensional identity type. The informal proof presented here
  has been formalised in Agda using a light-weight approach where Agda is used
  both for the object language and the meta language.
  
  This result gives way of adding generalised IID to theories with only
  restricted IID, such as Agda, without having to extend the meta-theory.
  
  \bibliographystyle{abbrv}
  \bibliography{../../../../bib/pmgrefs,iird}
  
  \end{document}
  
  % vim: et
  