# nLab linear implication

### 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.