# Univalent polymorphism

## TL;DR

This paper constructs models of Homotopy Type Theory within the effective topos using path categories, demonstrating univalent representations for propositions and sets, thus connecting to the Calculus of Constructions.

## Contribution

It introduces a path category model of the effective topos with univalent representations for propositions and sets, advancing the understanding of homotopy-theoretic models in type theory.

## Key findings

- Effective topos as homotopy category of a path category
- Existence of a univalent universe of propositions
- Construction of a univalent universe of sets

## Abstract

We show that Martin Hyland's effective topos can be exhibited as the homotopy category of a path category $\mathbb{EFF}$. Path categories are categories of fibrant objects in the sense of Brown satisfying two additional properties and as such provide a context in which one can interpret many notions from homotopy theory and Homotopy Type Theory. Within the path category $\mathbb{EFF}$ one can identify a class of discrete fibrations which is closed under push forward along arbitrary fibrations (in other words, this class is polymorphic or closed under impredicative quantification) and satisfies propositional resizing. This class does not have a univalent representation, but if one restricts to those discrete fibrations whose fibres are propositions in the sense of Homotopy Type Theory, then it does. This means that, modulo the usual coherence problems, it can be seen as a model of the Calculus of Constructions with a univalent type of propositions. We will also build a more complicated path category in which the class of discrete fibrations whose fibres are sets in the sense of Homotopy Type Theory has a univalent representation, which means that this will be a model of the Calculus of Constructions with a univalent type of sets.