Library UniMath.Bicategories.ComprehensionCat.Universes.UniverseBiequiv

Categories with universes versus comprehension categories with universes Clairambault and Dybjer established a biequivalence between the bicategory of democratic categories with families that support ∑-types and extensional identity types, and the bicategory of finitely complete categories. This biequivalence can be established in the univalent setting as well: specifically, the bicategory of univalent democratic full comprehension categories that support unit types, product types, ∑-types, and extensional identity types is equivalent to the bicategory of univalent categories with finite limits. One can extend this biequivalence in various ways by including more and more type formers. In this file, we extend the aforementioned biequivalence with universe types. Specifically, we show that the bicategory of univalent categories with finite limits and a universe type is biequivalence to the bicategory of univalent democratic full comprehension categories that support unit types, product types, ∑-types, extensional identity types, and a universe type. These universes are in Tarski-style, and they are represented in a way that is close to what one would expect from a type theoretic perspective. Specifically, all of the rules regarding Tarski-style universes are postulated. The necessary ingredients of the desired biequivalences are constructed in other files, and here we only put them to obtain a biequivalence. References

• "The biequivalence of locally cartesian closed categories and Martin-Löf type theories" by Clairambault and Dybjer
• "The internal languages of univalent categories" by Van der Weide