@inproceedings{Altenkirch,
    doi = {10.1109/lics.1999.782636},
    url = {https://doi.org/10.1109%2Flics.1999.782636},
    publisher = {{IEEE} Comput. Soc},
    author = {T. Altenkirch},
    title = {Extensional equality in intensional type theory},
    booktitle = {Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. {PR}00158)}
}

@inproceedings{Altenkirch, doi = {10.1109/lics.1999.782636}, url = {https://doi.org/10.1109%2Flics.1999.782636}, publisher = {{IEEE} Comput. Soc}, author = {T. Altenkirch}, title = {Extensional equality in intensional type theory}, booktitle = {Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. {PR}00158)} }