bibliography.bib

@InProceedings{Acz12,
  title =        {On Voevodsky's Univalence Axiom},
  author =       {Peter Aczel},
  booktitle =    {Mathematical Logic: Proof Theory, Constructive
                  Mathematics},
  volume =       8,
  ISSN =         {1660-8941},
  url =          {http://dx.doi.org/10.4171/OWR/2011/52},
  DOI =          {10.4171/owr/2011/52},
  number =       4,
  journal =      {Oberwolfach Reports},
  publisher =    {European Mathematical Society - EMS - Publishing
                  House GmbH},
  editors =      {Buss, Samuel R. and Kohlenbach, Ulrich and Rathjen,
                  Michael},
  year =         2012,
  month =        7,
  pages =        {2963–3002}
}

@Article{AGMV11,
  title =        {Mini-Workshop: The Homotopy Interpretation of
                  Constructive Type Theory},
  volume =       8,
  ISSN =         {1660-8941},
  url =          {http://dx.doi.org/10.4171/OWR/2011/11},
  DOI =          {10.4171/owr/2011/11},
  number =       1,
  journal =      {Oberwolfach Reports},
  publisher =    {European Mathematical Society - EMS - Publishing
                  House GmbH},
  author =       {Awodey, Steve and Garner, Richard and
                  Martin-L\"{o}f, Per and Voevodsky, Vladimir},
  year =         2011,
  month =        sep,
  pages =        {609–638}
}

@InProceedings{AGS12,
  author =       {Awodey, Steve and Gambino, Nicola and Sojakova,
                  Kristina},
  title =        {Inductive Types in Homotopy Type Theory},
  year =         2012,
  isbn =         9780769547695,
  publisher =    {IEEE Computer Society},
  address =      {USA},
  url =          {https://doi.org/10.1109/LICS.2012.21},
  doi =          {10.1109/LICS.2012.21},
  abstract =     {Homotopy type theory is an interpretation of
                  Martin-L\"{o}f's constructive type theory into
                  abstract homotopy theory. There results a link
                  between constructive mathematics and algebraic
                  topology, providing topological semantics for
                  intensional systems of type theory as well as a
                  computational approach to algebraic topology via
                  type theory-based proof assistants such as Coq. The
                  present work investigates inductive types in this
                  setting. Modified rules for inductive types,
                  including types of well-founded trees, or W-types,
                  are presented, and the basic homotopical semantics
                  of such types are determined. Proofs of all results
                  have been formally verified by the Coq proof
                  assistant, and the proof scripts for this
                  verification form an essential component of this
                  research.},
  booktitle =    {Proceedings of the 2012 27th Annual IEEE/ACM
                  Symposium on Logic in Computer Science},
  pages =        {95–104},
  numpages =     10,
  keywords =     {initial algebras, homotopy theory, Type theory},
  location =     {New Orleans, Louisiana},
  series =       {LICS '12}
}

@Software{Agda,
  author =       {{Agda Developers}},
  year =         2024,
  title =        {{Agda}},
  url =          {https://agda.readthedocs.io/},
  version =      {2.6.4},
  accessed =     2024
}

@Thesis{Bru16,
  title =        {On the homotopy groups of spheres in homotopy type
                  theory},
  author =       {Guillaume Brunerie},
  type =         {phdthesis},
  institution =  {Laboratoire Jean-Alexandre Dieudonné},
  year =         2016,
  eprint =       {1606.05916},
  archivePrefix ={arXiv},
  primaryClass = {math.AT},
  url =          {https://arxiv.org/abs/1606.05916},
}

@Misc{BW22,
  title =        {Synthetic fibered $(\infty,1)$-category theory},
  author =       {Ulrik Buchholtz and Jonathan Weinberger},
  year =         2022,
  eprint =       {2105.01724},
  archivePrefix ={arXiv},
  primaryClass = {math.CT}
}

@Article{Doe98,
  author =       {Doeraene, Jean-Paul},
  year =         1998,
  month =        01,
  title =        {Homotopy pull backs, homotopy push outs and joins},
  volume =       5,
  journal =      {Bulletin of the Belgian Mathematical Society - Simon
                  Stevin},
  doi =          {10.36045/bbms/1103408963}
}

@InProceedings{Hur95,
  author =       {Hurkens, Antonius J. C.},
  title =        {A Simplification of Girard's Paradox},
  year =         1995,
  isbn =         {354059048X},
  publisher =    {Springer-Verlag},
  address =      {Berlin, Heidelberg},
  booktitle =    {Proceedings of the Second International Conference
                  on Typed Lambda Calculi and Applications},
  pages =        {266–278},
  numpages =     13,
  series =       {TLCA '95}
}

@InProceedings{KvR19,
  author =       {Kraus, Nicolai and von Raumer, Jakob},
  title =        {Path spaces of higher inductive types in homotopy
                  type theory},
  year =         2019,
  publisher =    {IEEE Press},
  abstract =     {The study of equality types is central to homotopy
                  type theory. Characterizing these types is often
                  tricky, and various strategies, such as the
                  encode-decode method, have been developed.We prove a
                  theorem about equality types of coequalizers and
                  pushouts, reminiscent of an induction principle and
                  without any restrictions on the truncation levels.
                  This result makes it possible to reason directly
                  about certain equality types and to streamline
                  existing proofs by eliminating the necessity of
                  auxiliary constructions.To demonstrate this, we give
                  a very short argument for the calculation of the
                  fundamental group of the circle (Licata and Shulman
                  [1]), and for the fact that pushouts preserve
                  embeddings. Further, our development suggests a
                  higher version of the Seifert-van Kampen theorem,
                  and the set-truncation operator maps it to the
                  standard Seifert-van Kampen theorem (due to Favonia
                  and Shulman [2]).We provide a formalization of the
                  main technical results in the proof assistant Lean.},
  booktitle =    {Proceedings of the 34th Annual ACM/IEEE Symposium on
                  Logic in Computer Science},
  articleno =    7,
  numpages =     13,
  location =     {Vancouver, Canada},
  series =       {LICS '19}
}

@InProceedings{LS04,
  author =       "Lack, Stephen and Soboci{\'{n}}ski, Pawe{\l}",
  editor =       "Walukiewicz, Igor",
  title =        "Adhesive Categories",
  booktitle =    "Foundations of Software Science and Computation
                  Structures",
  year =         2004,
  publisher =    "Springer Berlin Heidelberg",
  address =      "Berlin, Heidelberg",
  pages =        "273--288",
  abstract =     "We introduce adhesive categories, which are
                  categories with structure ensuring that pushouts
                  along monomorphisms are well-behaved. Many types of
                  graphical structures used in computer science are
                  shown to be examples of adhesive categories.
                  Double-pushout graph rewriting generalises well to
                  rewriting on arbitrary adhesive categories.",
  isbn =         "978-3-540-24727-2"
}

@InProceedings{LS13,
  author =       {Licata, Daniel R. and Shulman, Michael},
  booktitle =    {2013 28th Annual ACM/IEEE Symposium on Logic in
                  Computer Science},
  title =        {Calculating the Fundamental Group of the Circle in
                  Homotopy Type Theory},
  year =         2013,
  pages =        {223-232},
  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.},
  doi =          {10.1109/LICS.2013.28},
  ISSN =         {1043-6871},
  month =        {June},
}

@Article{Mat76,
  title =        {Pull-Backs in Homotopy Theory},
  author =       {Michael Mather},
  journal =      {Canadian Journal of Mathematics},
  year =         1976,
  volume =       28,
  pages =        {225 - 263},
  doi =          {10.4153/CJM-1976-029-0}
}

@InCollection{ML75,
  title =        {An Intuitionistic Theory of Types: Predicative Part},
  editor =       {H.E. Rose and J.C. Shepherdson},
  series =       {Studies in Logic and the Foundations of Mathematics},
  publisher =    {Elsevier},
  volume =       80,
  pages =        {73-118},
  year =         1975,
  booktitle =    {Logic Colloquium '73},
  issn =         {0049-237X},
  doi =          {10.1016/S0049-237X(08)71945-1},
  url =
                  {https://www.sciencedirect.com/science/article/pii/S0049237X08719451},
  author =       {Per Martin-Löf},
  abstract =     {The theory of types is intended to be a full-scale
                  system for formalizing intuitionistic mathematics as
                  developed. The language of the theory is richer than
                  the languages of traditional intuitionistic systems
                  in permitting proofs to appear as parts of
                  propositions so that the propositions of the theory
                  can express properties of proofs. There are axioms
                  for universes that link the generation of objects
                  and types and play somewhat the same role for the
                  present theory as does the replacement axiom for
                  Zermelo–Fraenkel set theory. The present theory is
                  based on a strongly impredicative axiom that there
                  is a type of all types in symbols. This axiom has to
                  be abandoned, however, after it has been shown to
                  lead to a contraction. This chapter discusses
                  Normalization theorem, which can be strengthened in
                  two ways: it can be made to cover open terms and it
                  can be proved that every reduction sequence starting
                  from an arbitrary term leads to a unique normal term
                  after a finite number of steps. The definition of
                  the notion of convertibility and the proof that an
                  arbitrary term is convertible can no longer be
                  separated because the type symbols and the terms are
                  generated simultaneously.}
}

@Book{NPS90,
  author =       {Nordstr\"{o}m, Bengt and Petersson, Kent and Smith,
                  Jan M.},
  title =        {Programming in Martin-L\"{o}f's type theory: an
                  introduction},
  year =         1990,
  isbn =         0198538146,
  publisher =    {Clarendon Press},
  address =      {USA}
}

@InProceedings{Pau93,
  author =       {Paulin-Mohring, Christine},
  title =        {Inductive Definitions in the system Coq - Rules and
                  Properties},
  year =         1993,
  isbn =         3540565175,
  publisher =    {Springer-Verlag},
  address =      {Berlin, Heidelberg},
  booktitle =    {Proceedings of the International Conference on Typed
                  Lambda Calculi and Applications},
  pages =        {328–345},
  numpages =     18,
  series =       {TLCA '93}
}

@Thesis{Rij19,
  title =        {Classifying Types},
  author =       {Egbert Rijke},
  type =         {phdthesis},
  institution =  {Carnegie Mellon University},
  year =         2019,
  eprint =       {1906.09435},
  archivePrefix ={arXiv},
  primaryClass = {math.LO},
  url =          {https://arxiv.org/abs/1906.09435},
}

@Book{Rij22,
  title =        {Introduction to Homotopy Type Theory},
  author =       {Egbert Rijke},
  year =         2022,
  eprint =       {2212.11082},
  archivePrefix ={arXiv},
  primaryClass = {math.LO}
}

@Unpublished{Rij22Pre,
  title =        {Introduction to Homotopy Type Theory},
  author =       {Egbert Rijke},
  year =         2022,
  month =        4,
  note =         "Unpublished preprint used as study material for the
                  HoTTEST Summer School 2022",
  url =
                  {https://github.com/martinescardo/HoTTEST-Summer-School/blob/06dab2ca8ea0c760ac2dcb40006c280d619e5368/HoTT/hott-intro.pdf}
}

@Software{AU24,
  author =       {Rijke, Egbert and Stenholm, Elisabeth and
                  Prieto-Cubides, Jonathan and Bakke, Fredrik and
                  Štěpančík, Vojtěch and {others}},
  year =         2024,
  license =      {MIT},
  title =        {{The agda-unimath library}},
  url =          {https://github.com/UniMath/agda-unimath/},
  note =         {Accessed on 2024-17-07}
}

@Article{Soj15,
  author =       {Sojakova, Kristina},
  title =        {Higher Inductive Types as Homotopy-Initial Algebras},
  year =         2015,
  issue_date =   {January 2015},
  publisher =    {Association for Computing Machinery},
  address =      {New York, NY, USA},
  volume =       50,
  number =       1,
  issn =         {0362-1340},
  url =          {https://doi.org/10.1145/2775051.2676983},
  doi =          {10.1145/2775051.2676983},
  abstract =     {Homotopy Type Theory is a new field of mathematics
                  based on the recently-discovered correspondence
                  between Martin-L\"{o}f's constructive type theory
                  and abstract homotopy theory. We have a powerful
                  interplay between these disciplines - we can use
                  geometric intuition to formulate new concepts in
                  type theory and, conversely, use type-theoretic
                  machinery to verify and often simplify existing
                  mathematical proofs.Higher inductive types form a
                  crucial part of this new system since they allow us
                  to represent mathematical objects, such as spheres,
                  tori, pushouts, and quotients, in the type theory.
                  We investigate a class of higher inductive types
                  called W-suspensions which generalize
                  Martin-L\"{o}f's well-founded trees. We show that a
                  propositional variant of W-suspensions, whose
                  computational behavior is determined up to a higher
                  path, is characterized by the universal property of
                  being a homotopy-initial algebra. As a corollary we
                  get that W-suspensions in the strict form are
                  homotopy-initial.},
  journal =      {SIGPLAN Not.},
  month =        1,
  pages =        {31–42},
  numpages =     12,
  keywords =     {higher inductive type, homotopy type theory,
                  homotopy-initial algebra, w-suspension}
}

@InProceedings{SvDR20,
  author =       {Sojakova, Kristina and van Doorn, Floris and Rijke,
                  Egbert},
  title =        {Sequential Colimits in Homotopy Type Theory},
  year =         2020,
  isbn =         9781450371049,
  publisher =    {Association for Computing Machinery},
  address =      {New York, NY, USA},
  url =          {https://doi.org/10.1145/3373718.3394801},
  doi =          {10.1145/3373718.3394801},
  booktitle =    {Proceedings of the 35th Annual ACM/IEEE Symposium on
                  Logic in Computer Science},
  pages =        {845–858},
  numpages =     14,
  keywords =     {higher inductive types, homotopy type theory,
                  sequential colimits},
  location =     {Saarbr\"{u}cken, Germany},
  series =       {LICS '20}
}

@Book{UF13,
  title =        {Homotopy Type Theory: Univalent Foundations of
                  Mathematics},
  author =       {{The Univalent Foundations Program}},
  publisher =    {\url{https://homotopytypetheory.org/book}},
  address =      {Institute for Advanced Study},
  year =         2013
}

@Unpublished{War23,
  title =        {Path Spaces of Pushouts},
  author =       {David W{\"{a}}rn},
  year =         2023,
  url =          {https://dwarn.se/po-paths.pdf},
  note =         {Accessed on 2023-30-09}
}

@Misc{War24,
  title =        {Path Spaces of Pushouts},
  author =       {David W{\"{a}}rn},
  year =         2024,
  eprint =       {2402.12339},
  archivePrefix ={arXiv},
  primaryClass = {math.AT}
}