biblio.bib

@article{UFP2010,
    author = {Vladimir Voevodsky},
    title = {Univalent Foundations Project},
    year = {2010},
	language={english},
	hyphenation={english}
}

@book{hottbook,
  	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},
	language={english},
	hyphenation={english}
}

@article{MLTT,
    author = {Per Martin-Löf},
    title = {An intuitionistic theory of types},
    year = {1972},
	language={english},
	hyphenation={english}
}

@article{CohenCHM16,
  	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},
  	archivePrefix = {arXiv},
  	eprint    = {1611.02108},
  	timestamp = {Mon, 13 Aug 2018 16:48:16 +0200},
  	biburl    = {https://dblp.org/rec/bib/journals/corr/CohenCHM16},
  	bibsource = {dblp computer science bibliography, https://dblp.org},
	language={english},
	hyphenation={english}
}

@online{Grp1,
	title = {groupoid/arend},
	url = {https://github.com/groupoid/arend},
	language={english},
	hyphenation={english}
}

@online{Fiber,
	title = {Fiber.ard},
	url = {https://github.com/groupoid/arend/blob/master/src/Fiber.ard},
	language={english},
	hyphenation={english}
}

@online{Moebius,
	title = {Moebius.ard},
	url = {https://github.com/groupoid/arend/blob/master/src/Moebius.ard},
	language={english},
	hyphenation={english}
}

@online{nlab,
  	author = {{nLab authors}},
  	title = {ncatlab},
  	howpublished = {\url{http://ncatlab.org/}},
  	note = {\href{http://ncatlab.org/nlab/revision/HomePage/276}{Revision 276}},
  	month = may,
  	year = 2019,
	language={english},
	hyphenation={english}
}

@article{SyntheticHT,
  	author = {R. Licata, Daniel and Brunerie, Guillaume},
  	year = {2015},
  	month = {07},
  	pages = {92-103},
  	title = {A Cubical Approach to Synthetic Homotopy Theory},
  	doi = {10.1109/LICS.2015.19},
	language={english},
	hyphenation={english}
}

@online{Arend,
	title = {JetBrains/arend},
	url = {https://github.com/JetBrains/arend},
	language={english},
	hyphenation={english}
}

@article{Doorn1,
  	author = {van Doorn, Floris},
  	year = {2018},
  	pages = {},
  	title = {On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory},
	language={english},
	hyphenation={english}
}

@article{Wellen1,
	author = {Felix Wellen},
  	year = {2017},
  	pages = {},
  	title = {Formalizing Cartan Geometry in Modal Homotopy Type Theory},
  	language={english},
	hyphenation={english}
}

@article{Warren1,
	author = {Álvaro Pelayo, Michael A. Warren},
  	year = {2012},
  	pages = {},
  	title = {Homotopy type theory and Voevodsky's univalent foundations},
  	language={english},
	hyphenation={english}
}

@article{ProofAssistants1,
	author = {Geuvers, Herman},
	year = {2009},
	pages = {3-25},
	title = {Proof assistants: History, ideas and future},
	volume = {34},
	journal = {Sadhana},
	doi = {10.1007/s12046-009-0001-5},
	language={english},
	hyphenation={english}
}

@online{Coq,
	title = {Coq},
	url = {https://coq.inria.fr},
	language={english},
	hyphenation={english}
}

@online{Agda,
	title = {Agda},
	url = {https://github.com/agda/agda},
	language={english},
	hyphenation={english}
}

@online{Cubicaltt,
	title = {cubicaltt},
	url = {https://github.com/mortberg/cubicaltt},
	language={english},
	hyphenation={english}
}

@online{Redtt,
	title = {redtt},
	url = {https://github.com/RedPRL/redtt},
	language={english},
	hyphenation={english}
}

@online{Arenddocs,
	title = {Arend reference},
	url = {https://arend.readthedocs.io},
	language={english},
	hyphenation={english}
}