@article{daniel_r_licata_2-dimensional_2011,
	title = {2-{Dimensional} {Directed} {Type} {Theory}},
	volume = {276},
	copyright = {https://www.elsevier.com/tdm/userlicense/1.0/},
	issn = {15710661},
	url = {https://linkinghub.elsevier.com/retrieve/pii/S1571066111001174},
	doi = {10.1016/j.entcs.2011.09.026},
	language = {en},
	urldate = {2024-10-08},
	journal = {Electronic Notes in Theoretical Computer Science},
	author = {{Daniel R. Licata} and {Robert Harper}},
	month = sep,
	year = {2011},
	keywords = {Directed Type Theory},
	pages = {263--289},
	file = {PDF:/Users/eakubilo/Zotero/storage/S2RZ3IXU/Licata and Harper - 2011 - 2-Dimensional Directed Type Theory.pdf:application/pdf},
}

@article{licata_internal_2018,
	title = {Internal {Universes} in {Models} of {Homotopy} {Type} {Theory}},
	volume = {108},
	issn = {1868-8969},
	url = {http://arxiv.org/abs/1801.07664},
	doi = {10.4230/LIPIcs.FSCD.2018.22},
	abstract = {We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the CohenCoquand-Huber-Mörtberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny—a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.},
	language = {en},
	urldate = {2024-10-08},
	journal = {LIPIcs, Volume 108, FSCD 2018},
	author = {Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas},
	year = {2018},
	note = {arXiv:1801.07664 [cs]},
	keywords = {Computer Science - Logic in Computer Science, F.3.2, F.4.1},
	pages = {22:1--22:17},
	annote = {Comment: In H. Kirchner (ed), Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108, pp. 22:1-22:17, 2018},
	file = {PDF:/Users/eakubilo/Zotero/storage/Z5URS88A/Licata et al. - 2018 - Internal Universes in Models of Homotopy Type Theory.pdf:application/pdf},
}




@article{g_a_kavvos_quantum_nodate,
	title = {A {QUANTUM} {OF} {DIRECTION}},
	abstract = {I argue that the correct primitives for abstract directed homotopy theory have not yet been identified. This assertion is corroborated by examining the directed structure of small categories qua directed homotopy 1-types.},
	language = {en},
	author = {{G A Kavvos}},
	file = {PDF:/Users/eakubilo/Zotero/storage/BGMTE3IG/Kavvos - A QUANTUM OF DIRECTION.pdf:application/pdf},
}

@misc{gratzer_directed_2024,
	title = {Directed univalence in simplicial homotopy type theory},
	url = {http://arxiv.org/abs/2407.09146},
	doi = {10.48550/arXiv.2407.09146},
	abstract = {Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics -- where it allows for synthetic (higher) category theory -- and programming languages -- where it leads to a directed version of the structure identity principle. In this work, we construct the first types in simplicial type theory with non-trivial homomorphisms. We extend simplicial type theory with modalities and new reasoning principles to obtain triangulated type theory in order to construct the universe of discrete types \${\textbackslash}mathcal\{S\}\$. We prove that homomorphisms in this type correspond to ordinary functions of types i.e., that \${\textbackslash}mathcal\{S\}\$ is directed univalent. The construction of \${\textbackslash}mathcal\{S\}\$ is foundational for both of the aforementioned applications of simplicial type theory. We are able to define several crucial examples of categories and to recover important results from category theory. Using \${\textbackslash}mathcal\{S\}\$, we are also able to define various types whose usage is guaranteed to be functorial. These provide the first complete examples of the proposed directed structure identity principle.},
	language = {en},
	urldate = {2024-11-22},
	publisher = {arXiv},
	author = {Gratzer, Daniel and Weinberger, Jonathan and Buchholtz, Ulrik},
	month = jul,
	year = {2024},
	note = {arXiv:2407.09146 [cs]},
	keywords = {Computer Science - Logic in Computer Science, Mathematics - Category Theory, Mathematics - Algebraic Topology},
	file = {PDF:/Users/eakubilo/Zotero/storage/J6N4JS2C/Gratzer et al. - 2024 - Directed univalence in simplicial homotopy type theory.pdf:application/pdf;Snapshot:/Users/eakubilo/Zotero/storage/DLSTPQR2/2407.html:text/html},
}

@inproceedings{matthew_z_weaver_constructive_2020,
	address = {Saarbrücken Germany},
	title = {A {Constructive} {Model} of {Directed} {Univalence} in {Bicubical} {Sets}},
	isbn = {978-1-4503-7104-9},
	url = {https://dl.acm.org/doi/10.1145/3373718.3394794},
	doi = {10.1145/3373718.3394794},
	abstract = {Directed type theory is an analogue of homotopy type theory where types represent categories, generalizing groupoids. A bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based on equipping each type with both a notion of path and a separate notion of directed morphism. In this setting, a directed analogue of the univalence axiom asserts that there is a universe of covariant discrete  brations whose directed morphisms correspond to functions—a higher-categorical analogue of the category of sets and functions. In this paper, we give a constructive model of a directed type theory with directed univalence in bicubical, rather than bisimplicial, sets. We formalize much of this model using Agda as the internal language of a 1-topos, following Orton and Pitts. First, building on the cubical techniques used to give computational models of homotopy type theory, we show that there is a universe of covariant discrete  brations, with a partial directed univalence principle asserting that functions are a retract of morphisms in this universe. To complete this retraction into an equivalence, we re ne the universe of covariant  brations using the constructive sheaf models by Coquand and Ruch.},
	language = {en},
	urldate = {2024-11-22},
	booktitle = {Proceedings of the 35th {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science}},
	publisher = {ACM},
	author = {{Matthew Z. Weaver} and {Daniel R. Licata}},
	month = jul,
	year = {2020},
	keywords = {Bicubical Directed Type Theory},
	pages = {915--928},
	file = {PDF:/Users/eakubilo/Zotero/storage/4KH8779V/Weaver and Licata - 2020 - A Constructive Model of Directed Univalence in Bicubical Sets.pdf:application/pdf},
}


@article{north_towards_2019,
	title = {Towards a {Directed} {Homotopy} {Type} {Theory}},
	volume = {347},
	issn = {15710661},
	url = {https://linkinghub.elsevier.com/retrieve/pii/S1571066119301288},
	doi = {10.1016/j.entcs.2019.09.012},
	abstract = {In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new ‘homomorphism’ type former for Martin-L¨of type theory which is roughly analogous to the identity type former originally introduced by Martin-Lo¨f. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type homC(a, b) is indeed the set of morphisms between the objects a and b of the category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-L¨of’s identity types.},
	language = {en},
	urldate = {2024-11-22},
	journal = {Electronic Notes in Theoretical Computer Science},
	author = {North, Paige Randall},
	month = nov,
	year = {2019},
	keywords = {dependent type theory, directed homotopy theory, semantics of type theory},
	pages = {223--239},
	file = {PDF:/Users/eakubilo/Zotero/storage/JQVMYWJK/North - 2019 - Towards a Directed Homotopy Type Theory.pdf:application/pdf;ScienceDirect Snapshot:/Users/eakubilo/Zotero/storage/J5TZWVSI/S1571066119301288.html:text/html;Submitted Version:/Users/eakubilo/Zotero/storage/R75LH4AE/North - 2019 - Towards a Directed Homotopy Type Theory.pdf:application/pdf},
}

@article{vezzosi_cubical_2021,
	title = {Cubical {Agda}: {A} dependently typed programming language with univalence and higher inductive types},
	volume = {31},
	issn = {0956-7968, 1469-7653},
	shorttitle = {Cubical {Agda}},
	url = {https://www.cambridge.org/core/product/identifier/S0956796821000034/type/journal_article},
	doi = {10.1017/S0956796821000034},
	abstract = {Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types (HITs). This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of HITs. These new primitives allow the direct definition of function and propositional extensionality as well as quotient types, all with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. The adoption of cubical type theory extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.},
	language = {en},
	urldate = {2024-11-22},
	journal = {Journal of Functional Programming},
	author = {Vezzosi, Andrea and Mörtberg, Anders and Abel, Andreas},
	year = {2021},
	pages = {e8},
	file = {PDF:/Users/eakubilo/Zotero/storage/J5FCUMCG/Vezzosi et al. - 2021 - Cubical Agda A dependently typed programming language with univalence and higher inductive types.pdf:application/pdf},
}


@article{martin-lof_intuitionistic_nodate,
	title = {Intuitionistic {Type} {Theory}},
	language = {en},
	author = {Martin-Lof, Per},
	file = {PDF:/Users/eakubilo/Zotero/storage/AAVC46DL/Martin-Lof - Intuitionistic Type Theory.pdf:application/pdf},
}

@article{riehl_directed_nodate,
	title = {On the directed univalence axiom   joint with {Evan} {Cavallo} and {Christian} {Sattler} - {AMS} {Special} {Session} on {Homotopy} {Type} {Theory}, {Joint} {Mathematics} {Meetings}},
	language = {en},
	author = {Riehl, Emily},
	file = {PDF:/Users/eakubilo/Zotero/storage/CQ54Z2UU/Riehl - On the directed univalence axiom   joint with Evan Cavallo and Christian Sattler - AMS Special Sessi.pdf:application/pdf},
}

@misc{buchholtz_synthetic_2022,
	title = {Synthetic fibered \$({\textbackslash}infty,1)\$-category theory},
	url = {http://arxiv.org/abs/2105.01724},
	doi = {10.48550/arXiv.2105.01724},
	abstract = {We study cocartesian fibrations in the setting of the synthetic \$({\textbackslash}infty,1)\$-category theory developed in the simplicial type theory introduced by Riehl and Shulman. Our development culminates in a Yoneda Lemma for cocartesian fibrations.},
	urldate = {2024-11-22},
	publisher = {arXiv},
	author = {Buchholtz, Ulrik and Weinberger, Jonathan},
	month = aug,
	year = {2022},
	note = {arXiv:2105.01724},
	keywords = {Computer Science - Logic in Computer Science, Mathematics - Category Theory, Mathematics - Logic, Mathematics - Algebraic Topology},
	file = {Preprint PDF:/Users/eakubilo/Zotero/storage/7AAD8QTT/Buchholtz and Weinberger - 2022 - Synthetic fibered \$(infty,1)\$-category theory.pdf:application/pdf;Snapshot:/Users/eakubilo/Zotero/storage/W4PYTVSC/2105.html:text/html},
}


@article{weaver_bicubical_nodate,
	title = {Bicubical {Directed} {Type} {Theory}},
	language = {en},
	author = {Weaver, Matthew Zachary},
	file = {PDF:/Users/eakubilo/Zotero/storage/Y5NW7568/Weaver - Bicubical Directed Type Theory.pdf:application/pdf},
}

@article{awodey_voevodskys_2013,
	title = {Voevodsky’s {Univalence} {Axiom} in {Homotopy} {Type} {Theory}},
	volume = {60},
	issn = {0002-9920, 1088-9477},
	url = {http://www.ams.org/jourcgi/jour-getitem?pii=noti1043},
	doi = {10.1090/noti1043},
	language = {en},
	number = {09},
	urldate = {2024-11-22},
	journal = {Notices of the American Mathematical Society},
	author = {Awodey, Steve and Pelayo, Álvaro and Warren, Michael A.},
	month = oct,
	year = {2013},
	pages = {1164},
	file = {PDF:/Users/eakubilo/Zotero/storage/C4VKY956/Awodey et al. - 2013 - Voevodsky’s Univalence Axiom in Homotopy Type Theory.pdf:application/pdf},
}

@misc{kudasov_formalizing_2023,
	title = {Formalizing the \${\textbackslash}infty\$-{Categorical} {Yoneda} {Lemma}},
	url = {http://arxiv.org/abs/2309.08340},
	doi = {10.48550/arXiv.2309.08340},
	abstract = {Formalized \$1\$-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have "higher structure," rely on infinite-dimensional categories in place of \$1\$-dimensional categories, and \${\textbackslash}infty\$-category theory has thusfar proved unamenable to computer formalization. Using a new proof assistant called Rzk, which is designed to support Riehl-Shulman's simplicial extension of homotopy type theory for synthetic \${\textbackslash}infty\$-category theory, we provide the first formalizations of results from \${\textbackslash}infty\$-category theory. This includes in particular a formalization of the Yoneda lemma, often regarded as the fundamental theorem of category theory, a theorem which roughly states that an object of a given category is determined by its relationship to all of the other objects of the category. A key feature of our framework is that, thanks to the synthetic theory, many constructions are automatically natural or functorial. We plan to use Rzk to formalize further results from \${\textbackslash}infty\$-category theory, such as the theory of limits and colimits and adjunctions.},
	urldate = {2024-11-22},
	publisher = {arXiv},
	author = {Kudasov, Nikolai and Riehl, Emily and Weinberger, Jonathan},
	month = dec,
	year = {2023},
	note = {arXiv:2309.08340},
	keywords = {Computer Science - Logic in Computer Science, Mathematics - Category Theory, Mathematics - Logic, Mathematics - Algebraic Topology},
	file = {Preprint PDF:/Users/eakubilo/Zotero/storage/ZB8XFRF9/Kudasov et al. - 2023 - Formalizing the \$infty\$-Categorical Yoneda Lemma.pdf:application/pdf;Snapshot:/Users/eakubilo/Zotero/storage/6NXL2PFI/2309.html:text/html},
}

@misc{ahrens_bicategorical_2023,
	title = {Bicategorical type theory: semantics and syntax},
	shorttitle = {Bicategorical type theory},
	url = {http://arxiv.org/abs/2201.10662},
	doi = {10.48550/arXiv.2201.10662},
	abstract = {We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.},
	urldate = {2024-11-22},
	publisher = {arXiv},
	author = {Ahrens, Benedikt and North, Paige Randall and Weide, Niels van der},
	month = oct,
	year = {2023},
	note = {arXiv:2201.10662},
	keywords = {Computer Science - Logic in Computer Science, Mathematics - Category Theory},
	file = {Preprint PDF:/Users/eakubilo/Zotero/storage/JDI8YNZL/Ahrens et al. - 2023 - Bicategorical type theory semantics and syntax.pdf:application/pdf;Snapshot:/Users/eakubilo/Zotero/storage/7QCZQVSF/2201.html:text/html},
}

@misc{weinberger_internal_2024,
	title = {Internal sums for synthetic fibered \$({\textbackslash}infty,1)\$-categories},
	url = {http://arxiv.org/abs/2205.00386},
	doi = {10.48550/arXiv.2205.00386},
	abstract = {We give structural results about bifibrations of (internal) \$({\textbackslash}infty,1)\$-categories with internal sums. This includes a higher version of Moens' Theorem, characterizing cartesian bifibrations with extensive aka stable and disjoint internal sums over lex bases as Artin gluings of lex functors. We also treat a generalized version of Moens' Theorem due to Streicher which does not require the Beck--Chevalley condition. Furthermore, we show that also in this setting the Moens fibrations can be characterized via a condition due to Zawadowski. Our account overall follows Streicher's presentation of fibered category theory {\textbackslash}`\{a\} la B{\textbackslash}'\{e\}nabou, generalizing the results to the internal, higher-categorical case, formulated in a synthetic setting. Namely, we work inside simplicial homotopy type theory, which has been introduced by Riehl and Shulman as a logical system to reason about internal \$({\textbackslash}infty,1)\$-categories, interpreted as Rezk objects in any given Grothendieck--Rezk--Lurie \$({\textbackslash}infty,1)\$-topos.},
	urldate = {2024-11-22},
	publisher = {arXiv},
	author = {Weinberger, Jonathan},
	month = mar,
	year = {2024},
	note = {arXiv:2205.00386},
	keywords = {Computer Science - Logic in Computer Science, Mathematics - Category Theory, Mathematics - Logic, Mathematics - Algebraic Topology},
	file = {Preprint PDF:/Users/eakubilo/Zotero/storage/KM7VL5QH/Weinberger - 2024 - Internal sums for synthetic fibered \$(infty,1)\$-categories.pdf:application/pdf;Snapshot:/Users/eakubilo/Zotero/storage/APIJLJL5/2205.html:text/html},
}


@misc{program_homotopy_2013,
	title = {Homotopy {Type} {Theory}: {Univalent} {Foundations} of {Mathematics}},
	shorttitle = {Homotopy {Type} {Theory}},
	url = {http://arxiv.org/abs/1308.0729},
	doi = {10.48550/arXiv.1308.0729},
	abstract = {Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.},
	urldate = {2024-11-25},
	publisher = {arXiv},
	author = {Program, The Univalent Foundations},
	month = aug,
	year = {2013},
	note = {arXiv:1308.0729},
	keywords = {Mathematics - Category Theory, Mathematics - Logic, Mathematics - Algebraic Topology, Computer Science - Programming Languages},
	file = {Preprint PDF:/Users/eakubilo/Zotero/storage/Y3EWL5LE/Program - 2013 - Homotopy Type Theory Univalent Foundations of Mathematics.pdf:application/pdf;Snapshot:/Users/eakubilo/Zotero/storage/ZLFG5N8Y/1308.html:text/html},
}

@article{riehl_type_2017,
	title = {A type theory for synthetic $\infty$-categories},
	volume = {1},
	url = {http://articles.math.cas.cz/10.21136/HS.2017.06},
	doi = {10.21136/HS.2017.06},
	abstract = {We propose foundations for a synthetic theory of ($\infty$, 1)-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define Segal types, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities — a “local univalence” condition. And we define covariant fibrations, which are type families varying functorially over a Segal type, and prove a “dependent Yoneda lemma” that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition.},
	language = {en},
	number = {1},
	urldate = {2024-12-02},
	journal = {Higher Structures},
	author = {Riehl, Emily and Shulman, Michael},
	month = dec,
	year = {2017},
	pages = {147--224},
	file = {PDF:/Users/eakubilo/Zotero/storage/KCQ4C6EP/Riehl and Shulman - 2017 - A type theory for synthetic $\infty$-categories.pdf:application/pdf},
}
@article{berg_garner_richard,
    author = {van den Berg, Benno and Garner, Richard},
    title = {Types are weak $\omega$-groupoids},
    journal = {Proceedings of the London Mathematical Society},
    volume = {102},
    number = {2},
    pages = {370-394},
    year = {2010},
    month = {10},
    abstract = {We define a notion of weak $\omega$-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak $\omega$-category structure obtained from the tower of iterated identity types over that type. We show that the $\omega$-categories arising in this way are in fact $\omega$-groupoids.},
    issn = {0024-6115},
    doi = {10.1112/plms/pdq026},
    url = {https://doi.org/10.1112/plms/pdq026},
    eprint = {https://academic.oup.com/plms/article-pdf/102/2/370/4487337/pdq026.pdf},
}

@inproceedings{wadler1989theorems,
  title={Theorems for free!},
  author={Wadler, Philip},
  booktitle={Proceedings of the fourth international conference on Functional programming languages and computer architecture},
  pages={347--359},
  year={1989}
}


@article{hofmann1998groupoid,
  title={The groupoid interpretation of type theory},
  author={Hofmann, Martin and Streicher, Thomas},
  journal={Twenty-five years of constructive type theory (Venice, 1995)},
  volume={36},
  pages={83--111},
  year={1998}
}
@book{martin1984intuitionistic,
  title={Intuitionistic type theory},
  author={Martin-L{\"o}f, Per and Sambin, Giovanni},
  volume={9},
  year={1984},
  publisher={Bibliopolis Naples}
}

@phdthesis{nuyts2015towards,
  title={Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance.(2015)},
  author={Nuyts, Andreas},
  year={2015},
  school={Master thesis, available online at https://distrinet. cs. kuleuven. be~…}
}

@inproceedings{licata_shulman_fundamental,
author = {Licata, Daniel R. and Shulman, Michael},
title = {Calculating the Fundamental Group of the Circle in Homotopy Type Theory},
year = {2013},
isbn = {9780769550206},
publisher = {IEEE Computer Society},
address = {USA},
url = {https://doi.org/10.1109/LICS.2013.28},
doi = {10.1109/LICS.2013.28},
abstract = {Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.},
booktitle = {Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science},
pages = {223–232},
numpages = {10},
series = {LICS '13}
}
@misc{rijke2022introductionhomotopytypetheory,
      title={Introduction to Homotopy Type Theory}, 
      author={Egbert Rijke},
      year={2022},
      eprint={2212.11082},
      archivePrefix={arXiv},
      primaryClass={math.LO},
      url={https://arxiv.org/abs/2212.11082}, 
}
@inproceedings{Warren2008HomotopyTA,
  title={Homotopy Theoretic Aspects of Constructive Type Theory},
  author={M Warren},
  year={2008},
  url={https://api.semanticscholar.org/CorpusID:123575477}
}
@misc{kapulkin2018simplicialmodelunivalentfoundations,
      title={The Simplicial Model of Univalent Foundations (after Voevodsky)}, 
      author={Chris Kapulkin and Peter LeFanu Lumsdaine},
      year={2018},
      eprint={1211.2851},
      archivePrefix={arXiv},
      primaryClass={math.LO},
      url={https://arxiv.org/abs/1211.2851}, 
}
@article{Gambino_2008,
   title={The identity type weak factorisation system},
   volume={409},
   ISSN={0304-3975},
   url={http://dx.doi.org/10.1016/j.tcs.2008.08.030},
   DOI={10.1016/j.tcs.2008.08.030},
   number={1},
   journal={Theoretical Computer Science},
   publisher={Elsevier BV},
   author={Gambino, Nicola and Garner, Richard},
   year={2008},
   month=dec, pages={94–109} }
@article{AWODEY_2009,
   title={Homotopy theoretic models of identity types},
   volume={146},
   ISSN={1469-8064},
   url={http://dx.doi.org/10.1017/S0305004108001783},
   DOI={10.1017/s0305004108001783},
   number={1},
   journal={Mathematical Proceedings of the Cambridge Philosophical Society},
   publisher={Cambridge University Press (CUP)},
   author={AWODEY, STEVE and WARREN, MICHAEL A.},
   year={2009},
   month=jan, pages={45–55} }