A parametricity-based formalization of semi-simplicial and semi-cubical sets
| Autor: | Herbelin, Hugo, Ramachandra, Ramkumar |
|---|---|
| Přispěvatelé: | Les assistants à la démonstration au cœur du raisonnement mathématique (PICUBE), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité) |
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: |
Parametricity translation
Formalization [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] Simplicial set Proof assistant Coq [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic Cubical set |
| Popis: | Constructions such as semi-simplicial and semi-cubical sets can be defined in the "usual way" as presheaves over respectively, the semi-simplex or semi-cube category, which we call fibered definitions, but also defined like in e.g. Voevodsky or in previous work, as a dependently-typed construction, which we call indexed. This paper describes a uniform indexed characterization of both augmented semi-simplicial and semi-cubical sets arising respectively as unary and binary iterated parametricity-based constructions. Additionally, our construction is fully formalized in Coq's dependent type theory. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|