日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

A General Semantic Construction of Dependent
Reﬁnement Type Systems, Categorically
Satoshi Kura
Dependent reﬁnement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent reﬁnement type systems from underlying type systems and predicate logic, that is, a construction of liftingsof closed comprehension categories from given (underlying) closed comprehension categories and posetalﬁbrations for predicate logic. We give suﬃcient conditions to lift structures such as dependent products,
dependent sums, computational eﬀects, and recursion from the underlying type systems to dependent reﬁnement type systems. We demonstrate the usage of our construction by giving semantics to a dependent
reﬁnement type system and proving soundness.

1 Introduction
Dependent reﬁnement types [6] are types
equipped with predicates that restrict values in thetypes. They are used to specify preconditions andpostconditions which may depend on input values
and to verify that programs satisfy the speciﬁcations. Many dependent reﬁnement types systems
are proposed [5, 6, 13, 14, 25] and implemented in,e.g., F⋆ [23, 24] and LiquidHaskell [19, 26, 27].
In this paper, we address the question: “Howare dependent reﬁnement type systems, underlying type systems, and predicate logic related fromthe viewpoint of categorical semantics?” Althoughmost existing dependent reﬁnement type systems
are proved to be sound using operational semantics, we believe that categorical semantics is moresuitable for the general understanding of their nature, especially when we consider general computational eﬀects and various kinds of predicate logic(e.g., for relational veriﬁcation). This understanding will provide guidelines to design new dependent
reﬁnement type systems.
Our answer to the question is a general semantic
construction of dependent reﬁnement type systems
依存篩型システムの圏論的意味論による一般的な構成法

Satoshi Kura, 国立情報学研究所, National Institute ofInformatics.

from underlying type systems and predicate logic.
More concretely, given a closed comprehension category (CCompC for short) for interpreting an underlying type system and a ﬁbration for predicate
logic, we combine them to obtain another CCompC
that can interpret a dependent reﬁnement type system built from the underlying type system and thepredicate logic.
For example, consider giving an interpretation to
the term “x : {int | x ≥ 0} ` x + 1 : {v : int | v =x + 1}” in a dependent reﬁnement type system. Its
underlying term is “x : int ` x + 1 : int,” andwe assume that it is interpreted as the successor
function of Z in Set. The problem here is how to
reﬁne this interpretation with predicates. In dependent reﬁnement types, predicates may dependon the variables in contexts. In this example, thetype “x : {int | x ≥ 0} ` {v : int | v = x + 1}” depends on the variable x. Thus, the interpretationof such types must be a predicate on the context
and the type, i.e.,
Jx : {int | x ≥ 0} ` {v : int | v = x + 1}K= {(x, v) ∈ Z × Z | x ≥ 0 ∧ v = x + 1}.
As a result, the term in the dependent reﬁnement
type system is interpreted as the interpretation in
the underlying type system together with the property that if the input satisﬁes preconditions, thenthe output satisﬁes postconditions.
We formalize this reﬁnement process as a con-

{E | P}

E
p

P
Fig. 1q

B

Lifting.

struction of liftings of CCompCs, which are used
to interpret dependent type theories. Assume that
we have a pair of a CCompC p : E → B forinterpreting underlying type systems and a ﬁbration q : P → B for predicate logic satisfying certain conditions. Then we construct a CCompC{E | P} → P for interpreting dependent reﬁnement
type systems. This construction also yields a morphism of CCompCs from {E | P} → P to p : E → B
in Fig. 1. Given the simple ﬁbration s(Set) → Set
for underlying type systems and the subobject ﬁbration Sub(Set) → Set for predicate logic, thenwe get interpretations like Fig. 2.
We extend the construction of liftings of CCompCs to liftings of ﬁbred monads [1] on CCompCs,
which is motivated by the fact that many dependent reﬁnement type systems have computationaleﬀects, e.g., exception (like division and assertion), divergence, nondeterminism [25], and probability [5]. Assume that we have a ﬁbred monad T̂
on p : E → B, a monad T on B, and a lifting Ṫ
of T along q : P → B. Under a certain condition
that roughly claims that T̂ and T represent thesame computational eﬀects, we construct a ﬁbred
monad on {E | P} → P, which is a lifting of T̂ in thesame spirit of the given lifting Ṫ . This situation
is rather realistic because the ﬁbred monad T̂ on
the CCompC p : E → B is often induced from themonad T on the base category B. The lifting Ṫ ofthe monad T along p : P → B speciﬁes how to map
predicates P ∈ PX on values X ∈ B to predicatesṪ P ∈ PT X on computations T X, which enables us
to express, for example, total/partial correctness
and may/must nondeterminism [1].
We explain the usage of these categorical constructions by giving semantics to a dependent reﬁnement type system with computational eﬀects,
which is based on [4]. Our system also supports
subtyping relations induced by logical implication.
We prove soundness of the dependent reﬁnement
type system.
Finally, we discuss how to handle recursion in de-pendent reﬁnement type systems. In [4], Ahman
gives semantics to recursion in a speciﬁc model,i.e., the ﬁbration of continuous families of ω-cpos
CFam(CPO) → CPO. We consider more generalcharacterization of recursion by adapting Conway
operators for CCompCs, which enables us to lift
the structure for recursion. We show that a rule
for partial correctness in our dependent reﬁnement
type system is sound under the existence of a generalized Conway operator.
Our contributions are summarized as follows.
• We provide a general construction of liftingsof CCompCs from given CCompCs and posetal ﬁbrations satisfying certain conditions, as asemantic counterpart of construction of dependent reﬁnement type systems from underlying
type systems and predicate logic. We extend
this to liftings of ﬁbred monads on the underlying CCompCs to model computational eﬀects.
• We consider a type system (based on
EMLTT [2–4]) that includes most of basic
features of dependent reﬁnement type systems and prove its soundness in the liftings ofCCompCs obtained from the above construction.
• We deﬁne Conway operators for dependent
type systems. This generalizes the treatmentof general recursion in [4]. We prove soundness of the typing rule for partial correctnessof recursion under the existence of a lifting ofConway operators.

2 Preliminaries
We review basic deﬁnitions and ﬁx notations forcomprehension categories, which are used as categorical models for dependent type theories. We
assume basic knowledge of ﬁbrations (see e.g. [10]).
Let p : E → B be a ﬁbration (opﬁbration).
We denote the cartesian (cocartesian) lifting overu : I → J by u(Y ) : u∗ Y → Y (u(X) : X → u! X)
where u∗ : EJ → EI (u! : EI → EJ ) is the reindexing (coreindexing) functor. We call p : E → B
a posetal ﬁbration if p is a ﬁbration such that eachﬁbre category is a poset. Note that the ﬁbrationp : E → B is split and faithful if p is posetal.
A comprehension category is a functor P : E →B→ such that the composite cod ◦ P : E → B is aﬁbration and P maps cartesian morphisms to pull-{x ∈ Z | x ≥ 0}

Fig. 2⟨idZ ,(−)+1⟩⊆⊆Z{(x, v) ∈ Z × Z | x ≥ 0 ∧ v = x + 1}
Z×Z

The interpretation of x : {int | x ≥ 0} ⊢ x + 1 : {v : int | v = x + 1}.

