Kevin Quirin

Lawvere-Tierney sheafification in Homotopy Type Theory

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 mismatch 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.

INTRODUCTION

Sheafification [START_REF] Maclane | Sheaves in Geometry and Logic[END_REF] is a very powerful geometric construction that has been initially stated in topology and has quickly been lifted to mathematical logic. In topos theory, sheafification can be seen as a way to transform a topos into another one. It is used, for example, to build, from any topos T , a boolean topos (i.e. satisfying the excluded middle property) satisfying the axiom of choice and negating the continuum hypothesis [MM92, Theorem VI.2.1]. This is actually an adaptation of a slightly older method, in set theory, to change a model M of ZFC into a model M[G] of ZFC, satisfying other principles, called forcing. Its most famous application is the proof of consistency of ZFC with the negation of the continuum hypothesis, by Paul Cohen [START_REF] Cohen | Set theory and the continuum hypothesis[END_REF], answering (neither negatively nor positively) the first Hilbert's problem. Indeed, Gödel proved in 1938 the consistency of ZFC with continuum hypothesis [START_REF] Gödel | The consistency of the axiom of choice and of the generalized continuum-hypothesis[END_REF] using the constructible model L. The global The bottom of the article's title page contains acknowledgment of support, the author(s) address(es), a "permission to copy" statement, and a line containing a copyright symbol ( c ) and a mysterious number. This is all entered with a bottomstuff environment; there must be no blank line after the \begin{bottomstuff} command. The permission to copy statement is produced by the \permission command. Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee. c 2008 Journal of Formal Reasoning idea of this technique 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. Then, the compactness theorem allows to prove the consistency of ZFC with all approximations, i.e. with a witness of ¬CH.

Then, forcing has been adapted to the setting of topos theory by Myles Tierney [START_REF] Tierney | Sheaf theory and the continuum hypothesis[END_REF], through 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. 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 chose to treat, the topos Sh(T ) satisfies 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 be quite close to topos theory so one could wonder why similar techniques have not been developed in the field of type theory. The answer to this question has been given recently by the advent of homotopy type theory [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF], which is 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 [START_REF] Kapulkin | The simplicial model of univalent foundations[END_REF], which says that for any types T and U , the canonical map (T = U ) → (T U ) which transports equalities to equivalences is an equivalence. This new point of view on type theory has revealed the homotopy structure of types where for instance mere propositions (or Type -1 ) are just types with an irrelevant equality and sets (or Type 0 ) are types with a propositional equality and so on for Type n . The development of univalence has also shed some light on the difficulty to make 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 [START_REF] Lurie | Higher topos theory[END_REF]. Even if the connection between homotopy type theory and higher topos theory has not been made precise yet, it is commonly believed that the former constitutes an internal language for the latter (see [START_REF] Shulman | Univalence for inverse diagrams and homotopy canonicity[END_REF] for a more detail discussion on this topic).

Lurie has presented all the tools that have been defined in topos theory, but in a higher setting. In particular, the theory of sheaves has been lifted to higher topos theory. As the notion of higher toposes 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 homotopy type theory is not straightforward because the construction in higher toposes

