Model structure on the universe of all types in interval type theory

Model categories constitute the major context for doing homotopy theory. More recently, homotopy type theory (HoTT) has been introduced as a context for doing syntactic homotopy theory. In this paper, we show that a slight generalization of HoTT, called interval type theory (⫿TT), allows to define a model structure on the universe of all types, which, through the model interpretation, corresponds to defining a model structure on the category of cubical sets. This work generalizes previous works of Gambino, Garner, and Lumsdaine from the universe of fibrant types to the universe of all types. Our definition of ⫿TT comes from the work of Orton and Pitts to define a syntactic approximation of the internal language of the category of cubical sets. In this paper, we extend the work of Orton and Pitts by introducing the notion of degenerate fibrancy, which allows to define a fibrant replacement, at the heart of the model structure on the universe of all types. All our definitions and propositions have been formalized using the Coq proof assistant.

Infinite series of quaternionic 1-vertex cube complexes, the doubling construction, and explicit cubical Ramanujan complexes

We construct vertex transitive lattices on products of trees of arbitrary dimension [Formula: see text] based on quaternion algebras over global fields with exactly two ramified places. Starting from arithmetic examples, we find non-residually finite groups generalizing earlier results of Wise, Burger and Mozes to higher dimension. We make effective use of the combinatorial language of cubical sets and the doubling construction generalized to arbitrary dimension. Congruence subgroups of these quaternion lattices yield explicit cubical Ramanujan complexes, a higher-dimensional cubical version of Ramanujan graphs (optimal expanders).

OPERATOR BATAS PADA HOMOLOGI KUBIK

Algebra topology is a concept that classifies topological spaces particularlycubical sets based on the context of the algebraic objects namely homology groups. Atopological problem can also be viewed from the point of view of combinatorics whichcan be simplified to be graphs. In this paper it is discussed about the classification ofthe cubical sets based on its homology groups using the concept of boundary operatorsas homomorphisms of free Abelian groups.