Relational Sheaves for a Heyting Algebra

TL;DR

This paper establishes an equivalence between categories of relational-presheaves and relational-sheaves for a Heyting algebra, connecting them to the classical categories of presheaves and sheaves.

Contribution

It introduces the concepts of relational-presheaves and relational-sheaves for Heyting algebras and proves their categorical equivalence to presheaves and sheaves, respectively.

Findings

Relational-presheaves are characterized as idempotent symmetric order-preserving lax-semifunctors.

Relational-sheaves are identified as idempotent infima-preserving lax semifunctors.

Categories of relational-presheaves and relational-sheaves are equivalent to presheaves and sheaves for ${\

Abstract

We show that for a Heyting algebra ${\cal H}$, a relational-presheaf is an idempotent symmetric order-preserving lax-semifunctor. A relational-presheaf is a relational-sheaf, if it is an idempotent infima-preserving lax semifunctor. The associated relational-sheaf functor factors through the category of sheaves for ${\cal H}$. Using this and the appropriate comparison theorems we obtain the main result that the associated categories of relational-presheaves and relational-sheaves are each respectively equivalent to the categories of presheaves and sheaves for ${\cal H}$.