{'fraction_non_alphanumeric': 0.03328859060402684, 'fraction_numerical': 0.004026845637583893, 'mean_word_length': 4.619909502262443, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Towards Simplicial Complexes in Homotopy Type Theory

simplicial complexes and their homotopy types We present a slim definition of ordered abstract simplicial complexes in dependent type theory: A simplicial complex of dimension n is a dependent type that contains for each i ≤ n a list of faces of dimension i. A face of dimension i is a vector of i natural numbers, which stand for the vertices of the complex. The closure property of simplicial complexes, which requires that all non-empty subsets of a face are also in the complex, is formulated as a dependent function type. This representation is independent of the types-as-spaces interpretation and could be carried out in any dependent type theory. In order to reason about the homotopy type of simplicial complexes, we utilize a construction of CW complexes introduced by [3], in which cells are attached iteratively by homotopy pushouts. We port their formalization to Cubical Agda, which greatly reduces the required code due to the direct access to higher inductive types (HIT). We prove some basic results of CW complexes such as the equivalence to certain HIT representations of CW complexes. We then construct a function that takes any simplicial complex of dimension smaller than 3 to a CW complex with a corresponding homotopy type: The points of the simplicial complex remain discrete 0-cells, the lines are mapped to 1-cells, and the triangles are mapped to squares with two vertices identified. The combinatorial description ascribes which vertices of these standard simplices need to be identified. This allows us to reason about the homotopy type of simplicial complexes with the built-in path arithmetic of Cubical Agda. The code of this section can be found online: https://github.com/maxdore/cubical Semi-simplicial types in finite-dimensional type theory In the construction described above, we have to enforce the closure property of simplicial complexes explicitly. This makes further operations on the complexes cumbersome to implement, which would be avoided if the closure property is ensured intrinsically. Famously, it appears to be impossible to do this in HoTT. More precisely, the construction of Reedy fibrant n-truncated semi-simplicial types could not be carried out inside HoTT despite many efforts [7, 1, 10]. The main obstacle is that internally defined categories in HoTT do not preserve certain functor laws judgmentally, which is symptomatic of a bigger problem: Oftentimes, the equality proofs of a type beyond a certain dimension are of no interest in further constructions and only complicate formalizations. We propose the following variation of ITT to solve this “problem of coherences”: In finitedimensional type theory, the identity type of any type collapses at a specific level. The basic judgment of ITT, “A is a type”, is refined to “A is an n-type”, denoted A Type. We call n the dimension of A. Intuitively, a 0-type has at most one inhabitant and represents a proposition, a 1-type is a set with different inhabitants, but only unique identity proofs, a 2-type has a 1-groupoidal structure, and so on. The rules of ITT are refined by taking into account the dimension. For example, the dependent function type takes a dimension as parameter, e.g., Π(x : A)(B(x)) can be thought of as the “hom-set” of dependent morphisms between A and B, were A Type and B Type for arbitrary dimensions i, j. The introduction rule of the identity type is changed crucially to this: Γ ` A : Type Γ ` a : A Γ ` b : A Γ ` IdA(a, b) : Type Id-Intro The predecessor function pred sends suc(n) to n and 0 to 0. Hence, Id-Intro establishes that for A Type, all identity types on A from the n-th iteration on have dimension 0. For example,