### On the Semantics of Intensionality

**2016-02-03**

1602.01365 | cs.LO

In this paper we propose a categorical theory of intensionality. We first
revisit the notion of intensionality, and discuss we its relevance to logic and
computer science. It turns out that 1-category theory is not the most
appropriate vehicle for studying the interplay of extension and intension. We
are thus led to consider the P-categories of \v{C}ubri\'{c}, Dybjer and Scott,
which are categories only up to a partial equivalence relation (PER). In this
setting, we introduce a new P-categorical construct, that of exposures.
Exposures are very nearly functors, except that they do not preserve the PERs
of the P-category. Inspired by the categorical semantics of modal logic, we
begin to develop their theory. Our leading examples demonstrate that an
exposure is an abstraction of well-behaved intensional devices, such as G\"odel
numberings. The outcome is a unifying framework in which classic results of
Kleene, G\"odel, Tarski and Rice find concise, clear formulations, and where
each logical device or assumption involved in their proofs can be expressed in
the same algebraic manner.

**Login to like/save this paper, take notes and configure your recommendations**

# Related Articles

**2019-04-27**

1904.12137 | cs.LO

We introduce a new form of logical relation which, in the spirit of metric
relations, allows us to a… show more

**2019-05-01**

1905.00787 | cs.LO

Computational philosophy is the use of mechanized computational techniques to
unearth philosophical … show more

**2019-04-01**

1904.00827 | cs.LO

We show how the categorical logic of untyped, simply typed and dependently
typed lambda calculus can… show more

**2018-10-19**

1810.08380 | cs.LO

We present an extension to the $\mathtt{mathlib}$ library of the Lean theorem
prover formalizing the… show more

**2019-04-22**

1904.09810 | math.LO

We develop the Scott model of the programming language PCF in constructive
predicative univalent typ… show more

**2019-05-10**

1905.04058 | math.LO

Nets are generalisations of sequences involving possibly uncountable index
sets; this notion was int… show more

**2019-01-23**

1901.07820 | cs.LO

This paper describes how to use Lee, Jones and Ben Amram's size-change
principle to check correctnes… show more

**2018-05-09**

1805.03740 | cs.LO

We present a device for specifying and reasoning about syntax for datatypes,
programming languages, … show more

**2018-05-22**

1805.08605 | cs.LO

Reversible computing models settings in which all processes can be reversed.
Applications include lo… show more

**2017-12-13**

1712.04864 | cs.LO

The homotopical approach to intensional type theory views proofs of equality
as paths. We explore wh… show more

**2018-02-15**

1802.05629 | cs.LO

This paper introduces a new family of models of intensional Martin-L\"of type
theory. We use constru… show more

**2018-04-09**

1804.02809 | cs.LO

This paper investigates modal type theories by using a new categorical
semantics called change-of-ba… show more

**2019-04-02**

1904.01679 | math.CT

The humble $\dagger$ ("dagger") is used to denote two different operations in
category theory: Takin… show more

**2018-10-31**

1810.13261 | cs.LO

In type theory, coinductive types are used to represent processes, and are
thus crucial for the form… show more

**2016-02-15**

1602.04860 | cs.LO

We show how to derive natural deduction systems and modal lambda calculi for
constructive versions o… show more

**2015-07-19**

1507.05305 | cs.CC

We examine various categorical structures that can and cannot be constructed.
We show that total com… show more

**2018-01-31**

1802.00061 | cs.PL

We present gradual type theory, a logic and type theory for call-by-name
gradual typing. We define t… show more