Related papers: Idempotents in intensional type theory
We are presenting proofs of fundamental results related to homotopy idempotents, proofs that are sufficiently simple so that even the author can understand them. The first one is that homotopy idempotents in the category of pointed…
This paper investigates Voevodsky's univalence axiom in intensional Martin-L\"of type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various…
Building on previous work, we study the splitting of idempotents in the category of extensions $\mathbb{E}\operatorname{-Ext}(\mathcal{C})$ associated to a pair $(\mathcal{C},\mathbb{E})$ of an additive category and a biadditive functor to…
We provide a partial result on Taylor's modularity conjecture, and several related problems. Namely, we show that the interpretability join of two idempotent varieties that are not congruence modular is not congruence modular either, and we…
In this paper we define intensional models for the classical theory of types, thus arriving at an intensional type logic ITL. Intensional models generalize Henkin's general models and have a natural definition. As a class they do not…
Intersection types are an essential tool in the analysis of operational and denotational properties of lambda-terms and functional programs. Among them, non-idempotent intersection types provide precise quantitative information about the…
We extend a well-known theorem of Murski\v{\i} to the probability space of finite models of a system $\mathcal{M}$ of identities of a strong idempotent linear Maltsev condition. We characterize the models of $\mathcal{M}$ in a way that can…
We prove a conjecture about the constructibility of coinductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presence of inductive types, coinductive types are derivable.…
New splitting theorems in a semi-Riemannian manifold which admits an irrotational vector field (not necessarily a gradient) with some suitable properties are obtained. According to the extras hypothesis assumed on the vector field, we can…
Consider two non-degenerate algebras B and C over the complex numbers. We study a certain class of idempotent elements E in the multiplier algebra of the tensor product of B with C, called separability idempotents. The conditions include…
Let $k$ be a commutative ring with identity. A {\it $k$-plethory} is a commutative $k$-algebra $P$ together with a comonad structure $W_P$, called the {\it $P$-Witt ring} functor, on the covariant functor that it represents. We say that a…
We prove a representation theorem for totally ordered idempotent monoids via a nested sum construction. Using this representation theorem we obtain a characterization of the subdirectly irreducible members of the variety of semilinear…
Commutative semirings with divisible additive semigroup are studied. We show that an additively divisible commutative semiring is idempotent, provided that it is finitely generated and torsion. In case that a one-generated additively…
In this paper we use 3-manifold techniques to illuminate the structure of the category of tangles. In particular, we show that every idempotent morphism $A$ in such a category naturally splits as $A=B\circ C$ such that $C\circ B$ is an…
We consider the following practical question: given a finite algebra A in a finite language, can we efficiently decide whether the variety generated by A has a difference term? We answer this question (positively) in the idempotent case and…
The separability tensor element of a separable extension of noncommutative rings is an idempotent when viewed in the correct endomorphism ring; so one speaks of a separability idempotent, as one usually does for separable algebras. It is…
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do…
The "Modularity Conjecture" is the assertion that the join of two nonmodular varieties is nonmodular. We establish the veracity of this conjecture for the case of linear idempotent varieties. We also establish analogous results concerning…
We say that an idempotent term $t$ is an exact-$m$-majority term if $t$ evaluates to $a$, whenever the element $a$ occurs exactly $m$ times in the arguments of $t$, and all the other arguments are equal. If $m<n$ and some variety $\mathcal…
Idempotent elements are a well-studied part of ring theory, with several identities of the idempotents in $\mathbb{Z}/m\mathbb{Z}$ already known. Although the idempotents are not closed under addition, there are still interesting additive…