@phdthesis{sterling_2021,
  doi = {10.5281/ZENODO.5709838},
  url = {https://zenodo.org/record/5709838},
  author = {Sterling, Jonathan},
  keywords = {homotopy type theory, type theory, computer science, logic, topos theory},
  language = {en},
  title = {First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory},
  publisher = {Zenodo},
  year = {2021},
  copyright = {Creative Commons Attribution 4.0 International},
  school = {Carnegie Mellon University}
}