{"data":{"id":"10.48550/arxiv.1402.0761","type":"dois","attributes":{"doi":"10.48550/arxiv.1402.0761","prefix":"10.48550","suffix":"arxiv.1402.0761","identifiers":[{"identifier":"1402.0761","identifierType":"arXiv"}],"alternateIdentifiers":[{"alternateIdentifierType":"arXiv","alternateIdentifier":"1402.0761"}],"creators":[{"name":"Sojakova, Kristina","nameType":"Personal","givenName":"Kristina","familyName":"Sojakova","affiliation":[],"nameIdentifiers":[]}],"titles":[{"title":"Higher Inductive Types as Homotopy-Initial Algebras"}],"publisher":"arXiv","container":{},"publicationYear":2014,"subjects":[{"lang":"en","subject":"Logic in Computer Science (cs.LO)","subjectScheme":"arXiv"},{"lang":"en","subject":"Category Theory (math.CT)","subjectScheme":"arXiv"},{"lang":"en","subject":"Logic (math.LO)","subjectScheme":"arXiv"},{"subject":"FOS: Computer and information sciences","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"FOS: Computer and information sciences","schemeUri":"http://www.oecd.org/science/inno/38235147.pdf","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"FOS: Mathematics","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"FOS: Mathematics","schemeUri":"http://www.oecd.org/science/inno/38235147.pdf","subjectScheme":"Fields of Science and Technology (FOS)"}],"contributors":[],"dates":[{"date":"2014-02-04T15:22:49Z","dateType":"Submitted","dateInformation":"v1"},{"date":"2014-02-10T01:01:10Z","dateType":"Updated","dateInformation":"v1"},{"date":"2014-02","dateType":"Available","dateInformation":"v1"},{"date":"2014","dateType":"Issued"}],"language":null,"types":{"ris":"GEN","bibtex":"misc","citeproc":"article","schemaOrg":"CreativeWork","resourceType":"Article","resourceTypeGeneral":"Preprint"},"relatedIdentifiers":[],"relatedItems":[],"sizes":[],"formats":[],"version":"1","rightsList":[{"rights":"arXiv.org perpetual, non-exclusive license","rightsUri":"http://arxiv.org/licenses/nonexclusive-distrib/1.0/"}],"descriptions":[{"description":"Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs 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. A crucial ingredient in this new system are higher inductive types, which allow us to represent objects such as spheres, tori, pushouts, and quotients. We investigate a variant of higher inductive types whose computational behavior is determined up to a higher path. We show that in this setting, higher inductive types are characterized by the universal property of being a homotopy-initial algebra.","descriptionType":"Abstract"}],"geoLocations":[],"fundingReferences":[],"xml":"PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0idXRmLTgiPz4KPHJlc291cmNlIHhtbG5zPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCIgeG1sbnM6eHNpPSJodHRwOi8vd3d3LnczLm9yZy8yMDAxL1hNTFNjaGVtYS1pbnN0YW5jZSIgeHNpOnNjaGVtYUxvY2F0aW9uPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCBodHRwOi8vc2NoZW1hLmRhdGFjaXRlLm9yZy9tZXRhL2tlcm5lbC00LjMvbWV0YWRhdGEueHNkIj4KICA8aWRlbnRpZmllciBpZGVudGlmaWVyVHlwZT0iRE9JIj4xMC40ODU1MC9BUlhJVi4xNDAyLjA3NjE8L2lkZW50aWZpZXI+CiAgPGFsdGVybmF0ZUlkZW50aWZpZXJzPgogICAgPGFsdGVybmF0ZUlkZW50aWZpZXIgYWx0ZXJuYXRlSWRlbnRpZmllclR5cGU9ImFyWGl2Ij4xNDAyLjA3NjE8L2FsdGVybmF0ZUlkZW50aWZpZXI+CiAgPC9hbHRlcm5hdGVJZGVudGlmaWVycz4KICA8Y3JlYXRvcnM+CiAgICA8Y3JlYXRvcj4KICAgICAgPGNyZWF0b3JOYW1lIG5hbWVUeXBlPSJQZXJzb25hbCI+U29qYWtvdmEsIEtyaXN0aW5hPC9jcmVhdG9yTmFtZT4KICAgICAgPGdpdmVuTmFtZT5LcmlzdGluYTwvZ2l2ZW5OYW1lPgogICAgICA8ZmFtaWx5TmFtZT5Tb2pha292YTwvZmFtaWx5TmFtZT4KICAgIDwvY3JlYXRvcj4KICA8L2NyZWF0b3JzPgogIDx0aXRsZXM+CiAgICA8dGl0bGU+SGlnaGVyIEluZHVjdGl2ZSBUeXBlcyBhcyBIb21vdG9weS1Jbml0aWFsIEFsZ2VicmFzPC90aXRsZT4KICA8L3RpdGxlcz4KICA8cHVibGlzaGVyPmFyWGl2PC9wdWJsaXNoZXI+CiAgPHB1YmxpY2F0aW9uWWVhcj4yMDE0PC9wdWJsaWNhdGlvblllYXI+CiAgPHN1YmplY3RzPgogICAgPHN1YmplY3QgeG1sOmxhbmc9ImVuIiBzdWJqZWN0U2NoZW1lPSJhclhpdiI+TG9naWMgaW4gQ29tcHV0ZXIgU2NpZW5jZSAoY3MuTE8pPC9zdWJqZWN0PgogICAgPHN1YmplY3QgeG1sOmxhbmc9ImVuIiBzdWJqZWN0U2NoZW1lPSJhclhpdiI+Q2F0ZWdvcnkgVGhlb3J5IChtYXRoLkNUKTwvc3ViamVjdD4KICAgIDxzdWJqZWN0IHhtbDpsYW5nPSJlbiIgc3ViamVjdFNjaGVtZT0iYXJYaXYiPkxvZ2ljIChtYXRoLkxPKTwvc3ViamVjdD4KICAgIDxzdWJqZWN0IHN1YmplY3RTY2hlbWU9IkZpZWxkcyBvZiBTY2llbmNlIGFuZCBUZWNobm9sb2d5IChGT1MpIj5GT1M6IENvbXB1dGVyIGFuZCBpbmZvcm1hdGlvbiBzY2llbmNlczwvc3ViamVjdD4KICAgIDxzdWJqZWN0IHN1YmplY3RTY2hlbWU9IkZpZWxkcyBvZiBTY2llbmNlIGFuZCBUZWNobm9sb2d5IChGT1MpIj5GT1M6IE1hdGhlbWF0aWNzPC9zdWJqZWN0PgogIDwvc3ViamVjdHM+CiAgPGRhdGVzPgogICAgPGRhdGUgZGF0ZVR5cGU9IlN1Ym1pdHRlZCIgZGF0ZUluZm9ybWF0aW9uPSJ2MSI+MjAxNC0wMi0wNFQxNToyMjo0OVo8L2RhdGU+CiAgICA8ZGF0ZSBkYXRlVHlwZT0iVXBkYXRlZCIgZGF0ZUluZm9ybWF0aW9uPSJ2MSI+MjAxNC0wMi0xMFQwMTowMToxMFo8L2RhdGU+CiAgICA8ZGF0ZSBkYXRlVHlwZT0iQXZhaWxhYmxlIiBkYXRlSW5mb3JtYXRpb249InYxIj4yMDE0LTAyPC9kYXRlPgogIDwvZGF0ZXM+CiAgPHJlc291cmNlVHlwZSByZXNvdXJjZVR5cGVHZW5lcmFsPSJQcmVwcmludCI+QXJ0aWNsZTwvcmVzb3VyY2VUeXBlPgogIDx2ZXJzaW9uPjE8L3ZlcnNpb24+CiAgPHJpZ2h0c0xpc3Q+CiAgICA8cmlnaHRzIHJpZ2h0c1VSST0iaHR0cDovL2FyeGl2Lm9yZy9saWNlbnNlcy9ub25leGNsdXNpdmUtZGlzdHJpYi8xLjAvIj5hclhpdi5vcmcgcGVycGV0dWFsLCBub24tZXhjbHVzaXZlIGxpY2Vuc2U8L3JpZ2h0cz4KICA8L3JpZ2h0c0xpc3Q+CiAgPGRlc2NyaXB0aW9ucz4KICAgIDxkZXNjcmlwdGlvbiBkZXNjcmlwdGlvblR5cGU9IkFic3RyYWN0Ij5Ib21vdG9weSBUeXBlIFRoZW9yeSBpcyBhIG5ldyBmaWVsZCBvZiBtYXRoZW1hdGljcyBiYXNlZCBvbiB0aGUgc3VycHJpc2luZyBhbmQgZWxlZ2FudCBjb3JyZXNwb25kZW5jZSBiZXR3ZWVuIE1hcnRpbi1Mb2ZzIGNvbnN0cnVjdGl2ZSB0eXBlIHRoZW9yeSBhbmQgYWJzdHJhY3QgaG9tb3RvcHkgdGhlb3J5LiBXZSBoYXZlIGEgcG93ZXJmdWwgaW50ZXJwbGF5IGJldHdlZW4gdGhlc2UgZGlzY2lwbGluZXMgLSB3ZSBjYW4gdXNlIGdlb21ldHJpYyBpbnR1aXRpb24gdG8gZm9ybXVsYXRlIG5ldyBjb25jZXB0cyBpbiB0eXBlIHRoZW9yeSBhbmQsIGNvbnZlcnNlbHksIHVzZSB0eXBlLXRoZW9yZXRpYyBtYWNoaW5lcnkgdG8gdmVyaWZ5IGFuZCBvZnRlbiBzaW1wbGlmeSBleGlzdGluZyBtYXRoZW1hdGljYWwgcHJvb2ZzLiBBIGNydWNpYWwgaW5ncmVkaWVudCBpbiB0aGlzIG5ldyBzeXN0ZW0gYXJlIGhpZ2hlciBpbmR1Y3RpdmUgdHlwZXMsIHdoaWNoIGFsbG93IHVzIHRvIHJlcHJlc2VudCBvYmplY3RzIHN1Y2ggYXMgc3BoZXJlcywgdG9yaSwgcHVzaG91dHMsIGFuZCBxdW90aWVudHMuIFdlIGludmVzdGlnYXRlIGEgdmFyaWFudCBvZiBoaWdoZXIgaW5kdWN0aXZlIHR5cGVzIHdob3NlIGNvbXB1dGF0aW9uYWwgYmVoYXZpb3IgaXMgZGV0ZXJtaW5lZCB1cCB0byBhIGhpZ2hlciBwYXRoLiBXZSBzaG93IHRoYXQgaW4gdGhpcyBzZXR0aW5nLCBoaWdoZXIgaW5kdWN0aXZlIHR5cGVzIGFyZSBjaGFyYWN0ZXJpemVkIGJ5IHRoZSB1bml2ZXJzYWwgcHJvcGVydHkgb2YgYmVpbmcgYSBob21vdG9weS1pbml0aWFsIGFsZ2VicmEuPC9kZXNjcmlwdGlvbj4KICA8L2Rlc2NyaXB0aW9ucz4KPC9yZXNvdXJjZT4=","url":"https://arxiv.org/abs/1402.0761","contentUrl":null,"metadataVersion":0,"schemaVersion":"http://datacite.org/schema/kernel-4","source":"mds","isActive":true,"state":"findable","reason":null,"viewCount":0,"viewsOverTime":[],"downloadCount":0,"downloadsOverTime":[],"referenceCount":0,"citationCount":0,"citationsOverTime":[],"partCount":0,"partOfCount":0,"versionCount":0,"versionOfCount":0,"created":"2022-03-10T03:21:10.000Z","registered":"2022-03-10T03:21:11.000Z","published":"2014","updated":"2025-05-28T02:36:45.000Z"},"relationships":{"client":{"data":{"id":"arxiv.content","type":"clients"}},"provider":{"data":{"id":"arxiv","type":"providers"}},"media":{"data":{"id":"10.48550/arxiv.1402.0761","type":"media"}},"references":{"data":[]},"citations":{"data":[]},"parts":{"data":[]},"partOf":{"data":[]},"versions":{"data":[]},"versionOf":{"data":[]}}}}