backs in B. A comprehension category P is full if
P is fully faithful.
A comprehension category with unit is a ﬁbration p : E → B that has a ﬁbred terminal object 1 : B → E and a comprehension functor{−} : E → B which is a right adjoint of the ﬁbred terminal object functor 1 a {−}. Projection
1⊣{−}
πX : {X} → pX is deﬁned by πX = pϵX
foreach X ∈ E. Intuitively, E represents a collectionof types Γ ` A in dependent type theories; B represents a collection of contexts Γ; p : E → B is
the mapping (Γ ` A) 7→ Γ; 1 : B → E is theunit type Γ 7→ (Γ ` 1); and {−} is the mapping(Γ ` A) 7→ Γ, x : A where x is a fresh variable.
The comprehension category with unit p : E → B
induces several structures. It induces a comprehension category P deﬁned by PX = πX . The
adjunction 1 a {−} deﬁnes the bijection s :EI (1I, X) ∼= {f : I → {X} | πX ◦ f = idI }between vertical morphisms in E and sections in
B. For each X, Y ∈ EI , we have an isomorphism∗Y) ∼ϕ : E{X} (1{X}, πX= EI (X, Y ). Consider the
pullback square P(πX (Y )) where X, Y ∈ EI . By
the universal property of pullbacks, we have the∗Y } → {πY∗ X}
symmetry isomorphism σX,Y : {πX∗ Y
as a unique morphism σX,Y such that ππX={πY (X)} ◦ σX,Y and {πX (Y )} = ππY∗ X ◦ σX,Y .
Similarly, we have the diagonal morphism δX :∗{X} → {πXX} as a unique morphism δX such that∗
ππX X ◦ δX = {πX (X)} ◦ δX = id{X} .
Let p : E → B be a comprehension category withunit and q : D → B be a ﬁbration. The ﬁbration∗q has p-products if πX: DpX → D{X} has a rightQ∗
adjoint πX a X for each X ∈ E and these adjunctions satisfy the BC (Beck-Chevalley) condition foreach pullback square Pf where P is a comprehension category induced by p and f is a cartesianmorphism in E. Similarly, we deﬁne p-coproducts`∗∗
by X a πX
and p-equality by EqX a δX
plus theBC condition for each cartesian morphism (see [10,Deﬁnition 9.3.5] for detail).
A comprehension category with unit p : E → B
admits products (coproducts) if it has p-products(p-coproducts). The coproducts are strong if the`canonical morphism κ ⨿: {Y } → { X Y } deﬁned`∗
by {πX ( X Y ) ◦ η πX ⊣ X } is an isomorphism foreach X ∈ E and Y ∈ E{X} . A closed comprehension category (CCompC) is a full comprehension category with unit that admits products andstrong coproducts and has a terminal object in thebase category. A split closed comprehension category (SCCompC) is a CCompC such that p is a
split ﬁbration, and the BC condition for products
and coproducts holds strictly (i.e., canonical isomorphisms are identities). For example, the simple
ﬁbration sB : s(B) → B on a cartesian closed category B is a SCCompC (see [10, Theorem 10.5.5]).
Another example of SCCompCs is the family ﬁbration famSet : Fam(Set) → Set.
Fibred coproducts in a comprehension category
with unit p : E → B are strong if the functorh{ι1 }∗ , {ι2 }∗ i : E{X+Y } → E{X} × E{Y } is fully
faithful where ι1 : X → X + Y and ι2 : Y → X + Y
are injections for ﬁbred coproducts. Strong ﬁbred
coproducts are used to interpret ﬁbred coproducttypes A + B.

3 Lifting SCCompCs and Fibred Coproducts
In this section, we give a construction of liftingsof SCCompCs with strong ﬁbred coproducts fromgiven SCCompCs with strong ﬁbred coproducts forunderlying types and posetal ﬁbrations for predicate logic satisfying appropriate conditions.
3. 1 Lifting SCCompCs
Let p : E → B be a SCCompC for underlying
type systems. Let q : P → B be a posetal ﬁbration
with ﬁbred ﬁnite products for predicate logic.
Deﬁnition 1. We deﬁne a category {E | P} by the
pullback of q → : P→ → B→ along P : E → B→
where the comprehension category P is induced by
p : E → B.

{E | P}
∗

P (q

→

)

(q → )∗ P

⌟

P→
q

P
E
B→
That is, objects are tuples (X, P, Q) where X ∈∗E, P ∈ PpX , Q ∈ P{X} , and Q ≤ πX
P;
and morphisms are tuples (f, g, h) : (X, P, Q) →(X ′ , P ′ , Q′ ) where f : X → X ′ , g : P → P ′ ,h : Q → Q′ , pf = qg, and {f } = qh.
The intuition of this deﬁnition is as follows. For
each object (X, P, Q) ∈ {E | P}, X represents atype Γ ` A in the underlying type system, P represents a predicate on the context Γ, and Q represents the conjunction of a predicate on Γ, v : A and∗the predicate P (thus Q ≤ πX
P is imposed). Note∗ →that P (q ) : {E | P} → E is faithful because q isfaithful.
Let {p | q} : {E | P} → P be a functor deﬁned bycod ◦ (q → )∗ P, that is, (X, P, Q) 7→ P . The functor{p | q} inherits most of the CCompC structure ofp : E → B.
Lemma 2. The functor {p | q} : {E | P} → P
is a split ﬁbration. The cartesian lifting of g :P ′ → P is given by (qg(X), g, {qg(X)}(Q) ◦ π ′ ) :∗′∗((qg)∗ X, P ′ , π(qg)∗ X P ∧ {qg(X)} Q) → (X, P, Q)′
where π is a projection for ﬁbred products.
Lemma 3. The ﬁbration {p | q} : {E | P} → P is afull comprehension category with unit that admits
strong coproducts.

Proof. The main idea is that the structure in the
CCompC p : E → B can be lifted to {E | P} → P.
Here, we only show the deﬁnition of (object partsof) ﬁbred terminal objects 1 : P → {E | P}, thecomprehension functor {−} : {E | P} → P, and co`products (X,P,Q) : {E | P}Q → {E | P}P for each
(X, P, Q) ∈ {E | P}.
∗
1P = (1qP, P, π1qP
P){(X, P, Q)} = Qaa(Y, Q, R) = ( Y, P, (κ−1 )∗ R)(X,P,Q)

by Y(Y, Q, R) =→X

The rest of the proof is omitted.
The existence of products in {p | q} requires additional conditions.
Lemma 4. If q : P → B has ﬁbred exponentials
and p-products (in addition to ﬁbred ﬁnite products), then {p | q} : {E | P} → P admits products.
Q
Proof. We deﬁne (X,P,Q) : {E | P}Q → {E | P}PY

Y(X,P,Q)

∗
π∏

X Y

∗
Y, P, π∏
P∧
X Y

X

π∗ ⊣

∗
∗ ∏
σ∏
(ππ∗X
Q ⇒ {ϵYX
X Y,X
X Y

∏
X


}∗ R) .

X

Q ∈ P{X}R ∈ P{Y }∏π∗ ⊣ X

∗
ππ
∗ ∏
X Y
X
∗ ∏

P{πX

{ϵYX
X Y}

∗
σ∏
∗
P{π∏
∗
ππ
∗
∏

X Y

X

X Y

a

}∗

X Y,X

X}

∏

∗
π∏

X Y

X

P{ ∏ X Y }Then, this gives products in {p | q} but we omit thelengthy proof.
As a result, we get a lifting of SCCompCs over p :E→
B.
Theorem 5. If p : E → B
P ∗ (q → ){E | P}E
is a SCCompC and q :p
P → B is a ﬁbred ccc{p|q}qthat has p-products, thenP
B
{p | q} : {E | P} → P
is a SCCompC. Moreover,(P ∗ (q → ), q) : {p | q} → p is a morphism of SCCompCs, i.e., a split ﬁbred functor that preserves
the CCompC structure strictly.
Proof. By Lemma 3 and Lemma 4. A terminal object in P exists because B has a terminal object andq : P → B has ﬁbred terminal objects. It is almost
obvious that (P ∗ (q → ), q) preserves the structure ofCCompCs.
Example 6. Consider the simple ﬁbration sSet :s(Set) → Set and the subobject ﬁbration subSet :Sub(Set) → Set (see [10, §1.3]). Objects in{s(Set) | Sub(Set)} are tuples ((I, X), P, Q)
where (I, X) ∈ s(Set), P ⊆ I, and Q ⊆ P × X ⊆I × X, and morphisms are those in s(Set) that
preserve predicates. In {sSet | subSet } : {s(Set) |Sub(Set)}Y → Sub(Set), products are given by((I × X, Y ), Q, R)((I,X),P,Q)= (I, X ⇒ Y ), P,{(i, f ) ∈ I × (X ⇒ Y ) | i ∈ P ∧ ∀x ∈ X,
(i, x) ∈ Q =⇒ ((i, x), f (x)) ∈ R} .
(1)

Example 7. Let erel : ERel → Set be the ﬁbration of endorelations deﬁned by change-of-basefrom Sub(Set) → Set along the functor X 7→
X × X. The ﬁbration erel is a ﬁbred ccc andhas products (i.e. right adjoints of reindexing functors that satisfy the BC condition for each pullback square). Therefore, erel has p-products forany comprehension category with unit p. If weapply Theorem 5 to erel and the simple ﬁbrationsSet : s(Set) → Set, then products are deﬁned
similarly to Example 6.
Example 8. Consider the family ﬁbration famSet :Fam(Set) → Set [10, Def 1.2.1] and the subobject
ﬁbration subSet : Sub(Set) → Set. Objects in{Fam(Set) | Sub(Set)} are tuples ((I, X), P, Q)
where (I, X) ∈ Fam(Set), P ⊆ I, and Q ⊆``Note that subsets Q ⊆Xi ⊆i∈I Xi.
`i∈P
Xi
have
a
one-to-one
correspondence withi∈I
families of subsets (Qi ⊆ Xi)i∈I when we deﬁne`
Qi = ι∗i (Q) where ιi : Xi →i∈I Xi is the ith injection. So, we often identify Q with thefamily of subsets Qi ⊆ Xi. We get productsin {famSet | subSet } : {Fam(Set) | Sub(Set)} →Sub(Set) by modifying (1) for dependent functions.
3. 2 Lifting Fibred Coproducts
A suﬃcient condition for {p | q} : {E | P} → P tohave strong ﬁbred coproducts is given by the following lemma, which is analogous to [9, Prop. 4.5.8].
Lemma 9. If (1) p : E → B is a CCompC that has
strong ﬁbred coproducts (2) for each X, Y ∈ EI ,X ′ , Y ′ ∈ EI ′ , u : I → I ′ , and pair of cartesian
liftings f : X → X ′ and g : Y → Y ′ over u, thefollowing two squares are pullbacks
{X}
{f }
′

{ι1 }

⌟
{ι1 }

{X + Y }{f +g}
′

′

{ι2 }

⌞
{ι2 }

{Y }
{g}

{X }
{X + Y }{Y ′ }(3) q : P → B is a ﬁbred distributive category(4) for each X, Y ∈ EI and Z ∈ E{X+Y } , q has
cocartesian liftings of {ι1 } : {X} → {X + Y },{ι2 } : {Y } → {X + Y }, {{ι1 }(Z)} : {{ι1 }∗ Z} →{Z}, and {{ι2 }(Z)} : {{ι2 }∗ Z} → {Z} that satisfy the BC condition for each pullback squares
and Frobenius, then {p | q} : {E | P} → P has
strong ﬁbred coproducts, and the ﬁbred functor(P ∗ (q → ), q) : {p | q} → p strictly preserves ﬁbred
coproducts.

Proof. We deﬁne ﬁbred coproducts by (X, P, Q) +(Y, P, R) = (X + Y, P, {ι1 }! Q ∨ {ι2 }! R). We omit
the rest of the proof.
Note that if q is ﬁbred bicartesian closed, then q
is a ﬁbred distributive category.
Example 10. Consider sSet : s(Set) → Set
and subSet : Sub(Set) → Set (recall Example 6).
This combination satisﬁes four conditions in Lemma 9.
Fibred coproducts in{s(Set) | Sub(Set)} → Sub(Set) are deﬁned asfollows.
((I, X), P, Q) + ((I, Y ), P, R)= ((I, X + Y ), P, {(i, x) | (i, x) ∈ Q ∨ (i, x) ∈ R})

4 Lifting Monads on SCCompCs
Suppose we have a SCCompC p : E → B anda posetal ﬁbration q : P → B as ingredients for{p | q} : {E | P} → P in Theorem 5. We explain how to construct a ﬁbred monad on {p | q} :{E | P} → P from monads on p and q.
First, we assume that a monad T on B and aﬁbred monad T̂ on p : E → B are given. These
monads are intended to represent the same computational eﬀects in underlying type systems, but T
is more “primitive” than T̂ , and T̂ is induced fromT in some natural way. For example, we can use
the maybe monad or the powerset monad on Set as
T and deﬁne T̂ by (I, X) 7→ (I, T X) on the simple
ﬁbration s(Set) → Set. In such a situation, we often have an oplax monad morphism (Deﬁnition 11)
θ : {T̂ (−)} → T {−}. Intuitively, θ extends the action of T̂ on types to contexts, just like strengths ofstrong monads. We also need a lifting Ṫ of T alongq : P → B to specify a mapping from predicateson values in X ∈ B to predicates on computations
in T X [1]. Given all these ingredients and some
additional conditions, we deﬁne a ﬁbred monad on{p | q} : {E | P} → P, which is a lifting of the ﬁbred
monad T̂ on p : E → B.
Deﬁnition 11 (oplax monad morphism). Let C, D
be categories, F : C → D be a functor, and(S, η S , µS ), (T, η T , µT ) be monads on C and D, respectively. A natural transformation θ : F S → T F
is an oplax monad morphism if θ respects units andmultiplications.

FX

T
ηF
X

S
F ηX

F SX
F S2X
F µS
X

θSX

θX

TFX
T θX

T F SX

T 2F X
µT
FX

θX

F SX
TFX
Theorem 12. Let T be a monad on B, T̂ be a ﬁbred monad on p : E → B in the 2-category FibB ofﬁbrations over B, θ : {T̂ (−)} → T {−} be an oplax
monad morphism, and Ṫ be a ﬁbred lifting [1] of T
along q : P → B. If∗∗∗
πT̂∗ X P ∧ θX
Ṫ Q ≤ θXṪ (πXP ∧ Q)(2)
holds for each X ∈ E, P ∈ PpX and Q ∈ P{X} , thenthere exists a ﬁbred monad S on {p | q} : {E | P} →P in FibP such that the ﬁbred functor {p | q} → p
in Theorem 5 is a ﬁbred monad morphism from S
to T̂ .
Proof. We deﬁne S(X, P, Q) = (T̂ X, P, πT̂∗ X P ∧θ∗ Ṫ Q). Then the monad structure of T̂ lifts to
S. The assumption (2) is required to prove that S
is ﬁbred.
θ(Ṫ Q)Pθ∗ Ṫ Q
Ṫ Q

Ṫ2 are given by((I, X), P, Q)
7→ (I, X + {∗}), P,{(i, x) | (i ∈ P ∧ x = ∗) ∨ (i, x) ∈ Q}((I, X), P, Q)
7→ (I, X + {∗}), P, {(i, x) | (i, x) ∈ Q}
respectively. Here, we leave the left/right injectionof coproducts implicit.
Example 14. For each monad T on Set, wehave a split ﬁbred monad on the family ﬁbration Fam(Set) → Set deﬁned by T̂ (I, X) =(I, T ◦ X). We have an oplax monad morphism``θ : i∈I T Xi → T i∈I Xi deﬁned by the cotu``
pling [(T ιi )i∈I ] :i∈I T Xi → T
i∈I Xi where`ιi : Xi → i∈I Xi is the i-th injection. The condition (2) holds for any ﬁbred lifting of T along
the subobject ﬁbration Sub(Set) → Set. Moreover, we have ι∗i θ∗ Ṫ Q = Ṫ ι∗i Q for each Q ∈Sub(Set)⨿i∈I Xi , so the monad in Theorem 12 isgiven by
(I, X), P, (Qi ⊆ Xi)i∈I
7→ (I, T ◦ X), P, (Ṫ Qi ⊆ T Xi)i∈I .

q

B{T̂ X}θT {X}

Example 13. Any strong monad T on a CCC B
gives rise to a split ﬁbred monad T̂ on the simple
ﬁbration sB : s(B) → B (actually, there is a one-toone correspondence [10, Ex.2.6.10]). The monad T̂
is deﬁned by (I, X) 7→ (I, T X). An oplax monadmorphism θ : I × T X → T (I × X) is given by thestrength.
Now consider the case where B = Set. Since
the strength for the monad T on Set is given
uniquely [17, Proposition 3.4], we can prove that (2)holds for any ﬁbred lifting of T along the subobject
ﬁbration subSet : Sub(Set) → Set.
Let T be the maybe monad (−) + {∗}. There are
two ﬁbred liftings of T :Ṫ1 (P ⊆ I) = (P + {∗} ⊆ I + {∗})Ṫ2 (P ⊆ I) = (P ⊆ I + {∗})
for each (P ⊆ I) ∈ Sub(Set). The lifting Ṫ1
corresponds to partial correctness, and Ṫ2 corresponds to total correctness. The ﬁbred monads on{sSet | subSet } deﬁned in Theorem 12 from Ṫ1 and

5 Soundness
We consider a concrete dependent reﬁnement
type system with computational eﬀects and deﬁnesound semantics to show that the SCCompC deﬁned in Theorem 5 has suﬃcient structures for dependent reﬁnement types. Here, we consider two
type systems. One is an underlying type systemthat is a fragment of EMLTT [2–4]. The other isa reﬁnement of the underlying type system thathas reﬁnement types {v : A | p} and a subtyping
relation Γ ` A <: B induced by logical implication. The two type systems share a common syntax for terms while types are more expressive inthe reﬁnement type system. We consider liftingsof ﬁbred adjunction models to interpret the reﬁnement type system. Here, Theorem 12 can be used
to obtain a lifting of ﬁbred adjunction models via
Eilenberg-Moore construction. We prove a soundness theorem that claims if a term is well-typed
in the reﬁnement type system, then the interpretation of the term has a lifting along the morphismof CCompCs deﬁned in Theorem 5.

U : r → p between p : E → B and r : C → B is given
and that interpretations of base type constructors
JbK ∈ E and value constants JcK ∈ E1 (1, X) (forsome X ∈ E1 ) are given. We deﬁne a partial interpretation J−K of the following form for raw syntax.
F

E

C

a

5. 1 Underlying Type System
We deﬁne the underlying dependent type system by a slightly modiﬁed version of a fragmentof EMLTT [2–4]. We remove some of the types
and terms from the original for simplicity. We parameterize our type system with a set of base type
constructors (ranged over by b) and a set of value
constants (ranged over by c) for convenience.
We deﬁne value types (A, B, . . . ), computation
types (C, D, . . . ), contexts (Γ, . . . ), value terms(V, W, . . . ), and computation terms (M, N, . . . ) as
in Fig. 3.
We implicitly assume that variables in Γ are mutually diﬀerent. We use many type annotations inthe syntax of terms for a technical reason, but wemight omit them if they are clear from the context.
We deﬁne substitution A[V /x], C[V /x], W [V /x],and M [V /x] as usual.
For each type constructor b, let arg(b) be a closed
value type of the argument of b. We write b : A →Type if A = arg(b). For each value constant c, letty(c) be a closed value type of c.
We have several kinds of judgements: wellformed contexts ` Γ; well-formed (value or computation) types Γ ` A, Γ ` C; well-typed (value
or computation) terms Γ ` V : A, Γ ` M : C;and deﬁnitional equalities for contexts, types andterms ` Γ1 = Γ2 , Γ ` A = B, Γ ` C = D,Γ ` V = W : A, Γ ` M = N : C.
Typing rules are basically the same as EMLTT.
Rules for base type constructors and value constants are shown in Fig. 4
Semantics. We use ﬁbred adjunction models tointerpret terms and types. We adapt the deﬁnition
for our fragment of EMLTT as follows.
Deﬁnition 15 (Fibred adjunction models). A ﬁbred adjunction model is a ﬁbred adjunction F a
U : r → p where p : E → B is a SCCompC withstrong ﬁbred coproducts and r : C → B is a ﬁbration with p-products.
The Eilenberg-Moore ﬁbration of a CCompC p :E → B inherits products in p [2, Theorem 4.3.24]
and thus gives an example of ﬁbred adjunction
models.
Lemma 16. Given a SCCompC p : E → B withstrong ﬁbred products and a split ﬁbred monad T
on p, then the Eilenberg-Moore adjunction of T isa ﬁbred adjunction model.
We assume that a ﬁbred adjunction model F a

p

U

r

B
JΓK ∈ BJΓ; AK ∈ EJΓK
JΓ; CK ∈ CJΓK
JΓ; V K ∈ EJΓK (1JΓK, A)
for some AJΓ; M K ∈ EJΓK (1JΓK, U C)
for some C ∈ C
Most of the deﬁnition of J−K are the same as [2].
For base type constructors b and value constants c,
we deﬁne J−K as follows.
JΓ; bA (V )K = (sJΓ; V K)∗ {!JΓK (J; AK)}∗ JbK
JΓ; cA K = !∗JΓK JcK
Here, left-hand sides are deﬁned if right-hand sides
are deﬁned.
Proposition 17 (Soundness). Assume that JbK ∈E{J⋄;AK} holds for each b : A → Type such that
J; AK is deﬁned, and JcK ∈ E1 (1, J; ty(c)K) holds
if J; ty(c)K ∈ E1 is deﬁned. Interpretations J−K
of well-formed contexts and types and well-typed
terms are deﬁned. If two contexts, types, or terms
are deﬁnitionally equal, then their interpretations
are equal.
5. 2 Predicate Logic
We deﬁne syntax for logical formulas byp = > | p ∧ q | p ⇒ q | ∀x : A.p | V =A W | a(V )where a ranges over predicate symbols. Here, we
added > and V =A W for typing rule for the uniquevalue of the unit type and variables of base types(i.e. for selﬁﬁcation [18]), respectively, which we describe later. However, there is a large amount of
freedom to choose the syntax of logical formulas.
The least requirement here is that logical formulas
can be interpreted in a posetal ﬁbration q : P → B,
and interpretations of logical formulas admit semantic weakening, substitution, and conversion in
the sense of [2, Proposition 5.2.4, 5.2.6]. So, we canalmost freely add or remove logical connectives andquantiﬁers as long as q : P → B admits them.
We deﬁne a standard judgement of wellformedness for logical formulas. Some of the rules
for well-formedness are shown in Fig. 5
Logical formulas are interpreted in the ﬁbration
q : P → B. We assume that interpretation JaK ∈A := 1 | bA (V ) | Σx:A.B | U C | A + B
C := F A | Πx:A.C
Γ :=  | Γ, x : A
V := x | ∗ | cA | hV, W i(x:A).B | thunk M | inlA+B V | inrA+B V
M := return V | M to x : A inC N | forceC V | λx : A.M | M (V )(x:A).C |pm V as hx : A, y : Bi inz.C M | case V of z.C (inl (x : A) 7→ M, inr (y : B) 7→ N )Fig. 3`ΓSyntax of the underlying type system.

 ` ty(c)Γ ` cty(c) : ty(c)b : A → Type`AΓ`V :AΓ ` bA (V )b : A → Type`AΓ`V =W :AΓ ` bA (V ) = bA (W )Fig. 4

Some typing rules for the underlying
type system.

Γ`V :AΓ`W :AΓ ` V =A W : Propa : A → Prop`AΓ`V :AΓ ` a(V ) : Prop
Fig. 5

Some rules for well-formed predicates.

P{J⋄;AK} for each predicate symbol a : A → Prop is
given. The interpretation JΓ ` pK ∈ PJΓK is standard and deﬁned inductively for each well-formed
formulas. For example:JΓ ` V =A W K∗= (sJΓ; V K)∗ (s(πJΓ;AKJΓ; W K))∗ Eq(>{JΓ; AK})JΓ ` a(V )K= s(JΓ; V K)∗ {!JΓK (J; AK)}∗ JaK
where a : A → Prop is a predicate symbol and s isthe bijection deﬁned in §2.
5. 3 Reﬁnement Type System
We reﬁne the underlying type system by adding
predicates to base types and the unit type. From
now on, we use subscript Au for types in the underlying type system to distinguish them from types

in the reﬁnement type system.
A := {v : bAu (V ) | p} {v : 1 | p} Σx:A.B
UC | A + B
C := F A | Πx:A.C
Γ :=  | Γ, x : A
We use the same deﬁnition of terms as the underlying type system and the same set of base type
constructors and value constants. Argument typesof base type constructors b : Au → Type are also
the same, but types ty(c) assigned to value constants c are redeﬁned as reﬁnement types. Givena type A (or C) in the reﬁnement type system, wedeﬁne its underlying type |A| (or |C|) by induction
where predicates are eliminated in the base cases.
|{v : bAu (V ) | p}| = bAu (V )|{v : 1 | p}| = 1
Underlying contexts |Γ| are also deﬁned by |  | = 
and |Γ, x : A| = |Γ|, x : |A|.
Judgements in the reﬁnement type system are as
follows. We have judgements for well-formedness
or well-typedness for contexts, types and terms in
the reﬁnement type system, which are denoted in
the same way as the underlying type system. We
do not consider deﬁnitional equalities for terms because they are the same as the underlying type system. Instead, we add judgements for subtyping between types and contexts. They are denoted by` Γ1 <: Γ2 for context, Γ ` A <: B for value types,
and Γ ` C <: D for computation types.
Most of term and type formation rules are similar to the underlying type system. We listed someof the non-trivial modiﬁcations of typing rules inFig. 6. We add typing rules for {v : bBu (V ) | p}and {v : 1 | p}. Subtyping for these types are deﬁned by judgements Γ; v : Au | p ` q for logicalimplication. Here, Γ; v : Au | p ` q means “assumptions in Γ and p implies q” where p and q
are well-formed formulas in the context |Γ|, v : Au .
We do not specify derivation rules for the judgement Γ; v : Au | p ` q but assume soundness of thejudgement (explained later). We allow “selﬁﬁca-

Example 19. We can express conditional branching using the elimination rule of the ﬁbred coproduct type 1 + 1. For example, assume wehave a base type constructor int : 1 → Typefor integers and a value constant for comparison:(≤) : U (Πx:int.Πy:int.F ({v : 1 | x ≤ y} +{v : 1 | x > y})). We can deﬁne if x ≤y then M else N to be a syntax sugar for (x ≤′y) to z in (case z of (inl v 7→ M, inr v 7→ N ))where (≤′ ) = force (≤). Note that M and N are
typed in contexts that have v : {v : 1 | x ≤ y}or v : {v : 1 | x > y} depending on the result ofcomparison.
5. 4 Semantics
Deﬁnition 20 (lifting of ﬁbred adjunction models). Suppose that we have two ﬁbred adjunction
models F a U : q → p between p : E → B andq : C → B and Ḟ a U̇ : s → r between r : U → P
and s : D → P. The ﬁbred adjunction modelḞ a U̇ is a lifting of F a U if there exists functors u : U → E, v : D → C, and t : P → B suchthat these functors strictly preserve all structuresof Ḟ a U̇ to those of F a U . That is, (u, t) : r → p
and (v, t) : s → q are split ﬁbred functors, the pairof ﬁbred functor (u, t) and (v, t) is a map of adjunctions in the 2-category Fib, (u, t) strictly preserves
the CCompC structure and ﬁbred coproducts, and

E
p

F

C

{E | P}
{p|q}

B
{p|q}

D

U̇

U

{E | P}Ḟ

a

Proof. By induction on the derivation of judgements. Each typing rule in the reﬁnement typesystem has a corresponding rule in the underlying
system.

(v, t) maps r-products to p-products in the strict
sense.
We assume that a lifting of ﬁbred adjunction
models is given as follows.
ation” [18] for variables of base types. Subtyping forΣx:A.B, U C, F A, and Πx:A.C are deﬁned covariantly except the argument type A of Πx:A.C, whichis contravariant. We have the rule of subsumption.
Value constants are typed with a reﬁned type assignment ty(c). The unique value ∗ of the unit typehas type {v : 1 | >}.
Lemma 18. If we eliminate predicates in the reﬁnement types from well-formed contexts, types
and terms, then we get well-formed contexts, types
and terms of the underlying type system.
• If ` Γ, then ` |Γ|. If Γ ` A, then |Γ| ` |A|. IfΓ ` C, then |Γ| ` |C|.
• If ` Γ1 <: Γ2 , then ` |Γ1 | = |Γ2 |. If Γ ` A <:B, then |Γ| ` |A| = |B|. If Γ ` C <: D, then|Γ| ` |C| = |D|.

u

E

D

P
v

(3)
C

p
q

q
P
B
P
B
Here, we assume more than just a lifting of ﬁbred adjunction models by requiring the speciﬁc
SCCompC {p | q} with strong ﬁbred coproducts,
and the split functor (u, q) : {p | q} → p deﬁned in
Theorem 5 and Lemma 9. The underlying ﬁbred
adjunction model F a U is used for the underlying type system in §5. 1, and q : P → B is forpredicate logic in §5. 2. One way to obtain suchliftings of ﬁbred adjunction models is to apply the
Eilenberg-Moore construction to the monad morphism in Theorem 12, but in general we do not
restrict C and D to be Eilenberg-Moore categories.
We further assume that q has p-equalities to interpret logical formulas of the form V =A W .
We deﬁne partial interpretation of reﬁnement
types JΓK ∈ P, JΓ; AK ∈ {E | P}JΓK , and JΓ; CK ∈DJΓK similarly to the underlying type system butwith the following modiﬁcation. Here, we make useof the deﬁnition of {E | P}.
JΓ; {v : b(V ) | p}K= J|Γ|; b(V )K, JΓK,
∗
πJ|Γ|;b(V)K JΓK ∧ J|Γ|, v : b(V ) ` pK
JΓ; {v : 1 | p}K
∗= J|Γ|; 1K, JΓK, πJ|Γ|;1K
JΓK ∧ J|Γ|, v : 1 ` pK
For each (X, P, Q), (X ′ , P ′ , Q′ ) ∈ {E | P}, we deﬁne a semantic subtyping relation (X, P, Q) <:(X ′ , P ′ , Q′ ) by the conjunction of X = X ′ , P = P ′ ,and Q ≤ Q′ . In other words, we have (X, P, Q) <:(X ′ , P ′ , Q′ ) if and only if there exists a morphism(idX , idP , h) : (X, P, Q) → (X ′ , P ′ , Q′ ) that is
mapped to identities by u : {E | P} → E and{p | q} : {E | P} → P.
Lemma 21.
• If JΓK is deﬁned, then J|Γ|K is deﬁned and equal to qJΓK.
• If JΓ; AK is deﬁned, then J|Γ|; |A|K is deﬁned
and equal to uJΓ; AK.
• If JΓ; CK is deﬁned, then J|Γ|; |C|K is deﬁned
and equal to vJΓ; CK.

b : Au → Type`Γ
|Γ| ` bAu (V )|Γ|, v : bAu (V ) ` p : Prop`ΓΓ ` {v : bAu (V ) | p}|Γ| ` bAu (V ) = bAu (W )Γ; v : bAu (V ) | p ` qΓ ` {v : bAu (V ) | p} <: {v : bAu (W ) | q}` Γ1 , x : {v : bAu (V ) | p}, Γ2`ΓΓ1 , x : {v : bAu (V ) | p}, Γ2 ` x : {v : bAu (V ) | v = x} ` ty(c)Γ ` c|ty(c)| : ty(c)Γ ` A2 <: A1
Γ, x : A2 ` C 1 <: C 2
Γ, x : A1 ` C 1

Γ2 ` V : A` Γ1 <: Γ2
Γ1 ` A <: B`ΓΓ ` Πx:A1 .C 1 <: Πx:A2 .C 2

Γ1 ` V : BΓ ` ∗ : {v : 1 | >}`Γ|Γ|, v : 1 ` p : PropΓ ` {v : 1 | p}

Fig. 6`ΓΓ; v : 1 | p ` qΓ ` {v : 1 | p} <: {v : 1 | q}Some typing rules for the reﬁnement type system.

Proof. By simultaneous induction. The case of{v : Au | p} is obvious, and other cases follow fromthe deﬁnition of liftings of ﬁbred adjunction models.
We do not specify syntactic derivation rules forjudgement for logical implication Γ; v : Au | p ` q.
Instead, we assume soundness of Γ; v : Au | p ` q∗
in the following sense: πJ|Γ|;AJΓK ∧ J|Γ|, v : Au `uKpK ≤ J|Γ|, v : Au ` qK holds in PJ|Γ|,v:Au K . For example, we can deﬁne a derivation rule for logicalimplication Γ; v : Au | p ` q from derivation rules
for predicate logic Γu | p ` q (“p implies q in thecontext Γu ”). This is done by collecting predicatesin context Γ byLM = >(
LΓM ∧ p[x/v] if A = {v : Au | p}LΓ, x : AM =LΓMotherwiseand deﬁning a derivation rule for judgement for logical implication Γ; v : Au | p ` q by |Γ|, v : Au |LΓM ∧ p ` q. If the derivation rules for predicate
logic Γu | p ` q is sound (i.e., Γu | p ` q impliesJΓu ` pK ≤ JΓu ` qK), then so are the derivation
rule for Γ; v : Au | p ` q. This technique is used in,e.g., [27].
Theorem 22 (Soundness). Assume that Γ; v :Au | p ` q is sound in the sense described above,
JbK ∈ E{J⋄;AK} holds for each b : A → Type if J; AK
is deﬁned, and JcK ∈ {E | P}1 (1, J; ty(c)K) holds if
J; ty(c)K ∈ {E | P}1 is deﬁned. Then we have thefollowing.
• If ` Γ, then JΓK ∈ P is deﬁned. If Γ ` A, thenJΓ; AK ∈ {E | P}JΓK is deﬁned. If Γ ` C, thenJΓ; CK ∈ DJΓK is deﬁned.
• If ` Γ1 <: Γ2 , then JΓ1 K ≤ JΓ2 K in a ﬁbre
category of P.
• If Γ ` A <: B, then JΓ; AK <: JΓ; BK. If
Γ ` C <: D, then U̇ JΓ; CK <: U̇ JΓ; DK.
• If Γ ` V : A, then there exists a liftingJΓ; V K : 1JΓK → JΓ; AK above J|Γ|; V K alongu : {E | P} → E. If Γ ` M : C, then there
exists a lifting JΓ; M K : 1JΓK → JΓ; CK above
J|Γ|; M K along u : {E | P} → E.
Since we have the bijections : {E | P}P (1P, (X, P, Q)) →{f : P → Q | π(X,P,Q) ◦ f = idP }for each (X, P, Q) ∈ {E | P}, we obtain liftings ofinterpretations of terms along q : P → B.
Proposition 23. If Γ ` V : A, then sJ|Γ|; V K :J|Γ|K → {J|Γ|; AK} has a lifting sJΓ; V K : JΓK →{JΓ; AK} along q : P → B (and similarly for computation terms Γ ` M : C).
Proposition 24. Assume the lifting of ﬁbred adjunction models is given by applying the EilenbergMoore construction to a lifting of monads in Theorem 12. If Γ ` M : F A, then θ ◦ sJ|Γ|; M K : J|Γ|K →T {J|Γ|; AK} has a lifting of type JΓK → Ṫ {JΓ; AK}along q : P → B.

6 Toward Recursion in Reﬁnement
Type Systems
We consider how to deal with general recursion in dependent reﬁnement type systems. In [4],Ahman used a speciﬁc model of the ﬁbration
CFam(CPO) → CPO of continuous families of ω-cpos to extend EMLTT with recursion. However,
we need to identify the structure that characterizes recursion to lift recursion from the underlying
type system to dependent reﬁnement type systems.
So, we consider a generalization of Conway operators [22] and prove the soundness of the underlying and the dependent reﬁnement type system extended with typing rules for recursion. This extension enables us to reason about partial correctnessof general recursion.
Unfortunately, we still do not know an example of liftings of Conway operators, although (1)CFam(CPO) → CPO does have a Conway operator and (2) the soundness of the reﬁnement typesystem with recursion holds under the existence ofa lifting of Conway operators. We leave this problem for future work.
6. 1 Conway Operators
The notion of Conway operators for cartesiancategories is deﬁned in [22]. We adapt the deﬁnition for comprehension categories with unit. We
allow partially deﬁned Conway operators because
we need those deﬁned only on interpretations ofcomputation types.
Deﬁnition 25 (Conway operator for comprehension categories with unit). Let p : E → B be acomprehension category with unit and K ⊆ E bea collection of objects. A Conway operator for thecomprehension category with unit p deﬁned on K isa family of mappings (−)‡ : EI (X, X) → EI (1I, X)
for each X ∈ EI ∩ K such that the following conditions are satisﬁed.
(Naturality) For each X ∈ K, f ∈ EI (X, X),
and u : J → I, u∗ f ‡ = (u∗ f )‡ .
(Dinaturality) For each X, Y ∈ K, f ∈EI (X, Y ), and g ∈ EI (Y, X), (g ◦ f )‡ = g ◦(f ◦ g)‡ .
(Diagonal property) For each X ∈ K and∗∗∗f ∈ E{X} (πX
X, πX
X), if πX
X ∈ K, then
‡ ‡
∗
−1
‡
(ϕ(f )) = (ϕ(δX (ϕ (f )))) holds where ϕ :∗E{X} (1{X}, πXX) → EI (X, X) is the isomorphism deﬁned in §2.
Lemma 26. Let B be a cartesian category. Thereis a bijective correspondence between the following. (1) Conway operators (−)† on the cartesiancategory B. (2) Conway operators (−)‡ on the simple comprehension category s(B) → B→ that aredeﬁned totally on s(B).

Γ`CΓ, x : U C ` M : CΓ ` µx : U C.M : CΓ`C=DΓ, x : U C ` M = N : CΓ ` µx : U C.M = µx : U D.N : CΓ`CΓ, x : U C ` M : CΓ `M [thunk (µx : U C.M )/x]
= µx : U C.M : CΓ`CΓ, x : U C, y : U C ` M : CΓ `µx : U C.µy : U C.M= µx : U C.M [x/y] : C
Fig. 7

Typing rules for general recursion.

Example 27. Let K ⊆ CFam(CPO) be a collection of objects deﬁned by K = {(I, X) ∈CFam(CPO) | ∀i ∈ I, Xi has a least element}.
For each (I, X) ∈ K and vertical morphism f =(idI , (fi )i∈I ) : (I, X) → (I, X), we deﬁne f ‡ =(idI , (∗ 7→ lfpfi )i∈I ) : (I, 1) → (I, X). Then (−)‡ isa Conway operator, which is implicitly used in [4].
6. 2 Recursion in the Underlying Type
SystemSyntax. We add recursion µx : U C.M to thesyntax of computation terms. We also add typing
rules in Fig. 7.
Semantics. Assume we have a ﬁbred adjunction model F a U : r → p where p : E → B andr : C → B. We need a Conway operator deﬁned on
objects in {JΓ; U CK | Γ ` C} ⊆ E. However, here isa circular deﬁnition because JΓ; U CK may containterms of the form µx : U D.M , whose interpretations are deﬁned by the Conway operator. So, we
use a slightly stronger condition.
Deﬁnition 28. A Conway operator deﬁned oncomputation types is a Conway operator deﬁned on
K ⊆ E such that K satisﬁes the following conditions. (1) U F X ∈ K holds for each X ∈ E. (2)Q
X Y ∈ K holds for each X ∈ E and Y ∈ K∩E{X} .
(3) For each X ∈ K and Y ∈ E, X ∼= Y implies
Y ∈ K.
Given a Conway operator deﬁned on computation types, we interpret µx : U C.M by JΓ; µx :U C.M K = (ϕ(JΓ, x : U C; M K))‡ : 1JΓK → U JΓ; CK.
Proposition 29. Soundness (Proposition 17)

