# The Scott model of PCF in univalent type theory

## TL;DR

This paper constructs the Scott model of PCF within univalent type theory, demonstrating that partiality can be modeled constructively and predicatively using the lifting monad, avoiding choice or quotient inductive types.

## Contribution

It develops a constructive, predicative Scott model of PCF in univalent type theory using the lifting monad, avoiding additional axioms or complex type constructions.

## Key findings

- Lifting monad effectively models partiality in univalent type theory.
- Constructive and predicative Scott model of PCF is achievable.
- Avoids reliance on choice or quotient inductive-inductive types.

## Abstract

We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the lifting monad (also known as the partial map classifier monad) from topos theory, which has been extended to univalent type theory by Escard\'o and Knapp. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or quotient inductive-inductive types. We show that one can do without these extensions.