120 lines
3.8 KiB
BibTeX
120 lines
3.8 KiB
BibTeX
@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}}
|
|
} |