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.