Bicategorical W-types with reductions and elementary bitopos structure

Let $A$ be the partial combinatory algebra underlying the assembly category, and let $\mathrm{p}\mathbbm{Grpd}(\operatorname{Asm}(A))$ be the category of partitioned groupoid assemblies. A bicategorical $W$-type with reductions is the bicategorical analogue of a $W$-type with reductions. An elementary bitopos is a bicategory satisfying the finite bilimit and bicolimit, homotopy exponent, elementary-topos $0$-type, bipullback biadjoint, sub-object biclassifier, and univalent object-biclassifier conditions listed in the paper. Bicategorical W-type conjecture. $\mathrm{p}\mathbbm{Grpd}(\operatorname{Asm}(A))$ has bicategorical $W$-types with reductions and is an elementary bitopos. The paper says that the first three bitopos conditions already hold, while the remaining conditions and the relevant truncation and modestness notions remain to be checked.