Translating notions and results from category theory to the theory of computability models of Longley and Normann, we introduce the Grothendieck computability model. We define the corresponding firstprojection-simulation, and we prove some of its basic properties. With the Grothendieck computability model the category of computability models is shown to be a type-category, in the sense of Pitts, a result that bridges the categorical interpretation of dependent types with the theory of computability models. We introduce the notion of a fibration and opfibration-simulation, and we show that the ifrst-projection-simulation is a split opfibration-simulation.
between computability models, avoid equality too, involving certain forcing and tracking relations instead.
Working within the direction “from categories to computability models” in this paper too,
we “translate” the categorical Grothendieck construction and the categorical notion of split
(op)fibration to the partial and without equality, or relational framework of computability
models. The Grothendieck computability models become then the Sigma-objects, in the sense
of Pitts [
• In section 6 we include some questions and topics for future work.
For all notions and results from category theory that are used here without explanation or
proof we refer to [
Definition 2.1. A (strict) computability model C consists of the following data: a class , whose members are called type names; for each ∈ a set C() of data types; for each , ∈ a class C[, ] of computable functions, i.e., partial functions from C() to C(). Moreover, for every , , ∈ the following hold: 1. The identity 1C() is in C[, ]. 2. For every ∈ C[, ] and ∈ C[, ] we have that ∘ ∈ C[, ].
Next, we describe the computability model of sets and partial functions Sets, as the computability model-analogue to the category of sets and functions Sets.
The computability model Sets has as type names the class of sets and as data types the set itself, for every type name . If , are sets, the computable functions from to is the class of partial functions from to .
A partial arrow (, ) : ⇀ in a category consists of a monomorphism : dom() →
and an arrow : dom() → in . Given a (covariant) presheaf : → Sets, we write (, )
instead of (︀ (), ( ))︀ . In [
Let be a category and : → Sets a presheaf on . The total canonical computability model CMtot(; ) over and has as type names the class of objects 0 of and data types the sets (), for every ∈ 0. If 1, 2 ∈ 0, the (total) functions from (1) to (2) is the class {( ) | ∈ Hom(1, 2)}. The partial canonical computability model CMprt(; ) over and a pullback-preserving presheaf has the same type names and data types, while the partial functions from (1) to (2) is the class {(, ) | (, ) : 1 ⇀ 2}.
The pullback-preserving property on is necessary to prove that CMprt(; ) is a computability model. We can also use the category Setsprt of sets and partial functions, and the computability model CMtot(Setsprt, idSetsprt ) is the computability model Sets of Definition 2.2. Next, we describe the arrows in the category of computability models CompMod. A notion of contravariant simulation can also be defined, allowing the contravariant version of the Grothendieck construction for computability models.
A simulation from C (over ) to D (over ) consists of a class-function : → and a relation ⊩ ⊆ subject to the following conditions:
D︀( ())︀ ×
C(), for each ∈ (a so-called forcing relation), 1. For each ∈ C() there exists some ∈ D( ()), such that ⊩ . 2. For each ∈ C[, ] there exists some ′ ∈ D︀[ (), ()]︀ such that
∀∈C()∀∈D( ())︀( ∈ dom( ) ∧ ⊩ ⇒ ∈ dom( ′) ∧ ′() ⊩ ())︀ . In this case we say that ′ tracks , and we write ′ ⊩ (,) . We also write : C _ D for a ︀( ∘ , (⊩ ∘ )∈ ︀) , where the relation ⊩ ∘ ⊆
E︀( ( ()))︀ × C() is defined by simulation from C to D. We call a simulation : C _ for every ′, ∈ The identity simulation 1C : C _ C is the pair (︀ id , (⊩ C )∈ ︀) , where ′ ⊩ C :⇔ ′ = , C(). If : D _ E, the composite simulation ∘ : C _ E is the pair
⊩ ∘ :⇔ ∃∈D( ())︀( ⊩ () ∧ ⊩ ︀) .
The following presheaf-simulations on a computability model C correspond to the representable functors Hom(, − ) over in a category .
Example 2.5. Let C be a locally-small computability model over , i.e., the class C[, ] of C[0, ], for every ∈ , and the forcing relations ⊩ ⊆ C[0, ] × computable functions from C() to C() is a set, for every , ∈ . If 0 ∈ , the representablesimulation 0 : C _ Sets consists of the class-function 0 : → Sets, defined by 0 () :=
0 ⊩ 0 :⇔ ∃∈dom()︀( () = )︀ . To show that 0 is a simulation, we also need to suppose that C is left-regular i.e., ∀∈ ∀∈C()∃∈C[0,]∃∈dom()︀( () = )︀ .
All computability models that include the constant functions are left-regular (such as Kleene’s ifrst model 1 over = {0} with C(0) = N, and C[0, 0] the Turing-computable partial 0 functions from N to N). If ∈ C[, ], it is easy to show that * ⊩ (,) , where * is the total function from C[0, ] to C[0, ], defined by * () := ∘ , for every ∈ C[0, ]. A right-regularity condition on a locally-small computability model is needed, to define the contravariant representable-simulations 0 : C _ Sets, where 0 : C → Sets is defined by 0 () := C[, 0], for every ∈ .
Next follows the notion of an arrow between simulations.
Definition 2.6. If , : C _ D, then is transformable to , in symbols ⪯ , if for every ∈ there is ∈ D[ (), ()] such that
∀∈C()∀′∈D( ())︀( ′ ⊩ ⇒ ′ ∈ dom( ) & (′) ⊩ ︀) . 3. The Grothendieck computability model The Grothendieck computability model is the categorical counterpart to the category of elements, a special case of the general categorical Grothendieck construction. A category is replaced by a computability model C, and a (covariant) presheaf : → Sets by a (covariant) simulation : C _ Sets. Moreover, the first-projection functor is replaced by the ifrst-projection-simulation.
Proposition 3.1. Let C be a computability model over the class together with a simulation : C _ Sets. The structure ∑︀C with type names the class with data types, for every (, ) ∈ ∑︀∈ (), the sets ∑︁ () := {︀ (, ) | ∈ and ∈ ()}︀ , ∈ ︁( ∑︁ )︁ (, ) := {︀ ∈ C() | ⊩ ︀} ,
C and computable functions from ︁( ∑︀C ︁) (, ) to ︁( ∑︀C ︁) (, ) the classes {︁ ∈ C[, ] | ∀∈dom()︁( ∈ ︁( ∑︁ )︁ (, ) ⇒ () ∈ ︁( ∑︁ )︁ (, )︁)}︁ ,
C
C is a computability model. The class-function pr1 : ∑︀∈ () → , defined by the rule (, ) ↦→ , and the forcing relations, defined, for every (, ) ∈ ∑︀∈ (), by determine the first-projection-simulation pr1 : ∑︀C _ C.
′ ⊩ (pr,1) :⇔ ′ = , Proof. We show that the computable functions include the identities and are closed under ∑︀∈ composition. Notice that the defining property of the computable functions in the Grothendieck model is equivalent to the condition ⊩ ⇒ ⊩ (), for every ∈ dom( ). If (, ) ∈ (), then the identity on ∑︀C (, ) is the identity on C(), i.e., 1C() is a computable function from
(, ) to itself: if ∈ C(), then the implication ⊩ ⇒ ⊩ holds hence ⊩ ( ()). Next, we show that pr1 is a simulation. If ∈ trivially. If is a computable function from ∑︀C (, ) to ∑︀C (, ) and is a computable function from ∑︀C (, ) to ∑︀C (, ), then ∘ is a computable function from ∑︀C (, ) to ∑︀C (, ). For that, let ∈ dom( ) and () ∈ dom(). If ⊩ , then ⊩ (), and ∑︀C (, ), then ⊩ (pr,1) , pr1 and if is a computable function from ∑︀C (, ) to ∑︀C (, ), then ⊩ ((,),(,)) .
The following proposition expresses that the Grothendieck construction on a computability model obtained from a category with a presheaf can be presented as the canonical partial computability model associated to the category of elements. The proof is omitted as it is straightforward. let [( )]() := . Then Proposition 3.2. Let be a category and : → Sets a pullback-preserving presheaf on . Let : 0 _ Sets be defined via () = () and the relations ⊩ are simply the diagonal, and let {pr2} : ∑︀ → Sets be defined by {pr2}(, ) := {} and if : (, ) → (, ) in ∑︀ , ∑︁ CMprt(;) = CMprt (︁ ∑︁ ; {pr2})︁ .
id1 : 1 _ Sets, and show that
Remark 3.3. The functor C ↦→ sm(C), studied in [
= 1
∑︁ sm (1) sm(id1).
Next we show an analogous result to [6, Proposition 1.1.7]. Our goal is to show that for any presheaf simulation : C _ Sets we obtain an equivalence We do this by exhibiting a full, faithful and essentially surjective functor
C
C [︁ ∑︁ , Sets ]︁ ∼= [C, Sets]/ . : [︁ ∑︁ , Sets ]︁
→ [C, Sets]/ . Notice, that for both categories the morphism structure is thin and thus a preorder, thus we only need to define our functor on morphisms and show that it preserves this preorder. More explicitly the objects of [C, Sets]/ themselves are simply simulations : C _ Sets such that ⪯ . For all simulations : C _ Sets we have that for all ∈ the set () is nonempty. This stems from the fact that otherwise ⊩ could not fulfil the first condition on simulations as () is empty so no ∈ () with ⊩ for any ∈ C(). (There is the possibility that C() is empty, but we shall exclude this from now on). Due to space restrictions the proof of the following proposition is omitted. ( ) be the underlying class function ( ) : → Sets, where, for every ∈ , There is a functor : [︀ ∑︀C , Sets ]︀
→ [C, Sets]/ defined as follows: if : ∑︀C Proposition 3.4. Let C over be a computability model and : C _ Sets be a simulation. _ Sets, let The tracking relation ⊩ ( )⊆ (︀ ⋃︀ ∈ () (, ))︀ × C() is defined as follows: ( )() =
⋃︁ (, ).
∈ () ⊩ ( ) :⇔ ∃∈ ()︀( ⊩ (,) ︀) .
The functor is full, faithful, and essentially surjective.
4. Computability models form a type-category
In this section we show that the category of computability models CompMod is a type-category,
in the sense of Pitts [
∑︀D , such that the following is a : C _ D, : D _ Sets defined by the rule Proof. To define ∑︀ , let the underlying class-function ∑︀ : ∑︀∈
() → ∑︀∈ () be ︀( (), ). The corresponding forcing relations are defined by ′ ⊩ (∑︀,) :⇔ ′ ⊩ . It is straightforward to show that ∑︀ is a simulation. Next we show that the above square commutes. On the underlying classes this is immediate as pr1 (︀ ∑︁ (, ))︀ = pr1 (︀ ())︀ = (︀ pr1(, ))︀ .
On the forcing relations we observe that if ′ ⊩ (,) , which is also equivalent to ′ ⊩ (∘,p)r1 . Finally, we show the pullback property. Let a computability model E over a class with simulations , be given, such that the following pr1 ∘ ∑︀ , then ′ ⊩ (∑︀,) , and thus ′ ⊩ rectangle commutes We find a unique simulation : E _ ∑︀C( ∘ ) such that both following triangles _
E C _ ∑︀D ∑︀C( ∘ )
_ pr1 _ C ∑︀ _
_ ∑︀D _
D Next we define the forcing relations. Let commute. First we define on the level of the underlying classes. If ∈ , let () = (︀ (), )︀ , where ∈ ( ()) is the unique such that () = (, ) for some . Clearly, is well-defined.
′ ⊩ :⇔ ′ ⊩ . ∈ and ′′ ∈ E(), ′ ∈ ︁( ∑︀D
︁) (︀ ())︀ and ∈ C︀( ())︀ such that This relations are well-defined and in conjunction with the aforementioned class-function they constitute a simulation. Observe that the two triangles already commute on the level of the underlying class-functions, so it remains to check the forcing relations. Assume we are given ′ ⊩ ′′ and ⊩ ′′.
By definition we have to show that there exist 1, 2 such that ′ ⊩ ∑(︀) 1 and 1 ⊩ ′′, and ⊩ pr(1) 2 and 2 ⊩ ′′.
pr1 We know that the square (1) commutes and ′ ⊩ (∑︀ )( ()) ′, thus from ′ ⊩ ′′ we conclude that ′ ⊩ ∘ ′′. This in turn ensures that there is such that ′ ⊩ () and ⊩ ′′. By definition of ∑︀ we then have that ′ ⊩ ∑︀( ) and thus is our desired 1. For 2 we simply choose and it is easy to see that this fulfills the requirements. The above implications also work in the reverse direction. It is immediate to show that is the unique simulation making the triangles commutative, as it is determined by the definition of , . (ii) ∑︀ ( ∘ ) = ∑︀ ∘ ∑︀( ∘ ) .
Proof. (i) It sufices to observe that by its definition the simulation underlying class takes a pair (, ) to (1E(), ) = (, ), so on the level of the underlying class-functions the two simulations agree. For the forcing relations we see that both simulations ∑︀ 1E on the level of the are the corresponding diagonal. (ii) To verify this equation on the level of underlying classes we have that ∑︁( ∘ )(, ) = (︀ , ( ∘ )())︀ = ∑︁ (︀ , ())︀ = ∑︁ (︁ ∑︁ )︁ ∘ (, ) .
︁) For the forcing relations we simply remark that ⊩ (,) we have that ⊩ (∑︀,) if and only if ⊩ , and ⊩ (,) ∑︀ ∘ if and only if ⊩ . Hence, ⊩ (,) ∑︀ ∘ ∑︀ ∘ if and only if ⊩ ∘ , which by the above is equivalent to ⊩ (,) ∑︀ ∘ .
∑︀ ∘ if and only if ⊩ ∘ . Similarly, Theorem 4.3. The category CompMod is a type-category.
Proof. This follows immediately from Lemma 4.1, Lemma 4.2, and the fact that CompMod has a terminal object, as explained in Remark 3.3.
This result bridges the categorical interpretation of dependent types with the theory of computability models. In section 6 we discuss its importance and its role in our future work. 5. Fibration-simulations and opfibration-simulations The (covariant) Grothendieck construction allows the generation of fibrations (opfibrations), as the first-projection functor pr1 : ∑︀
→ is a (split) opfibration, if is a covariant presheaf, or a (split) fibration, if is a contravariant presheaf. In this section we introduce the notion of a fibration and opfibration-simulation and we show that the first-projectionsimulation pr1 : ∑︀C presheaf-simulations. The dual result is shown similarly.
_ C is a (split) opfibration-simulation, as we work with covariant In this section, E is a computability model over and B a computability model over . Moreover, the pair := ︂( : : → , (︀ ⊩ )︀ ∈ ︂) is a simulation of type E _ B.
In contrast to what it holds for functors, for simulations : E _ in E is tracked, in general, by a multitude of maps ′ in B. Thus, for each opspan
E(1) _
E(2)
E(3) we have a whole class, in general, of opspans
B( (2)) B( (1))
′_ such that ′ tracks and ′ tracks .
B( (3)) 1–13 E(′′)
B((′′)) ⊩ ′′
E()
E(′)
⊩ ′′ E() E(′) ⊩ ⊩ ′ ⊩ ⊩ ′ ℎ
′ ′ ℎ
B(())
′ B((′)) B(()) B((′)) Definition 5.1 (Cartesian computable function). Let ′ ∈ B[, ′] and ′ ∈ , such that (′) = ′ be given. We call a computable function ∈ E[, ′] cartesian for ′ and ′, if ′ ⊩ (,′) , and given computable functions ∈ E[′′, ′], ′ ∈ B[(′′), (′)], and ℎ ∈ B[(′′), ()] as in the following diagram that is ′ tracks , there is some ∈ E[′′, ] satisfying the following property: ℎ ⊩ (′′,) , and for every ∈ E(′′), ∈ B((′′)), such that ⊩ ′′ , ∈ dom( ′ ∘ ℎ) ∩ dom(′), and ′(ℎ()) = ′(), then ∈ dom( ∘ ) ∩ dom() and () = (()).
Definition 5.2 (Opcartesian computable function). Let ′ ∈ B[′, ] and ′ ∈ , such that (′) = ′ be given We call a computable function ∈ E[′, ] opcartesian for ′ and ′, if ′ ⊩ (′,′) , and given computable functions ∈ E[′, ′′], ′ ∈ B[(′), (′′)] and ℎ ∈ B[(), (′′)] as in the following diagram
E(′′)
B((′′)) ′ that is ′ tracks , there is some ∈ E[, ′′] satisfying the following property: ℎ tracks , and for every ∈ E(′), ∈ B((′)), such that ⊩ ′ , ∈ dom(ℎ ∘ ′) ∩ dom(′), and ′(ℎ()) = ′(), then ∈ dom( ∘ ) ∩ dom() and () = ( ()).
Note that the computable functions ∈ E[′′, ] and ∈ E[, ′′] in the above two definitions, respectively, are not unique.
tDioenfin,iitfiofonr 5ev.3ery(Fcoibmraptuiotanb-lsei mfuunlacttiioonn). W∈eBc︀[ all, (:E)]︀ _there is ∈ E[′, ] cartesian for and .
B a fibration-simulacase, we call a lift of .
Definition 5.4 (Opfibration-simulation) . We call : E → B an opfibration-simulation, if for every computable function ∈ B︀[ (), ︀] , there is ∈ E[, ′] opcartesian for and . In this Example 5.5. Let ℰ , ℬ be categories with presheaves , ′ and let : ℰ → ℬ be a fibration, such that ′ ∘ = . Then, : CMtot(ℰ ; ) _ CMtot(ℬ; ′) is a fibration-simulation.
To see this, assume we are given a computable function in CMtot(ℬ; ′), that is a function ′( ) : ′() → ′(′), and ∈ ℰ such that (′) = ′. As is a fibration, we find an arrow ′( ) and (′). For this, let functions (ℎ), (ℎ2), (2) as in the following diagram, : → ′ cartesian over and ′ . We show that () is the desired cartesian function over () (′′) ()
⊩ ′′ (2) () (′) ⊩
′(′′)
⊩ ′ ′(ℎ) ′()
′() ′(ℎ2) ′(′) over ′( ) and (′). be given, where we used that CMprt(ℰ ; )() = () and CMprt(ℬ; ′)() = (), for every and , respectively. As is cartesian over and ′, we obtain an arrow : ′′ → , such that ∘ = 2 and () = ℎ2. Obviously, () is the function needed, and hence () is cartesian Proposition 5.6. If C is a computability model and : C ifrst-projection-simulation pr1 : ∑︀C _ C is an opfibration-simulation.
→ Sets a simulation, then the Proof. Assume we are given a computable function ∈ C[, ′] and pr1(, ) = . We need to find some ∈ ︁) [︀ (, ), (′, ′)]︀ , such that ⊩ ((,),(′,′)) ′. By definition we know that ⊩ ((,),(′,′)) pr1 pr1
C(′), such that pr1(′, ′) = ′, and a computable function ′ ∈ ′ if and only if = ′, so we have to find
∈ C(′), such that () = ′. For this, we simply take ′ := (). To show that is opcartesian for and , we consider the following diagram
C()
C(′) and we observe that ℎ fills also the triangle on the left, as we have that = ℎ ∘ whenever they are defined, so in particular () = ℎ︀( ())︀ , and thus ′ = ℎ(′′). Hence, ℎ is a computable function from
Next we define split fibration-simulations and split opfibration-simulations.
Definition 5.7. A splitting for a fibration-simulation : E _ B is a rule △ that corresponds a pair (, ), where ∈ B[1, 2] and () = 2, to a function ′ ∈ E[, ′] cartesian for and . This rule △ is subject to the following conditions: • For every ∈ B[1, 2] and every ∈ B[2, 3] we have that
△( ∘ , 1) = △(, 1) ∘ △(, 2).
• For every ∈ we have that △(1B(), ) = (1E(), ).
A splitting for an opfibration-simulation : E _ B is a rule △ that corresponds a pair (, ), where ∈ B[1, 2] and () = 1, to a function ′ ∈ E[, ′] opcartesian over and . This rule △ is subject to the following conditions: • For every ∈ B[1, 2] and every ∈ B[2, 3] we have that
△( ∘ , 1) = △(, 2) ∘ △(, 1).
• For every ∈ we have that △(1B(), ) = (1E(), ).
A (op)fibration-simulation is split, if it admits a splitting △.
Corollary 5.8. The simulation pr1 : ∑︀C _ C is a split opfibration-simulation.
Proof. We can simply take pr1△ to be defined by the rule pr1△(, ) := (, ).
6. Conclusions and future work
In [
Table 1 includes the correspondences between categorical and computability model theorynotions presented here. It is natural to ask whether the category of presheaves, or more generally of all functors between two categories, can be translated within computability models. As a consequence, a Yoneda-type embedding and a corresponding Yoneda lemma for computability models and appropriate presheaf-simulations can be formulated. In such a framework the Grothendieck computability model is expected to have the same crucial role to the proof of a corresponding density theorem with that of the Grothendieck category to the proof of the categorical density theorem. For that, we need to introduce forcing and tracking-moduli in (op)cartesian arrow (op)fibration : ℰ → ℬ split (op)fibration pr1 : ∑︁ _ C
C (op)cartesian computable function (op)fibration-simulation : E _ B split (op)fibration-simulation the definition of a simulation i.e., realisers for the forcing and tracking relations. We hope to elaborate these concepts in subsequent work.
In [
C
with pr1 ∘ = 1C are the canonical dependent functions over C and .
Our approach to (op)fibration-simulations and (op)cartesian functions is diferent from the
2-categorical approach to fibrations in [