10.6092/issn.1972-5787/6232
Sheafification is a popular tool in topos theory which allows to extend the internal logic of a topos with new principles. One of its most famous applications is the possibility to transform a topos into a boolean topos using the dense topology, which corresponds in essence to Gödel’s double negation translation. The same construction has not been developed in Martin-Löf type theory because of a mismatch between topos theory and type theory. This mismatched has been fixed recently by considering homotopy type theory, an extension of Martin-Löf type theory with new principles inspired by category theory and homotopy theory, and which corresponds closely to higher toposes. In this paper, we give a computer-checked construction of Lawvere-Tierney sheafification in homotopy type theory.
application/pdf
1972-5787
6232
2
en
Nicolas Tabareau
Journal of Formalized Reasoning
modalities
Lawvere-Tierney sheafification in Homotopy Type Theory
Text.Serial.Journal
https://jfr.unibo.it/
9
Articles
2016-12-30
2016-07-12
2016-12-01
2017-09-04
131-161
JFR
Nicolas Tabareau
2016/12/30
10.6092/issn.1972-5787/6232
131
Inria
1972-5787
2
modalities
en
161
Lawvere-Tierney sheafification in Homotopy Type Theory
https://jfr.unibo.it/article/download/6232/6389
9
Lawvere-Tierney sheafification in Homotopy Type
Theory
Kevin Quirin
École des Mines de Nantes, France
and
Nicolas Tabareau
Inria, France


Sheacation is a popular tool in topos theory which allows the extension of the internal logic of
a topos with new principles. One of its most famous applications is the transformation of a given
topos into a boolean topos using the dense topology, a construction which corresponds in essence to
Gödel's double negation translation. The same construction has not yet been developed in Martin-
Löf type theory due to a mismatch between topos theory and type theory. This mismatch has
been xed recently by the introduction of homotopy type theory, an extension of Martin-Löf type
theory with new principles inspired by category theory and homotopy theory, and corresponding
closely with the theory of higher toposes. In this paper, we give a computer-checked construction
of Lawvere-Tierney sheacation in homotopy type theory.




1.   INTRODUCTION
Sheafification [MM92] is a very powerful geometric construction which arose initially
in topology and algebraic geometry but which, nonetheless, quickly found important
applications to mathematical logic. In topos theory, sheafification can be seen as a
way to transform one topos into another. It is used, for example, to build, from any
topos T , a boolean topos (i.e. one which validates the excluded middle principle)
satisfying the axiom of choice and negating the continuum hypothesis [MM92,
Theorem VI.2.1]. This is, in fact, an adaptation of a slightly older set theoretic
method called forcing which transforms a model M of ZFC into a model M[G] of ZFC,
satisfying new principles. Its most famous application is the proof of consistency
of ZFC with the negation of the continuum hypothesis by Paul Cohen [Coh66],
answering (neither negatively nor positively) Hilbert’s first problem. Indeed, Gödel
proved in 1938 the consistency of ZFC with continuum hypothesis [Göd38] using
the constructible model L. The central idea of forcing is to add to the theory
ZFC partial information about the witness of ¬CH. Then, supposing that ZFC is
coherent, it is provable that ZFC together with a finite number of approximation of
the desired object is still consistent. Finally, the compactness theorem allows one to
prove the consistency of ZFC with all approximations, i.e. with a witness of ¬CH.
   Subsequently, forcing was adapted to topos theory by Myles Tierney [Tie72a]
making use of the notion of sheaves. Note that, in topos theory, there are two
different kind of sheaves: Grothendieck sheaves, which only exist on a presheaf
topos, and Lawvere-Tierney sheaves. One can show that Lawvere-Tierney sheaves,
when considered on a presheaf topos, are exactly the Grothendieck sheaves; thus,
Lawvere-Tierney sheaves can be seen as a generalization of Grothendieck sheaves.

                                      Journal of Formalized Reasoning Vol. 9, No. 2, 2016, Pages 131–161.
132     ·      K. Quirin and N. Tabareau

Given a topos T , one can build another topos – the topos of sheaves Sh(T ) –
together with a geometric embedding from Sh(T ) to T whose left adjoint is called
sheafification. Depending on the sheaves we choose to treat, the topos Sh(T ) may
satisfy new principles. The construction of the geometric embedding is done in
[MM92, Section V.3], and briefly recalled in section 4.
   Type theory is known to have a close relationship with topos theory, prompting one
to wonder if similar techniques might not be developed for type theory. The answer to
this question has been given recently by the advent of homotopy type theory [UFP13],
an extension of Martin-Löf type theory with principles inspired by (higher) category
theory and homotopy theory, such as higher inductive types [LS13, UFP13] and
Voevodsky’s univalence principle [KL12], which says that for any types T and U ,
the canonical map
                                      (T = U ) → (T ' U )
transporting equalities to equivalences, is itself an equivalence. This new point
of view on type theory has revealed how types carry homotopical structure. For
instance, mere propositions (or Type−1 ) are just types with an irrelevant equality
and sets (or Type0 ) are types with a propositional equality and so on for Typen .
The development of univalence has also shed some light on the difficulty of making
AC and EM coexist in type theory. Indeed, it has been shown that a naive (non-
propositional) version of EM is inconsistent with univalence.
   When restricted to mere propositions and sets, homotopy type theory corresponds
quite closely to topos theory but the mismatch starts when considering higher
homotopy types. Fortunately, a higher version of topos theory has been developed
recently, synthesized in the monograph of Lurie on higher topos theory [Lur09]. Even
if the connection between homotopy type theory and higher topos theory has not
yet been made perfectly precise, it is commonly believed that the former constitutes
an internal language for the latter (see [Shu15b] for a more detail discussion on this
topic).
   Lurie has adapted a considerable number of the tools of topos theory to a higher
setting. In particular, the theory of sheaves has been lifted to higher topos theory.
As the notion of higher topos appears to correspond very closely to homotopy type
theory, this provides a new hope that tackling the problem of extending the power
of homotopy type theory using sheafification is actually possible.
   Nevertheless, the adaptation of the sheafification in higher topos theory to ho-
motopy type theory is not completely straightforward because the construction
in higher toposes is restricted to the initial Grothendieck setting which is still
very topologically oriented, and hence not very amenable to formalization in type
theory. It seems more promising to use a synthetic notion of sheafification, called
Lawvere-Tierney sheafification [Tie72b, MM92], but this construction has not been
considered yet in the setting of higher topos theory. This raises two issues that
this paper addresses: (i) how to lift the notion of Lawvere-Tierney sheafification to
higher topos theory and (ii) whether is it possible to formalize this new definition
in homotopy type theory.
   This paper presents a definition of the sheafification functor in the setting of
homotopy type theory. As Lawvere-Tierney sheaves have not, to our knowledge,
been considered in the higher setting, the contribution of this article is twofold:
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                    Lawvere-Tierney sheafification in Homotopy Type Theory           ·     133

(i) we propose a construction which coincides with Lawvere-Tierney sheafification
when restricted to hSets by connecting it to the work on higher modalities [UFP13],
(ii) we formalize all the definitions and theorems internally inside the Coq proof
assistant [CDT15].
Plan of the paper
Section 2 introduces the necessary preliminaries on Homotopy Type Theory while
Section 3 presents the version of higher modalities that we use. Section 4 recalls the
definition of sheafification in toposes. Section 5 presents the main contribution of
this article, the definition of sheafification in Homotopy Type Theory, and Section 6
discusses its formalization inside the Coq proof assistant.
Related Work
Similar questions have been considered in relation to the Curry-Howard isomorphism,
that is, the possibility of extending a programming language close to type theory with
new logical or computational principles while keeping consistency automatically. For
instance, much effort has been invested in providing a computational content for the
law of excluded middle in order to define a constructive version of classical logic. This
has lead to various calculi, most notably the λµ-calculus of Parigot [Par93]. However,
this line of work has not appeared to be fruitful in defining a new version of type
theory with classical principles. Other authors have tried to extend the continuation-
passing-style (CPS) transformation to type theory. They have been faced, however,
with the difficulty that the CPS transformation is incompatible with (full) dependent
sums [BU02], emphasizing the fragile link between the axiom of choice and the law of
excluded middle in type theory. Nevertheless the axiom of choice has been shown to
be realizable by computational meaning in a classical setting by techniques turning
around the notion of (modified) bar induction [BBC98], Krivine’s realizability [Kri03]
and even more recently with restriction on elimination of dependent sums and lazy
evaluation [Her12]. The work on forcing in type theory [JTS12, JLP+ 16] also gives a
computational meaning to a type theory enriched with new logical or computational
principles. Actually, this construction is entirely complementary to forcing in type
theory, as forcing corresponds to the presheaf construction while Lawvere-Tierney
sheafification corresponds to the topological transformation that allows the passage
from the presheaf construction to the sheaf construction.

2.   PRELIMINARIES ON HOMOTOPY TYPE THEORY
In this section, we review some basic definitions in homotopy type theory which
will be central to our formalization but not specific to sheafification. Some of the
definitions and theorems of Section 2.1 appear in [UFP13] (or are direct applications
of results which do) while others are specific to our formalization.
   As a prerequisite, we encourage the reader to be familiar with type theory and
in particular the point of view developed in [UFP13]. Nevertheless, we recall
most of the central definitions that we use so that the paper is sufficiently
                                                                            Q self-
contained. Given a type T and P   a type  family U : T →  Type,  we  denote   x:T U x
for the dependent product, x:T U x for the dependent sum, and π1 , π2 for the
first and second projection of a dependent pair (denoted (a; b)). The identity
path will be denoted 1. We use informal mathematical language instead of type
                                           Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
134     ·      K. Quirin and N. Tabareau

theory whenever it is possible, to ease in reading without making our statements
imprecise. In particular, (higher) inductive types are defined using itemization to
avoid an overhead of notation. Throughout the paper, Type must be seen in an
universe-polymorphic way.
  Section 2.1 will present homotopy levels and object classifiers, section 2.2 intro-
duces a theory of colimits in homotopy type theory, illustrated by an important
example in section 2.3.
2.1   Homotopy Types and Classifying Objects
One of the most direct applications of homotopical notions to type theory is the
introduction of homotopy types. Using the analogy that points in a space correspond
to elements of a type and that paths between two points correspond to elements of
the corresponding identity type (which defines equality in type theory), an n-type
is simply a type for which equality becomes trivial above level n. Voevodsky has
realized that this notion admits a compact inductive definition internal to type
theory, given by
  Definition 2.1. Is-n-type is defined by induction on n > −2:
—Is-(−2)-type X if X is a contractible type, i.e. X is pointed by c : X, and every
 other point in X is equal to c.
                   def Q
—Is-(n + 1)-type X = x,y:X Is-n-type(x = y).
                def   P
Then, Typen =          X:Type   Is-n-type X.
  When n = −1, we will use IsHProp and HProp instead of Is-(−1)-type and
Type−1 .
  From any type T , the type kT kn : Typen can be constructed as the HIT generated
by
—a function | · |n : T → kAkn ,
—a proof of Is-n-type kT kn ,
satisfying the following universal property:
  Lemma 2.2. For any A : Type and B : Typen , if f : A → B then there is an
induced g : kAkn → B such that g(|a|n ) = f (a) for any a : A.
We refer the reader to [UFP13, 7.3] for more details on truncations.
                                                                                    def
PThe homotopy fiber of a function f at element b is defined as fibf (b) =
  a:A f (a) = b. A function f has n-truncated homotopy fibers (or simply is an
n-truncated function) when fibf (b) is in Typen for any b. Again, we define some
syntactic sugar. A function f is
—an embedding if f is (−1)-truncated
—a surjection if every fiber of f is merely inhabited (i.e kfibf (y)k holds for all y).
One can show [UFP13, Lemma 7.6.4] that any map f factors uniquely through
       def P
Im(f ) =    y:B kfibf (y)k as a surjection followed by an embedding.



Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                        Lawvere-Tierney sheafification in Homotopy Type Theory            ·     135

  Following [RS15], it is possible to show that, for any homotopy level n and any
type B, Typen classifies subobjects of B with n-truncated homotopy fibers in the
sense that there is an equivalence
                                                      ∼
                   X X Y
              χ:                   Is-n-type fibf (b) −
                                                      → (B → Typen )
                      A:Type f :A→B b∈B

such that the usual subobject classifier diagram ([UFP13, Theorem 4.8.4]) is a pull-
back. Therefore, in our construction, we will represent a subobject of a type B with
n-truncated homotopy fibers either as a map f : A → B such that Is-n-type fibf (b),
or as a map B → Typen .
2.2     Colimits in Homotopy Type Theory
One desireable construction we would like to consider is the Čech nerve (Section 2.3).
In order to do so, this section presents a definition of colimits in a type theoretic
setting. Following the definition of graphs and diagrams defined in [AKL15], we
recall the definition of colimits of diagrams overs graphs presented in [RS15].
  A colimit of a diagram D over a graph G is given by a type P that defines a
cocone on D, plus the universal property that for any type X, the canonical map
that transforms a function f : P → X to a cocone of D on X is an isomorphism.
  Definition 2.3. Let G be a graph, and D be a diagram on G. Let P : Type
together with
                                                       Q
—a map qi : D0 (i) → P for any vertex i : G0 , i.e. q : i:G0 D0 (i) → P
—for anyQ verticesQi, j : G0 and all edges φ : G1 (i, j), a path pφi,j : qj ◦ D1 (φ) = qi ,
 i.e. p : i,j:G0 φ:G1 (i,j) qj ◦ D1 (φ) = qi .
     Then P is the colimit of D if for any other X : Type,
                                                                   
                 IsEquiv λf : P → X, λi, f ◦ qi ; λi j φ, f (pφi,j )) .
