In the middle of the Mediterranean sea, historically characterised by large spatial and temporal climate variability, the island of Sicily, a unique ethnic and cultural crossroad for millennia, has not been spared by global warming and environmental change. On the island, remote rural areas suffer today the severe progressive degradation of their biocultural heritage, accompanied by serious marginalisation due to contrasting and simultaneous processes of rural depopulation and land abandonment on the one side and agricultural intensification on the other. This chapter looks at climate and environmental changes as reported by locals in one of these remote areas, the Morello Valley, a fluvial system in central Sicily, and compares local observations with temperature and rainfall data collected by the nearest meteorological stations. Then, inspired by historical ecology, the chapter discusses the results of a longer-term reconstruction of the climatic, environmental, and societal past of this part of Sicily, covering the entire Holocene. Conclusions highlight the importance of taking into account both different spatial and temporal scales when approaching the climate discourse, cultural constructs derived from socio-cultural and historical events, and contemporary and place-based local perceptions.

This thesis contains three papers, all in the general area of categorical logic, together with an introductory part with some minor results and proofs of known results which does not appear to be (easily) available in the literature.

In Papers I and II we investigate the formal system Intuitionistic Ramified Type Theory (IRTT), introduced by Erik Palmgren, as an approach to predicative topos theory. In Paper I we construct and study the category of "local sets" in IRTT, including an extension with inductive definitions. We there also give a model of IRTT in univalent type theory using h-sets. In Paper II we adapt triposes and hyperdoctrines to the ramified setting. These give a categorical semantics for certain formal languages ramified in the same way as IRTT.

Paper III, which is part of a joint project with Henrik Forssell, concerns logical aspects of the localic groupoid/category representations of Grothendieck toposes that originate from the work of Joyal and Tierney. Working constructively, we give explicit logical descriptions of locales and localic categories used for representing classifying toposes of geometric theories. Aspects of these descriptions are related to work by Coquand, Sambin et al in formal topology, and we show how parts of their work can be captured and extended in our framework.