holds for the underlying type system extended withgeneral recursion.
Proof. By induction. We can prove that the given
Conway operator is deﬁned on {JΓ; U CK | Γ ` C} ⊆E by [2, Proposition 4.1.14].
6. 3 Recursion in Reﬁnement Type System
Syntax. We add the typing rule for Γ `µx:U C.M : C in Fig. 7 to the reﬁnement type system. Here, recall that we remove deﬁnitional equalities when we consider the reﬁnement type system.
Semantics. We consider liftings of Conway operators to interpret recursion in the reﬁnement typesystem.
Deﬁnition 30. Let p : E → B and q : D → A be
comprehension categories with unit, (u, v) : p → q
be a morphism of comprehension categories withunit. Assume q has a Conway operator (−)‡ deﬁned
on K ⊆ D. A lifting of the Conway operator (−)‡
along (u, v) is a Conway operator (−)♮ for p deﬁned
on L ⊆ E such that uL ⊆ K and u(f ♮ ) = (uf )‡ foreach f ∈ EI (X, X) where X ∈ L.
Lemma 31. Let (u, v) be a morphism of CCompCs deﬁned in Theorem 5. Assume p : E → B
has a Conway operator (−)‡ deﬁned on K ⊆E. The CCompC {E | P} → P has a lifting of
the Conway operator deﬁned on L ⊆ {E | P} if
uL ⊆ K and for each (X, P, Q) ∈ L and f ∈{E | P}P ((X, P, Q), (X, P, Q)), {f ‡ } has a lifting∗
P → Q along q : P → B.
π1pX
Proof. Let (f, idP , h) : (X, P, Q) → (X, P, Q)
be a morphism in {E | P} where (X, P, Q) ∈ L.
We deﬁne a Conway operator by (f, idP , h)♮ =∗P ) → (X, P, Q) where(f ‡ , idP , h′ ) : (1pX, P, π1pX′‡
h is a lifting of {f }.
We assume that a lifting of ﬁbred adjunction
models (3) together with a lifting of Conway operators deﬁned on computation types is given.
Theorem 32. Soundness (Theorem 22) holds forthe reﬁnement type system extended with generalrecursion.
Consider the ﬁbration CFam(CPO) → CPO
for the underlying type system with recursion.
To support recursion in our reﬁnement type system, a natural choice of a ﬁbration for predicate logic is the ﬁbration of admissible subsets

Adm(CPO) → CPO because the least ﬁxed pointof an ω-continuous function f : X → X is given byW
lfpf = n f n (⊥). However, we cannot apply Theorem 5 because Adm(CPO) → CPO is not a ﬁbred
ccc [9, §4.3.2]. Speciﬁcally, it is not clear whether
this combination admits products. We believe that
our approach is quite natural but leave giving concrete examples of liftings of Conway operators for
future work.

7 Related Work
Dependent reﬁnement types. Historically,
there are two kinds of reﬁnement types. One isdatasort reﬁnement types [7], which are subsets ofunderlying types but not necessarily dependent.
The other is index reﬁnement types [28]. A typical example of index reﬁnement types is a typeof lists indexed by natural numbers that represent
the length of lists. Nowadays, the word “reﬁnement types” includes datasort and index reﬁnement
types, and moreover, mixtures of them.
Among a wide variety of the meaning of reﬁnement types, we focus on types equipped with predicates that may depend on other terms [6,20], which
we call dependent reﬁnement types or just reﬁnement types. Dependent reﬁnement types are widely
studied [5, 13, 14, 25], and implemented in, e.g.,F⋆ [23, 24] and LiquidHaskell [19, 26, 27]. However,most studies focus on decidable type systems, andonly a few consider categorical semantics.
We expect that some of the existing reﬁnement
type systems are combined with eﬀect systems. For
example, a dependent reﬁnement type system for
nondeterminism and partial/total correctness proposed in [25] contains types for computations indexed by quantiﬁers Q1 Q2 where Q1 , Q2 ∈ {∀, ∃}.
Here, Q1 represents may/must nondeterminism,
and Q2 represents total/partial correctness. It
has been shown that Q1 Q2 corresponds to four
cartesian liftings of the monad P+ ((−) + 1) [1, 12].
We conjecture that these liftings are connected bymonad morphisms and hence yield a lattice-gradedmonad. Another example is a relational reﬁnement
type system for diﬀerential privacy [5]. Their system seems to use a graded lifting of the distribution
monad where the lifting is graded by privacy parameters, as pointed out in [21]. We leave for future
work combining our reﬁnement type system witheﬀect systems based on graded monads [8, 11, 15].

Categorical semantics. Our interpretation of
reﬁnement type systems is based on a morphism ofCCompCs, which is a similar strategy to [16]. The
diﬀerence is that our paper focuses on dependent
reﬁnement types and makes the role of predicate
logic explicit by giving a semantic construction of
reﬁnement type systems from given underlying typesystems and predicate logic.
Combining dependent types and computationaleﬀects is discussed in [2–4]. Although their aim
is not at reﬁnement types, their system is a basis
for the design and semantics of our reﬁnement typesystem with computational eﬀects.
Semantics for types of the form {v : Au | p} arecharacterized categorically as right adjoints of terminal object functors in [10, Chapter 11]. Suchtypes are called subset types there. They consider
the situation where a given CCompC p : E → B
is already rich enough to interpret {v : Au | p},
and do not aim to interpret reﬁnement type systems by liftings of CCompCs. Moreover, we cannot directly use the interpretations in [10] for our
CCompC {E | P} → P because we are not given aﬁbration for predicate logic whose base category isP.

8 Conclusion and Future Work
We provided a general construction of liftingsof CCompCs from combinations of CCompCs andposetal ﬁbrations satisfying certain conditions.
This can be seen as a semantic counterpart of constructing dependent reﬁnement type systems fromunderlying type systems and predicate logic. We
identiﬁed suﬃcient conditions for several structuresin underlying type systems (e.g. products, coproducts, ﬁbred coproducts, ﬁbred monads, and Conway operators) to lift to dependent reﬁnement typesystems. We proved the soundness of a dependent
reﬁnement type system with computational eﬀects
with respect to interpretations in CCompCs obtained from the general construction.
We aim to extend our dependent reﬁnement
type system by combining eﬀect systems based on
graded monads [8,11,15]. We hope that this extension will give us a more expressive framework that
subsumes, for example, dependent reﬁnement typesystems in [5, 25]. Another direction is to deﬁne
interpretations of {v : Au | p} in the style of subset
types in [10, Chapter 11]. Lastly, we are interested

in ﬁnding more examples of possible combinationsof underlying type systems and predicate logic (especially for recursion in dependent reﬁnement typesystems but not limited to this) so that we can ﬁnd
a new practical application of this paper.
Acknowledgement. We thank Shin-ya Katsumata, Hiroshi Unno and the anonymous referees
for helpful comments. This work was supported by
JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603).
References[ 1 ] Aguirre, A. and Katsumata, S.: Weakest preconditions in ﬁbrations, Proceedings of the ThirtySixth Conference on the Mathematical Foundationsof Programming Semantics, MFPS 2020, Paris,
France, June 2020. to appear.
[ 2 ] Ahman, D.: Fibred Computational Eﬀects, PhD
Thesis, University of Edinburgh, 2017.
[ 3 ] Ahman, D.: Handling Fibred Algebraic Eﬀects,
Proceedings of the ACM on Programming Languages, Vol. 2(2018), pp. 1–29.
[ 4 ] Ahman, D., Ghani, N., and Plotkin, G. D.:
Dependent Types and Fibred Computational Effects, Foundations of Software Science and Computation Structures, Jacobs, B. and Löding, C.(eds.),
Vol. 9634, Springer Berlin Heidelberg, 2016, pp. 36–
54.
[ 5 ] Barthe, G., Gaboardi, M., Gallego Arias, E. J.,
Hsu, J., Roth, A., and Strub, P.-Y.: HigherOrder Approximate Relational Reﬁnement Types
for Mechanism Design and Diﬀerential Privacy,
Proceedings of the 42nd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming
Languages - POPL ’15, Mumbai, India, ACM Press,
2015, pp. 55–68.
[ 6 ] Flanagan, C.: Hybrid Type Checking, Conference Record of the 33rd ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages - POPL’06, Charleston, South Carolina,
USA, ACM Press, 2006, pp. 245–256.
[ 7 ] Freeman, T. and Pfenning, F.: Reﬁnement
Types for ML, ACM SIGPLAN Notices, Vol. 26,
No. 6(1991), pp. 268–277.
[ 8 ] Fujii, S., Katsumata, S.-y., and Melliès, P.A.: Towards a Formal Theory of Graded Monads, Foundations of Software Science and Computation Structures, Jacobs, B. and Löding, C.(eds.),
Vol. 9634, Springer Berlin Heidelberg, Berlin, Heidelberg, 2016, pp. 513–530.
[ 9 ] Hermida, C.: Fibrations, logical predicates andindeterminates, PhD Thesis, University of Edinburgh, UK, 1993.
[10] Jacobs, B.: Categorical Logic and Type Theory,
Studies in Logic and the Foundations of Mathematics, No. 141, Elsevier, paperback edition, 2001.