Using higher inductive types, every diagram D on a graph G admits a colimit in
homotopy type theory.
  In 5.2.1, we will need to know how colimits behave with respect to truncations.
An answer is given by the following lemma.
   Lemma 2.4. Let D be a diagram, m a truncation index, and P : Typem a colimit
of D. Then, if kDkm is the same diagram as D where every type is m-truncated, P
is a m-colimit1 of kDkm .
The proof is quite straightforward: a cocone over D into P can be changed equiv-
alently into a cocone over kDkm into kP km , using the elimination principle of
truncations, and then we can show that the following diagram commutes for any
X : Typem
                             kP km → X             / cocone(kDkm , X)
                                                             O
                                    ∼




                                                          ∼




                                 
                               P →X
                                               ∼    / cocone(D, X)

1P    is a m-colimit if P satisfies the same property as in 2.3 when we replace Type by Typem
                                                Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
136      ·     K. Quirin and N. Tabareau

2.3    On Giraud-Rezk-Lurie axioms
The Giraud-Rezk-Lurie axioms are the ∞-version of Giraud’s axioms that charac-
terize a topos. Namely, there are four axioms on a (∞, 1)-category that have been
shown to be equivalent to (∞, 1)-topos axioms [Lur09, Chapter 6]. A consequence
which we would like to use here is the fact that a surjection (i.e. (−1)-connected
function) is the colimit of its Čech nerve. In [Bou16], the authors propose an
analogue of this property: they give, for any map f , a diagram C(f ) whose colimit
is Im(f ).
   This property will be essential in the proof that the construction n+1 , defined
in Section 5.2.1, gives rise to a modality.
   Definition 2.5. Let f : X → Y be a map. The coequalizer Tf of the kernel pair
of f is the higher inductive type given by
—t : X → Tf
—α : ∀a b : X, f (a) = f (b) → t(a) = t(b)
—α1 : ∀a : X, α(a, a, 1) = 1
                                                            π1
                                                                 /
                                                                 / X preserving the iden-
                                 P
We view Tf as the coequalizer of   a,b:X f (a) = f (b)      π2

tity. We call f˜ the map Tf → Y given by induction.
  Then, the considered diagram C(f ) is the mapping telescope of the iterations of
T.
   Definition 2.6. Let f be a map from X to Y . Then the iterated kernel pair of f
                                      t /      t /         / ···
is given by the diagram C(f ) := X        Tf       Tf˜

     Let’s recall the main theorem:
   Theorem 2.7 (Colimit of C(f ) [Bou16]). For any morphism f : X → Y ,
the colimit of C(f ) is Im(f ), the image of f .

3.    MODALITIES
This section presents modalities in Homotopy Type Theory as defined in [UFP13]
and later developed in [SS14, Shu15a]. We have added proofs of various properties of
modalities when they are not already present in the literature. A truncated version
of modalities, specific to our work, is then presented together with a discussion of
the formalization.
     Definition 3.1. A left exact modality is the data of
