{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:51Z","timestamp":1779836751113,"version":"3.53.1"},"reference-count":53,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2016,9,13]],"date-time":"2016-09-13T00:00:00Z","timestamp":1473724800000},"content-version":"unspecified","delay-in-days":256,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2016]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Homotopy type theory is an extension of Martin-L\u00f6f type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type is proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches\u2014syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.<\/jats:p>","DOI":"10.1017\/s0956796816000198","type":"journal-article","created":{"date-parts":[[2016,9,13]],"date-time":"2016-09-13T04:09:05Z","timestamp":1473739745000},"source":"Crossref","is-referenced-by-count":6,"title":["Homotopical patch theory"],"prefix":"10.1017","volume":"26","author":[{"given":"CARLO","family":"ANGIULI","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"EDWARD","family":"MOREHOUSE","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DANIEL R.","family":"LICATA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ROBERT","family":"HARPER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2016,9,13]]},"reference":[{"key":"S0956796816000198_ref10","unstructured":"Cavallo E. (2015) Synthetic Cohomology in Homotopy Type Theory. M.Phil. Thesis, Carnegie Mellon University."},{"key":"S0956796816000198_ref8","unstructured":"Bezem M. , Coquand T. & Huber S. (2014) A model of type theory in cubical sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), Matthes R. & Schubert A. (eds), Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, vol. 26, pp. 107\u2013128."},{"key":"S0956796816000198_ref39","volume-title":"Programming in Martin-L\u00f6f's Type Theory, an Introduction","author":"Nordstr\u00f6m","year":"1990"},{"key":"S0956796816000198_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.018"},{"key":"S0956796816000198_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"S0956796816000198_ref49","doi-asserted-by":"crossref","unstructured":"Swierstra W. & L\u00f6h A. (2014) The semantics of version control. In Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Onward! 2014). New York, NY, USA: ACM, pp. 43\u201354.","DOI":"10.1145\/2661136.2661137"},{"key":"S0956796816000198_ref35","unstructured":"Lumsdaine P. L. & Shulman M. (2013) Higher Inductive Types. In preparation."},{"key":"S0956796816000198_ref26","first-page":"1","volume-title":"Proceedings of the Third International Conference on Certified Programs and Proofs","author":"Licata","year":"2013"},{"key":"S0956796816000198_ref5","unstructured":"Altenkirch T. , McBride C. & Swierstra W. (2007) Observational equality, now! In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification (PLPV '07). New York, NY, USA: ACM, pp. 57\u201368."},{"key":"S0956796816000198_ref23","doi-asserted-by":"publisher","DOI":"10.2307\/2269016"},{"key":"S0956796816000198_ref14","unstructured":"Dagit J. (2009) Type-Correct Changes\u2013-A Safe Approach to Version Control Implementation. MS Thesis. Corvallis, Oregon, USA: Oregon State University."},{"key":"S0956796816000198_ref40","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis, Chalmers University of Technology."},{"key":"S0956796816000198_ref21","unstructured":"Jacobson J. (2009) A formalization of Darcs patch theory using inverse semigroups. Available at: ftp:\/\/ftp.math.ucla.edu\/pub\/camreport\/cam09-83.pdf. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref15","unstructured":"Darcs Project. (2013) Available at: http:\/\/darcs.net\/. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref13","unstructured":"Coq Development Team. (2015) The Coq proof assistant reference manual, version 8.5. INRIA. Available at: http:\/\/coq.inria.fr\/. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"S0956796816000198_ref50","unstructured":"Univalent Foundations Program. (2013) Homotopy Type Theory: Univalent Foundations of Mathematics. Available at: http:\/\/homotopytypetheory.org\/book. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref34","unstructured":"Lumsdaine P. L. (2011 April) Higher Inductive Types: A Tour of the Menagerie. Available at: http:\/\/homotopytypetheory.org\/2011\/04\/24\/higher-inductive-types-a-tour-of-the-menagerie\/. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref25","doi-asserted-by":"crossref","unstructured":"Lawvere F. W. (1963) Functorial Semantics of Algebraic Theories and Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories. PhD Thesis, Columbia University.","DOI":"10.1073\/pnas.50.5.869"},{"key":"S0956796816000198_ref42","unstructured":"Polonsky A. (2015) Internalization of Extensional Equality. arXiv.1401.1148."},{"key":"S0956796816000198_ref45","unstructured":"Roundy D. (2009 April) Theory of Patches. Available at: http:\/\/www.cs.tufts.edu\/comp\/150GIT\/archive\/david-roundy\/theory-patches-2009.pdf. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"S0956796816000198_ref28","doi-asserted-by":"crossref","unstructured":"Licata D. R. & Finster E. (2014) Eilenberg\u2013MacLane spaces in homotopy type theory. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS '14). New York, NY, USA: ACM, pp. 66:1\u201366:9.","DOI":"10.1145\/2603088.2603153"},{"key":"S0956796816000198_ref12","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"Constable","year":"1986"},{"key":"S0956796816000198_ref48","unstructured":"Sittampalam G. et al. (2005) Some Properties of Darcs Patch Theory. Available at: http:\/\/urchin.earth.li\/darcs\/ganesh\/darcs-patch-theory\/theory\/formal.pdf. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref30","doi-asserted-by":"crossref","unstructured":"Licata D. R. & Harper R. (2012) Canonicity for 2-dimensional type theory. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '12). New York, NY, USA: ACM, pp. 337\u2013348.","DOI":"10.1145\/2103656.2103697"},{"key":"S0956796816000198_ref9","unstructured":"Camp Project. (2010) Available at: http:\/\/projects.haskell.org\/camp\/. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref11","unstructured":"Cohen C. , Coquand T. , Huber S. & M\u00f6rtberg A. (2016) Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. Preprint. Available at: http:\/\/www.cse.chalmers.se\/~coquand\/cubicaltt.pdf. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref24","first-page":"101","volume-title":"Constructivity in Mathematics","author":"Kreisel","year":"1959"},{"key":"S0956796816000198_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007646"},{"key":"S0956796816000198_ref44","doi-asserted-by":"crossref","unstructured":"Roundy D. (2005) Darcs: Distributed version management in haskell. In Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell (Haskell '05). New York, NY, USA: ACM, pp. 1\u20134.","DOI":"10.1145\/1088348.1088349"},{"key":"S0956796816000198_ref32","unstructured":"L\u00f6h A. , Swierstra W. & Leijen D. (2007) A Principled Approach to Version Control. Preprint. Available at: http:\/\/www.andres-loeh.de\/VersionControl.html. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref46","unstructured":"Shulman M. (2011 April) Homotopy Type Theory VI: Higher Inductive Types. Available at: http:\/\/golem.ph.utexas.edu\/category\/2011\/04\/homotopy_type_theory_vi.html. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref2","unstructured":"Aczel P. (1977) The strength of Martin-L\u00f6f's intuitionistic type theory with one universe. In Proceedings of the Symposium on Mathematical Logic, Oulu, 1974. Dept. of Philosophy, University of Helsinki, Helsinki, Finland. Report No. 2, pp. 1\u201332."},{"key":"S0956796816000198_ref43","doi-asserted-by":"crossref","unstructured":"Reynolds J. C. (2002) Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS '02). Washington, DC, USA: IEEE Computer Society, pp. 55\u201374.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"S0956796816000198_ref3","volume-title":"Containers in Homotopy Type Theory","author":"Altenkirch","year":"2014"},{"key":"S0956796816000198_ref27","doi-asserted-by":"crossref","unstructured":"Licata D. R. , & Brunerie G. (2015) A Cubical Approach to Synthetic Homotopy Theory. In Proceedings of the 2015 30th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS '15). Washington, DC, USA: IEEE Computer Society, pp. 92\u2013103.","DOI":"10.1109\/LICS.2015.19"},{"key":"S0956796816000198_ref53","unstructured":"Warren M. A. (2008) Homotopy Theoretic Aspects of Constructive Type Theory. PhD Thesis, Carnegie Mellon University."},{"key":"S0956796816000198_ref33","doi-asserted-by":"crossref","unstructured":"Lumsdaine P. L. (2009) Weak \u03c9-categories from intensional type theory. In Typed Lambda Calculi and Applications: 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1\u20133, 2009. Proceedings. Curien P.-L. (ed), Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 172\u2013187.","DOI":"10.1007\/978-3-642-02273-9_14"},{"key":"S0956796816000198_ref18","doi-asserted-by":"crossref","unstructured":"Hofmann M. & Streicher T. (1998) The groupoid interpretation of type theory. Twenty-Five Years of Constructive Type Theory. Oxford University Press.","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"S0956796816000198_ref47","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"S0956796816000198_ref52","unstructured":"Voevodsky V. (2006) A very short note on homotopy \u03bb-calculus. Unpublished, September, 1\u20137."},{"key":"S0956796816000198_ref37","unstructured":"McBride C. (2000) Dependently Typed Functional Programs and Their Proofs. PhD Thesis, University of Edinburgh."},{"key":"S0956796816000198_ref41","unstructured":"Pijul Project. (2015) Available at: https:\/\/pijul.org\/. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref22","unstructured":"Kapulkin C. , Lumsdaine P. L. & Voevodsky V. (2012) The Simplicial Model of Univalent Foundations. arXiv:1211.2851."},{"key":"S0956796816000198_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000504"},{"key":"S0956796816000198_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.026"},{"key":"S0956796816000198_ref36","unstructured":"Lynagh I. (2012 January) Camp Patch Theory. Available at: http:\/\/projects.haskell.org\/camp\/files\/theory.pdf. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref4","unstructured":"Altenkirch T. & Kaposi A. (2015) Towards Cubical Type Theory. Preprint. Available at: http:\/\/akaposi.bitbucket.org\/nominal.pdf. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref51","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"S0956796816000198_ref31","doi-asserted-by":"crossref","unstructured":"Licata D. R. & Shulman M. (2013) Calculating the fundamental group of the circle in homotopy type theory. In Proceedings of the 2013 28th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS '13). Washington, DC, USA: IEEE Computer Society, pp. 223\u2013232.","DOI":"10.1109\/LICS.2013.28"},{"key":"S0956796816000198_ref20","unstructured":"Houston R. (2012) On editing text. Available at: http:\/\/bosker.wordpress.com\/2012\/05\/10\/on-editing-text\/. (last accessed date 25\/08\/2016)"},{"key":"S0956796816000198_ref19","unstructured":"Hou K.-B. (Favonia) (2014) Covering spaces in homotopy type theory. Talk at TYPES 2014."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000198","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:39Z","timestamp":1779834999000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000198\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"references-count":53,"alternative-id":["S0956796816000198"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000198","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"article-number":"e18"}}