3 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…