Contents

# Contents

## Idea

A reflective sub-universe. If closed under dependent sum, then this is the universe of modal types for a modal operator.

For the relation to modal type theory see Rijke, Shulman, Spitters.

## Properties

…in categorical semantics this means that it is an exponential ideal, hence that the reflector preserves finite products

## References

Last revised on June 28, 2017 at 04:40:43. See the history of this page for a list of all contributions to it.