• TBD is restricted to the initial Grothendieck setting which is still very topologically oriented, and not very amenable to formalization in type theory. It seems more promising to use a synthetic notion of sheafification, called Lawvere-Tierney sheafification [START_REF] Tierney | Sheaf theory and the continuum hypothesis[END_REF][START_REF] Maclane | Sheaves in Geometry and Logic[END_REF], 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) 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 were, to our knowledge, not considered in the higher setting, the contribution of this article is twofold: (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 [START_REF] Coq | The Coq proof assistant reference manual[END_REF].

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 around the Curry-Howard isomorphism, to extend a programming language close to type theory with new logical or computational principle while keeping consistency automatically. For instance, much efforts have been done to provide a computational content to the law of excluded middle in order to define a constructive version of classical logic. This has lead to various calculi, with most notably the λµ-calculus of Parigot [START_REF] Parigot | Classical proofs as programs[END_REF], but this line of work has not appeared to be fruitful to define a new version of type theory with classical principles. Other works have tried to extend continuation-passing-style (CPS) transformation to type theory, but they have been faced with the difficulty that the CPS transformation is incompatible with (full) dependent sums [START_REF] Barthe | CPS translating inductive and coinductive types[END_REF], which puts emphasis on 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 [START_REF] Krivine | Dependent choice,'quote'and the clock[END_REF] and even more recently with restriction on elimination of dependent sums and lazy evaluation [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]. 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 principle. 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 to go from the presheaf construction to the sheaf construction.

PRELIMINARIES ON HOMOTOPY TYPE THEORY

In this section, we review some basic definitions in homotopy type theory that are central in our formalization but not specific to sheafification. The definitions of Section 2.1 are part, or direct applications of [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF], while other definitions and theorems 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 [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF]. Nevertheless, we recall most of the central definitions that we use so that the paper is sufficiently self-contained. Given a type T and 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 theory whenever it is possible, to ease the reading without making our statements imprecise. In particular, (higher) inductive types are defined using itemization to avoid an overhead of notation. In the rest of the paper, Type must be seen in an universe-polymorphic way.

Section 2.1 will present homotopy levels and object classifiers, section 2.2 introduces a theory of colimits in homotopy type theory, illustrated by an important example in section 2.3.

Homotopy Types and Classifying Objects

One of the most direct application 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.

-Is-(n + 1)-type X def = x,y:X Is-n-type(x = y).

Then, Type n def = 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 T n : Type n can be constructed as the HIT generated by y:B fib f (y) as a surjection followed by an embedding. Following [START_REF] Rijke | Sets in homotopy type theory[END_REF], it is possible to show that, for any homotopy level n and any type B, Type n classifies subobjects of B with n-truncated homotopy fibers in the sense that there is an equivalence χ :

A:Type f :A→B b∈B Is-n-type fib f (b) ∼ -→ (B → Type n )
such that the usual subobject classifier diagram ([UFP13, Theorem 4.8.4]) is a pullback. 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 fib f (b), either as a map B → Type n .

Colimits in Homotopy Type Theory

One desired property we would like to consider concerns the colimits of Čech nerves (Section 2.3). This section presents a definition of colimits in a type theoretic setting. Following the definition of graphs and diagrams defined in [START_REF] Avigad | Homotopy limits in type theory[END_REF], we recall the definition of colimits of diagrams overs graphs presented in [START_REF] Rijke | Sets in homotopy type theory[END_REF].

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 -a map q i : D 0 (i) → P for any vertex i : G 0 , i.e. q : i:G0 D 0 (i) → P -for any vertices i, j : G 0 and all edges φ : G 1 (i, j), a path p φ i,j :

q j • D 1 (φ) = q i , i.e. p : i,j:G0 φ:G1(i,j) q j • D 1 (φ) = q i .
Then P is the colimit of D if for any other X : Type, IsEquiv λf : P → X, λi, f • q i ; λ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. The proof of this is really straightforward: a cocone over D into P can be changed equivalently into a cocone over D m into P m , using the elimination principle of truncations, and then we can show that the following diagram commutes for any

X : Type m P m → X / / ∼ cocone( D m , X) P → X ∼ / / cocone(D, X) ∼ O O

On Giraud-Rezk-Lurie axioms

The Giraud-Rezk-Lurie axioms are the ∞-version of Giraud's axioms that characterize a topos. Namely, there are four axioms on a (∞, 1)-category that have been shown to be equivalent to (∞, 1)-topos axioms [START_REF] Lurie | Higher topos theory[END_REF]Chapter 6]. The consequence we want to use here is the fact that a surjection (i.e. (-1)-connected function) is the colimit of its Čech nerve. In [START_REF] Bauer | The HoTT Library: A formalization of homotopy type theory in Coq[END_REF], 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 T f of the kernel pair of f is the higher inductive type given by -t :

X → T f -α : ∀a b : X, f (a) = f (b) → t(a) = t(b) -α 1 : ∀a : X, α(a, a, 1) = 1 We view T f as the coequalizer of a,b:X f (a) = f (b) / / π1 π2
/ / X preserving the identity. We call f the map T f → 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 is given by the diagram C(f

) := X t / / T f t / / T f / / • • •
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 .
• TBD

MODALITIES

This section presents modalities in Homotopy Type Theory as defined in [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF] and later developed in [START_REF] Schreiber | Quantum gauge field theory in cohesive homotopy type theory[END_REF][START_REF] Shulman | Brouwer's fixed-point theorem in real-cohesive homotopy type theory[END_REF]. 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 on 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 → f • η A
is an equivalence. (5) for any A : Type and B : A → Type such that P (A) and x:A P (Bx), then 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) will be denoted 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

