@article{cohen-2016,
  author    = {Cyril Cohen and
               Thierry Coquand and
               Simon Huber and
               Anders M{\"{o}}rtberg},
  title     =
    { Cubical Type Theory:
      a constructive interpretation of the univalence axiom
    },
  journal   = {CoRR},
  volume    = {abs/1611.02108},
  year      = {2016},
  url       = {http://arxiv.org/abs/1611.02108},
  timestamp = {Thu, 01 Dec 2016 19:32:08 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/CohenCHM16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@book{hott-2013,
  author =    {The {Univalent Foundations Program}},
  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{https://homotopytypetheory.org/book}},
  address =   {Institute for Advanced Study},
  year =      2013
}
@book{awodey-2006,
  title={Category Theory},
  author={Awodey, S.},
  isbn={9780191513824},
  series={Oxford Logic Guides},
  url={https://books.google.se/books?id=IK\_sIDI2TCwC},
  year={2006},
  publisher={Ebsco Publishing}
}
@misc{cubical-demo,
  author = {Andrea Vezzosi},
  title = {Cubical Type Theory Demo},
  year = {2017},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/Saizan/cubical-demo}},
  commit = {a51d5654c439111110d5b6df3605b0043b10b753}
}
@misc{cubical-agda,
  author = {Andrea Vezzosi},
  title = {Cubical Extension to Agda},
  year = {2017},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/agda/agda}},
  commit = {92de32c0669cb414f329fff25497a9ddcd58b951}
}
@misc{agda,
  author = {Ulf Norell},
  title = {Agda},
  year = {2017},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/agda/agda}},
  commit = {92de32c0669cb414f329fff25497a9ddcd58b951}
}
@inproceedings{bezem-2014,
  title={A model of type theory in cubical sets},
  author={Bezem, Marc and Coquand, Thierry and Huber, Simon},
  booktitle={19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  volume={26},
  pages={107--128},
  year={2014}
}
@article{coquand-2013,
  title={Isomorphism is equality},
  author={Coquand, Thierry and Danielsson, Nils Anders},
  journal={Indagationes Mathematicae},
  volume={24},
  number={4},
  pages={1105--1120},
  year={2013},
  publisher={Elsevier}
}
@inproceedings{dybjer-1995,
  title={Internal type theory},
  author={Dybjer, Peter},
  booktitle={International Workshop on Types for Proofs and Programs},
  pages={120--134},
  year={1995},
  organization={Springer}
}
@inproceedings{voevodsky-2011,
  title={Univalent foundations of mathematics},
  author={Voevodsky, Vladimir},
  booktitle={International Workshop on Logic, Language, Information, and Computation},
  pages={4--4},
  year={2011},
  organization={Springer}
}
@article{huber-2016,
  title={Cubical Intepretations of Type Theory},
  author={Huber, Simon},
  year={2016}
}
@article{hofmann-1995,
  title={Extensional concepts in intensional type theory},
  author={Hofmann, Martin},
  year={1995},
  publisher={University of Edinburgh. College of Science and Engineering. School of Informatics.}
}
@MISC{mo-formalizations,
    TITLE = {Formalizations of category theory in proof assistants},
    AUTHOR = {Jason Gross},
    NOTE = {Version: 2014-01-19},
    year={2014},
    EPRINT = {\url{https://mathoverflow.net/q/152497}},
    url = {https://mathoverflow.net/q/152497},
    howpublished = {MathOverflow: \url{https://mathoverflow.net/q/152497}}
}
@Misc{UniMath,
    author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
    title = {{UniMath --- a computer-checked library of univalent mathematics}},
    url = {https://github.com/UniMath/UniMath},
    howpublished = {{available} at \url{https://github.com/UniMath/UniMath}}
}