+}
+
+@article{dybjer1997representing,
+ title={Representing inductively defined sets by wellorderings in Martin-L{\"o}f's type theory},
+ author={Dybjer, Peter},
+ journal={Theoretical Computer Science},
+ volume={176},
+ number={1},
+ pages={329--335},
+ year={1997},
+ publisher={Elsevier}
+}
+
+@inbook{Nordstrom1990,
+ author = {Nordstr{\"o}m, Bengt and Petersson, Kent and Smith, Jan M.},
+ title = {Programming in Martin-L{\"o}f Type Theory: An Introduction},
+ publisher = {Oxford University Press},
+ year = {1990}
+}