# Constructive Univalent Foundations

## An NSF EAGER Project

### Introduction

We investigate concepts unique to Nuprl's constructive type theory that are playing a critical role in the formalization of homotopy type theory, a proposed theoretical basis for next generation proof assistants.

...more