research-article

Public Access

A Higher Structure Identity Principle

Authors:

Benedikt Ahrens,

Paige Randall North,

Michael Shulman,

Dimitris TsementzisAuthors Info & Claims

LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 53 - 66

https://doi.org/10.1145/3373718.3394755

Published: 08 July 2020 Publication History

PDF eReader

Abstract

The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with "isomorphisms" between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call "indiscernibilities," using only the dependency structure rather than any notion of composition.

References

[1]

Peter Aczel. 2011. On Voevodsky's Univalence Axiom. In Mathematical Logic: Proof Theory, Constructive Mathematics, Samuel R. Buss, Ulrich Kohlenbach, and Michael Rathjen (Eds.). Mathematisches Forschungsinstitut Oberwolfach, Oberwolfach, Chapter 1, 2967. https://doi.org/10.4171/OWR/2011/52

Crossref

Google Scholar

[2]

Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. 2015. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science 25, 05 (2015), 1010--1039. https://doi.org/10.1017/S0960129514000486

Crossref

Google Scholar

[3]

Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis. 2020. A Higher Structure Identity Principle. (2020). arXiv:2004.06572

Google Scholar

[4]

Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. 2019. Two-Level Type Theory and Applications. (2019). https://arxiv.org/abs/1705.03307v3

Google Scholar

[5]

Georges Blanc. 1978. Équivalence naturelle et formules logiques en théorie des catégories. Arch. Math. Logik Grundlag. 19, 3-4 (1978), 131--137. https://doi.org/10.1007/BF02011874

Crossref

Google Scholar

[6]

Thierry Coquand and Nils Anders Danielsson. 2013. Isomorphism is equality. Indagationes Mathematicae 24, 4 (2013), 1105--1120. https://doi.org/10.1016/j.indag.2013.09.002 In memory of N.G. (Dick) de Bruijn (1918-2012).

Crossref

Google Scholar

[7]

Peter Freyd. 1976. Properties invariant within equivalence types of categories. In Algebra, topology, and category theory (a collection of papers in honor of Samuel Eilenberg). Academic Vress, New York, 55--61.

Google Scholar

[8]

Chris Kapulkin and Peter LeFanu Lumsdaine. 2019. The simplicial model of univalent foundations (after Voevodsky). Journal of the European Mathematical Society (2019). arXiv:1211.2851 To appear. arXiv:1211.2851.

Google Scholar

[9]

Michael Makkai. 1995. First Order Logic with Dependent Sorts, with Applications to Category Theory. (1995). http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf.

Google Scholar

[10]

Dimitris Tsementzis. 2017. A Higher Structure Identity Principle. (2017). arXiv:1702.07776 arXiv:1702.07776.

Google Scholar

[11]

The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study.

Google Scholar

[12]

Vladimir Voevodsky. 2015. An experimental library of formalized Mathematics based on the univalent foundations. Mathematical Structures in Computer Science 25, 5 (2015), 1278--1294. https://doi.org/10.1017/S0960129514000577

Crossref

Google Scholar

Cited By

View all

Ahrens BNorth PShulman MTsementzis D(2025)The Univalence PrincipleMemoirs of the American Mathematical Society10.1090/memo/1541305:1541Online publication date: 14-Jan-2025
https://doi.org/10.1090/memo/1541
Van Muylder ANuyts ADevriese D(2024)Internal and Observational Parametricity for Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328508:POPL(209-240)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632850
Prieto-Cubides JGylterud H(2024)On planarity of graphs in homotopy type theoryMathematical Structures in Computer Science10.1017/S0960129524000100(1-41)Online publication date: 8-May-2024
https://doi.org/10.1017/S0960129524000100
Show More Cited By

Index Terms

A Higher Structure Identity Principle
1. Theory of computation
  1. Logic

Recommendations

A Constructive Model of Directed Univalence in Bicubical Sets
LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

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 ...
Constructing Higher Inductive Types as Groupoid Quotients
LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

In this paper, we show that all finitary 1-truncated higher inductive types (HITs) can be constructed from the groupoid quotient. We start by defining internally a notion of signatures for HITs, and for each signature, we construct a bicategory of ...
An equational notion of lifting monad
Category theory and computer science

We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any equational lifting monad has a representation by a partial ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

July 2020

986 pages

ISBN:9781450371049

DOI:10.1145/3373718

Conference Chairs:
Holger Hermanns,
Lijun Zhang,
Naoki Kobayashi,
General Chair:
Dale Miller

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 July 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

Air Force Office of Scientific Research
Engineering and Physical Sciences Research Council
Centre for Advanced Study, Oslo, Norway
National Science Foundation

Conference

LICS '20

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science

July 8 - 11, 2020

Saarbrücken, Germany

Acceptance Rates

LICS '20 Paper Acceptance Rate 69 of 174 submissions, 40%;

Overall Acceptance Rate 215 of 622 submissions, 35%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
428
Total Downloads

Downloads (Last 12 months)170
Downloads (Last 6 weeks)27

Reflects downloads up to 08 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ahrens BNorth PShulman MTsementzis D(2025)The Univalence PrincipleMemoirs of the American Mathematical Society10.1090/memo/1541305:1541Online publication date: 14-Jan-2025
https://doi.org/10.1090/memo/1541
Van Muylder ANuyts ADevriese D(2024)Internal and Observational Parametricity for Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328508:POPL(209-240)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632850
Prieto-Cubides JGylterud H(2024)On planarity of graphs in homotopy type theoryMathematical Structures in Computer Science10.1017/S0960129524000100(1-41)Online publication date: 8-May-2024
https://doi.org/10.1017/S0960129524000100
Myers DSati HSchreiber U(2024)Topological Quantum Gates in Homotopy Type TheoryCommunications in Mathematical Physics10.1007/s00220-024-05020-8405:7Online publication date: 8-Jul-2024
https://doi.org/10.1007/s00220-024-05020-8
Annenkov DCapriotti PKraus NSattler C(2023)Two-level type theory and applicationsMathematical Structures in Computer Science10.1017/S0960129523000130(1-56)Online publication date: 30-May-2023
https://doi.org/10.1017/S0960129523000130
Ahrens BFrumin DMaggesi MVeltri Nvan der Weide N(2022)Bicategories in univalent foundationsMathematical Structures in Computer Science10.1017/S096012952200003231:10(1232-1269)Online publication date: 9-Mar-2022
https://doi.org/10.1017/S0960129522000032

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

A Constructive Model of Directed Univalence in Bicubical Sets

Constructing Higher Inductive Types as Groupoid Quotients

An equational notion of lifting monad