# nLab linear implication

Contents

### Context

#### Mapping space

internal hom/mapping space

# Contents

## Idea

Linear implication is the most common version of implication/function type in linear logic/linear type theory.

The categorical semantics of linear implication is as the internal hom in the closed monoidal category of types.

Closely related is the multiplicative implication of bunched implication logic, though they behave somewhat differently.

Last revised on May 3, 2016 at 15:43:26. See the history of this page for a list of all contributions to it.