# Retractions in Intersection Types

## TL;DR

This paper characterizes when one intersection type can be embedded into another via retraction, providing necessary and sufficient conditions and exploring implications in standard intersection types.

## Contribution

It introduces a precise criterion for retraction in intersection types and extends the understanding of type embeddings in lambda calculus.

## Key findings

- Established necessary and sufficient conditions for retraction between strict intersection types.
- Characterized retraction in standard intersection types.
- Provided insights into type isomorphisms and embeddings in lambda calculus.

## Abstract

This paper deals with retraction - intended as isomorphic embedding - in intersection types building left and right inverses as terms of a lambda calculus with a bottom constant. The main result is a necessary and sufficient condition two strict intersection types must satisfy in order to assure the existence of two terms showing the first type to be a retract of the second one. Moreover, the characterisation of retraction in the standard intersection types is discussed.