f def = 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 ).

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. •(R)
Type is closed under dependent products, i.e. x:A B x is modal as soon as 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 -• η A : z: A B z -→ a:A B(η A a) f -→ 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 (fib f (y)) → fib f (η B y)
• TBD is an equivalence, and the following diagram commutes

fib f (y) η / / γ (fib f (y))
w w fib f (η B y) Remark 3.5. Again, the inverse of -• η A will be denoted ind : a:A B(η A a) → z: A B x, and its computation rule β ind : f : -Again, it suffice to show that η x=y is an equivalence. We begin by showing that

a:A B(η A a) x:A ind (f )(η A x) = f x 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,
(λ _ : (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 modal by induction 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

x,y:A Is-n-type x = y.
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 f x = y → x: X f x = η Y y,
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 , (fib f (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) fib s (y; p -1 ) for

s : fib η X (x) -→ fib η Y ( f x) (a, q) -→ (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 (fib f (b)) for any b : B.
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, (fib s (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.

A:Type x,y:A

IsEquiv( (ap η A ))

where

(ap η A ) : (x = y) → η A x = η A y.
Proof. We will rather prove something slightly more general, using an encodedecode proof [UFP13, Section 8.9]; we will characterize, for a type A and a fixed inhabitant x : A the type 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 = η 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.
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

x,y: T

x = y

For any x : 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

x,y:T

η T x = η T y.
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.

P :HProp

IsHProp( P ).

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 Type p are closed under the reflector , i.e. P :Type p Is-p-type( P ).

Examples of modalities

3.1.1 The identity modality. Let us begin with the most simple modality one can imagine: the one doing nothing. We can define it by letting A def = A for any type A, and η A def = 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. It remains to check that for any x : ¬¬ x:A B x, B(κ x).

But the previous map can be easily 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.

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 consistent a modality such that 0 is empty.

• TBD 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 = 1, that is when there is no proof of 0.

In topos theory, Lawvere-Tierney topologies give rise to subtoposes Sh j 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].

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 Type n . 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 : Type n → HProp (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 → f • η A
is an equivalence. (5) for any A : Type n and B : A → Type n such that P (A) and x:A P (Bx), then P ( x:A B(x)) (6) for any A : Type n 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.

Formalization

Let us discuss here about the formalization of the theory of modalities. General modalities are formalized in the Coq/HoTT library [BGL + 17], thanks to a huge work of Mike Shulman [Shu]. The formalization might seem to be straightforward, but the universe levels (at least, their automatic handling by Coq) are here a great 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 : Type i → Type i ; 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 : Type i → Type k , i k; it maps any universe to a possibly higher one. Other components of the modality will have types

P : Type i → HProp k , i k η : A:Type i A : Type k , i k -: A:Type i B:Type j h:P (B) IsEquiv(-• η A ), i, j k
Fortunately, this change is small enough to preserve usual properties of modalities. Of course, the examples of modalities mapping any universe to itself are still an example of generalized modality, it just does not use the possibility to inhabit a higher universe.

We would like to have the same generalization for truncated modalities. But there are a lot of new universe levels appearing, mostly because in Type n = T :Type Is-n-type T , Is-n-type come with its own universes. Hence, handling "by hand" so many universes together with their constraints quickly go 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 generalized modalities.

In our formalization, we decided to work with the type-in-type Coq option, to avoid any issue with universes.

SHEAVES IN TOPOSES

In this section, we will rather 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 to speak about locally true things instead of true things. Definition 4.1 (Lawvere-Tierney topology [START_REF] Maclane | Sheaves in Geometry and Logic[END_REF]). 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 Theorem 4.2 ([MM92, Theorem V.1.2]). Every Grothendieck topology J on a small category C determines a Lawvere-Tierney topology j on the presheaf topos Sets C op .

Any Lawvere-Tierney topology j on E induces a closure operator A → 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 . • TBD A subobject A of E is said to be dense when A = E.
Then, 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 as 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 Hom E (E, F ) → Hom E (A, F ) is an isomorphism.

One can show that Sh E , 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 a j to the inclusion E → Sh E , exhibiting Sh E as a reflective subcategory of E. In particular, that implies that logical principles valid in E are still valid in Sh E .

For any object E of E, a j (E) is defined as in the following diagram

E {•} E / / θ E Ω E j E E / / closure ! ! Ω E j a j (E) < <
The proof that a j defines a left adjoint to the inclusion can be found in [START_REF] Maclane | Sheaves in Geometry and Logic[END_REF].

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 proof of the construction by Paul Cohen of a model of ZFC negating the continuum hypothesis [START_REF] Cohen | Set theory and the continuum hypothesis[END_REF]. Together with the model of constructible sets L by Kurt Gödel [START_REF] Gödel | The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory[END_REF], it proves that CH is independent of ZFC, solving first Hilbert's problem.

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 extensively use this idea, applying it to every subobject classifier Type n we described in section 2. The subobject classifier Ω of a topos is seen as the truth values of the topos, which corresponds to the type HProp in our setting; the topos is considered proof irrelevant, corresponding to our HSet. Sheafification in toposes is thus a way, when translated to the setting of homotopy type theory, 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 by applying it to the subobject classifier HSet equipped with a left-exact modality, to build a new left-exact modality on Type 1 , 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]. Even worse, some types are not even the limit of its successive truncations, even in an hypercomplete setting [START_REF] Morel | A 1 -homotopy theory of schemes[END_REF]. It suggests that defining a sheafification functor for all truncated types won't give (at least easily) a sheafification functor on whole Type. Another issue that can be pointed is the complexity of proofs. If, in a topos-theoretic setting, everything is proof-irrelevant, it won't be the case for higher settings, forcing us to prove results that were previously true on the nose. This will oblige us to write long and technical proofs of coherence, and more deeply, to modify completely some lemmas, such as Proposition [MM92, Theorem IV.7.8], stating that epimorphisms are coequalizers of their kernel pair.

The main idea is thus to follow as closely as possible the topos-theoretic construction, and change it as few times as possible to make it work in our higher setting.

Note that the principles we want to add are added 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 Type n , as in the following theorem.

Theorem 5.1. The sequence defined by induction by

: ∀ (n : nat), Type n → Type n -1 (T ) given n+1 (T ) def = u:T →Type n -1 a:T u = (λt, 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 : Type n , where P is P seen as an inhabitant of Type n+1 .

P ∼ / / ηn P ηn+1 n P ∼ / / n+1 P
In what follows, formalized results are indicated by the name of the result in the library in this special font.

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 to give the "good" definition is the choice of the subobject classifier in which dense subobjects will be chosen: two choices appear, HProp and Type n ; we will actually use both. What guided our choice is the crucial property that the type of all n-sheaves has to 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, short), classified by χ : E → Type n , 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
Topos-theoretic sheaves are characterized by a property of existence and uniqueness, 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

Φ χ E : E → F -→ e:E χe → F f -→ f • π 1 .
Here, we need to distinguish between dense (-1)-subobjects, that will be used in the definition of sheaves, and dense n-subobjects, that will be used in the definition of separated types. Definition 5.4 (Separated Type (separated)). A type F in Type n+1 is separated if for any type E, and all dense n-subobject of E classified by χ, Φ χ E is an embedding.

With topos theory point of view, it means that given a map e:E χ e → F , if there is an extension f : E → F , then it is unique, as in

e:E χe f / / π1 F E ! ; ;
Definition 5.5 (Sheaf (Snsheaf_struct)). A type F of Type n+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.

In topos-theoretic words, it means that given a map f : e:E χ e → F , one can extend it uniquely to f : E → F , as in

e:E χe f / / π1 F E ∃! ; ;
Note that these definitions are almost the same as the ones in [START_REF] Maclane | Sheaves in Geometry and Logic[END_REF]. 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 Type n+1 is separated if, and only if all its path types are n-modal.

Proof. Let F : Type n+1 a separated type, and a, b : F . We want to find an inverse to η a=b . We consider the following diagram One can check that this defines an inverse to η a=b . Conversely, let E : Type, χ : E → Type n and f, g : E → F such that p : f • π 1 = g • π 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. It 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 : Type n+1 , there is at most one way for it to be separated (resp. a sheaf). In particular, when needed to prove equality between two sheaves, it suffices to show the equality between the underlying types.

As said 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 sheafness.

• TBD -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 m x : n (χ x). But as φ 2 (x) is modal, we can obtain a term h x : χ 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 that Type n is a sheaf. Let E : Type and χ : E → HProp, dense in E. Let f : e:E χ e → Type n . We want to extend f into a map E → Type n . We define g as g(e) = n (fib φ (e)), where φ :

b:

e:E χ e (f b) → E
defined by φ(x) = (x 1 ) 1 . Using the following lemma, one can prove that the map f → g defines an inverse of Φ χ E . Lemma 5.8 (nj_fibers_compose). Let A, B, C : Type n , f : A → B and g : B → C. Then if all fibers of f and g are n-truncated, then

c:C ( n (fib g•f (c))) n   w:fibg(c) n (fib f (w 1 ))   .
Proof. This is just a modal counterpart of the property characterizing fibers of composition of function.

Another fundamental property on sheaves we will need is that the type of (dependent) functions is a sheaf as soon as its codomain is a sheaf. Proposition 5.9 (dep_prod_SnType_j_Type). If A : Type n+1 and B : A → Type n+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: Let E : Type and χ : E → Type n dense in E. Let φ 1 , φ 2 : E → a:A B a equal on e:E χ e i.e. such that φ 1 • π 1 = φ 2 • π 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.

-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.

Sheafification

The sheafification process will be defined in two steps. The first one will build, from any T : Type n+1 , a separated object n+1 T : Type n+1 ; one can show that n+1 defines a modality on Type n+1 . The second step will build, from any separated type T : Type n+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 Type n , compatible with -1 as in Condition 5.10. For any mere proposition P (where P is P seen as a Type n ), n P = -1 P and the following coherence diagram commutes

P ∼ / / η-1 P ηn -1 P ∼ / / n P 5.
2.1 From types to separated types. Let T : Type n+1 . We define n+1 T as the image of T n • {•} T , as in

T {•} T / / µ T (Type n ) T T n n+1 T / / Type n T ,
where {•} T is the singleton map λ(t : T ), λ(t : T ), t = t . n+1 T can be given explicitly by

n+1 T def = Im(λ t : T, λ t , n (t = t )) def = u:T →Type n a:A (λt, n (a = t)) = u .
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 : Type n+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.

Proof. Let E : Type and χ :

E → Type n dense in E. Let φ 1 , φ 2 : e:E χ e → T such that φ 1 • π 1 ∼ φ 2 • π 1 . Postcomposing 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 .
As n+1 T embeds in Type n T , we only have to show that the latter is separated.

But it 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 leftexactness of n+1 will come from the second part of the process. The first thing This lemma allows to prove that, in the iterated kernel pair diagram of f

X / / f ) ) KP(f ) / / f1 % % KP(f 1 ) / / f2 KP(f 2 ) / / f3 y y • • • S if f satisfies (
A, f (a) = f (b) (a = b), then Coeq 1   a,b:A f a = f b π2 / / π1 / / A   Coeq 1   a,b:B (a = b) π2 / / π1 / / B  
Proof of lemma 5.14. As said, it suffices to show that C(µ T ) n+1 = T .

KP 0 (µ T ) n+1 / / ∼ KP 1 (µ T ) n+1 / / ∼ KP 2 (µ T ) n+1 / / ∼ • • • T0 / / T1 / / T2 / / • • •
The first equivalence is trivial. Let's then start with the second. What we need to show is The latter remains true by univalence. The fact that these two form an equivalence is technical, we refer to the formalization for an explicit proof.

KP(µ T ) n+1 TT n+1 , i.e.
Let's show the other equivalences by induction. Suppose that, for a given i : N, KP i (µ T ) n+1 Ti . We want to prove KP i+1 (µ T ) n+1 Ti+1 , i.e.

• TBD

Coeq 1    a,b:KP i (µ T ) f i a = f i b π2 / / π1 / / KP i (µ T )    n+1 Coeq 1    a,b: Ti n+1 (a = b) π2 / / π1 / / Ti n+1    n+1
where f i is the map KP i (µ T ) → n+1 T . But lemma 5.15 just asserted that f i satisfies (1), hence the previous nota yields the result.

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 Type n+1 , and f : X → Q. Then the following diagram commutes

X n+1 / / % % TX n+1 / / TT X n+1 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 Type n+1 .

To show that n+1 is a modality, it remains to show that separation is a property stable under sigma-types. Let A : Type n+1 be a separated type and B : A → Type n+1 be a family of separated types. We want to show that x:A B x is separated. Let E be a type, and χ : E → Type 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 . y:

e:E χ e x = y 1 π2•f •π1•π1 / / π2•g•π1•π1 / / dense B x y:E x = y π2•f •π1 6 6 π2•g•π1 6 6
Using the separation property of B x, one can show that second components, transported correctly along the first components equality, are equal. The complete proof can be found in the formalization. This proves the following proposition Proposition 5.18 (separated_modality). ( n+1 , µ) defines a truncated modality on Type n+1 .

As this modality is just a step in the construction, we do not need to show that it is left exact, we will only do it for the sheafification modality.

5.2.2

From Separated Type to Sheaf. For any T in Type n+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

n+1 T def = u:T →Type n -1 a:T (λt, n (a = t)) = u .
To prove that n+1 T is a sheaf for any T : Type n+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 be a closed (-1)-subobject. Let E : Type 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 a sheaf, it can be extended into ψ : E → U . 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. Then, by retraction property, ψ(e) = φ(e, w), and by π 2 • φ, we have hence our term of type κ(ψ e).

• TBD As T → Type n is a sheaf, and n+1 T is closed in T → Type n , 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 subuniverse.

Proof. Let T, Q : Type n+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, the composition is.

The next step is the closure under dependent sums, to state:

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 : Type n+1 a sheaf and B : A → Type n+1 a sheaf family. By proposition 5.18, we already know that a:A B a is separated. Let E be a type, and χ : E → HProp a dense subobject. Let f : e:E χ e → x:A B x ; we want to extend it into a map E → x:A B x.

e:E χ e f / / x:A B x E 8 8
As A is a sheaf, and π 1 • f : e:E χ e → A, we can recover a map g 1 : E → A. We then want to show e:E B(g 1 e). Let e : E. As χ is dense, we have a term w : n (χ e), and as B(g 1 e) is a sheaf, we can recover a term w : χ e. Then g 1 (e) = f (e, w), and π 2 • f gives the result.

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 actually every modality n+1 is compatible with n on lower homotopy types.

Proposition 5.22. If T : Type n , then n+1 T = n T , where T is T seen as a Type n+1 .

Proof. We prove it by induction on n:

-For n = -1: Let T : HProp. Then

0 T def = u:T →Type n -1 a:T (λt, -1 (a = t)) = u -1 = u:T →Type n -1 a:T (λt, -1 (a = t)) = u
because the type inside the truncation is already in HProp. Now, let define φ :

-1 T → 0 T by φt = (λt , 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 : Type n+1 . Then, as n+1 is compatible with n , and (a = t) is in Type n ,

n+2 T = u:T →Type n+1 -1 a:T (λt, n (a = t)) = u -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) : Type n .

This proves in particular that n+1 is compatible with -1 in the sense of condition 5.10. The last step is the left-exactness of n+1 . Let T be in Type n+1 such that n+1 T is contractible. Thanks to the just shown compatibility between n+1 and n for Type n , left-exactness means that for any x, y : T , n (x = y) is contractible.

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: As n+1 T is contractible, path spaces of n+1 T are contractible, in particular (ν T a = ν T b), which proves left exactness.

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 Type n , 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 P :HProp ¬¬ (P + ¬P ).

Journal of Formalized Reasoning Vol. ?, No. ?, Month Year.

FORMALIZATION

A Coq formalization of the sheafification process based on the Coq/HoTT library [BGL + 17] is available at https://github.com/KevinQuirin/sheafification.

After reviewing the content and some statistics about the formalization in Section 6.1, we present the limitations of our formalization in Section 6.2, in particular the issues relative to universe polymorphism.

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, and it 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 seems quite reasonable and encouraging, because it suggests that homotopy type theory provides a convenient tool to formalize some part of the theory of higher topoï.

Limitations of the formalization

In the formalization, we had 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 need 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 [START_REF] Sozeau | Universe polymorphism in Coq[END_REF] 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.

If Coq handles cumulativity on Type natively, it is not the case for the Σ-type Type n , which requires propositional resizing. This issue could be solved by adding an axiom of cumulativity for Type n with an explicit management of universes. But as it would not have any computational content, such a solution would really complicate the proofs as the axiom would appear everywhere cumulativity is needed and it would need explicit annotations for universe levels everywhere in the formalization.

One issue with universe polymorphism lies in the management of recursive definitions. Indeed, the following recursive definition of sheafification is not allowed. This is because Coq forces the universe of the first Type n occurring in the definition to be the same for every n, whereas the universe of the first Type n+1 occurring in n+1 should be at least one level higher as the one of Type n 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 increasing in the universe levels occurs in the Rezk completion for categories [START_REF] Ahrens | Univalent Categories and the Rezk completion[END_REF]. In the definition of the completion, they use the Yoneda embedding and representable functors, which is similar to our use of characteristic functions. This restriction in our formalization may be solved by generalizing the management of universe polymorphism for recursive definition or by the use of general "resizing axiom" which is still under discussion in the community.

CONCLUSION AND FUTURE WORKS

In this paper, we have defined a way to leverage Lawvere-Tierney sheafification to truncated types in homotopy type theory.

Beyond this result, our work is part of a more general line of work which aims to illustrate that homotopy type theory is a very promising theory for formalizing mathematics inside a proof assistant.

As future works, 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 examples 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 [START_REF] Lurie | Higher topos theory[END_REF]. 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 modalities) 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 it with sheafification, to exhibit a model of homotopy type theory, with computational mere excluded middle.

-

  a function | • | n : T → A n , -a proof of Is-n-type T n , satisfying the following universal property: Lemma 2.2. For any A : Type and B : Type n , if f : A → B then there is an induced g : A n → B such that g(|a| n ) = f (a) for any a : A. • TBD We refer the reader to [UFP13, 7.3] for more details on truncations. The homotopy fiber of a function f at element b is defined as fib f (b) def = a:A f (a) = b. A function f is with n-truncated homotopy fibers (or simply n-truncated function) when fib f (b) is in Type n for any b. Again, we define some sugar. A function f is -an embedding if f is (-1)-truncated -a surjection if every fiber of f is merely inhabited (i.e fib f (y) holds for all y). Then one can show [UFP13, Lemma 7.6.4] that any map f factors uniquely through Im(f ) def =

Lemma 2. 4 .

 4 Let D be a diagram, m a truncation index, and P : Type m a colimit of D. Then, if D m is the same diagram as D where every type is m-truncated, P is a m-colimit 1 of D m .

η

  A x = y for any y : A. Let Cover : A → Type be defined by induction by Cover(y) def = rec (λy, (x = y)). Note that for any y : A, Cover(y) 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 Encode(y, p) def = transport p Cover transport β rec ((λz, (x=z)),x) idmap (η x=x 1) • TBD and Decode : y: A Cover(y) → η A x = y by Decode def = ind λy p, (ap η A ) transport β rec ((λz, (x=y)),y) idmap p

  3.1.2 Truncations. The first class of non-trivial examples might be the truncations modalities, as described in [UFP13, Section 7.3]. 3.1.3 Double negation modality Proposition 3.11. The double negation modality A def = ¬¬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 η A def = λ x : A, λ y : ¬A, y a matches this requirement. Now, we can define P to be exactly A:Type IsEquiv η A . (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. (5) Let A : Type and B : A → Type such that P (A) and a:A P (B a). There is a map x:A B x → A thus by the previous point, we can extend it into κ : ¬¬ x:A B x → A.

F

  (a,b):F ×F a = b fst•π1 / / ι Both fst • π 1 and snd • π 1 make the diagram commute, hence they are equal: a,b:f (a = b) → a = b.

  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 ways, forming an equivalence. -Suppose 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 → (T → Type n ). ι is an embedding, thus it suffices to prove ι(µ T a) = ι(µ T b), i.e.

  t) = n (b = t).

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

  Proposition 5.23 (good_sheafification_unit_paths_are_nj_paths). For all a, b : T , n (a = b) (ν T a = ν T b).

:-

  ∀ (n : nat), Type n → Type n

  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].

  1), then each |f i | n+1 does. Remark 5.16. It is clear that if A and B are equivalent types, and for all a, b :

Journal of Formalized Reasoning Vol. ?, No. ?, Month Year, Pages TBD.

Journal of Formalized Reasoning Vol. ?, No. ?, Month Year.

P is a m-colimit if P satisfies the same property as in

2.3 when we replace Type by Type mJournal of Formalized Reasoning Vol. ?, No. ?, Month Year.

Properties needing only a reflective subuniverse are annotated by (R), a modality by (M), a left-exact modality by (L) Journal of Formalized Reasoning Vol. ?, No. ?, Month Year.

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

• TBD to show is that n+1 T is universal among separated types below T . In the topostheoretic sheafification, it comes easily from the fact that epimorphims are coequalizers 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 KP(µ T ) n+1 , which is enough. We do it by defining another diagram T , equivalent to KP(µ T ) n+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 . Definition 5.13 (OTid). Let X : Type. Let TX be the higher inductive type generated by t :

We consider the diagram T :

The main result we want about T is the following:

Lemma 5.14 (separation_colimit_OTtelescope). Let T : Type n+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 KP(µ T ) n+1 are equivalent. We will need the following lemma: Lemma 5.15 (OT_Omono_sep). Let A, S : Type n+1 , S separated, and f :

Proof (Sketch). By induction on truncation, we need to show that

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.

• TBD

Proof. Let P : HProp, and pose Q def = 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))).

Extension to Type

In the previous section, we have defined a (countably) infinite family of modalities Type i → Type i . One can extend them to whole Type by composing with truncation:

Lemma 5.25. Let i : Type i → Type i be a modality. Then

modality in the sense of section 3

Proof. It is straightforward to check every properties 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 Type i , 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:

Proof. For i-truncated types, = i , and i is left-exact.

The compatibility between the modalities n and between the modalities • n allow us to chose the truncation index as high as desired. Taking it as a non-fixed parameter allows to work in an 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, the 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 associated to n as defined in lemma 5.25. Then, for any type A, B : Type n , if ϕ is the canonical arrow

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 and A 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.