[11] Katsumata, S.: Parametric Eﬀect Monads andSemantics of Eﬀect Systems, Proceedings of the 41st
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’14, San
Diego, California, USA, ACM Press, 2014, pp. 633–
645.
[12] Katsumata, S.: private communication, 2020.
[13] Knowles, K. and Flanagan, C.: Compositional
Reasoning and Decidable Checking for Dependent
Contract Types, Proceedings of the 3rd Workshop
on Programming Languages Meets Program Veriﬁcation - PLPV ’09, Savannah, GA, USA, ACM
Press, 2008, pp. 27.
[14] Lehmann, N. and Tanter, É.: Gradual Reﬁnement Types, ACM SIGPLAN Notices, Vol. 52,
No. 1(2017), pp. 775–788.
[15] McDermott, D. and Mycroft, A.: Extended Callby-Push-Value: Reasoning About Eﬀectful Programs and Evaluation Order, Programming Languages and Systems, Caires, L.(ed.), Vol. 11423,
Springer International Publishing, Cham, 2019,
pp. 235–262.
[16] Melliès, P.-A. and Zeilberger, N.: Functors Are
Type Reﬁnement Systems, Proceedings of the 42nd
Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages - POPL ’15,
Mumbai, India, ACM Press, 2015, pp. 3–16.
[17] Moggi, E.:
Notions of Computation andMonads, Information and Computation, Vol. 93,
No. 1(1991), pp. 55–92.
[18] Ou, X., Tan, G., Mandelbaum, Y., and Walker,
D.: Dynamic Typing with Dependent Types, Exploring New Frontiers of Theoretical Informatics,
Levy, J.-J., Mayr, E. W., and Mitchell, J. C.(eds.),
Vol. 155, Kluwer Academic Publishers, Boston,
2004, pp. 437–450.
[19] Rondon, P. M., Kawaguci, M., and Jhala, R.:
Liquid Types, Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’08, Tucson, AZ,
USA, ACM Press, 2008, pp. 159.
[20] Rushby, J., Owre, S., and Shankar, N.: Subtypes for Speciﬁcations: Predicate Subtyping in
PVS, IEEE Transactions on Software Engineering,Vol. 24, No. 9(Sept./1998), pp. 709–720.
[21] Sato, T., Barthe, G., Gaboardi, M., Hsu, J.,
and Katsumata, S.-y.: Approximate Span Liftings:
Compositional Semantics for Relaxations of Diﬀer-

