Indexed and Fibred category theory have a long tradition in computer science as a language to formalize different presentations of the notion of a logic, as for instance, in the theory of institutions and general logics, and as unifying models of logic and type theory as well. Here we introduce the notions of indexed and fibred frames and construct a rich mathematical workspace where many relevant and useful concepts of logics can be elegantly modelled. To demonstrate the applicability of these …
Read moreIndexed and Fibred category theory have a long tradition in computer science as a language to formalize different presentations of the notion of a logic, as for instance, in the theory of institutions and general logics, and as unifying models of logic and type theory as well. Here we introduce the notions of indexed and fibred frames and construct a rich mathematical workspace where many relevant and useful concepts of logics can be elegantly modelled. To demonstrate the applicability of these tools, essential ideas around the theory of institutions are recasted and described