(1) A predicate P : Type → HProp
(2) For every type A, a type #A such that P (#A)
(3) For every type A, a map ηA : A → #A
such that
(4) For every types A and B, if P (B) then
                            
                               (#A → B) → (A → B)
                                        f 7→ f ◦ ηA
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                    Lawvere-Tierney sheafification in Homotopy Type Theory             ·     137

    is an equivalence.
                                                                   Q
        any A : Type and B : A → Type such that P (A) and x:A P (Bx), then
(5) for P
    P ( x:A B(x))
(6) for any A : Type and x, y : A, if #A is contractible, then #(x = y) is contractible.
Conditions (1) to (4) define a reflective subuniverse, (1) to (5) a modality.
   Remark 3.2. The inverse of − ◦ ηA from point (4)
                                                 Q will beQdenoted #rec : (A →
B) → (#A → B), and its computation rule #βrec : f :A→B x:A #rec (f )(ηA x) =
f x.
   If # is a modality, the type of modal types will be denoted Type# . Let us fix a
left-exact modality # for the rest of this section. A modality acts functorialy on
Type, in the sense that
  Lemma 3.3 (Functoriality of modalities). Let A, B : Type and f : A →
B. Then there is a map #f : #A → #B. Moreover
—For all A, B : Type and f : A → B, #f ◦ ηA = ηB ◦ f .
—For all X : T ype, Y, Z : Type# , f : X → Y and g : Y → Z,
                               g ◦ #rec (f ) = #rec (g ◦ f ).
—For all X, Y : T ype, Z : Type# , f : X → Y and g : Y → Z,
                              #rec (g) ◦ #f = #rec (g ◦ f ).
—For all X, Y, Z : Type, f : X → Y and g : Y → Z,
                                     #(g ◦ f ) = #g ◦ #f.
—If IsEquiv f , then IsEquiv #f .
  Proof. We define #f by
                                       def
                                 #f = #rec (ηB ◦ f ).
Then
—By the computation principle of #rec , the first point is obvious.
—As Z is modal and both functions are #X → Z, it suffices to show that
                           g ◦ #rec g ◦ ηX = #rec (g ◦ f ) ◦ ηX .
 But both sides are equal to g ◦ f using computational rules.
—We will show that each side is equal to
                               def
                             ϕ = #rec ((#rec g) ◦ (ηY ◦ f )).
 The left-hand side is equal to ϕ using the previous point, applied to ηY ◦ f . For
 the right-hand side, it suffices to show that g ◦ f = #rec (g) ◦ ηY ◦ f, which is
 exactly the computation rule of #rec composed with f .
—This is a particular case of the previous point, applied to f and ηZ ◦ g.
—If f is an equivalence, an obvious inverse for #f is #(f −1 ).

                                             Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
138      ·     K. Quirin and N. Tabareau



  Proposition 3.4. Any left-exact modality # satisfies the following properties2 .
•(R)    A is modal if and only if ηA is an equivalence.
•(R)    1 is modal.
        Type# is closed under dependent products, i.e. x:A B x is modal as soon as
                                                        Q
•(R)
  all   B x are modal.
•(R)    For any types A and B, the map
                                     #(A × B) → #A × #B
  is an equivalence.
•(R) If A is modal, then for all x, y : A, (x = y) is modal.
•(M) For every type A and B : #(A) → Type# , then
                                Q                 Q
                                  z:#A  B z −→ a:A B(ηA a)
                     − ◦ ηA :
                                     f       7−→ f ◦ ηA
  is an equivalence.
•(M) If A, B : Type are modal, then so are Is-n-type A, A ' B and IsEquiv f for
  all f : A → B.
•(L) If X, Y : Type and f : X → Y , then the map
                                    # (fibf (y)) → fib#f (ηB y)
  is an equivalence, and the following diagram commutes

                                     fibf (y)
                                                   η
                                                       / # (fibf (y))

                                       γ
                                           w
                                  fib#f (ηB y)
                                                                 Q
  Remark 3.5. Again, the inverse of − ◦ ηA will be denoted #ind : a:A B(ηA a) →
Q                                     β    Q Q               Q
 z:#A B x, and its computation rule #ind :   f:      B(ηA a)  x:A #ind (f )(ηA x) =
                                                             a:A
fx
 Proof. —If ηA is an equivalence, then A ' #A, so A is modal.
 Now if A is modal, then we have #rec (id) : #A → A, and one can easily check
 that it is an inverse to ηA .
—Given the previous proof, it suffices to prove that η1 is an equivalence. The only
 way to inhabit #1 → 1 is with λ x, ?. It is straightforward to check that this
 forms an equivalence.
—This is [UFP13, Theorem 7.7.2].
—This is [UFP13, Corollary 7.7.3].

2 Propertiesneeding only a reflective subuniverse are annotated by (R), a modality by (M), a
left-exact modality by (L)



Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                   Lawvere-Tierney sheafification in Homotopy Type Theory            ·     139

—Again, it suffice to show that ηx=y is an equivalence. We begin by showing that
                      (λ _ : #(x = y), x) = (λ _ : #(x = y), y).
  As A is modal, ηA is an equivalence, as well as apηA : x = y → #(x = y). Thus,
  it suffices to show that
              (λ _ : #(x = y), x) ◦ apηA ) = (λ _ : #(x = y), y) ◦ apηA ,
 and the latter is obvious using functional extensionality. Now, applying the just
 proved equality to any u : #(x = y) yields x = y. One can prove that this defines
 an inverse to ηx=y .
—This is [UFP13, Theorem 7.7.7].
—We show that Is-n-type A is modalP   by induction
                                            Q      on the truncation level n.
 If n = −2, we have Is-n-type A ' a:A b:A b = a. The latter is modal using
 stability by dependent sums, dependent products and paths type.
 Now, if for every A, Is-n-type A is modal, then Is-(n + 1)-type A is equivalent to
                                Y
                                     Is-n-type x = y.
                                   x,y:A

 Again, using stability by dependent products and the induction hypothesis, the
 latter is modal.
 The facts that A ' B and IsEquiv f for any modal types A, B and map f : A → B
 are modal are technical, but don’t involve new methods. They can be found in
 the formalization.
—It is straightforward to define a map
                            X             X
                         φ:     fx = y →      #f x = ηY y,
                             x:X              x:#X

  using η functions. We will use the following lemma to prove that the function
  induced by φ defines an equivalence:
     Lemma 3.6. Let X : Type, Y : Type# and f : X → Y . If for all y :
  Y , #(fibf (y)) is contractible, then the function #X → Y induced by f is an
  equivalence.
  Hence we just need to check that every #-fiber #(fibφ (x; p)) is contractible.
  Technical transformations allow one to prove
                                fibφ (x; p) ' fibs (y; p−1 )
  for
                                   fibηX (x) −→ fibηY (#f x)
                           s:
                                     (a, q) 7−→ (f a, −)
  But left-exactness allows to characterize the contractibility of fibers:
     Lemma 3.7. Let A, B : Type. Let f : A → B. If #A and #B are contractible,
  then so is #(fibf (b)) for any b : B.



                                           Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
140     ·      K. Quirin and N. Tabareau

  Thus, we just need to prove that #(fibηX (a)) and #(fibηY (b)) are contractible. But
  one can check that η maps always satisfy this property. Finally, #(fibs (y; p−1 )) is
  contractible, so #(fibφ (x; p)) also, and the result is proved.



  Let us finish these properties by the following proposition, giving an equivalent
characterization of left-exactness.
  Proposition 3.8. Let # be a modality. Then # is left-exact if and only if #
preserves path spaces, i.e.
                            Y Y
                                 IsEquiv(#(apηA ))
                                A:Type x,y:A

where #(apηA ) : #(x = y) → ηA x = ηA y.
  Proof. We will rather prove something slightly more general, using an encode-
decode proof [UFP13, Section 8.9]; we will characterize, for a type A and a fixed
inhabitant x : A the type
                                                ηA x = y
for any y : #A.
  Let Cover : #A → Type# be defined by induction by
                                          def
                              Cover(y) = #rec (λy, #(x = y)).
Note that for any y : #A, Cover(y)
                            Q      is always modal. We will show that ηA x = y '
Cover(y). Now, let Encode : y:#A ηA x = y → Cover(y) be defined by
                                               #β
                     def
                                                                               
                                                 rec ((λz, #(x=z)),x)
       Encode(y, p) = transportpCover transportidmap                   (ηx=x 1)
              Q
and Decode : y:#A Cover(y) → ηA x = y by
                                                   #β
                 def
                                                                           
                                                      rec ((λz, #(x=y)),y)
         Decode = #ind λy p, #(apηA ) transportidmap                       p

Then one can show, using #-induction and path-induction, that for any y : #A,
Encode(y, −) and Decode(y, −) are each other inverses. Then, taking y 0 = ηA y,
we have just shown that ηA x = ηA y ' Cover(ηA y), which is itself equivalent, by
#βrec , to #(x = y). It is straightforward to check that the composition #(x = y) →
Cover(ηA y) → ηA x = ηA y is exactly #(apηA ).
   Now, let us prove the backward implication. Let A be a type such that #A
is contractible, and x, y : A. As ηA x, ηA y : #A, we know that ηA x = ηA y is
contractible. But as ηA x = ηA y ' #(x = y) by assumption, #(x = y) is also
contractible.
  As this whole paper deals with truncation levels, it should be interesting to see
how they are changed under a modality. We already know that if a type T is
(−2)-truncated, i.e. contractible, then it is unchanged by the reflector:
                                      #T ' #1 ' 1 ' T.

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                       Lawvere-Tierney sheafification in Homotopy Type Theory           ·     141

Thus, Type−2 is closed by any reflective subuniverse. Now, let T : HProp. To check
that #T is an h-proposition, it suffices to check that
                                      Y
                                           x=y
                                         x,y:#T
                               Q
For any x :Q#T , the type y:#T x = y is modal, as all x = y are; by the same
argument, x:#T x = y is modal too for any y : #T . Using twice the dependent
eliminator of #, it now suffices to check that
                                   Y
                                        ηT x = ηT y.
                                      x,y:T

As T is supposed to be an h-proposition, this is true. It suffices to state
  Lemma 3.9. For any modality, Type−1 is closed under the reflector #, i.e.
                            Y
                                 IsHProp(#P ).
                                   P :HProp

  A simple induction on the truncation level, together with the left-exactness
property allows to state
  Lemma 3.10. For any left-exact modality, all Typep are closed under the reflector
#, i.e.
                             Y
                                   Is-p-type(#P ).
                                   P :Typep

3.1    Examples of modalities
  3.1.1    The identity modality. Let us begin with the most simple modality one
                                                                                  def
can imagine: the one doing nothing. We can define it by letting #A = A for any
                 def
type A, and ηA = idmap. Obviously, the desired computation rules are satisfied,
so that the identity modality is indeed a left-exact modality.
  It might sound useless to consider such a modality, but it can be precious when
looking for properties of modalities: if it does not hold for the identity modality, it
cannot hold for an abstract one.
   3.1.2 Truncations. The first class of non-trivial examples might be the trunca-
tions modalities, as described in [UFP13, Section 7.3].
  3.1.3    Double negation modality
                                                                    def
  Proposition 3.11. The double negation modality #A = ¬¬A is a modality.
  Proof. We define the modality with
(1) We will define the predicate P later.
(2) # is defined by #A = ¬¬A
(3) We want a term ηA of type A → ¬¬A. The term
                                      def
                                   ηA = λ x : A, λ y : ¬A, y a
      matches this requirement.         Q
      Now, we can define P to be exactly A:Type IsEquiv ηA .
                                              Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
142      ·     K. Quirin and N. Tabareau

(4) Let A, B : Type, and ϕ : A → ¬¬B. We want to extend it into ψ : ¬¬A → ¬¬B.
    Let a : ¬¬A and b : ¬B. Then a(λ x : A, ϕ x b) : 0, as wanted. One can check
    that it forms an equivalence.
                                                          Q
(5) Let A : Type and B : A → Type such that P (A) and a:A P (B a). There is a
    map
                                   X
                                      Bx→A
                                             x:A
      thus by the previous point, we can extend it into
                                          X
                                   κ : ¬¬    B x → A.
                                                   x:A
                                              P
      It remains to check that for any x : ¬¬ x:A B x, B(κ x).
      But the previous map can be easily
                                       P extended to the dependent case, and thus it
      suffices to show that for all x : x:A B x, B(κ(η x). As κ ◦ η = idmap, the goal
      is solved by π2 x.


  Unfortunately, it follows that the only types which can be modal are h-propositions,
as they are equivalent to their double negation which is always an h-proposition.
Thus, the type of modal types consists only of h-propositions, which is not satisfactory.
The main purpose of this paper is to extend this modality into less destructive one.
3.2    Toward a new type theory
We suppose here that # is a left-exact modality such that Type# is modal. This is
for example the case when the modality is accessible (see [BGL+ 17] for definition
and proof). We call a modality # consistent if #0 is empty.
   Proposition 3.12. The modal universe Type# is non-trivial (non contractible)
if the type #0 is empty.
  Proof. By condition (iv) of Definition 3.1, #0 is an initial object of Type# ,
and thus corresponds to false for modal mere proposition. As #1 = 1, Type# is
non-trivial when #0 6= 1, that is when there is no proof of #0.
   In topos theory, Lawvere-Tierney topologies give rise to subtoposes Shj E ,→ E;
actually, every subtopos F ,→ E comes from a Lawvere-Tierney topology [MM92,
Corollary VII.4.7]. In the same way, left-exact modalities should induce sub-type
theories, and we should be able to exhibit a translation from this sub-type theory
into the ground type theory, as in [JLP+ 16].
3.3    Truncated modalities
As for colimits, we define a truncated version of modalities, in order to use it in
section 5. Basically, a truncated modality is the same as a modality, but restricted
to Typen .
  Definition 3.13 (Truncated modality). Let n ≥ −1 be a truncation index.
A left exact modality at level n is the data of
(1) A predicate P : Typen → HProp
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Lawvere-Tierney sheafification in Homotopy Type Theory          ·     143

(2) For every n-truncated type A, a n-truncated type #A such that P (#A)
(3) For every n-truncated type A, a map ηA : A → #A
such that
(4) For every n-truncated types A and B, if P (B) then
                             
                               (#A → B) → (A → B)
                                       f 7→ f ◦ ηA
    is an equivalence.
                                                            Q
        any A : Typen and B : A → Typen such that P (A) and x:A P (Bx), then
(5) for P
    P ( x:A B(x))
(6) for any A : Typen and x, y : A, if #A is contractible, then #(x = y) is
    contractible.
  Properties of truncated left-exact modalities described in 3.4 are still true when
restricted to n-truncated types, except the one that does not make sense: Type#    n
cannot be modal, as it is not even a n-truncated type.
3.4   Formalization
Let us discuss here the formalization of the theory of modalities. General modalities
are formalized in the Coq/HoTT library [BGL+ 17], thanks to the work of Mike
Shulman [Shu]. The formalization might seem straightforward, but the universe
levels (at least, their automatic handling by Coq) become a major issue. Hence, we
have to explicitly give the universe levels and their constraints in a large part of the
library. For example, the reflector # of a modality is defined in [BGL+ 17] as
                                  # : Typei → Typei ;
it maps any universe to itself.
   In section 5, we will need a slightly more general definition of modality. The
actual definitions stay the same, but the universes constraints we consider change.
The reflector # will now have type
                              # : Typei → Typek ,      i 6 k;
it maps any universe to a possibly higher one. Other components of the modality
will have types
            P : Typei → HPropk ,                          i6k
                Q                k
            η : A:Typei #A : Type ,                       i6k
                Q       Q        Q
            − : A:Typei B:Typej h:P (B) IsEquiv(− ◦ ηA ), i, j 6 k
   Fortunately, this change is small enough as to preserve usual properties of modal-
ities. Of course, the examples of modalities mapping any universe to itself are
still examples of generalized modalities, simply ones which do not make use of the
possibility of inhabiting a higher universe.
   We would like to have the same generalization for truncated modalities. How-
ever,
P in this case many new universe levels appear, mostly because in Typen =
   T :Type Is-n-type T , and Is-n-type each comes with its own universe. As a result,
handling “by hand” so many universes together with their constraints quickly gets
                                            Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
144     ·      K. Quirin and N. Tabareau

out of control. One idea to fix this issue could be to use resizing rules [Voe], allowing
h-propositions to live in the smallest universe. We could then get rid of the universes
generated by Is-n-type, and treat the truncated modality exactly as any other
generalized modality.
  In our formalization, we decided to work with the type-in-type Coq option, to
avoid any issue with universes.

4.    SHEAVES IN TOPOSES
In this section, we will work in an arbitrary topos rather than in type theory. The
next section will present a generalization of the results presented here.
  Let us fix for the whole section a topos E, with subobject classifier Ω. A Lawvere-
Tierney topology on E is a way to modify slightly truth values of E. It allows one to
speak about locally true things instead of true things.
   Definition 4.1 (Lawvere-Tierney topology [MM92]). A Lawvere-Tierney
topology is an endomorphism j : Ω → Ω preserving > (j > = >), idempotent
(j ◦ j = j) and commuting with products (j ◦ ∧ = ∧ ◦ (j, j)).
  A classical example of Lawvere-Tierney topology is given by double negation.
Other examples are given by Grothendieck topologies, in the sense of the following:
   Theorem 4.2 ([MM92, Theorem V.1.2]). Every Grothendieck topology J on
a smallopcategory C determines a Lawvere-Tierney topology j on the presheaf topos
SetsC .
  Any Lawvere-Tierney topology j on E induces a closure operator A 7→ A on
subobjects. If we see a subobject A of E as a characteristic function χA , the closure
A corresponds to the subobject of E whose characteristic function is
                                          χA = j ◦ χA .
A subobject A of E is said to be dense when A = E.
   Next, we are interested in objects of E for which it is impossible to make a
distinction between objects and their dense subobjects, i.e. for which “true” and
“locally true” coincide. Such objects are called sheaves, and are defined by
   Definition 4.3 (Sheaves[MM92, Section V.2]). On object F of E is a sheaf
(or j-sheaf) if for every dense monomorphism m : A ,→ E in E, the canonical map
HomE (E, F ) → HomE (A, F ) is an isomorphism.
  One can show that ShE , the full sub-category of E given by sheaves, is again a
topos, with classifying object
                                   Ωj = {P ∈ Ω | jP = P }.
   Lawvere-Tierney sheafification is a way to build a left adjoint aj to the inclusion
E ,→ ShE , exhibiting ShE as a reflective subcategory of E. In particular, this implies
that logical principles valid in E are still valid in ShE .




Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Lawvere-Tierney sheafification in Homotopy Type Theory             ·     145

     For any object E of E, aj (E) is defined as in the following diagram
                                              {·}E
                                E                          / ΩE

                              θE                               jE
                                                            
                                                         / ΩE
                                E0
                                                           <    j


                                   closure
                                              !
                                             aj (E)

   The proof that aj defines a left adjoint to the inclusion can be found in [MM92].
   One classical example of use of sheafification is the construction, from any topos,
of a boolean topos negating the continuum hypothesis. More precisely:
   Theorem 4.4 (Negation of CH [MM92, Theorem VI.2.1]). There exists a
Boolean topos satisfying the axiom of choice, in which the continuum hypothesis
fails.
  The proof actually follows almost exactly the famous construction by Paul Cohen
of a model of ZFC negating the continuum hypothesis [Coh66]. Together with
the model of constructible sets L by Kurt Gödel [Gö40], this proves that CH is
independent of ZFC, solving Hilbert’s first problem.

5.    SHEAVES IN HOMOTOPY TYPE THEORY
The idea of this section is to consider sheafification in toposes as only the first step
towards sheafification in type theory. We remark that axioms for a Lawvere-Tierney
topology on the subobject classifier Ω of a topos are very close to those of a modality
on Ω. We will use this idea extensively, applying it to every subobject classifier
Typen as described in section 2. The subobject classifier Ω of a topos is seen as
the object of truth values of the topos, which corresponds to the type HProp in our
setting; the topos itself is considered proof irrelevant, corresponding to our HSet.
Sheafification in toposes, when translated to the setting of homotopy type theory, is
thus a way to build from a left-exact modality on HProp, a left-exact modality on
HSet. Our hope in this section is to iterate this construction, extending a left-exact
modality on HSet to one on Type1 , and so on.
   The first thing we can note is that such a construction will not allow to reach
every type: it is known that there exist types with no finite truncation level [UFP13,
Example 8.8.6]. Worse, some types are not even the limit of their successive
truncations, even in an hypercomplete setting [MV99]. This suggests that defining a
sheafification functor for all truncated types won’t give (at least easily) a sheafification
functor on the whole of Type. Another issue which must be pointed out is the
complexity of proofs. Whereas in a topos-theoretic setting everything is proof-
irrelevant, this is no longer the case in a higher setting, forcing us to reason about
witnesses for results which were previously true on the nose. This will oblige us
to write long and technical proofs of coherence, and occasionally to completely
modify some lemmas, such as Proposition [MM92, Theorem IV.7.8], stating that
epimorphisms are coequalizers of their kernel pairs.
                                               Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
146     ·      K. Quirin and N. Tabareau

   The main idea is thus to follow as closely as possible the topos-theoretic con-
struction, and change it as few times as possible to make it work in our higher
setting.
   Note that, as the principles we want to add are inherited directly from the HProp
level, the extension to all truncated types is automatic. The choice of the left-exact
modality on HProp is thus crucial. For the rest of the section, we fix one, denoted
#−1 . The reader can think of the double negation #¬¬ defined in 3.1.3. We will
define, by induction on the truncation level, left-exact modalities on all Typen , as
in the following theorem.
  Theorem 5.1. The sequence defined by induction by
                 # : ∀ (n : nat), Typen → Typen
                 #−1 (T ) given
                           def    X        X
                 #n+1 (T ) =          #−1     u = (λt, #n (a = t))
                                 u:T →Type#
                                          n
                                                    a:T

defines a sequence of left-exact modalities, coherent with each others in the sense
that the following diagram commutes for any P : Typen , where P̂ is P seen as an
inhabitant of Typen+1 .

                                        P
                                                ∼         / Pb

                                      ηn                        ηn+1
                                                           
                                      #n P
                                                ∼      / #n+1 Pb

In what follows, formalized results are indicated by the name of the result in the
library in this special font.
5.1   Sheaf theory
Let n be a truncation index greater that −1, and #n be the left-exact modality
given by our induction hypothesis. As in the topos-theoretic setting, we will define
what it means for a type to be a n-sheaf (or just “sheaf”, if the context is clear),
and consider the reflective subuniverses of these sheaves; the reflector will exactly be
the sheafification functor. The main issue in order to arrive at the “right” definition
is the choice of the subobject classifier in which dense subobjects will be chosen:
two choices appear, HProp and Typen ; we will actually use both. This principle
guiding our choice is that the type of all n-sheaves should be a (n + 1)-sheaf.
   From the modality #n , one can build a closure operator.
  Definition 5.2 (cloture,closed,EnJ). Let E be a type.
—The closure of a subobject of E with n-truncated homotopy fibers (or n-subobject
 of E, for short), classified by χ : E → Typen , is the subobject of E classified by
 #n ◦ χ.
—An n-subobject of E classified by χ is said to be closed in E if it is equal to its
 closure, i.e. if χ = #n ◦ χ.
—An n-subobject of E classified by χ is said to be dense in E if its closure is E,
 i.e. if #n ◦ χ = λe, 1
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                    Lawvere-Tierney sheafification in Homotopy Type Theory            ·     147

  Topos-theoretic sheaves are characterized by a property of existence and unique-
ness, which will be translated, as usual, into a proof that a certain function is an
equivalence.
  Definition 5.3 (Restriction (E_to_χmono_map, E_to_χ_map)). Let E, F : Type
and χ : E → Type. We define the restriction map ΦχE as
                                          P
                            E → F −→        e:E χe → F .
                      ΦχE :
                              f     7−→ f ◦ π1
   Here, we need to distinguish between dense (−1)-subobjects, which will be used in
the definition of sheaves, and dense n-subobjects, which will be used in the definition
of separated types.
   Definition 5.4 (Separated Type (separated)). A type F in Typen+1 is sep-
arated if for any type E, and all dense n-subobject of E classified by χ, ΦχE is an
embedding.
                                                                      P
   From the point of view of topos theory, this means that given a map e:E χ e → F ,
if there is an extension f˜ : E → F , then it is unique, as in
                                  P
                                           χe
                                                    f
                                                        /F
                                    e:E                 ;
                                    π1
                                               !

                                      E

   Definition 5.5 (Sheaf (Snsheaf_struct)). A type F of Typen+1 is a (n + 1)-
sheaf if it is separated, and for any type E and all dense (−1)-subobject of E
classified by χ, ΦχE is an equivalence.
                                                P
   In this case, this means that given a map f : e:E χ e → F , one can extend it
uniquely to f˜ : E → F , as in
                                  P
                                           χe
                                                    f
                                                        /
                                    e:E                 ;F
                                    π1
                                               ∃!
                                      E
  Note that these definitions are almost the same as those given in in [MM92]. The
main difference is that separated is defined for n-subobjects, while sheaf only for
(−1)-subobjects. It might seem bizarre to make such a distinction, but the following
proposition gives a better understanding of the situation.
  Proposition 5.6 (nj_paths_separated). A type F is Typen+1 is separated if,
and only if all its path types are n-modal.




                                            Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
148     ·      K. Quirin and N. Tabareau

  Proof. Let F : Typen+1 a separated type, and a, b : F . We want to find an
inverse to ηa=b . We consider the following diagram

                                                                             8/8 F
                                  P                                 fst◦π1
                                      (a,b):F ×F       a=b
                                                           snd◦π1
                                             ι
                                                                    fst◦π1
                                P                
                                    (a,b):F ×F       #(a = b)

Both fst ◦ π1 and snd ◦ π1 make the diagram commute, hence they are equal:
                              Y
                                  #(a = b) → a = b.
                                    a,b:f

One can check that this defines an inverse to ηa=b .
   Conversely, let E : Type, χ : E → Typen and f, g : E → F such that p : f ◦ π1 =
g ◦ πP
     1 . Using functional extensionality, we want to show that f x = g x for any x : E.
As e:E χ e is a dense n-subobject of E, #n (χ x) is inhabited. By hypothesis,
f x = g x is modal, thus by induction principle of #, we can suppose that we can
inhabit χ x with a term w. We can then apply the equality p to the dependent pair
(x; w) to have f x = g x, as required.
   A (n + 1)-sheaf is hence just a type satisfying the usual property of sheaves
(i.e. existence of uniqueness of arrow extension from dense (−1)-subobjects), with
the condition that all its path types are n-sheaves. This is a way to force the
compatibility of the modalities we are defining.
   One can check that the property IsSeparated (resp. IsSheaf) is HProp: given a
X : Typen+1 , there is at most one way for it to be separated (resp. a sheaf). In
particular, when one needs to prove equality between two sheaves, it suffices to show
the equality between the underlying types.
   As mentioned earlier, these definitions allow us to prove the fundamental property
that the type of all n-sheaves is itself a (n + 1)-sheaf .
  Proposition 5.7 (nType_j_Type_is_SnType_j_Type). Type#
                                                       n is a (n+1)-sheaf.

  Proof. We have two things to prove here: separation, and the sheaf property.
—Let E : Type and χ : E → Type, dense in E. Let φ1 , φ2 : E → Type#   n , such that
 φ1 ◦ π1 = φ2 ◦ π1 and let x : E. We show φ1 (x) = φ2 (x) using univalence.
 As χ is dense, we have a term mx : #n (χ x). ButP     as φ2 (x) is modal, we can
 obtain a term hx : χ x. As φ1 and φ2 are equal on e:E χ e, we have an arrow
 φ1 (x) → φ2 (x). The same method leads to an arrow φ2 (x) → φ1 (x), and one can
 prove that they are each other inverse.
                           #
—Now, we prove Pthat Typen is a# sheaf. Let E : Type and χ : E → HProp, dense
 in E. Let f : e:E χ e → Typen . We want to extend f into a map E → Type#        n.
 We define g as g(e) = #n (fibφ (e)), where
                                      X
                               φ:           (f b) → E
                                   P
                                            b:             χe
                                                     e:E

  defined by φ(x) = (x1 )1 . Using the following lemma, one can prove that the map
                                 χ
  f 7→ g defines an inverse of ΦE  .
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                       Lawvere-Tierney sheafification in Homotopy Type Theory           ·     149

     Lemma 5.8 (nj_fibers_compose). Let A, B, C : Typen , f : A → B and
  g : B → C. Then if all fibers of f and g are n-truncated, then
                                                                  
               Y                              X
                  (#n (fibg◦f (c))) ' #n           #n (fibf (w1 )) .
                  c:C                              w:fibg (c)

     Proof. This is just a modal counterpart of the property characterizing the
  fibers of composition of functions.
  Another fundamental property on sheaves we will need is that the type of (depen-
dent) functions is a sheaf as soon as its codomain is a sheaf.
  Proposition 5.9 (dep_prod_SnType_j_Type). If A Q      : Typen+1 and B : A →
Typen+1 such that for any a : A, (B a) is a sheaf, then a:A B a is a sheaf.
  Proof. Again, when proving equivalences, we will only define the maps. The
proofs of section and retraction are technical, not really interesting, and present in
the formalization.
—Separation:
 Q             Let E P: Type and χ : E → Typen dense in E. Let φ1 , φ2 : E →
   a:A  B a equal on    e:E χ e i.e. such that φ1 ◦ π1 = φ2P
                                                           ◦ π1 . Then for any a : A,
 (λx : E, φ1 (x, a)) and (λx : E, φ2 (x, a)) coincide on e:E (χ e), and as B a is
 separated, they coincide also on all E.
                                                             P             Q
—Sheaf: Let E : Type, χ : E → HProp dense in E and f : e:E χ e → a:A B a.
 Let a : A; the map (λx, f (x, a)) is valued in the sheaf B a, so it can be extended
 to all E, allowing f to be extended to all E.



5.2   Sheafification
The sheafification process will be defined in two steps. First one will build, from
any T : Typen+1 , a separated object n+1 T : Typen+1 ; one can then show that
n+1 defines a modality on Typen+1 . Second, one builds, from any separated type
T : Typen+1 , a sheaf #n+1 (T ); one can show that #n+1 is indeed the left-exact
modality we are searching.
  Let n be a fixed truncation index, and #n a left-exact modality on Typen ,
compatible with #−1 as in
 Condition 5.10. For any mere proposition P (where Pb is P seen as a Typen ),
#n Pb = #−1 P and the following coherence diagram commutes

                                       P
                                               ∼      / Pb

                                    η−1                     ηn
                                                       
                                     #−1 P
                                               ∼    / #n Pb




                                              Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
150     ·      K. Quirin and N. Tabareau

  5.2.1 From types to separated types. Let T : Typen+1 . We define n+1 T as the
image of #Tn ◦ {·}T , as in
                                                {·}T
                                         T             / (Typen )T ,

                                    µT                       #T
                                                            
                                                              n

                                       
                                                       / Type#
                                                                T
                                    n+1 T                    n

where {·}T is the singleton map λ(t : T ), λ(t0 : T ), t = t0 . n+1 T can be given
explicitly by
                             def
                   n+1 T = Im(λ t : T, λ t0 , #n (t = t0 ))
                             def      X          X
                              =                        (λt, #n (a = t)) = u .
                                   u:T →Type#
                                            n
                                                 a:A

This corresponds to the free separated object used in the topos-theoretic construction,
but using Type#n instead of the j-subobject classifier Ωj .

 Proposition 5.11 (separated_Type_is_separated). For any T : Typen+1 ,
n+1 T is separated.
  Proof. We use the following lemma:
  Lemma 5.12 (separated_mono_is_separated). A (n+1)-truncated type T with
an embedding f : T → U into a separated (n + 1)-truncated type U is itself separated.
                                                                         P
  Proof. Let E : Type and χ : E → Typen dense in E. Let φ1 , φ2 : e:E χ e → T
such that φ1 ◦ π1 ∼ φ2 ◦ π1 . Postcomposing
                                   P             by f yields an homotopy f ◦ φ1 ◦ π1 ∼
f ◦ φ2 ◦ π1 . As f ◦ φ1 , f ◦ φ2 : e:E χ e → U , and U is separated, we can deduce
f ◦ φ1 ∼ f ◦ φ2 . As f is an embedding, φ1 ∼ φ2 .
                                  T
As n+1 T embeds in Type#       n    , we only have to show that the latter is separated.
But this is the case because Type#     n is a sheaf (by Proposition 5.7) and a function
type is a sheaf as soon as its codomain is a sheaf (by Proposition 5.9).
   We will now show that n+1 defines a modality, with unit map µ. The left-
exactness of #n+1 will come from the second part of the process. The first thing
to show is that n+1 T is universal among separated types below T . In the topos-
theoretic sheafification, it comes easily from the fact that epimorphims are coequal-
izers of their kernel pairs. As it is not true anymore in our setting, we will use its
generalization, the proposition 2.7. Here is a sketch of the proof: as µT is a surjection
(it is defined by the surjection-embedding factorization), n+1 T is the colimit of
its iterated kernel pair. Hence, for any type Q defining a cocone on KP(µT ), there
is a unique arrow n+1 T → Q. What remains to show is that any separated type
Q defines a cocone on KP(µT ); we will actually show that any separated type Q
defines a cocone on k KP(µT )kn+1 , which is enough. We do it by defining another
diagram T̊ , equivalent to k KP(µT )kn+1 , for which it is easy to define a cocone into
any separated type Q.
   This comes from the following construction which connects n+1 T to the colimit
of the iterated kernel pair of µT .
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                        Lawvere-Tierney sheafification in Homotopy Type Theory                   ·     151

  Definition 5.13 (OTid). Let X : Type. Let T̊X be the higher inductive type
generated by
—t̊ : kXkn+1 → T̊X
—α̊ : ∀a b : kXkn+1 , # (a = b) → t̊(a) = t̊(b)
—α̊1 : ∀a : kXkn+1 , α̊(a, a, ηa=a 1) = 1
  We view T̊ as the coequalizer of

                                                                       // kXkn+1
                          X                                  π1
                                           #(a = b)
                                                             π2
                             a,b:kXkn+1

preserving ηa=a 1.
  We consider the diagram T̊ :

                 kXkn+1               / kT̊X kn+1             / kT̊ kn+1           / ···
                                                                   T̊X

  The main result we want about T̊ is the following:
 Lemma 5.14 (separation_colimit_OTtelescope). Let T : Typen+1 . Then
n+1 T is the (n + 1)-colimit of the diagram T̊ .
 The key point of the proof is that diagrams T̊ and k KP(µT )kn+1 are equivalent.
We will need the following lemma:
  Lemma 5.15 (OT_Omono_sep). Let A, S : Typen+1 , S separated, and f : A → S.
Then if
                             ∀a, b : A, f (a) = f (b) ' #(a = b),                                      (1)
then
                ∀a, b : k KPf kn+1 , |f˜|n+1 (a) = |f˜|n+1 (b) ' #(a = b).
  Proof (Sketch). By induction on truncation, we need to show that
              ∀a, b : KPf , f˜(|a|n+1 ) = f˜(|b|n+1 ) ' #(|a|n+1 = |b|n+1 ).
We use the encode-decode [UFP13, Section 8.9] method to characterize f˜(|a|n+1 ) = x,
and the result follows. We refer to the formalization for details.
  This lemma allows one to prove that, in the iterated kernel pair diagram of f
                X          / KP(f )             / KP(f1 )              / KP(f2 )     / ···
                                           f1
                                                  f2
                                                   %)  y
                                f                                 f3
                                                     S
if f satisfies (1), then each |fi |n+1 does.
  Remark 5.16. It is clear that if A and B are equivalent types, and for all a, b :
A, f (a) = f (b) ' #(a = b), then
                                                                       

      Coeq1 
                 X
                    fa = fb
                               π1
                                  // A  ' Coeq   X
                                                       #(a = b)
                                                                  π1
                                                                     // B 
                                      π2       1                                           π2
                a,b:A                                                    a,b:B

                                                       Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
152      ·     K. Quirin and N. Tabareau

   Proof of lemma 5.14. As said, it suffices to show that kC(µT )kn+1 = T̊ .

         k KP0 (µT )kn+1              / k KP1 (µT )kn+1               / k KP2 (µT )kn+1                  / ···


                   ∼




                                                     ∼




                                                                                      ∼
                                                                                    
                 T̊0                            / T̊1                             / T̊2                  / ···

The first equivalence is trivial, so let us begin with the second. What we need to
show is
                                      k KP(µT )kn+1 ' kT̊T kn+1 ,
i.e.
                                                                                                          

       Coeq1 
                 X
                         µT a = µT b
                                           π1
                                                 // T  ' Coeq           X
                                                                                   #(a = b)
                                                                                                    π1
                                                                                                         // T  .
                                           π2                 1                                     π2
                 a,b:T                                                    a,b:T


Q By the previous remark, it suffices to show that µT satisfies condition (1), i.e.
  a,b:T #n (a = b) = (µT a = µT b). By univalence, we want arrows in both directions,
forming an equivalence.
—Suppose
      Q     p : (µT a = µT b). Then projecting p along first components yields
 q : t:T #n (a = t) = #n (b = t). Taking for example t = b, we deduce #n (a =
 b) = #n (b = b), and the latter is inhabited by ηb=b 1.
—Suppose now p : #n (a = b). Let ι be the first projection from n+1 T →
              #
 Q → Typen ). ι is an embedding, thus it suffices to prove ι(µT a) = ι(µT b), i.e.
 (T
    t:T #n (a = t) = #n (b = t). The latter remains true by univalence.

As the fact that these two form an equivalence is rather technical, we refer to the
formalization for an explicit proof.
   Let us now show the other equivalences by induction. Suppose that, for a given
i : N, k KPi (µT )kn+1 ' T̊i . We want to prove k KPi+1 (µT )kn+1 ' T̊i+1 , i.e.
                                                                                         

                                                                       // KPi (µT ) 
                                       X                         π1
                       Coeq1                      fi a = fi b
                                                                                   
                                                                 π2
                                 a,b:KPi (µT )
                                                                                              n+1
                                                                                         

                  ' Coeq1 
                                        X
                                                     #(a = b)
                                                                 π1
                                                                          // kT̊ k    
                                                                                i n+1 
                                                                 π2
                                     a,b:kT̊i kn+1
                                                                                              n+1
                                 i
where fi is the map KP (µT ) → n+1 T . But lemma 5.15 just asserted that fi
satisfies (1), hence the previous yields the result.
  Next one would need to show that, modulo these equivalences, the arrows of
the two diagrams are equal. We leave that to the reader, who can refer to the
formalization if needed.
  Now, let Q be any separated Typen+1 , and f : X → Q. Then the following
diagram commutes
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                   Lawvere-Tierney sheafification in Homotopy Type Theory                                  ·   153



                kXkn+1                  / kT̊X kn+1                / kT̊ kn+1                      / ···
                                                                        T̊X



                                              %  x
                                               Q

  But we know (lemma 5.14) that n+1 T is the (n + 1)-colimit of the diagram T̊ ,
thus there is an universal arrow n+1 T → Q. This is enough to state the following
proposition.
   Proposition 5.17 (separation_reflective_subuniverse). (n+1 , µ) defines
a reflective subuniverse on Typen+1 .
   To show that n+1 is a modality, it remains to show that separation is a property
stable under sigma-types. Let A : Typen+1 be a separated type and       PB : A →
Typen+1 be a family of separated types. We want to show that               x:A B x is
separated. Let E be a type, and
                            P    χ : E  → Type
                                          P n     a dense subobject  of E.
   Let f, g be two maps from e:E χ e to x:A B x, equal when precomposed with
π1 .
                                                        f ◦π1
                                                                  // 9 x:A B x
                              P                                     P
                                    e:E      χe
                                                        g◦π1           9
                                                        f
                             dense
                                                            g
                                         
                                        E
We can restrict the previous diagram to
                                                        π1 ◦f ◦π1
                                                                           : // : A
                                        P
                                             e:E   χe
                                                        π1 ◦g◦π1
                                                        π1 ◦f
                                    dense
                                                                π1 ◦g
                                               
                                              E

     PA is separated, π1 ◦ f = π1 ◦ g. For the
and as                                      P second components, let x : E. Notice
that y:E x = y has a dense n-subobject, y:P χ e x = y1 :
                                                                        e:E


                                                            π2 ◦f ◦π1 ◦π1
                                                                                      6 // 6 B x
                    P P
                       y:           χe       x = y1
                              e:E                           π2 ◦g◦π1 ◦π1

                                                        π2 ◦f ◦π1
                            dense
                                                                π2 ◦g◦π1

                        P           
                             y:E        x=y

Using the separation property of B x, one can show that second components, correctly
transported along the first component’s equality, are themselves equal. The complete
proof can be found in the formalization. This proves the following proposition
                                                         Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
154     ·      K. Quirin and N. Tabareau

   Proposition 5.18 (separated_modality). (n+1 , µ) defines a truncated modal-
ity on Typen+1 .
  As this modality forms just one step in our construction, we do not need to show
that it is left exact. This we will do only for the sheafification modality.
  5.2.2 From Separated Type to Sheaf. For any T in Typen+1 , #n+1 T is defined
as the closure of n+1 T , seen as a subobject of T → Type#
                                                          n . #n+1 T can be given
explicitly by
                           def      X                   X
                 #n+1 T =                     #−1             (λt, #n (a = t)) = u .
                                 u:T →Type#
                                          n
                                                        a:T

  To prove that #n+1 T is a sheaf for any T : Typen+1 , we use the following lemma.

  Lemma 5.19 (closed_to_sheaf). Any closed (−1)-subobject of a sheaf is a
sheaf.
   Proof. Let U be a sheaf, and κ : U → HProp P      be a closed (−1)-subobject.
                                                                 P               Let
E : Type P and χ : E → HProp dense in E. Let φ : e:E χ e → u:U κ u. As π1 ◦ φ
is a map e:E χ e → U and U is Q    a sheaf, it can be extended into ψ : E →PU . As κ
is closed, it suffices now to prove e:E #n (κ (ψ e)) to obtain a map E → u:U κ u.
   Let e : E. As χ is dense, we have a term w : #n (χ e), and by #n -induction, a
term w                                                          e and by π2 ◦ φ, we
       e : χ e. Then, by the retraction property, ψ(e) = φ(e, w),
have hence our term of type κ(ψ e).
As T → Type#                                              #
            n is a sheaf, and #n+1 T is closed in T → Typen , #n+1 T is a sheaf.
We now prove that it forms a reflective subuniverse.
  Proposition 5.20 (sheafification_subu). (#n+1 , ν) defines a reflective sub-
universe.
   Proof. Let T, Q : Typen+1 such that Q is a sheaf. Let f : T → Q. Because Q is
a sheaf, it is in particular separated; thus we can extend f to n+1 f : n+1 T → Q.
   But as #n+1 T is the closure of n+1 T , n+1 T is dense into #n+1 T , so the sheaf
property of Q allows to extend n+1 f to #n+1 f : #n+1 T → Q.
   As all these steps are universal, so is the composition.
  The next step is the closure under dependent sums, specifically:
  Proposition 5.21 (sheafification_modality). (#n+1 , ν) defines a modality.
  Proof. The proof uses the same ideas as in subsection 5.2.1. Let A : Typen+1 a
sheafPand B : A → Typen+1 a sheaf family. By proposition 5.18, we already know
       P B a is separated.
that a:A           P       Let E be a type, and χ : E → HProp a densePsubobject.
Let f : e:E χ e → x:A B x ; we want to extend it into a map E → x:A B x.

                                   P
                                            χe
                                                    f
                                                         /P      Bx
                                      e:E                  8 x:A

                                        
                                       E
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                    Lawvere-Tierney sheafification in Homotopy Type Theory               ·     155

                                 P
   As A is a sheaf, and πQ1 ◦f :   e:E χ e → A, we can recover a map g1 : E → A.
We then want to show e:E B(g1 e). Let e : E. As χ is dense, we have a term
w : #n (χ e), and as B(g1 e) is a sheaf, we can recover a term w  e : χ e. Then
               e and π2 ◦ f gives the result.
g1 (e) = f (e, w),
  It remains to show that #n+1 is left exact and is compatible with #−1 . To do
that, we need to extend the notion of compatibility and show that, in fact, every
modality #n+1 is compatible with #n on lower homotopy types.
  Proposition 5.22. If T : Typen , then #n+1 Tb = #n T , where Tb is T seen as a
Typen+1 .
  Proof. We prove it by induction on n:
—For n = −1: Let T : HProp. Then

                      def      X               X
                #0 Tb =                  #−1         (λt, #−1 (a = t)) = u
                            u:T →Type#
                                     n
                                               a:T                             −1
                                                                             !
                              X                X
                      =                #−1           (λt, #−1 (a = t)) = u
                          u:T →Type#
                                   n
                                               a:T

  because the type inside the truncation is already in HProp. Now, let define
  φ : #−1 T → #0 T by
                                         φt = (λt0 , 1; κ)
 where κ is defined by #−1 -induction on t. Indeed, as T is an HProp, (a = t) ' 1.
 Let ψ : #0 T → #−1 T by obtaining the witness a : T (which is possible because
 we are trying to inhabit a modal proposition), and letting ψ(u; x) = ηT a. These
 two maps form an equivalence (the section and retraction are trivial because the
 equivalence is between mere propositions).
—Suppose now that #n+1 is compatible with all #k on lower homotopy types. Let
 #n+2 be as above, and let T : Typen+1 . Then, as #n+1 is compatible with #n ,
 and (a = t) is in Typen ,
                                X              X
                #n+2 Tb =                #−1    (λt, #n (a = t)) = u              .
                                     #         a:T
                            u:T →Typen+1                                     −1

  It remains to prove that for every (u, x) inhabiting the Σ-type above, u is in
  T → Type#  n , i.e. that for every t : T , Is-n-type(u t). But for any truncation index
  p, the type Is-p-type X : HProp is a sheaf as soon as X is, so we can get rid of #−1
  and of the truncation, which tells us that for every t : T , u t = #n (a = t) : Typen .


This proves in particular that #n+1 is compatible with #−1 in the sense of condi-
tion 5.10.
   The last step is the left-exactness of #n+1 . Let T be in Typen+1 such that #n+1 T
is contractible. Thanks to the just shown compatibility between #n+1 and #n for
Typen , left-exactness means that for any x, y : T , #n (x = y) is contractible.
                                               Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
156     ·      K. Quirin and N. Tabareau

  Using a proof by univalence as we have done for proving #n (a = b) ' (µT (a) =
µT (b)) in Proposition 5.14, we can show that:
   Proposition 5.23 (good_sheafification_unit_paths_are_nj_paths). For all
a, b : T , #n (a = b) ' (νT a = νT b).
  As #n+1 T is contractible, path spaces of #n+1 T are contractible, in particular
(νT a = νT b), which proves left exactness.
5.3   Summary
Starting from any left-exact modality #−1 on HProp, we have defined for any
truncation level n, a new left-exact modality #n on Typen , which corresponds to
#−1 when restricted to HProp.
  When #−1 is consistent (in the sense of section 3.2), #n 0 = #−1 0 is also not
inhabited, hence #n is consistent. In particular, the modality induced by the double
negation modality on HProp is consistent.
  In topos theory, the topos of Lawvere-Tierney sheaves for the double negation
topology is a boolean topos. In homotopy type theory, this result can be expressed
as:
   Proposition 5.24. Taking (#¬¬ )n , the modality obtained by sheafification of
the double negation modality, the following holds
                                Y
                                       #¬¬ (P + ¬P ).
                                    P :HProp

                                               def
  Proof. Let P : HProp, and pose Q = P + ¬P . Then, as P and ¬P are disjoint
h-propositions, P + ¬P is itself a h-proposition [BGL+ 17, ishprop_sum]. Thus,
#¬¬ Q ' ¬¬Q, and the latter is inhabited by the usual
                             λ (x : ¬Q), x(inr(λ y : P, x(inl y))).


5.4   Extension to Type
In the previous section, we have defined a (countably) infinite family of modalities
Typei → Typei . One can extend them to whole Type by composing with truncation:
                                                                      def
  Lemma 5.25. Let #i : Typei → Typei be a modality. Then # = #i ◦ k · ki :
Type → Type is a modality in the sense of section 3
  Proof. It is straightforward to check each property of a modality.
If #−1 is the double negation modality on HProp and i = −1, # is exactly the
double negation modality on Type described in 3.1.3. Choosing i > 0 is a refinement
of this double negation modality on Type: it will collapse every type to a Typei ,
instead of an HProp.
   Obviously, as truncation modalities are not left-exact [UFP13, Exercise 7.11], #
isn’t either. But in the following sense, when restricted to i-truncated types, it is:
  Lemma 5.26. Let A : Typei . Then if #(A) is contractible, for any x, y : A,
#(x = y) is contractible.
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                     Lawvere-Tierney sheafification in Homotopy Type Theory           ·     157

     Proof. For i-truncated types, # = #i , and #i is left-exact.
   The compatibility between the modalities #n and between the modalities k · kn
allows us to take the truncation index as high as desired. Taking it as a non-fixed
parameter allows one to work in a universe where the new principle (e.g. mere
excluded middle) is true for any explicit truncated type. Indeed, i can be chosen
dynamically along a proof, and thus be increased as much as needed, without
changing results for lower truncated types.
   Furthermore, univalence remains true in this new type theory in the following
sense:
   Proposition 5.27. Let n be a given truncation index, and # the modality asso-
ciated to n as defined in lemma 5.25. Then, for any type A, B : Type#
                                                                    n , if ϕ is the
canonical arrow
                                      A = B → A ' B,
then IsEquiv(ϕ) is modal.
   Proof. The first thing to notice is that, if X and Y are modal, and f : X → Y ,
then the mere proposition IsEquiv f is also modal. Therefore, it suffices to show
that both A = B andPA ' B are modal. By proposition 3.4, A = B is modal.
Moreover, (A ' B) ' f :A→B IsEquiv f . Therefore, as A and B are modal, A ' B
is too.
   Hence, IsEquiv ϕ is modal.

6.    FORMALIZATION
A Coq formalization of the sheafification process based on the Coq/HoTT li-
brary [BGL+ 17] is available at https://github.com/KevinQuirin/sheafification.
   After reviewing the content and some statistics about the formalization in Sec-
tion 6.1, we present the limitations of our formalization in Section 6.2, in particular
the issues relative to universe polymorphism.
6.1    Content of the formalization
We provide a more detailed insight of the structure of our formalization:
—Colimits and iterated kernel pairs are formalized in Limit, T.v, OT.vv OT_Tf.v,
 T_telescope.v, Tf_Omono_sep.v.
—Reflective subuniverses and modalities are formalized in
 reflective_subuniverse.v, modalities.v.
—The definition of the dense topology as a left exact modality on HProp is given
 in sheaf_base_case.v.
—Section 5.1 is formalized in sheaf_def_and_thm.v.
—Section 5.2 is formalized in sheaf_induction.v.
  Overall, the project contains 8000 lines. This, however, could be reduced a bit by
improving the way Coq tries to rewrite and apply lemmas automatically. The coqwc
tool counts 1600 lines of specifications (definitions, lemmas, theorems, propositions)
and 5500 lines of proof script. This constitutes a significant amount of work but the
part dedicated to sheaves and sheafification is only 2200 lines of proof script, which
                                            Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
158     ·      K. Quirin and N. Tabareau

seems quite reasonable and encouraging. Moreover it suggests that homotopy type
theory provides a convenient tool in which to formalize some parts of the theory of
higher toposes.

6.2   Limitations of the formalization
In the formalization, we we forced to use the type-in-type option to handle the
universe issues we faced. However, a lot of the code compiles without this flag (but
still needs universe polymorphism).
   Universes are used in type theory to ensure consistency by checking that definitions
are well-stratified according to a certain hierarchy. Universe polymorphism [ST14]
supports generic definitions over universes, reusable at different levels. Although
the presence of universe polymorphism is mandatory for our formalization, its
implementation is still too rigid to allow a complete formalization of our work for
the following reasons.
   While Coq handles cumulativity on Type natively, this is not the case for the
Σ-type Typen , which requires propositional resizing. This issue could be solved by
adding an axiom of cumulativity for Typen with an explicit management of universes.
However, as it would not have any computational content, such a solution would
needlessly complicate the proofs. Indeed, the axiom would then appear everywhere
cumulativity is needed and one would need explicit annotations for universe levels
throughout the formalization.
   One issue with universe polymorphism lies in the management of recursive defini-
tions. Indeed, the following recursive definition of sheafification

                 # : ∀ (n : nat), Typen → Typen
                             def
                 #−1 (T ) = ¬¬T
                           def X     X
                 #n+1 (T ) =     #−1   u = (λt, #n (a = t))
                                   u:T →Type#
                                            n
                                                   a:T

is not allowed. This is because Coq forces the universe of the first Typen occurring
in the definition to be the same for every n, whereas the universe of the first
Typen+1 occurring in #n+1 should be at least one level higher as the one of Typen
occurring in #n because of the use of Σ-type over T → Type#         n and equality on
the return type of #n . Thus, the induction step presented in this paper has been
formalized, but the complete recursive sheafification can not be defined for the
moment. Note that the same increase in the universe levels occurs in the Rezk
completion of categories [AKS15]. In the definition of the completion, one uses the
Yoneda embedding and representable functors, which is similar in spirit to our use
of characteristic functions.
   This restriction in our formalization may be solved by generalizing the management
of universe polymorphism for recursive definitions or by the use of more general
“resizing axioms” which are still under discussion in the community.

7.    CONCLUSION AND FUTURE WORKS
In this paper, we have demonstrated a way to extend Lawvere-Tierney sheafification
to truncated types in homotopy type theory.
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                    Lawvere-Tierney sheafification in Homotopy Type Theory          ·     159

   Above and beyond this individual result, our work is part of a larger program
which aims to illustrate that homotopy type theory is a promising candidate for the
formalization of mathematics inside a proof assistant.
   In future work, we would like to improve this construction in three ways. (i)
The extension to whole Type in lemma 5.25 is not totally satisfactory, as every
type is collapsed to a truncated one. But some types in homotopy type theory
are not truncated [UFP13, Example 8.8.6]. (ii) We would like to have more ex-
amples of left-exact modalities on HProp, in order to have sheaves for different
properties than excluded middle. (iii) In topos theory, Lawvere-Tierney subsumes
Grothendieck [MM92, Section V.4] in the sense that any Grothendieck topology
gives rise to a Lawvere-Tierney topology with the same notion of sheaves. Higher
Lawvere-Tierney sheaves are presented here, and higher Grothendieck sheaves have
been defined in [Lur09]. It should be interesting to check if the subsumption remains
true in higher topos theory.
   Moreover, we highly suspect that modalities (at least, left-exact accessible modal-
ities) induces new type theories, as Grothendieck sheaves exhibits some (∞, 1)-
subtoposes. It would be nice to give a better sense to sub-type theories and to
instantiate them with sheafification, giving, for example, a model of homotopy type
theory with computational mere excluded middle.

ACKNOWLEDGMENTS
We would like to thank all maintainers of the Coq/HoTT library, who have provided
a very solid base for our formalization. We also would like to thank Bas Spitters for
helpful discussions on the subject. This work has been funded by the CoqHoTT
ERC Grant 637339.

References
[AKL15]   Jeremy Avigad, Krzysztof Kapulkin, and Peter LeFanu Lumsdaine. Ho-
          motopy limits in type theory. Mathematical Structures in Computer
          Science, January 2015.
[AKS15] Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univa-
          lent Categories and the Rezk completion. Mathematical Structures in
          Computer Science, January 2015.
[BBC98] Stefano Berardi, Marc Bezem, and Thierry Coquand. On the computa-
          tional content of the axiom of choice. Journal of Symbolic Logic, pages
          600–622, 1998.
[BGL+ 17] Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman,
          Matthieu Sozeau, and Bas Spitters. The HoTT Library: A formalization
          of homotopy type theory in Coq. In Certified Programs and Proofs
          (CPP), 6th ACM SIGPLAN Conference on, 2017.
[Bou16]   Simon Boulier.        Colimits in HoTT.          Blog post, http://
          homotopytypetheory.org/2016/01/08/colimits-in-hott/, 2016.
[BU02]    Gilles Barthe and Tarmo Uustalu. CPS translating inductive and coin-
          ductive types. ACM SIGPLAN Notices, 37(3):131–142, 2002.
[CDT15] The Coq Development Team. The Coq proof assistant reference manual.
          2015. Version 8.5.
                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
160     ·      K. Quirin and N. Tabareau

[Coh66]   Paul Cohen. Set theory and the continuum hypothesis. WA Benjamin
          New York, 1966.
[Göd38] Kurt Gödel. The consistency of the axiom of choice and of the generalized
          continuum-hypothesis. Proceedings of the National Academy of Sciences,
          24(12):556–557, 1938.
[Gö40]    Kurt Gödel. The Consistency of the Axiom of Choice and of the Gener-
          alized Continuum Hypothesis with the Axioms of Set Theory. Princeton
          University Press, 1940.
[Her12]   Hugo Herbelin. A constructive proof of dependent choice, compatible
          with classical logic. In Proceedings of the 2012 27th Annual IEEE/ACM
          Symposium on Logic in Computer Science, pages 365–374. IEEE Com-
          puter Society, 2012.
[JLP+ 16] Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu
          Sozeau, and Nicolas Tabareau. The Definitional Side of the Forcing. In
          LICS, New York, United States, May 2016.
[JTS12] Guilhem Jaber, Nicolas Tabareau, and Matthieu Sozeau. Extending type
          theory with forcing. In Logic in Computer Science (LICS), 27th Annual
          IEEE Symposium on, pages 395–404. IEEE, 2012.
[KL12]    Krzysztof Kapulkin and Lumsdaine Peter LeFanu. The simplicial model
          of univalent foundations. arXiv preprint arXiv:1211.2851, 2012.
[Kri03]   Jean-Louis Krivine. Dependent choice,‘quote’and the clock. Theoretical
          Computer Science, 308(1):259–276, 2003.
[LS13]    Peter LeFanu Lumsdaine and Michael Shulman. Higher inductive types.
          preparation, 2013.
[Lur09]   Jacob Lurie. Higher topos theory. Annals of mathematics studies. Prince-
          ton University Press, Princeton, N.J., Oxford, 2009.
[MM92] Saunders MacLane and Ieke Moerdijk. Sheaves in Geometry and Logic.
          Springer-Verlag, 1992.
[MV99]    Fabien Morel and Vladimir Voevodsky. A1 -homotopy theory of schemes.
          Publications Mathématiques de l’IHÉS, 90:45–143, 1999.
[Par93]   Michel Parigot. Classical proofs as programs. In Computational logic
          and proof theory, pages 263–276. Springer, 1993.
[RS15]    Egbert Rijke and Bas Spitters. Sets in homotopy type theory. Mathe-
          matical Structures in Computer Science, 25(5):1172–1202, 2015.
[Shu]     Mike Shulman.          Module for Modalities.       Blog post, http://
          homotopytypetheory.org/2015/07/05/modules-for-modalities/.
[Shu15a] Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homo-
          topy type theory. arXiv preprint arXiv:1509.07584, 2015.
[Shu15b] Michael Shulman. Univalence for inverse diagrams and homotopy canon-
          icity. arXiv preprint arXiv:1203.3253, 2015.
[SS14]    Urs Schreiber and Michael Shulman. Quantum gauge field theory in
          cohesive homotopy type theory. In Ross Duncan and Prakash Panan-
          gaden, editors, Proceedings 9th Workshop on Quantum Physics and


Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                   Lawvere-Tierney sheafification in Homotopy Type Theory          ·     161

           Logic, Brussels, Belgium, 10-12 October 2012, volume 158 of Electronic
           Proceedings in Theoretical Computer Science, pages 109–126, 2014.
[ST14]     Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in Coq.
           In Interactive Theorem Proving, 2014.
[Tie72a]   Myles Tierney. Sheaf theory and the continuum hypothesis. Springer,
           1972.
[Tie72b]   Myles Tierney. Sheaf theory and the continuum hypothesis. LNM 274,
           pages 13–42, 1972.
[UFP13]    The Univalent Foundations Program. Homotopy Type Theory: Univalent
           Foundations of Mathematics. http://homotopytypetheory.org/book,
           IAS, 2013.
[Voe]      Vladimir Voevodsky. Resising Rules - their use and semantic justifica-
           tion. www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_
           files/2011_Bergen.pdf.




                                         Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