ential Privacy, 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vancouver, BC, Canada, IEEE, June 2019, pp. 1–14.
[22] Simpson, A. and Plotkin, G.: Complete Axioms for Categorical Fixed-Point Operators, Proceedings Fifteenth Annual IEEE Symposium on
Logic in Computer Science (Cat. No.99CB36332),
Santa Barbara, CA, USA, IEEE Comput. Soc, 2000,
pp. 30–41.
[23] Swamy, N., Chen, J., Fournet, C., Strub, P.-Y.,
Bhargavan, K., and Yang, J.: Secure Distributed
Programming with Value-Dependent Types, Journal of Functional Programming, Vol. 23, No. 4(2013),
pp. 402–451.
[24] Swamy, N., Weinberger, J., Schlesinger, C.,
Chen, J., and Livshits, B.: Verifying Higher-Order
Programs with the Dijkstra Monad, Proceedings ofthe 34th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI
’13, Seattle, Washington, USA, ACM Press, 2013,
pp. 387.
[25] Unno, H., Satake, Y., and Terauchi, T.: Relatively Complete Reﬁnement Type System for Veriﬁcation of Higher-Order Non-Deterministic Programs, Proceedings of the ACM on Programming
Languages, Vol. 2(2018), pp. 1–29.
[26] Vazou, N., Rondon, P. M., and Jhala, R.: Abstract Reﬁnement Types, Programming Languages
and Systems, Hutchison, D., Kanade, T., Kittler,J., Kleinberg, J. M., Mattern, F., Mitchell, J. C.,
Naor, M., Nierstrasz, O., Pandu Rangan, C., Steffen, B., Sudan, M., Terzopoulos, D., Tygar, D.,
Vardi, M. Y., Weikum, G., Felleisen, M., and Gardner, P.(eds.), Vol. 7792, Springer Berlin Heidelberg,
Berlin, Heidelberg, 2013, pp. 209–228.
[27] Vazou, N., Seidel, E. L., Jhala, R., Vytiniotis, D., and Peyton-Jones, S.: Reﬁnement types
for Haskell, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming - ICFP ’14, Gothenburg, Sweden, ACM
Press, 2014, pp. 269–282.
[28] Xi, H. and Pfenning, F.: Eliminating Array
Bound Checking through Dependent Types, Proceedings of the ACM SIGPLAN 1998 Conference on
Programming Language Design and Implementation - PLDI ’98, Montreal, Quebec, Canada, ACM
Press, 1998, pp. 249–257.