W-types in setoids

We present a construction of W-types in the setoid model of extensional Martin-L\"of type theory using dependent W-types in the underlying intensional theory. More precisely, we prove that the internal category of setoids has initial algebras for polynomial endofunctors. In particular, we characterise the setoid of algebra morphisms from the initial algebra to a given algebra as a setoid on a dependent W-type. We conclude by discussing the case of free setoids. We work in a fully intensional theory and, in fact, we assume identity types only when discussing free setoids. By using dependent W-types we can also avoid elimination into a type universe. The results have been verified in Coq and a formalisation is available on the author's GitHub page.

Further remarks on group-2-groupoids

The aim of this paper is to obtain a group-2-groupoid as a 2-groupoid object in the category of groups and also as a special kind of an internal category in the category of group-groupoids. Corresponding group-2-groupoids, we obtain some categorical structures related to crossed modules and group-groupoids and prove categorical equivalences between them. These results enable us to obtain 2-dimensional notions of group-groupoids.

Duplicity in possessive merger: evidence from Spanish alienable possessive constructions

In this paper, I argue that Spanish prenominal and postnominal possessives target different external merge positions focusing on alienable possessive constructions. The analysis is developed alongside a proposal on the organization of DPs, according to which articles are merged as a DP-internal category between the domains assigned to direct and indirect modifiers. Prenominal possessives are determiners reanalyzed from direct modification adjectives whereas postnominal possessives are indirect modification adjectives that arise as predicates of reduced relative clauses. This analysis provides a principled explanation on the behavior of Spanish possessives that is lacking in the generalized idea that they are pronouns with a unique merge position. Arguments are also presented showing that syntax-driven phonological restrictions condition the derivation of DPs. The account successfully derives the core properties of word order variation and related issues within possessive constructions.