We develop the Scott model of the programming language PCF in constructive predicative univalent type theory. To account for the non-termination in PCF, we work with the partial map classifier monad (also known as the lifting monad) from topos theory, which has been extended to constructive type theory by Knapp and Escardo. 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 higher inductive-inductive types. We show that one can do without these extensions.
Partiality in type theory has been the subject of recent study. We briefly discuss the different approaches. First, there are Capretta's delay monad and its quotient by weak bisimilarity, which have been studied by Uustula, Chapman and Veltri @cite_1 . A drawback of the quotient is that some form of choice is needed (countable choice suffices) to show that it is again a monad. Another approach is laid out in @cite_3 by Altenkirch, Danielsson and Kraus. They construct (essentially by definition) the free @math -cpo with a least element using a higher inductive-inductive type. Moreover, show that, assuming countable choice, their free @math -cpo coincides with the quotiented delay monad. In @cite_2 , Knapp showed that, assuming countable choice, a restricted version (using a dominance) of the lifting is isomorphic to the quotiented delay monad.
@cite_1 @cite_3 @cite_2
2963889233 2905240033 2565502105 2215703121
Capretta's delay monad can be used to model partial computations, but it has the wrong'' notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the right''notion of equality, weak bisimilarity. However, recent work by suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory---a higher inductive-inductive type---we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications. We investigate partial functions and computability theory from within a constructive, univalent type theory. The focus is on placing computability into a larger mathematical context, rather than on a complete development of computability theory. We begin with a treatment of partial functions, using the notion of dominance, which is used in synthetic domain theory to discuss classes of partial maps. We relate this and other ideas from synthetic domain theory to other approaches to partiality in type theory. We show that the notion of dominance is difficult to apply in our setting: the set of �0 1 propositions investigated by Rosolini form a dominance precisely if a weak, but nevertheless unprovable, choice principle holds. To get around this problem, we suggest an alternative notion of partial function we call disciplined maps. In the presence of countable choice, this notion coincides with Rosolini’s. Using a general notion of partial function,we take the first steps in constructive computability theory. We do this both with computability as structure, where we have direct access to programs; and with computability as property, where we must work in a program-invariant way. We demonstrate the difference between these two approaches by showing how these approaches relate to facts about computability theory arising from topos-theoretic and typetheoretic concerns. Finally, we tie the two threads together: assuming countable choice and that all total functions N - N are computable (both of which hold in the effective topos), the Rosolini partial functions, the disciplined maps, and the computable partial functions all coincide. We observe, however, that the class of all partial functions includes non-computable partial functions. A family of syntactic models for the calculus of construction with universes (CCω) is described, all of them preserving conversion of the calculus definitionally, and thus giving rise directly to a program transformation of CCω into itself. Those models are based on the remark that negative type constructors (e.g. dependent product, coinductive types or universes) are underspecified in type theory-which leaves some freedom on extra intensional specifications. The model construction can be seen as a compilation phase from a complex type theory into a simpler type theory. Such models can be used to derive (the negative part of) independence results with respect to CCω, such as functional extensionality, propositional extensionality, univalence or the fact that bisimulation on a coinductive type may not coincide with equality. They can also be used to add new principles to the theory, which we illustrate by defining a version of CCω with ad-hoc polymorphism that shows in particular that parametricity is not an implicit requirement of type theory. The correctness of some of the models program transformations have been checked in the Coq proof assistant and have been instrumented as a Coq plugin. Whereas formal category theory is classically considered within a @math -category, in this paper a double-dimensional approach is taken. More precisely we develop such theory within the setting of hypervirtual double categories, a notion extending that of virtual double category by adding cells with nullary target. [...] After this the notion of weak' Kan extension within a hypervirtual double category is considered, together with three strengthenings. [...] The notion of yoneda embedding is then considered in a hypervirtual double category, and compared to that of a good yoneda structure on a @math -category; the latter in the sense of Street-Walters and Weber. Conditions are given ensuring that a yoneda embedding @math defines @math as the free small cocompletion of @math , in a suitable sense. In the second half we consider formal category theory in the presence of algebraic structures. In detail: to a monad @math on a hypervirtual double category @math several hypervirtual double categories @math of @math -algebras are associated, [...]. This is followed by the study of the creation of, amongst others, left Kan extensions by the forgetful functors @math . The main motivation of this paper is the description of conditions ensuring that yoneda embeddings in @math lift along these forgetful functors, as well as ensuring that such lifted algebraic yoneda embeddings again define free small cocompletions, now in @math . As a first example we apply the previous to monoidal structures on categories, hence recovering Day convolution of presheaves and Im-Kelly's result on free monoidal cocompletion, as well as obtaining a "monoidal Yoneda lemma".