@article{Dybjer1994,
    Abstract = {A general formulation of inductive and recursive definitions in Martin-L{\"o}f's type theory is presented. It extends Backhouse's `Do-It-Yourself Type Theory' to include inductive definitions of families of sets and definitions of functions by recursion on the way elements of such sets are generated. The formulation is in natural deduction and is intended to be a natural generalisation to type theory of Martin-L{\"o}f's theory of iterated inductive definitions in predicate logic.},
    Author = {Dybjer, Peter},
    File = {Inductive\_Families (0) (0) - a - a - y.pdf},
    ISSN = {1433-299X},
    Journal = {Formal Aspects of Computing},
    Keywords = {readme},
    Month = {Jul},
    Number = {4},
    Pages = {440--465},
    Title = {Inductive families},
    URL = {https://doi.org/10.1007/BF01211308},
    Volume = {6},
    Year = {1994},
    bdsk-url-1 = {https://doi.org/10.1007/BF01211308},
    date-added = {2019-03-21 20:14:58 +0100},
    date-modified = {2019-03-21 20:15:10 +0100},
    day = {01},
    doi = {10.1007/BF01211308}
}

@article{Dybjer1994, Abstract = {A general formulation of inductive and recursive definitions in Martin-L{\"o}f's type theory is presented. It extends Backhouse's `Do-It-Yourself Type Theory' to include inductive definitions of families of sets and definitions of functions by recursion on the way elements of such sets are generated. The formulation is in natural deduction and is intended to be a natural generalisation to type theory of Martin-L{\"o}f's theory of iterated inductive definitions in predicate logic.}, Author = {Dybjer, Peter}, File = {Inductive_Families (0) (0) - a - a - y.pdf}, ISSN = {1433-299X}, Journal = {Formal Aspects of Computing}, Keywords = {readme}, Month = {Jul}, Number = {4}, Pages = {440--465}, Title = {Inductive families}, URL = {https://doi.org/10.1007/BF01211308}, Volume = {6}, Year = {1994}, bdsk-url-1 = {https://doi.org/10.1007/BF01211308}, date-added = {2019-03-21 20:14:58 +0100}, date-modified = {2019-03-21 20:15:10 +0100}, day = {01}, doi = {10.1007/BF01211308} }