Contents

# Contents

## Idea

The refinement of modal type theory to homotopy type theory: hence homotopy type theory equipped with higher modalities.