Metatheory

This directory contains files that prove important metatheoretic results about HoTT, but that are not important for internal development of mathematics in HoTT. Thus, no files in this directory should ever need to be imported by files outside of this directory. Many of these results are about ways to prove univalence and function extensionality (which in the main library we simply assert as axioms, though we track their usage with dummy typeclasses). For convenience, here we define the types of these two statements.

Univalence is a property of a single universe; its statement lives in a higher universe