4 problems

Tricategorical univalence conjecture. The tricategory of univalent weak double categories is univalent.

Enriched profunctor conjecture. (Enriched) categories, (enriched) functors and (enriched) profunctors assemble into a univalent weak double category, but not into a univalent doubl…

A path category with homotopy $\Pi$-types is a category equipped with the path-category structure and dependent products needed to interpret homotopy type theory. A fibration is ca…

In Martin-Löf type theory, let $\mathtt{N}$ be the type of natural numbers, let $t:\mathtt{N}$ be an arbitrary term, and let a numeral $n:\mathtt{N}$ denote a canonical natural-num…