Existence of an univalent path category of infinity-types over the effective topos

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 called discrete when it belongs to the proposed class of discrete fibrations, and a class of small fibrations is impredicative when it is closed under the relevant impredicative constructions; a univalent representation is a representing fibration satisfying the univalence condition. The $\mathbb{EFF}_\infty$ conjecture. There should exist a path category with homotopy $\Pi$-types $\mathbb{EFF}_\infty$ in which the class of small discrete fibrations is impredicative and has a univalent representation. These discrete fibrations should be definable using an internal orthogonality condition, and propositional resizing should hold for them. This is proposed as the limiting member of a hierarchy extending the path categories $\mathbb{EFF}_n$, with each $\mathbb{EFF}_n$ expected to arise as the path category of $n$-types in $\mathbb{EFF}_\infty$. The existence and the asserted properties of this path category are directions for future research rather than results established in the paper.