Simon Gsell
email: simon.gsell@univ-amu.fr

Sham Tlili
email: sham.tlili@univ-amu.fr

Matthias Merkel
email: matthias.merkel@univ-amu.fr

Pierre-François Lenne
email: pierre-francois.lenne@univ-amu.fr

Marangoni-like tissue flows enhance symmetry breaking of embryonic organoids

During early development of multi-cellular animals, cells self-organize to set up the body axes, such as the primary head-to-tail axis, based on which the later body plan is defined. Several signaling pathways are known to control body axis formation. Here, we show, however, that tissue mechanics plays an important role during this process. We focus on the emergence of a primary axis in initially spherical aggregates of mouse embryonic stem cells, which mirrors events in the early mouse embryo. These aggregates break rotational symmetry to establish an axial organization with domains of different expression profiles, e.g. of the transcription factor T/Bra and the adhesion molecule E-cadherin. Combining quantitative microscopy and physical modeling, we identify largescale tissue flows with a recirculation component and demonstrate that they significantly contribute to symmetry breaking. We show that the recirculating flows are explained by a difference in tissue surface tension across domains, akin to Marangoni flows, which we further confirm by aggregate fusion experiments. Our work highlights that body axis formation is not only driven by biochemical processes, but that it can also be amplified by tissue flows. We expect this type of amplification to operate in many other organoid and in-vivo systems.

I. INTRODUCTION

Deciphering the mechanisms underlying the formation of the mammalian body plan is an important challenge in biology. This process takes place in the early embryo and is characterized by the establishment of a multicellular spatial organization with reference to an emerging system of orthogonal axes: the head-to-tail axis, also called the anteroposterior (AP) axis, and an orthogonal dorsoventral axis [1]. There is evidence that a small number of conserved morphogens, including Wnt, BMP, Activin/Nodal, and FGF, control the emergence of the body axes [2]. These signals participate in tissue patterning and trigger differential behaviors, which ultimately partition an isotropic group of cells into different territories. Yet, the physical mechanisms underlying axis formation remain largely unknown.

Here we focus on the emergence of the head-to-tail body axis, which breaks the initial rotational symmetry. In vertebrates, the AP axis establishes first by locating the expression of an evolutionarily conserved transcription factor, T/Brachyury (T/Bra), to one end of the embryo. Understanding the emergence of the AP axis, and the appearance of the T/Bra pole in particular, is a daunting task because of the experimental difficulty in accessing the embryo [3][4][5]. However, mouse and human embryonic stem cells (ESCs) provide excellent experi-mental systems to address this question. 3D spherical aggregates of mouse or human ESCs self-organize into gastruloids, which are embryonic organoids that undergo symmetry breaking and exhibit axial organization and gene expression patterns that mirror events in the embryo [START_REF] Van Den Brink | Martinez Arias[END_REF][7][8][9][START_REF] Moris | Current Opinion in Genetics & Development Cell Reprogramming[END_REF]. Depending on the differentiation protocol, i.e. depending on the culture conditions and the signaling molecules present in the medium, gastruloids have the capacity to develop advanced structures strikingly similar to organs such as (1) somites and neural-tube [11][12][13][14] or (2) gut and heart [11,15,16]. Past works on gastruloids have identified the temporal sequence of gene expression [7] and networks of genes that regulate the main steps of their early development, including during symmetry breaking [17].

Yet, there is growing evidence that tissue mechanics and flows are crucial for many stages of embryonic development [18][19][20][21][22]. Indeed, in avians it has recently been pointed out that tissue mechanics and flows could also contribute to embryonic axis formation [23][24][25], but their potential role for axis formation in mammals remains unclear.

At least for one differentiation protocol, we have recently shown that symmetry breaking in mouse gastruloids is accompanied by large-scale tissue flows and heterogeneities in cell-cell adhesion and cell differentiation [16]. In this protocol derived from the standard protocol in the field [26], we first seed a controlled number of pluripotent mouse ESCs into non-adherent microwells (Figure 1a, Methods). After a few hours, the cells form 3D aggregates. 48 hours after aggregate formation (hAAF), differentiation is stimulated by adding the Wntagonist Chiron, which is washed out 24 hours later. At the end of Chiron exposure (72 hAAF), gastruloids are spherical and express T/Bra throughout. Between 72 and 96 hAAF, gastruloids start to elongate and display AP-graded T/Bra and E-cadherin (E-cad) expression pattern with higher expression posteriorly (Figure 1ad). These heterogeneities are linked to an epithelial-tomesenchymal transition (as evidenced by the differential expression of Snail, Figure 1d, Supplementary Figure 1), which has since been identified in other differentiation protocols [27]. The main tissue types produced after symmetry breaking in our differentiation protocol are endoderm and mesoderm ( [16], Supplementary Figures 2a-3-4).

Here we quantitatively show that large-scale tissue flows contribute substantially to symmetry breaking in our mouse gastruloids. We show that the dominating component of the tissue flows is a recirculating flow whose direction correlates strongly with the T/Bra or E-cad polarization of the aggregate.

We then present a minimal effective model for the emergence of these flows. In particular, we show that effective interfacial tensions between low and high T/Bra or E-cad domains, as well as differential surface tensions of these domains, are sufficient to explain the recirculating flows. Finally, we further validate our hypothesis of differential tensions by measuring interface angles in fu-sion experiments between gastruloids. Taken together, our work quantitatively shows that not only genetic and biochemical interactions, but also tension-driven largescale tissue flows promote symmetry breaking in gastruloids.

II. RESULTS

Tissue flows substantially contribute to gastruloid symmetry breaking. In previous work, we provided experimental evidence for the existence of largescale tissue flows, which differently advected cells with different levels of T/Bra or E-cad expression [16]. Motivated by these results, here we aim to precisely quantify the contribution of such tissue flows to the overall symmetry breaking. To this end, we need to simultaneously measure tissue flows and T/Bra or E-cad expression patterns.

We generate the gastruloids following our previouslypublished protocol (Figure 1a, Methods) [16], where we focus on the time between 72 and 96 hAAF, where gastruloids start to elongate and display polarized T/Bra and E-cad levels. Quantifying tissue flows and expression patterns in the gastruloids is challenging, as gastruloids are 3D cell aggregates with a diameter of a few hun-

T/Bra

Cell differentation

Reaction-diffusion

Reaction-diffusion, dred micrometers, which scatter light and are sensitive to prolonged illumination. To reduce light scattering while preventing phototoxic effects, we have used two-photon microscopy (see Methods) and imaged 60 µm-thick subvolumes around the mid-plane of the gastruloids (Figure 1b, Methods). We ensured that the T/Bra and E-cad polarization direction, as well as the flow field directionality was approximately aligned with the imaging plane. To reduce drift during live-imaging, we transfer the gastruloids into arrays of 500 µm microwells at 72 hAAF (see Methods). We have used two cell lines: one with a T-Bra GFP live reporter, and one with an E-cad GFP live reporter (see Methods). To quantify tissue flows, we also added one of two different live cell markers, one for cell membranes and extra-cellular space (Sulforhodamin B, see Supplementary movie 1), or one for cell nuclei (SPY555-DNA; see Supplementary movies 2-5).

Reaction-diffusion

Advection

To quantify flow fields, we combined (1) global image registration of the gastruloids to remove any global translation and rotation, followed by (2) optical flow to compute the tissue flow fields (see Methods, Supplementary Figure 5, Supplementary movie 6).

To quantify the degree of symmetry breaking of a gastruloid, i.e. its polarization, we use the dipole moment of its T/Bra or E-cad distribution (Figure 2a-c). It is represented at each time point t by the 2D vector P , which we define as:

P (t) = Ω ϕ(r, t) r -c(t) dS, (1)
where Ω represents the 2D cross section of the aggregate, ϕ denotes the T/Bra or E-cad fluorescence intensity field, r is the position vector that we integrate over, and c is the barycenter of the aggregate. The direction of the vector P points towards the pole with a high fluorescence intensity of T/Bra or E-cad, and its magnitude quantifies the degree of symmetry breaking (i.e. polarization).

In our plots, we normalize the polarization vector P (t) at each time point by some reference value P 0 (t) that depends on the instantaneous overall expression level and the total projected area of the gastruloid (Figure 2b,c, see SI). This allows us to compensate for both time dependence and sample variability of overall expression level and size when comparing different gastruloids. Compared to a time-independent normalization, this results in a better collapse of polarization dynamics over samples (Figure 2c and Supplementary Figure 6b).

We found that after registration, the direction of the dipole moment does not change significantly over time (Supplementary Figure 6a). This indicates that very early processes already define an axis that is kept later on. However, we also see that the polarization magnitude increases over time, reflecting gastruloid symmetry breaking (Figure 2b,c).

We wondered how important different cellular processes are for the progressive increase in gastruloid polarization over time. There are different cell-scale processes that might contribute, which include (i) spatially heterogeneous cell differentiation, (ii) individual cell motion, (iii) collective cell motion (i.e. tissue flows), and differential (iv) cell division and/or (v) apoptosis (Figure 2d). To differentiate the contribution of all these processes to aggregate polarization, segmentation and tracking of the cell nuclei would be required, which is currently difficult due to light scattering and nuclei high density. Thus, we base our analysis here on coarse-grained optical flow and fluorescence data, which still allows us to differentiate three different contributions to gastruloid polarization: (1) the combined effect of cell differentiation, and individual cell motion (contributions i and ii), which we call for brevity "reaction-diffusion" (RD) contribution, (2) advection of T/Bra or E-cad with tissue flows (contribution iii), and (3) differential volume growth, arising for instance from cell division and apoptosis (contributions iv and v), which we call for brevity just "growth" contribution (Figure 2d).

Using the optical flow and fluorescence data, we can quantify the contributions 1-3 to the overall increase in polarization. To this end, we decompose the time derivative of P into four parts (Figure 2e, see SI):

dP dt = R + A + G + Q 3D , (2)
with

R(t) = Ω ∂ϕ ∂t + v • ∇ϕ r -c dS (RD) (3)
A(t) = Ω ϕ v -v dS (advection) (4) G(t) = Ω ϕ -ϕ (∇ • v) r -c dS (growth). (5)
Here, v is the local tissue velocity (Figure 1c) and a line over a symbol, • , denotes averaging over the aggregate cross section. The first three terms on the right-handside of Eq. ( 2) respectively represent the contributions 1-3 (Figure 2e), and Q 3D is a geometric contribution related to 3D motion of the aggregate (see SI). Besides the geometric contribution Q 3D , this mathematical decomposition also formally confirms that there can be no other contribution to gastruloid polarization than contributions 1-3. For all samples, we quantify each term in Eq. ( 2) over time and plot their respective cumulative contributions to the overall dipole moment. For one gastruloid, this is shown in Figure 2e, and for the other gastruloids in Supplementary Figures 6c-i. We compare the final overall contributions across all gastruloids in Figure 2f. We find that reaction-diffusion processes generally contribute most to the overall polarization. However, our analysis also reveals a significant contribution of advection, which is responsible for approximately 1/3 of the total polarization. This overall contribution is not evenly distributed over time: while the relative advective contribution tends to be smaller at the beginning of the polarization process, it increases as the dipole moment increases (Figure 2g). By the end of the process, advection can even become the dominant contribution to the instantaneous increase in polarization (Figure 2e).

Taken together, our analysis shows that advection with large-scale tissue flows significantly contributes to gastruloid symmetry breaking. To better understand how, we next analyzed the structure of the flow pattern across different gastruloids.

Tissue flows exhibit a dominant recirculating component. Qualitatively, tissue flows emerging during the polarization process exhibit substantial fluctuations, both spatio-temporally and across different gastruloids (see Supplementary Figures 5 and7). In order to capture the dominant large-scale flow structures and compare them across gastruloids, we decomposed the tissue flow field into different modes (Figure 3 and SI). To this end, we define a disk that encompasses most of the aggregate projection (Figure 3a), and express the coarsegrained tissue velocity v(r) in polar form, i.e. with radial and angular velocity components v r (r) and v θ (r) (Figure 3b). We then decompose both spatial functions v r (r) and v θ (r) into different modes, again using polar coordinates. To capture the variation of both functions with the angular coordinate θ, we decompose them into angular Fourier modes (mode index n, Figure 3c). Similarly, we decompose the radius-dependent part of both functions into polynomial modes (mode index p, Figure 3c). As a result, both v r (r) and v θ (r) are decomposed into a sum of base modes v r n,p (r) and v θ n,p (r), each weighted by a complex amplitude, denoted A r n,p and A θ n,p :

v r (r) = n,p A r n,p v r n,p (r) (6) v θ (r) = n,p A θ n,p v θ n,p (r). (7)
We display a few of the base modes v r n,p (r) and v θ n,p (r) in Figure 3d. Generally, the modes with smaller indices (n, p) correspond to larger-scale features of the flow field. Each of the complex mode amplitudes A r/θ n,p provides information about an angle and a magnitude. The angle corresponds to a rotation of the respective base mode around the barycenter, and the squared magnitude reflects the contribution of the respective base mode to the spatial variance of the flow field (Figure 3e,f; see SI). In other words, the modes with the largest amplitudes correspond to the dominant features of the flow field.

We apply our mode decomposition analysis on 9 gastruloids taken between 78hAAF and 88hAAF. The analysis reveals that about 50% of the tissue flow field is provided by only 5 low-index modes, i.e. large-scale features, which are robustly observed across different gastruloids (Figure 3e-g). In particular, the three modes of highest amplitude, which are A θ 1,1 , A θ 1,0 and A r 1,0 , together contribute approximately 40% to the total flow field. The superposition of these three modes corresponds to a largescale recirculating pattern (Figure 3h). The next most relevant mode identified in Figure 3g,v r 2,0 (r) with amplitude A r 2,0 (Figure 3e right), contributes to gastruloid elongation. It corresponds to a flow field that extends along one axis and contracts along the perpendicular axis, consistent with gastruloid elongation between 72 and 96hAAF.

We find that the direction of the large-scale recirculating pattern strongly correlates with the T/Bra polarization, where the direction of the flow in the aggregate center points towards high T/Bra concentrations (Figure 3i). This correlation between the directions of T/Bra polarization and recirculating flow could be created by the advection of T/Bra with the tissue flows. However, could it also be possible that, conversely, aggregate polarization drives the recirculating flows?

The recirculating flows could be driven by patterning-induced tension. To understand how the aggregate polarization -in terms of gene expression patterns -could affect tissue mechanics and flows, we first noted that from a coarse-grained perspective, the expression patterns of many genes are qualitatively similar in showing a distinct AP gradient (Figure 1c,d and Supplementary Figures 1234). We thus studied a minimal model that represents these AP patterning genes by a single effective expression pattern ϕ(r), which ranges from -1 (anterior-most) to +1 (posterior-most). The field ϕ(r) reflects the combined effect of the AP patterning genes on tissue flows. In particular, the AP patterning genes include differentially expressed cadherins such as E-cad [16], which are known to lead to tension-driven phase separation [28][29][30][31][32].

To understand whether the observed gastruloid patterning can drive the recirculating flow, we study a simple continuum model that describes the gastruloid as an incompressible viscous fluid whose flows are driven by gradients of the field ϕ(r). Formally, this is described by Stokes' equations:

0 = ∇ • v (8a) 0 = -∇Π + η∇ 2 v + ∇ • (σ i + σ s ), ( 8b
)
where Π is the hydrodynamic pressure ensuring incompressibility, η is the effective tissue viscosity, and σ i and σ s are symmetric, traceless tensors that denote additional mechanical stresses driving tissue flows. The stress σ i is internally created by the effective expression pattern ϕ(r), and σ s represents the tension at the aggregate surface.

There are different ways in which the internal stress σ i could depend on ϕ(r). However, as has been pointed out before [33], the leading-order effect that drives incompressible flow is given by

σ i = -κ i (∇ϕ) • (∇ϕ) - 1 2 (∇ϕ) 2 I . (9)
Here, the coefficient κ i controls the magnitude of the internal mechanical stress σ i , the symbol • denotes the dyadic product, and I denotes the identity tensor. The internal stress tensor σ i is locally aligned with the gradient of ϕ(r), and its magnitude increases monotonically with the magnitude of the gradient (Figure 4a). At an interface between regions of low and high ϕ(r), the tensor σ i determines an effective interface tension γ i , which is obtained by integrating σ i across the interface width (Figure 4a,b).

To describe aggregate surface tension σ s , we introduce a second field ψ(r), which is equal to 1 inside the aggregate and 0 outside (Figure 4c). The stress σ s can be computed from gradients of ψ(r) analogously to Eq. ( 9), but with a magnitude κ s that depends on local cell fate, i.e. on the ϕ(r) field. In the two limiting cases of ϕ = -1 (anterior regions) and ϕ = +1 (posterior regions), we denote the surface stress magnitude by κ - s and κ + s , respectively (Figure 4c, details in the SI).

To test how far our simple effective model can account for the observed tissue flows, we solve Eqs. ( 8) and (9) using a lattice Boltzmann approach [34,35] (see details in the SI), where we use for ϕ(r) the coarsegrained experimentally determined T/Bra field, as a representative AP expression pattern. In Figure 4d, we plot the resulting tissue flow field varying two dimensionless stress ratios, a relative surface stress difference, s -κ - s )/κ i and a interface-to-surface stress ratio, r := 2κ i /(κ + s + κ - s ). We find that the surface tension difference ∆κ s indeed creates a recirculating flow pattern. This is because the surface tension gradient drives surface flows, a mechanism known as Marangoni effect. For ∆κ s < 0 the flow on the aggregate surface is oriented towards the anterior pole, similarly to what we observe in our experiments, while for ∆κ s > 0 it is oriented towards the posterior pole (Figure 4d). This qualitative comparison suggests that in our gastruloids the surface tension of anterior regions may be higher than that of posterior regions.

We further quantitatively compared the flow fields obtained from our model to the experimentally observed one. We quantify the deviation between simulated and experimentally observed flow fields using a residual, which we define as the fraction of the spatial variance in the experimental flow field that is not reproduced by our simulations. Since our simulations use dimensionless units, in order to compare to experimental data, we need to adjust a velocity magnitude for the simulated flow fields. We thus always choose the velocity magnitude value that minimizes the residual (see SI). In Figure 4f left, we plot the residual depending on the two model parameters ∆κ s and r. We find indeed that the residual is smallest for negative ∆κ s . However, we also find that the deviation becomes larger for a small interface-to-surface stress ratio r. This is because, for small r, internally created tension are smaller than surface tension, which induces flows that would lead to a more circular aggregate shape (e.g. (∆κ s , r) = (0, 0.5) in Figure 4d). However, we observe that even at negative ∆κ s and large r, the residual is still very large, on the order of 85%. Do dissect the possible reasons for the relatively large residual between measured and predicted flow field (Figure 4f left), we suspected that small-scale spatio-temporal fluctuations contribute to the experimental flow fields. We thus compared between simulation and experiment only the flow contributions provided by the modes v θ 1,1 , v θ 1,0 and v r 1,0 , which together create the recirculating flow pattern. The residual between just these contributions between simulation and experiment is shown in Figure 4f right. We find that our simulations predict the observed recirculation flow in a wide parameter region defined by ∆κ s < 0 with a residual that is reduced to ∼ 40-50%, independent of the precise values of ∆κ s and r. However, varying ∆κ s and r does affect the amplitude of other large-scale flow components that do not contribute to the recirculating flow. For example, reducing the values of r and |∆κ s | results in an important flow contribution by the mode v r 2,0 (Figure 4g), which corresponds to a rounding up of the gastruloid (e.g. (∆κ s , r) = (0, 0.5) in Figure 4d).

Taken together, the comparison between our model and experimental data suggests: (i) a higher surface tension in anterior (T/Bra-) than in posterior (T/Bra+) tissues and (ii) an interface tension between these tissues. To further test this, we performed fusion experiments be-tween gastruloids.

Fusion experiments confirm the existence of T/Bra-dependent tensions. To assess the existence of T/Bra-dependent tensions in the gastruloids, we performed fusion experiments to force T/Bra+ tissues to mechanically interact with T/Bra-tissues (Figure 5, Supplementary Movie 7). To this end, we used our observations that gastruloids at 72hAAF display high T/Bra levels almost everywhere, while 84hAAF gastruloids are already polarized, exhibiting both T/Bra+ and T/Braregions. We thus brought 72hAAF gastruloids in contact with 84hAAF gastruloids.

Different fusion scenarios occur depending on the relative position of both aggregates (Figure 5, Supplementary Movie 8). For example, when a 72hAAF gastruloid was in contact with both T/Bra+ and T/Bra-regions of a 84hAAF gastruloid, we occasionally observed an asymmetric fusion (Figure 5a, see two cases in Supplementary Movie 8): The homotypic interface between T/Bra+ and T/Bra+ regions (++) extends in length while the heterotypic interface between T/Bra+ and T/Bra-regions (+-) slightly shrinks (Figure 5b). This behavior suggests that the affinity between two T/Bra+ regions is larger than that between T/Bra+ and T/Bra-regions. In other words, there is an effective interface tension between T/Bra+ and T/Bra-regions and an effective surface tension of T/Bra+ regions.

To further characterize the different tensions in the system, we focused on interactions between T/Bra+ and T/Bra-tissues by selecting experiments with only a heterotypical +-contact of the 72hAAF gastruloid with a T/Bra-region of the 84hAAF gastruloid (Figure 5c). As a control experiment, we also consider homotypical ++ fusion experiments between two 72hAAF T/Bra+ aggregates (Supplementary Movie 9). We track the fusion angles θ 1 , θ 2 and θ 3 over time during the fusion process (Figure 5c,e,f, Methods). In the case of homotypical ++ fusions, the outer fusion angle θ 1 saturates to 180 • (red solid curve in Figure 5e), while the inner angles θ 2 and θ 3 both saturate at approximately 90 • (red and orange solid curves in Figure 5f). This behavior is expected and quantitatively reproduced by our model when we set κ - s = κ + s and r = 0 (Figure 5d, simulation 1; red dashed curves in Figure 5e,f).

For heterotypical +-fusions, the outer fusion angle saturates to a lower value of θ 1 ≈ 140 • (blue solid curve in Figure 5e). Moreover, the inner angle θ 2 in the T/Bra+ tissue saturates to a lower value than the inner angle θ 3 in the T/Bra-tissue (blue and green solid curves, respectively, in Figure 5d). These observations are consistent with our previous conclusions that (i) T/Bratissues have a higher surface tension than T/Bra+ tissues (θ 2 < θ 3 ), and (ii) there is a finite interface tension between T/Bra+ and T/Bra-tissues (θ 1 < 180 • ). Indeed, simulations of our model with ∆κ s = -0.2 and r = 0.8 quantitatively reproduce our experimental observations (Figure 5d, simulation 2; blue and green dashed We then consider fusion experiments with either a homotypical ++ contact between two 72hAAF gastruloids or a heterotypical +-contact between a 72hAAF gastruloid and the T/Braregion of a 84hAAF gastruloid. We define the fusion angles θ1, θ2 and θ3 as indicated. (d) Experiments are compared to model simulations of fusing droplets. we consider two particular cases: simulation 1 is performed in the absence of tension between the droplets, while simulation 2 is performed in the presence of interface tension and surface tension difference, namely r = 0.8 and ∆κs = -0.2. (e,f) Time evolution of the (e) outer angle θ1 and (f) inner angles θ2 and θ3, averaged over samples and compared to the angles in the respective simulation. The shaded areas indicate the 95% confidence interval.

curves in Figure 5e,f). As discussed before, in this part of parameter space, our simulations predict a recirculation flow together with a strong flow component relaxing gastruloids towards a circular shape (Figure 4g). We believe that in real gastruloids, such rounding up is counteracted by additional mechanisms that lead to gastruloid elongation along the AP axis. However, an explicit tendency of the aggregates to elongate requires additional, active stresses, which are not included in our model, as we focus here on the recirculating flows and AP symmetry breaking.

While in the previous section we needed to fit the absolute velocity amplitude in our simulations, the fusion experiments allow us to estimate an order of magnitude of the reciculating flow speed. The time scale on which two droplets with viscosity η, radius R, and surface ten-sion γ s fuse is given by t F ∼ Rη/γ s [36,37]. According to Figure 5e, we estimate t F ∼ 1 h. Moreover, in a droplet whose surface tension varies between γ - s and γ + s , recirculating Marangoni flows traverse the size of the droplet on the time scale [38]. Using ∆κ s = -0.2 and r = 0.8, we thus obtain t M ∼ 6 h, which is close to the time scale of gastruloid symmetry breaking t SB ∼ 10 h. This confirms that the differential tension observed in our fusion experiments is sufficient to drive recirculation flows that promote symmetry breaking.

t M ∼ Rη/|γ + s -γ - s | ≃ t F /(r|∆κ s |)

III. DISCUSSION

In this paper, we study aggregates of mouse embryonic stem cells, which form a primary axis through rotational symmetry breaking, during which a pole of high T/Bra and E-Cad expression forms at one end (Figure 1). Several cellular mechanisms can contribute to such symmetry breaking (Figure 2c): biochemical reactions and cellular diffusion (RD), advection of regions with high T/Bra or E-Cad, and heterogeneous growth. We show that RD and advection both significantly contribute to polarization (Figure 2). RD contributions, important during the initial phases of symmetry breaking, are accompanied by significant advection contributions persisting over longer periods. We demonstrate that a recirculating component dominates these flows (Figure 3), and we show that the flows are consistent with Marangoni flows that are induced by differential tensions in an already polarized aggregate (Figure 4). We further confirm the existence of these tension differences by measuring interface angles in fusion experiments (Figure 5). Taken together, our observations suggest a positive feedback loop where recirculating flows amplify and thus stabilize an early aggregate polarization.

Since the middle of the 20th century, effective tissue surface tensions have been proposed to drive the separation of cell populations [30,31,[39][40][41][42][START_REF] Manning | Proceedings of the National Academy of Sciences[END_REF]. Such effective tensions can for instance be created by differential cadherin expression [31,32]. Indeed, in our gastruloids, cells progressively lose E-cadherin expression [16], and display a spatial anti-correlation between N-cadherin and Ecadherin [16] and between OB-cadherin and E-cadherin (Supplementary Figure 8). However, much of the past work on differential tissue tensions driving the separation of cell populations considered tissue separation as a diffusive unmixing process, including in stem cell aggregates [START_REF] Bao | [END_REF][START_REF] De Jong | A combination of convergent extension and differential adhesion explains the shapes of elongating gastruloids[END_REF]. In contrast, our work shows for the first time that differential tissue surface tensions can drive long-range hydrodynamic flows that are maintained over a long time ( > ∼ 10 hours). In previous work, some of us have shown that such long-range flows can be important to substantially accelerate cellular unmixing [START_REF] Gsell | [END_REF].

There are a number of possible future extensions of this work. First, much of the past work on cellular unmixing focused on already differentiated cells [47]. However, if all cells kept their initial differentiation state over time, flows driven by differential tissue tensions may at some point cease [START_REF] Gsell | [END_REF]. However, the cells in our system are in the process of differentiating, and the observed recirculating flows are maintained over several hours, which makes us wonder whether the flows might be maintained through patterned cell differentiation. Indeed, in previous work, some of us have shown that (i) some of the T/Bra-negative cells are pluripotent cells, which divide and differentiate into T/Bra-positive cells, while (ii) the T/Bra-and E-Cad-positive cells progressively divide and differentiate into T/Bra-and E-Cad-negative cells [16]. Whether and how precisely such cell division and differentiation events might help to sustain the observed flows will be interesting to dissect in future work.

Second, here we have studied a 2D section of the 3D flows in the aggregates. This is because of current technical limitations to in toto imaging of the aggregates, due to photo-toxicity constraints and line scanning speed limitations. Here, we have filtered out aggregates where the inferred out-of-plane flow component was too high (see SI, Supplementary movie 10). It remains a future challenge to analyze the full 3D expression patterns and flows using in toto imaging of the aggregates.

Third, it will be interesting to examine the precise cellular mechanisms underlying the differences in effective tissue surface tension [30,[START_REF] Manning | Proceedings of the National Academy of Sciences[END_REF]48]. Possibilities are adhesion by itself, differential levels of cell contractility, or cell motility (Supplementary figures 8-9). These different microscopic contributions are not mutually exclusive and dissecting the exact contribution of each of them will necessitate the generation of specific knock-out mutant cell lines which is beyond the scope of this work.

Fourth, while we have focused here on the recirculating flows in the aggregate, we did not include any mechanism creating aggregate elongation, which would necessitate both active driving forces and globally aligned orientational information [49]. Indeed, it has been shown for fish embryonic stem cell aggregates, that cell polarity proteins are present and play an important role for gastruloid elongation [50,51]. Alternative mechanisms could be based on heterogeneous mechanical properties [52]. It will be interesting to identify the precise mechanisms driving gastruloid elongation in future work.

We expect that Marangoni-effect-driven recirculating tissue flows operate also in many other organoid systems, i.e. systems formed from pluripotent cells. While such Marangoni flows can be artificially induced [53], they can also be driven internally. The emergence of such flows requires only the existence of distinct cell populations, which will typically display different surface tensions, thus providing a general mechanism for amplification of symmetry breaking. These flows may also be relevant in the gastrulating mouse embryo, where they interact with other internal and external mechanisms [2]. For instance, recirculating flows have been identified during mouse heart morphogenesis, e.g. during the creation of the first cardiac crescent during gastrulation [3]. We thus anticipate that the feedback loop that we observe in our mouse embryonic stem cell aggregates may turn out to play a role in many systems both in vitro and in vivo.

IV. METHODS

Cell culture and gastruloid formation. We used the two cell lines, E-cad-GFP/Oct4-mCherry and T-Bra-GFP/NE-mKate2 (Histone GFP under the T-Bra promoter). In brief, between 100 and 200 cells were seeded in low adhesive 96 wells plates in a neural differentiation medium. In order to promote the formation of endoderm formation and to reduce symmetry breaking variability compared to the standard gastruloids protocol, we enrichted the medium with Fibroblast Growth Factor and Activin. A complete description of the cell lines, the culture conditions and the protocol for making gastruloids is presented in [16]. All cell lines were tested to be free from mycoplasma contamination using qPCR.

Two-photon imaging. The gastruloids were imaged in a chamber maintained at 37 • C, 5% CO2 with a humidifier. We performed two-photon imaging using a Zeiss 510 NLO (Inverse -LSM) with a femtosecond laser (Laser Mai Tai DeepSee HP) with a 40 x/1.2 C Apochromat objective. 72hAAF gastruloids were transferred from 96-well plates to either MatTek dishes (Mat-Tek corporation, ref: P35G-1.5-14 C) or to microwell plates (500 µm wells, SUNBIOSCIENCE ref: Gri3D).

To visualize inter-cellular space, we added 10 µL/mL of a Sulforhodamin B solution (1 mg/mL of Sulforhodamin B powder, 230,162 Aldrich) to the medium and excited both GFP and Sulforhodamin B at 900 nm. To image cell nuclei, we added 1 µL of a SPY555-DNA (spirochrome) 1000x stock solution per mL of medium and excited both GFP and SPY555-DNA at 880 nm. Nuclei staining progressively improved over time, likely due to a progressive decrease in cell packing density and to nuclei accessibility (Supplementary movies 2-5).

We imaged sub-volumes of gastruloids around their midplane (z-stacks of 60 µm (with 12 to 30 slices at intervals between 5 µm and 2 µm depending on the movie)) for a total duration between 10 h and 24 h (time interval between two frames between 3 and 10 min depending on the experiment). We imaged the GFP and the red fluorophores (either Sulforhodamin B or SPY555-DNA) channels using two non-descanned detectors.

Immunostaining Samples were immunostained using the same protocol than in [16] apart from the fact that primary antibodies were incubated during 3 consecutive days. Secondary antibodies (AF488, A568, AF647) and Hoechst were chosen to be compatible with four-color two-photon imaging. Optical flow measurements. To measure coarsegrained velocity fields, we use the signal collected in the red channel (either inter-cellular space with the Sulforhodamin B (SRB) or nuclear signal with the SPY555-DNA probe). The SRB signal corresponds to (i) cell contours, (2) dead cells, and (3) bright spots of subcellular size moving rapidly corresponding probably to vesicles are visible. As dead cells and bright spots are much brighter than cell contours, we filter them with a thresholding operation. The SPY555-DNA signal also accumulates more in bright spots and dead cells which are filtered by the same thresholding process. The mid-plane of the z-stack is determined (maximal area of the gastruloid) and an average projection is made between the mid-plane and the two planes under and above it (separated usually of 2 microns). The same averaging is performed on the GFP channel. We then perform 2D timelapse registration using the ImageJ Plugin MultiStackReg to remove rapid rotations and translations of the aggregate (the transformation is calculated on the red channel and applied both to the red and green channels). We then use a custommade Matlab optical flow code based on the Kanade Lucas Tomasi (KLT) algorithm with a level 2 pyramid and a window size corresponding to a square of 2 cells by 2 cells [START_REF] Lucas | Proceedings of the 7th international joint conference on Artificial intelligence[END_REF]. The velocity fields are averaged overs 12 consecutive frames (1 hour) to smooth both measurement noise and temporal fluctuations.

Fusion experiments. Two gastruloid batches were prepared from the T/Bra GFP line with a 14 hours delay from one another. Both batches were incubated during the 24h long Chiron pulse in different CellTracker colors (CMTMR orange CellTracker, Thermofischer) for the older batch and blue (CMAC blue CellTracker, Thermofischer) for the youngest batch. They were rinsed in transparent medium (Neural differentiation medium enriched in FGF and Activin) at the time of fusion (t = 72hAAF for the youngest gastruloid and t = 86hAAF for the oldest one) and were put in contact in pairs (either a young/young pair or a young/old pair) in an individual well from a 96 wells plate. Pairs of fusing gastruloids were imaged with epifluorescence and brightfield at 10x magnification with a Zeiss microscope every 20 minutes in the red, blue, green and brightfield channels using a multiposition configuration.

Fusion interface/angle analysis. We used the T/Bra and CellTracker color channels to define three scalar fields: (i) a field ψ(r) equal to 1 inside any one of the two gastruloids and 0 outside, (ii) a field χ(r) equal to 1 in the first aggregate (e.g. blue in Figure 5c) and -1 in the second aggregate (e.g. red in Figure 5c), and (iii) a field ϕ(r) ∈ [0, 1] representing the T/Bra signal. We defined the fusion interface as the iso-line χ = 0 with curvilinear coordinate s χ . The fusion interface length was then defined as

L = χ=0 ψ ds χ . (10)
In addition, the length of the homotypic ++ interface between T/Bra+ tissues was computed as

L ++ = χ=0 ϕ ds χ . (11)
The heterotypic +-interface length was then computed as L +-= L -L ++ . We defined the gastruloids' surface as the iso-line ψ = 0.5 with curvilinear coordinate s ψ . The triple points where both gastruloids and the outer medium meet are then characterized by the coordinate s t ψ on the aggregate surface that satisfies χ(s t ψ ) = 0. At a given triple point, we computed the outer fusion angle θ 1 using cos(θ 1 ) = n ψ (s t ψ + δ s ) • n ψ (s t ψ -δ s ), (12) where n ψ = -∇ψ/|∇ψ| is the outward-pointing unit vector normal to the aggregate surface and δ s is a length scale parameter. We checked that the choice of δ s does not affect the results in Figure 5. Inner angles θ 2 and θ 3 were determined following a similar approach, but using the gastruloid-gastruloid interface χ = 0 with curvilinear coordinate s χ . At a triple point, the coordinate s t χ on the gastruloid-gastruloid interface satisfies ψ(s t χ ) = 0.5. The inner angles were com-puted using cos(θ 2 ) = n ψ (s t ψ + δ s ) • n χ (s t χ -δ s ) (13) and cos(θ 3 ) = n ψ (s t ψ -δ s ) • n χ (s t χ -δ s ), (14) where n χ = ∇χ/|∇χ| is the unit vector normal to the fusion interface on the iso-line χ = 0.

FIG. 1 .

 1 FIG. 1. Gastruloid symmetry breaking. (a) Protocol to form gastruloids in low-adherent microwells. (b) Inverted two-photon microscopy is used to image sub-volumes of gastruloids: each orange plane corresponds to a scan at a different depth. (c) Live imaging enables to obtain tissue flows associated to gastruloids symmetry breaking (averaged over one hour) and the corresponding T/Bra pattern (gray levels are inverted for better visibility). (d) E-cadherin and Snail pattern obtained by immunochemistry at the same timing that in (c) (gray levels are inverted for better visibility).

FIG. 2 .

 2 FIG. 2. Quantitative analysis of the polarization process. (a) Example of T/Bra distribution and corresponding coarse-grained field ϕ. (b) Example of the time evolution of the T/Bra dipole moment and corresponding T/Bra distributions. (c) Time evolution of T/Bra and Ecad dipole moments for different samples. (d) At the cellular level, the polarization process relies on the interplay between cell differentiation, cell rearrangements and cell division/apoptosis, resulting in three effective mechanisms at the coarse-grained level, namely reaction-diffusion, advection and growth. (e) Example of time evolution of the cumulative contributions to T/Bra polarization. For instance, P (t) := t t i (dP (t ′ )/dt ′ ) dt ′ = P (t) -P (ti), R := t t i R(t ′ ) dt ′ , etc (see SI). (f) Relative total contribution of each process at the end of the polarization. (g) Advective contribution to polarization, averaged over all samples, as a function of the relative polarization magnitude |P |/|P |max; error bars indicate the standard error of the mean.

3 FIG. 3 .

 33 FIG. 3. Analysis of tissue flow during polarization. (a) Coarse-grained tissue flows are analyzed in a circular disk, centered on the aggregate barycenter c. (b) Tissue velocity v is decomposed as the sum of a radial component vr and an angular component v θ . Similarly, positions within the aggregate can be expressed in polar coordinates (r, θ). (c) The velocity components vr(r) and v θ (r) are decomposed into a series of angular (index n) and radial (index p) modes. These modes are plotted for n ≤ 4 and p ≤ 4. (d) The first few modes are illustrated by their spectrum, the corresponding angular and radial functions, and the resulting radial and angular velocity fields. (e) Example of tissue velocity field expressed as a sum of the base modes in panel d, where the modes are weighted by the amplitudes A r n,p and A θ n,p . Below each mode we indicate the approximate contribution to the total variance of the flow. (f) Spectra displaying the contributions of each mode to the overall flow (compare panel d, leftmost column). Same sample as in (e). (g) Leading mode contributions over different samples. (h) We reconstruct the dominant recirculation mode over samples using median amplitudes of the three leading modes A θ 1,1 , A θ 1,0 and A r 1,0 . (i) Scatter plot showing the orientation angle of the recirculation mode versus the orientation angle of the T/Bra dipole moment for each sample.

3 FIG. 4 .

 34 FIG. 4. Computational modelling of the recirculating tissue flows. (a) Gradients of a scalar field ϕ control stresses, which results in an effective tension γi at the interface between domains of high and low ϕ. (b) We construct coarse-grained scalar fields from the experimentally observed T/Bra fields and we compute the resulting active stresses within the aggregate. (c) We describe the aggregate surface as a smooth interface using a second scalar field ψ. The effective tension at the aggregate surface is controlled by a ϕ-dependent stress coefficient, with two limit values κ - s and κ + s corresponding to surfaces of T/Bra-and T/Bra+ tissues, respectively. (d) We compute tissue flows driven by the T/Bra-dependent stresses over ranges of the interface (κi) and surface (κ + s and κ - s ) stress coefficients, varied through the non-dimensional parameters r and ∆κs. The simulated flow fields shown here were computed from the T/Bra field plotted in panel b. (e) Experimental velocity field corresponding to panels b and d. (f) Residual between simulated and experimentally observed flow field, averaged over all gastruloids, as a function of the model parameters ∆κs and r. (left) Residual between the full flow fields, (right) residual between the modes contributing to the recirculation flow only. (g) Dominant modes contributing to the simulated flow field for two parameter sets, respectively minimizing the total flow residual (r = 2.5, ∆κs = -1) and the recirculating flow residual (r = 0.9, ∆κs = -0.2). (h) Reconstructed recirculation flow in experiments and simulations.

  ∆κ s := (κ +

FIG. 5 .

 5 FIG. 5. Quantitative analysis of aggregate fusion experiments. (a)Example of hybrid fusion, where a 72hAAF gastruloid is in contact with both a T/Bra+ and a T/Bra-region of a 84hAAF gastruloid. (b) Time evolution of the fusion interface length, decomposed as the sum of homotypic contact length between two T/Bra+ tissue regions (++), and heterotypic contact length between a T/Bra+ and a T/Bra-region (+-). (c) We then consider fusion experiments with either a homotypical ++ contact between two 72hAAF gastruloids or a heterotypical +-contact between a 72hAAF gastruloid and the T/Braregion of a 84hAAF gastruloid. We define the fusion angles θ1, θ2 and θ3 as indicated. (d) Experiments are compared to model simulations of fusing droplets. we consider two particular cases: simulation 1 is performed in the absence of tension between the droplets, while simulation 2 is performed in the presence of interface tension and surface tension difference, namely r = 0.8 and ∆κs = -0.2. (e,f) Time evolution of the (e) outer angle θ1 and (f) inner angles θ2 and θ3, averaged over samples and compared to the angles in the respective simulation. The shaded areas indicate the 95% confidence interval.

ACKNOWLEDGMENTS

M.M. thanks the Centre Interdisciplinaire de Nanoscience de Marseille (CINaM) for providing office space. This work is supported by the French National Research Agency ("France 2030", ANR-16-CONV-0001 from Excellence Initiative of Aix-Marseille University -A*MIDEX and generic grant to P.-F.L. ANR-19-CE13-0022) and the Fondation de la Recherche Médicale (to P.-F.L. EQU202003010407). We also acknowledge the France-Bioimaging Infrastructure (ANR-10-INBS-04). S.T. thanks Daniel Sapede for his invaluable help on implementing multiposition timelapse.


Pursuing Shtuck

Keywords: CCS Concepts:, Theory of computation → Type theory, Control primitives, Constructive mathematics Sheaf, type theory, syntactic model, side-effect, interaction tree

INTRODUCTION

Sheaves are an ubiquitary structure in topos theory [START_REF] Peter | Sketches of an elephant: a Topos theory compendium[END_REF][START_REF] Mac | Sheaves in Geometry and Logic[END_REF], that historically arose from algebraic geometry. They define an important class of topoi called Grothendieck topoi. Abstractly, sheaves can be understood as a refinement of presheaves which preserves more structure from the base category. In the field of logic, they are notably used to prove completeness results over a wide variety of rich deduction systems, and are even claimed to constitute a unifying framework for mathematics [START_REF] Caramello | The unification of Mathematics via Topos Theory[END_REF].

It is a well-known fact that topos theory and type theory are very close objects. Empirically, many techniques developed in one field can be transfered to the other one with a few tweaks. Despite their superficial similarity, the subtle but foundational differences that do exist between them can sometimes result in serious hurdles in the process, though. For instance, porting the dull presheaf construction to type theory proved to be non-trivial and required heavy amendments to overcome issues with intensionality [START_REF] Jaber | The Definitional Side of the Forcing[END_REF][START_REF] Jaber | Extending Type Theory with Forcing[END_REF][START_REF] Pédrot | Russian Constructivism in a Prefascist Theory[END_REF].

Given the paramount importance of sheaves in topos theory on the one hand, and the arguable success of porting presheaves to a type-theoretic setting on the other, it is a natural question to ask whether sheaves are amenable to the same type-theoretic adaptation. So natural that there has actually already been a wealth of research on a generalization of this question to the study of modalities in the context of homotopy type theory [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF]. This line of work, inspired from higher topos theory, led to a somewhat comprehensive literature [START_REF] Quirin | Lawvere-Tierney sheafification in Homotopy Type Theory[END_REF][START_REF] Rijke | Modalities in homotopy type theory[END_REF].

The last paper, notably, contains many non-trivial results and studies a much more general case. It is thus a legitimate question to ask whether there is much more to say on the topic of type-theoretical sheaves. As type theorists leaning towards computer science, we answer positively to this rhetorical question. Thus, taken at face value, the results from this paper are not particularly new, but our point of view is remarkably different.

Our first qualm about the HoTT-style sheafification is its degree of generalization. Abstraction, a landmark of category theory, effectively hides the sheer simplicity of sheaves defined in a pedestrian way. It also has the unfortunate consequence to obscure the kinship of sheaves with well-known structures in computer science. This paper aims at demistifying sheaves for the average type theorist.

The second source of frustration is the complete disconnection of topos theory with computation. And indeed the HoTT account of modalities eschews their computational content, hiding it under non-trivial equality proofs. As staunch supporters of the Curry-Howard correspondence, we believe that it is a categorical imperative of a type-theoretic account of sheaves to expose their operational behaviour. This stance aligns with similar results from classical realizability [START_REF] Krivine | The Curry-Howard Correspondence in Set Theory[END_REF]. It turns out that the underlying side-effect of sheaves is simple, if not disappointing.

Finally, we care about minimalism. As fashionable as HoTT might be, it makes very strong assumptions about the resulting type theory, and is incompatible with a lot of alternative interpretations. In this paper, we study the sheaf model from what we belive to be a neutral intensional ground, essentially a weak variant of CIC. We crucially need a distinguished sort of propositions, Author's address: Pierre-Marie Pédrot, pierre-marie.pedrot@inria.fr, INRIA, France. but we will not even require impredicativity. The validity of the different constructions is then explicitly tied to some additional principles.

THE STANDARD WAY

For completeness of the exposition, we will recall in this section the usual definition of presheaves and sheaves and state the standard results from topos theory we will try to mimic in type theory. In particular, we will work in this section, and only in this section, in a set-theoretic metatheory. Let us fix a small category P that we will call the base category. Definition 2.1. A presheaf is a functor P op → Set.

Lemma 2.2. Presheaves with natural morphisms between them form a topos PSh(P).

A sieve on 𝑝 ∈ P is a set 𝑃 ⊆ Σ𝑞 ∈ P. Hom P (𝑞, 𝑝) that is closed under precomposition. We will write 𝔖 𝑝 for the set of sieves on 𝑝. Definition 2.3. A Grothendieck topology 𝔗 on P is a P-indexed family of collection of sieves, i.e. 𝔗 𝑝 ⊆ 𝔖 𝑝 for all 𝑝 ∈ P, that enjoys the following closure properties.

• If 𝑃 ∈ 𝔗 𝑝 and 𝛼 ∈ Hom P (𝑞, 𝑝) then 𝛼 * 𝑃 ∈ 𝔗 𝑞 where 𝛼 * 𝑃 is the pullback of 𝑃 along 𝛼.

• The maximal sieve on 𝑝 is always in

𝔗 𝑝 . • If 𝑃 ∈ 𝔗 𝑝 , 𝑄 ∈ 𝔖 𝑝 and 𝑃 ⊆ 𝑞 ∈P (𝑞, 𝛼) | 𝛼 ∈ Hom P (𝑞, 𝑝), 𝛼 * 𝑄 ∈ 𝔗 𝑞 then 𝑄 ∈ 𝔗 𝑝 .
We fix a topology 𝔗 in the rest of this section, and recall the main result of interest.

Definition 2.4. Let 𝐴 be a presheaf and 𝑃 ∈ 𝔖 𝑝 . A compatible family of 𝐴 on 𝑃 is a family of elements 𝑥 𝑞,𝛼 ∈ 𝐴 𝑞 for every (𝑞, 𝛼) ∈ 𝑃 that satisfies the equation 𝐴[𝛽] (𝑥 𝑞,𝛼 ) = 𝑥 𝑟,𝛽•𝛼 for all (𝑞, 𝛼) ∈ 𝑃 and 𝛽 ∈ Hom P (𝑟, 𝑞). Definition 2.5. A presheaf 𝐴 is a 𝔗-sheaf whenever for every 𝑃 ∈ 𝔗 𝑝 and every compatible family 𝑥 of 𝐴 on 𝑃 there exists a unique element x ∈ 𝐴 𝑝 s.t. 𝐴[𝛼] ( x) = 𝑥 𝑞,𝛼 for all (𝑞, 𝛼) ∈ 𝑃.

Theorem 2.6. The full subcategory Sh(P, 𝔗) of 𝔗-sheaves is a topos.

Theorem 2.7. The inclusion Sh(P, 𝔗) ⊆ PSh(P) has a left adjoint, called sheafification.

THE BIG PLAN

The starting point of this paper is a very well-known fact about sheaves. As their name implies, sheaves came historically first, and then only in a second time were generalized into presheaves. Surprisingly, it turned out that presheaves were not only providing a rich logical system known as a topos, but also that sheaves could be presented directy from within the presheaf topos itself. Pictorially, it means we have two models

Sh(P, 𝔗) internal sheaf model -→ PSh(P) presheaf model

-→ Set

where the historical or external sheaf model is given by the composition of those two interpretations 1 . Thanks to this factorization, one can then replace PSh(P) with an arbitrary topos [START_REF] Mac | Sheaves in Geometry and Logic[END_REF]. The goal of this paper is to present the internal sheaf model as a translation between type theories rather than between topoi.

Can it be that hard? Despite their similarity, topoi are very weird as type theories. The first oddity is that topoi are defined by their models, rather than by their syntax. Instead, syntax is a derived notion known as the internal language of the topos. This model-theoretic stance has nasty consequences, because the ambient metatheory may surreptitiously flow into the semantics of topoi.

A second source of queasiness is that the internal logic of topoi validates by construction many principles that are absent from MLTT. Some of these principles could be considered desirable, but quite a few are outright anti-features of topos theory. In that regard, Grothendieck topoi are even more outrageous since they inherit a lot of properties from Set, the theory they are built on. We list below a few principles that hold in Grothendieck topoi.

Fig. 1. Major additional principles in presheaf topoi

Equality reflection is notoriously troublesome [START_REF] Hofmann | Extensional constructs in intensional type theory[END_REF][START_REF] Jaber | Extending Type Theory with Forcing[END_REF][START_REF] Oury | Extensionality in the Calculus of Constructions[END_REF][START_REF] Winterhalter | Eliminating reflection from type theory[END_REF] and its absence in intensional type theory is usually the main issue in this kind of endeavour. While we will explicitly require some extensionality principles in some definitions, we will not need reflection at all.

CUTTING THE MIDDLE-MAN

We present here the internal versions of the constructs from Section 2 in a type-theoretical way. We will work in an ambient type theory that we will call SetTT. It can be thought of as an extension of CIC with a few extensionality principles and quotient types. In particular it can be modeled inside any presheaf topos, and the intended standard model is some flavour of setoid type theory [START_REF] Altenkirch | Extensional Equality in Intensional Type Theory[END_REF][START_REF] Altenkirch | Setoid Type Theory -A Syntactic Translation[END_REF][START_REF] Altenkirch | Observational equality, now![END_REF][START_REF] Pujet | Observational Equality: Now For Good[END_REF]. Critically, SetTT has both a full-blown hierarchy of universes Type 𝑖 where 𝑖 ∈ N and a universe of propositions Prop. As usual, we will rely on typical ambiguity although all our constructions can be explicitly annotated. The equality type will implicitly be interpreted as a proposition rather than a proof-relevant Type. For analysis purposes, we will explicitly mention when we rely on principles that are absent from CIC. Let us reassess that we will never rely on equality reflection in this paper. Proof. Sieves on 𝑝 are (local) elements of Prop. The P-indexed family of sets is the functional part of T, and the closure under pullback is saying exactly that it is natural. The two remaining axioms are literally interpreted as the maximal sieve condition and the union condition. □

The standard topos-theoretic phrasing is slightly different because it hardwires propext. In this setting, the above implications are typically written as equalities, and presented in a first-order way using the axiomatics of filters, i.e. as monotonicity w.r.t. predicate inclusion and closure under ∧.

Written this way, it is obvious that a topology is just a monad over Prop. We do not require any of the expected equations because SetTT is implicitly assumed to satisfy proof-irrelevance. In this setting, all equations hold trivially. We will say that a type 𝐴 is a T-sheaf whenever there is some term of type isSh T 𝐴. This lenient phrasing is justified by the proposition below. Proof. With the notations from Definition 4.3, a compatible family of 𝐴 on 𝑃 is just a (local) element of 𝑃 → 𝐴. Unicity of the glueing of the family ensures that the assignement is natural, and thus that we get a function in SetTT. The unicity requirement is translated straightforwardly into its presheaf equivalent. □

Note that the definition of isSh T can be performed inside CIC, it does not require any extensionality principle.

The usual definition of sheafification in an elementary topos relies on Grothendieck's (-) + construction. The type itself can be expressed in CIC very easily, but in absence of unique choice it cannot be exploited. Even with unique choice, it corresponds to an encoding through equivalence classes and has no intrinsic computational content. For completeness of the exposition we write it explicitly below but will not use it further. Assuming SetTT is a topos, then 𝐴 ++ is indeed the sheafification of 𝐴.

A SHEAFY TYPE THEORY 5.1 A Semi-formal Definition of ShTT

Before venturing any further into the type-theoretic exploration of sheaves, we will generalize a bit the structures we are paying attention to. Instead of picking a fixed topology T, we will suppose given two terms I : Type and O : I → Prop, which will be respectively called the input and output types. As explained in Lemma 5.2, the topology case is a simple instance of this situation. Lemma 4.4 still holds with this slightly generalized formulation. From now on, we will say that a type 𝐴 is a sheaf whenever there is a proof of isSh 𝐴, and with a slight abuse of language, we will also call sheaves the inhabitants of □ □. Definition 5.3 (ShTT). We define ShTT as the type theory obtained through the syntactic translation interpreting types as sheaves. Semi-formally, if we present ShTT as a CwF,

• contexts and substitutions of ShTT are those of SetTT

• Γ ⊢ ShTT 𝐴 type := Γ ⊢ SetTT 𝐴 : □ □ • Γ ⊢ ShTT 𝑀 : 𝐴 := Γ ⊢ SetTT 𝑀 : 𝐴.𝜋 1
It is legitimate to call this model a syntactic translation [START_REF] Hofmann | Extensional constructs in intensional type theory[END_REF] because conversion in ShTT is interpreted as conversion in SetTT. In particular, it does not fall into the coherence hell and nowhere we rely on equality reflection to escape from it. As usual we abuse typical ambiguity, but the judgements can be easily annoted with explicit universe levels.

Dependent Products

Lemma 5.4. Assuming funext, dependent products are closed under sheafness on the codomain. Formally, there is a term

Π 𝜀 : Π(𝐴 : Type) (𝐵 : 𝐴 → Type) (𝐵 𝜀 : Π𝑥 : 𝐴. isSh (𝐵 𝑥)). isSh (Π𝑥 : 𝐴. 𝐵 𝑥)
Proof. The oracle function is given pointwise, i.e.

ϙ (Π𝑥:𝐴. 𝐵) (𝑖 : I) (𝑘 : O 𝑖 → Π𝑥 : 𝐴. 𝐵) := 𝜆(𝑥 : 𝐴). ϙ 𝐵 𝑖 (𝜆𝑜 : O 𝑖. 𝑘 𝑜 𝑥)
and uniqueness is proved similarly, although funext is crucially needed for it. □

We insist that this only holds thanks to funext because one needs to rewrite under a context in the unicity proof. This proposition ensures that ShTT has dependent products, regardless of the actual computational content of funext. Since the underlying first projection of the product type of ShTT is the one of SetTT, we will often confuse both.

Free Sheaves

In order to interpret inductive types, we need to define the sheafification functor in an internal way. The usual topos-theoretic definition relies on Grothendieck's (-) + functor. As already mentioned, in the context of type theory, this encoding behaves very badly because it boils down to an encoding of quotients using equivalence classes, which requires some form of choice to be effectively used. Fortunately, sheafification is by design a free construction, given by generators and relations. As such, it can be trivially given by a quotient inductive construction, which we give below. This type will be critical for the remainder of the paper.

Inductive X (𝐴 : Type) : Type := | 𝜂 : Π𝑥 : 𝐴. X 𝐴 | ϙ : Π𝑖 : I. (O 𝑖 → X 𝐴) → X 𝐴 | e : Π(𝑖 : I) ( x : X 𝐴). ϙ 𝑖 (𝜆𝑜 : O 𝑖. x) =
x. This inductive type comes with a recursor specified at Figure 2. Here, we write 𝑢 = 𝑒 𝑃 𝑣 for the heterogeneous equality between 𝑢 : 𝑃 𝑥 and 𝑣 : 𝑃 𝑦 along 𝑒 : 𝑥 = 𝑦 and we write ap : Π{𝐴 : Type} {𝐵 : 𝐴 → Type} (𝑓 : Π𝑥 : 𝐴. 𝐵 𝑥). Π{𝑥 𝑦 : 𝐴} (𝑒 : 𝑥 = 𝑦). 𝑓 𝑥 = 𝑒 𝐵 𝑓 𝑦 for the standard congruence combinator rewriting under an application.

This presentation is agnostic w.r.t. the choice of a semantics of equality. In presence of UIP, the third equation becomes trivial, at least propositionally so. Lemma 5.5. For any 𝐴 : Type, X 𝐴 is a sheaf. Lemma 5.6. Assuming funext, X is a monad. Moreover, sheaves and X-algebras are isomorphic. The reliance on funext in the above lemmas is due to that fact that the internal definition of monads and their algebras are fundamentally given in an extensional way. Without funext, one cannot even prove that the free algebra of an arbitrary monad is indeed an algebra. As a matter of fact, we give these results merely to provide intuition to the functional programmer, but we will not use them in a deep way. Furthermore, as we will see in Section 9, isSh is a better behaved way to define algebras of the free monad X in an intensional setting.

Inductive Types

Following the standard encoding of inductive types in a call-by-name monadic translation, we can interpret inductive types in ShTT simply as their SetTT equivalent, where we freely add the ϙ and e constructors. We give the example of unary natural numbers below. Note in passing that for recursive inductive types, this is not the same as wrapping the corresponding SetTT type into X, since the recursive subterms are also sheafified.

Inductive N X : Type := | O X : N X | S X : N X → N X | ϙ N : Π𝑖 : I. (O 𝑖 → N X ) → N X | e N : Π(𝑖 : I) (𝑛 : N X ). ϙ 𝑖 (𝜆𝑜 : O 𝑖. 𝑛) = 𝑛.
The recursive principle of this inductive type is similar to the one of Figure 2, so we will not write it explicitly here. Now comes the bit of magic that makes sheaves very special. In general, monadic encodings of inductive types do not satisfy dependent elimination, due to the presence of non-standard or effectful terms [START_REF] Pédrot | The fire triangle: how to mix substitution, dependent elimination, and effects[END_REF]. As we will see below, the effects introduced by sheafification are innocuous enough not to introduce observable effects, which allows proving a form of dependent elimination. We focus on the example of sheafified natural numbers to explain what is going on. We will spell out the computational content of the recursor in order to highlight how sheaves escape from the effectful pitfall. Lemma 5.7. Assuming funext and pi, there is a SetTT term

rec X N : Π(𝑃 : N X → □ □). (𝑃 O X ).𝜋 1 → (Π𝑛 : N X . (𝑃 𝑛).𝜋 1 → (𝑃 (S X 𝑛)).𝜋 1 ) → Π(𝑛 : N X ). (𝑃 𝑛).𝜋 1
that furthermore satisfies the definitional equalities

rec X N 𝑃 𝑝 𝑂 𝑝 𝑆 O X ≡ 𝑝 𝑂 rec X N 𝑃 𝑝 𝑂 𝑝 𝑆 (S X 𝑛) ≡ 𝑝 𝑆 𝑛 (rec X N 𝑃 𝑝 𝑂 𝑝 𝑆 𝑛). Proof.
As expected, we prove it by induction over 𝑛. The cases for O X and S X are already given by the definitional equations, so we only have to handle the ϙ N and e N cases.

For the ϙ N case, assume 𝑖 : I and 𝑘 : O 𝑖 → N X , we define rec X N 𝑃 𝑝 𝑂 𝑝 𝑆 (ϙ N 𝑖 𝑘) : (𝑃 (ϙ N 𝑖 𝑘)).𝜋 1 . W.l.o.g. the recursive call provides us with a term of type Π𝑜 : O 𝑖. (𝑃 (𝑘 𝑜)).𝜋 1 . Since ϙ N corresponds to a (free) effect, a standard call-by-name semantics would mandate that we must use the algebra structure of 𝑃 to propagate it outwards. We would thus have to prove Π𝑜 : O 𝑖. (𝑃 (ϙ N 𝑖 𝑘)).𝜋 1 .

There is clearly a type mismatch w.r.t. the recursive call which seems to prevent its use. Yet, we can close the gap using two critical facts.

• First, O 𝑖 is a proposition and thus proof-irrelevant. Together with funext we get a canonical proof of Π(𝑜 : O 𝑖). 𝑘 = (𝜆(_ : O 𝑖). 𝑘 𝑜). • Second, N X enjoys an additional quotient rule e N : Π(𝑖 : I) (𝑛 : N X ). ϙ N 𝑖 (𝜆𝑜 : O 𝑖. 𝑛) = 𝑛.

Combining those two ingredients, we get a canonical proof

𝑟 : Π(𝑖 : I) (𝑘 : O 𝑖 → N X ) (𝑜 : O 𝑖). ϙ N 𝑖 𝑘 = 𝑘 𝑜.
We thus simply define

rec X N 𝑃 𝑝 𝑂 𝑝 𝑆 (ϙ N 𝑖 𝑘) := (𝑃 (ϙ N 𝑖 𝑘)).𝜋 2 .ϙ 𝑖 (𝜆𝑜 : O 𝑖. (𝑟 𝑖 𝑘 𝑜) # (rec X N 𝑃 𝑝 𝑂 𝑝 𝑆 (𝑘 𝑜))
). where # is the transport operation.

For the e N case, given 𝑖 : I, 𝑛 : N X and 𝑝 : (𝑃 𝑛).𝜋 1 we have to prove (𝑃 (ϙ N 𝑖 (𝜆_. 𝑛))).𝜋 2 .ϙ 𝑖 (𝜆_. (𝑟 𝑖 (𝜆_. 𝑛) 𝑜) # 𝑝) = e N 𝑖 𝑛 𝑝 This is easily obtained through standard dependent equality manipulation. We do not even need to resort to UIP, assuming equivalence properties on funext is enough, but having set equality in Prop in SetTT makes this even more trivial. □

Although we do not provide the explicit proof, the same technique scales to the standard class of inductive types available in CIC. Thus, ShTT provides some form of dependent elimination. Contrarily to systems such as Baclofen Type Theory [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF] where elimination must be restricted to strict predicates, ShTT allows arbitrary predicates, even though the interpretation of inductive types features constructors that do not correspond to a value in ShTT. Still, we emphasize that this is not a bona fide large elimination. The first quantification over 𝑃 is not internal to ShTT, since there is no reason a priori for the type N X → □ □ to be a sheaf. To cut the suspense short, it is actually not in general. This failure will be discussed more thoroughly thereafter.

Universe of Propositions

Just as a sheaf topos is indeed a topos, one can equip ShTT with a universe of propositions. We do not have to require uniqueness of glueing because in presence of pi, it will hold trivially. Assuming propext, it is easy to turn this into a universe of propositions inside ShTT. Without loss of generality, we can always freely turn it into an algebra with X, the only hard part being the existence of an element function. We must also provide a proof that the quotient is respected for the e case, that is given 𝑖 : I and 𝐴 : X ⊛ we must show El * (ϙ 𝑖 (𝜆_. 𝐴)) = e 𝑖 𝐴 El * 𝐴 By pi, it is sufficient to provide an equality between the first components, i.e.

(Π𝑜 : O 𝑖. (El * 𝐴).𝜋 1 ) = (El * 𝐴).𝜋 1 which can be proved by a critical appeal to propext. The reverse implication is trivial, and the forward one is a call to the oracle function of El * 𝐴.

This forms a universe of propositions, which can be shown to be closed under all the usual connectives with the standard monadic encoding which we will not make explicit here. Using the dependent eliminator from Lemma 5.7, one can therefore define propositions by recursion. Hence, ShTT features a form of large elimination and goes beyond HOL.

Universe of Types?

Now, it is tempting to apply the same construction to □ □, in order to show that ShTT inherits a hierarchy of universes from SetTT. In other words, we pick the free sheaf completion of □ □ and try to write a function El : X □ □ → □ □ satisfying a few constraints. Unfortunately, this does not seem possible, as a well-known issue arises. Namely, the universe of sheaves is not strictly a sheaf [START_REF] Grothendieck | Éléments de géométrie algébrique : I. Le langage des schémas, Première partie[END_REF].

This issue is surprisingly easy to explain in our setting. First, note that the equation on 𝜂 is constrained to be the identity if we want to follow the weaning translation [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF], which does not seem to be a strong requirement. So the main question is to define El (ϙ 𝑖 𝐾) : □ □ given 𝑖 : I and 𝐾 : O 𝑖 → X □ □. Following the Prop case, it is natural to pick (El (ϙ 𝑖 𝐾)).𝜋 1 := Π(𝑜 : O 𝑖). (El (𝐾 𝑜)).𝜋 1 where the second component is a proof of sheafness obtained out of Π 𝜀 . Now, we simply have to prove that El function preserves the quotient, which is almost the case.

Lemma 5.10. Assuming funext and pi, if 𝐴 : Type is a sheaf then there is an isomorphism 𝐴 (O 𝑖 → 𝐴) for any 𝑖 : I, where the left-to-right function is weakening.

Unluckily, this is not enough for our needs, since we must show that 𝐴 = (O 𝑖 → 𝐴) for an arbitrary sheaf 𝐴, i.e. an equality rather than an isomorphism. There is no reason for this isomorphism to be an equality. Actually, in a wide class of models of CIC, including Set and the presheaf topoi, this equality is disprovable in the general case and only holds when 𝐴 is proof-irrelevant. This mismatch between equality and isomorphism is the reason why stacks were introduced in the first place [START_REF] Grothendieck | Éléments de géométrie algébrique : I. Le langage des schémas, Première partie[END_REF][START_REF] Streicher | Universes in Toposes[END_REF] as more general notion than sheaves.

In our setting, it seems to be possible to side-step this issue using highly non-constructive principles in SetTT, such as global choice. Indeed, if one can pick an arbitrary representative for each equivalence class of sheaves it is possible to work around the requirement of quotient preservation. This is not desirable, for two reasons. First, global choice does not hold in presheaf topoi, so this trick can only be used for sheaves in degenerated models such as Set. Second, it completely destroys the computational content of the theory since one cannot exhibit the representative, effectively turning El into a blocking axiom. This also means one must now rewrite explicitly to show that a code stands for some type, or said otherwise, introducing a coherence hell and the need for equality reflection.

We believe that universes are a critical feature of type theory. We will propose three different solutions which will be developed in Sections 8, 9 and 10.

A SUSTAINED LOOK AT ShTT

We now look at the metatheoretical properties of ShTT. The first result is a trivial adaptation of the topos-theoretic equivalent and is proved by a literal unfolding of the definitions. Theorem 6.1. ShTT is consistent iff SetTT ⊬ X ⊥.

By contrast, the second theorem is not usually discussed in the topos realm. The reason is that it does not make sense in a model-centric view of the world. Yet, it is of paramount importance to a type theorist. Theorem 6.2. ShTT does not enjoy canonicity even if SetTT does. Indeed, translated inductive types have now an additional canonical proof ϙ when compared to CIC. We find this to be highly problematic. In addition to their failure at interpreting large universes, this also means that they feature non-standard tree-like closed inductive terms. In fact, this structure has been known for a long time, because sheafification is essentially an intuitionistic variant of Herbrand trees [START_REF] Herbrand | Recherches sur la théorie de la démonstration[END_REF][START_REF] Rieg | On Forcing and Classical Realizability[END_REF].

A COMPUTATIONAL INTERPRETATION OF ShTT

We elaborate on the above observation and give an intuitive explanation of the computational content of the sheaf model, or, rather a series of explanations.

The major observation is that, written as a tree, sheafification is a member of a large family of relatives known under many names [START_REF] Kiselyov | Freer monads, more extensible effects[END_REF][START_REF] Mcbride | Turing-Completeness Totally Free[END_REF][START_REF] Piróg | The Coinductive Resumption Monad[END_REF][START_REF] Swierstra | Data types à la carte[END_REF][START_REF] Xia | Interaction trees: representing recursive and impure programs in Coq[END_REF], including but not limited to Herbrand trees, interaction trees, free monad, dialogue monad, etc. Amongst these tree-like structures, the free sheaf monad stands out because of three characteristic properties. Specifically, it is inductively defined, branches over a proposition and enjoys an additional quotient enforced by the e constructor.

As such, and similarly to interaction trees, sheafification can be seen as a very specific kind of operating system. A term ϙ 𝑖 𝑘 : X 𝐴 corresponds to a system call where 𝑖 : I is the argument passed to the call, and 𝑘 : O 𝑖 → X 𝐴 is the continuation that will be resumed when the system returns. This operating system is conditioned by the three characteristic properties. It is inductively defined, thus a program can only interact a finite number of times with the system, and in particular it cannot loop. It branches over a proposition, hence a program cannot computationally depend on the return value of a call, i.e. system calls are proof-irrelevant. Finally, the quotient e 𝑖 𝑥 : ϙ 𝑖 (𝜆_. 𝑥) = 𝑥 is a standard property of labelled transition systems. It corresponds to bisimulation up to silent transitions. It equates a system call that does not use its return value, i.e. a silent transition, with the same term that did not perform the call. Both proof-irrelevance and quotienting are necessary to ensure that the operating system does not introduce observable effects in the sense of [START_REF] Pédrot | The fire triangle: how to mix substitution, dependent elimination, and effects[END_REF].

From the user point of view, sheafification in its restricted form can be seen as a way to enlarge the so-called singleton elimination criterion of CIC [START_REF] Gilbert | A type theory with definitional proof-irrelevance[END_REF]. In CIC, there are three archetypical inductive types in Prop that can be eliminated to Type: falsity, equality and accessibility. Sheafification over a monad T allows to relax this restriction to any proposition of the form T 𝑃 where 𝑃 is a singleton.

Finally, we would like to relate the computational content of sheafification with another closely related technique. It is folklore that Cohen's forcing can be presented as a sheaf model [START_REF] Mac | Sheaves in Geometry and Logic[END_REF] for the double-negation monad. Miquel gave a computational interpretation of Cohen's forcing [START_REF] Miquel | Forcing as a Program Transformation[END_REF] from the point of view of classical realizability [START_REF] Krivine | The Curry-Howard Correspondence in Set Theory[END_REF]. One would expect that Miquel's explanation is at least consistent with our description of sheafification. Lemma 7.1. Miquel's presentation of Cohen's forcing can be factorized as a non-standard Lafont-Streicher-Reus CPS [START_REF] Lafont | Continuations Semantics or Expressing Implication by Negation[END_REF] inside a presheaf model.

Proof. In a presheaf model over a monoid, one can define a closed monoidal structure via Day convolution, i.e. the connectives * and - * from separation logic. The LRS CPS only requires a binary conjunction and a negation. Miquel's forcing is isomorphic to LRS over - *and -- * ⊥ ⊥ for a cleverly chosen bottom type. □

In this presentation, there is no explicit tree construction, let alone a quotient. The reason for the simplicity of Miquel's presentation is that it is a model of HOL, rather than MLTT. The quotient construction becomes critical for the topos-theoretic not-so-large elimination, i.e. when constructing a proposition by induction over a term living in a type. Without large elimination, as in HOL, the X construction is useless and one can rely on what amounts to a monadic encoding, here a CPS. Similarly, Beth models [5] can also be presented as a monadic encoding over a presheaf model, without any trace of trees nor quotients.

THE HoTT PATH

There has been much work devoted to the study of generalizations of Lawvere-Tierney topologies in the context of higher topos theory, which was in turn expressed in the context of HoTT [START_REF] Thierry Coquand | Stack semantics of type theory[END_REF][START_REF] Coquand | Constructive sheaf models of type theory[END_REF][START_REF] Quirin | Lawvere-Tierney sheafification in Homotopy Type Theory[END_REF][START_REF] Rijke | Modalities in homotopy type theory[END_REF]. We refer in particular to the comprehensive paper [START_REF] Rijke | Modalities in homotopy type theory[END_REF] which handles the much more general situation of localization. While the latter work subsumes this paper, it also hides the triviality of sheafification under the complexity of localization. In their framework, sheafification is an instance of an accessible topological modality. When restricting our attention to sheaves, much of the paraphernalia they need to design to make the generic localization work trivializes. As we will see, we will not even need to add higher equalities to the sheafness predicate to ensure that it is a mere proposition.

In this section, we replace SetTT with HoTT [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF]. In particular, we assume univalence and the availability of higher inductive types. Equality is now assumed to live in Type, Prop is defined to be the type of mere propositions from a fixed universe, and QITs are interpreted as HITs. We will reuse the previous definitions verbatim up to this implicit relexification. The general miracle is that first, all the results from the SetTT case are lifted to this setting, and more importantly, in presence of univalence ShTT features universes. Lemma 8.1. For any 𝐴, isSh 𝐴 is a mere proposition.

The proof essentially the same as for Lemma 4.4, except that we now globally accept funext as a theorem of HoTT. Lemma 8.2. For any 𝐴, we have an equivalence isSh 𝐴 (Π𝑖 :

I. isEquiv 𝐴 (O 𝑖 → 𝐴) (𝜆(𝑥 : 𝐴) (_ : O 𝑖). 𝑥)).
The above result is once again a generalization of the SetTT case where equivalences are interpreted as isomorphisms. Nonetheless, in presence of univalence it has much farther-reaching consequences. Lemma 8.3. There exists a function El : X □ □ → □ □ s.t.

(El (𝜂 𝑃)).𝜋 1 ≡ 𝑃 .𝜋 1 (El (ϙ 𝑖 𝐾)).𝜋 1 ≡ Π(𝑜 : O 𝑖). El (𝐾 𝑜).𝜋 1 Proof. The 𝜂 and ϙ cases are defined similarly to El * and the failed attempt in SetTT. We face the same problem as before, i.e. given 𝐴 : X □ □ we must prove El (ϙ 𝑖 (𝜆_. 𝐴)) = e 𝑖 𝐴 El 𝐴 Since isSh is a mere proposition, this amounts to

(O 𝑖 → (El 𝐴).𝜋 1 ) = e 𝑖 𝐴 (El 𝐴).𝜋 1
but this is a consequence of univalence and Lemma 8.2. □

In the above proof, we critically used the univalence principle to turn the equivalence 𝐴 (O 𝑖 → 𝐴) into an equality. This was not available in SetTT, where isomorphism does not entail equality in general. This is worth insisting on. The usual workaround of stacks consists in replacing the quotient by a generalized notion externally, i.e. in the Set target after the presheaf interpretation. Univalence allows solving the issue internally, i.e. we did not have to change anything in the definitions of sheafness and sheafification. What changed is the intended standard model of the ambient theory and the principles it provides. Theorem 8.4. There exists a syntactic sheaf model of MLTT into HoTT.

This model was already briefly sketched in a generalized form in [START_REF] Rijke | Modalities in homotopy type theory[END_REF]. It is a trivial variant of the Eilenberg-Moore construction for dependenty type theory as found in the weaning [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF] and exceptional [START_REF] Pédrot | Failure is Not an Option -An Exceptional Type Theory[END_REF] interpretations. Contrarily to the former it interprets unrestricted dependent elimination, and contrarily to the latter, it is consistent with the proviso of Theorem 6.1. Obviously, the pitfall of Theorem 6.2 applies and the result theory totally obliterates canonicity.

ACKNOWLEDGING SIDE-EFFECTS WITH BTT

We have explained previously that sheaves can be understood as an effectful translation that constrains the observation of effects in order to preserve dependent elimination. Instead of adding more equalities as in HoTT to enrich the structure of constrains, what about dropping them altogether? By doing so, we would embrace the possibility of side-effects in our type theory. This point of view is clearly heterodox for the topos-theoretic tradition.

As already mentioned, it turns out that allowing effects in type theory is not free. If we want to preserve the usual equational theory, we also have to weaken dependent elimination. The resulting theory is known as Baclofen Type Theory [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF][START_REF] Pédrot | The fire triangle: how to mix substitution, dependent elimination, and effects[END_REF]. The flip side is that we easily obtain an effectful sheaf syntactic model that features universes, and moreover the translation can be carried in CIC, i.e. we do not need any extensionality principle. The resulting model has already been described as the dialogue interpretation of BTT in [START_REF] Baillon | Gardening with the Pythia A Model of Continuity in a Dependent Setting[END_REF]. For the sake of conciseness we will not spell it out in full here but only recall the key points. That is, assuming extensionality principles one can show that effectful sheaves and D-algebras are isomorphic, but in vanilla CIC a dependent product is an effectful sheaf as soon as its codomain is. Theorem 9.2. There exists a syntactic effectful sheaf model of BTT into CIC [START_REF] Baillon | Gardening with the Pythia A Model of Continuity in a Dependent Setting[END_REF].

The syntactic model simply interprets types as effectful sheaves. In particular, the underlying type of the universe is just D □ □ E and inductive types are interpreted freeely. One still has to define a function El : D □ □ E → □ □ E . This part is underspecified, the major constraint being that El (𝜂 E 𝐴) ≡ 𝐴. In [START_REF] Baillon | Gardening with the Pythia A Model of Continuity in a Dependent Setting[END_REF], El (ϙ E 𝑖 𝑘) is defined as a dummy inhabited type but we can also make the same choice as pure sheaves, i.e. (El (ϙ E 𝑖 𝑘)).𝜋 1 := Π𝑜 : O 𝑖. El (𝑘 𝑜).

The main difference between MLTT and BTT lies in the specialization of inductive recursors in two different primitives. Both enjoy the same computational rules as their MLTT counterpart, but their type is different. The first one is non-dependent, and the second one must be restricted to strict or linear predicates [START_REF] Blain | Contextual isomorphisms[END_REF][START_REF] Munch-Maccagnoni | Syntax and Models of a non-Associative Composition of Programs and Proofs[END_REF]. In this simple case, a function 𝑓 : 𝐴 → 𝐵 is linear exactly when 𝑓 (ϙ E 𝐴 𝑖 𝑘) ≡ ϙ E 𝐵 𝑖 (𝜆𝑜 : O 𝑖. 𝑓 (𝑘 𝑜)) for any 𝑖 : I and 𝑘 : O 𝑖 → 𝐴. Note that when 𝐴 and 𝐵 are pure sheaves this equation holds propositionally under funext and pi. Thus, the pure sheaf quotient can be seen as a way to force all functions to be propositionally linear a priori, while BTT only requires it at dependent elimination time, but definitionally so.

YOU DO NOT NEED SHEAVES WITH SProp

In this section we completely shift our point of view, and rather ponder about the type-theoretical motivations for sheaves. (case for e omitted) which turns structured calls to an implicit oracle 𝛼 : Q into actual, structureless calls to this oracle. If we only consider the above motivations, the difference between X 𝐴 and Q → 𝐴 are not significant, because both types validate the Q axiom.

So, what happens if instead of doing such a complex and half-broken model as ShTT, we would simply consider the theory AxTT obtained by the trivial axiomatic syntactic model of CIC which simply adds a variable 𝛼 : Q to all contexts? Such a model is readily available in all proof assistants, e.g. in Coq it amounts to postulating a global Axiom.

Is AxTT any better than ShTT? On the good side, AxTT is a full-blown model of CIC, in particular it interprets universes trivially. Since O is a Prop, it is also compatible with the erasure semantics of extraction and thus compatible with most flavours of realizability. On the bad side, consistency is harder to prove since one has to provide a distinct model, which sort of defeats the purpose of sheaves. Worse, canonicity is still broken in general as axioms block computation. Still, for some specific instances of O, one can recover canonicity. This is the case when all values of O are negated and AxTT is consistent [START_REF] Thierry Coquand | Negative consistent axioms can be postulated without loss of canonicity[END_REF].

We propose below a generalization of this result by relying on a sort of strict propositions [START_REF] Altenkirch | Extensional Equality in Intensional Type Theory[END_REF][START_REF] Gilbert | Definitional proof-irrelevance without K[END_REF]. In the remainder of this section, we will extend our ambient theory with a sort SProp as described in [START_REF] Gilbert | Definitional proof-irrelevance without K[END_REF]. Intuitively, SProp is similar to the sort Prop of CIC, save for two major differences. First, all inhabitants of a type 𝐴 : SProp, hereafter called a strict proposition, are convertible. Second, to preserve decidability of the resulting theory the singleton elimination criterion of Prop is even stricter for SProp. Indeed, only empty types can be eliminated from SProp to another sort.

This restriction can be seen as a semantic trick to guarantee that only logical explosions can leak from strict propositions to relevant types. And as expected, it generalizes the canonicity result of [START_REF] Thierry Coquand | Negative consistent axioms can be postulated without loss of canonicity[END_REF].

Definition 10.1. We say that a context Γ is consistent whenever there is no term Γ ⊢ 𝑀 : ⊥. Definition 10.2. We say that a context is propositional if it is inductively built of strict propositions only.

Theorem 10.3 (Relative Canonicity). If Γ is a consistent propositional context and Γ ⊢ 𝑀 : N then 𝑀 ≡ O or there exists Γ ⊢ 𝑁 : N such that 𝑀 ≡ S 𝑁 .

Proof. The proof is a variant of the one from [START_REF] Thierry Coquand | Negative consistent axioms can be postulated without loss of canonicity[END_REF] and can be presented as a NbE argument. It was written in Agda as a trivial extension of the formalization of [START_REF] Gilbert | Definitional proof-irrelevance without K[END_REF]. The result can be generalized to an arbitrary inductive type. See also [START_REF] Coquand | Reduction Free Normalisation for a proof irrelevant type of propositions[END_REF] for a similar endeavour. □

It is now only a matter of putting all the pieces together. If we pick O : I → SProp instead of returning a Prop, by adding a global axiom 𝛼 : Π𝑖 : I. O 𝑖 we still get a theory AxTT that models CIC, as well as strict propositions. But by Theorem 10.3, AxTT enjoys canonicity as long as the axiom is consistent. Therefore, if the only goal of sheaves is to force truth, AxTT is arguably better than ShTT. It is worth mentioning that presheaf models implement strict propositions when presented as prefascist types [START_REF] Pédrot | Russian Constructivism in a Prefascist Theory[END_REF], so we can simply compose those two translations.

When ShTT Hits the Fan

If it is so easy to postulate axioms, why do we need sheaves at all? A priori, there is no reason for the two types X 𝐴 and Q → 𝐴 to be isomorphic. The first one exposes the list of calls to the oracle, while the second one does not. The call trace of X 𝐴 is not completely available though, because of the quotient. Most notably, one cannot observe the relative order between two calls, nor superfluous calls that do not use their return value. Still, by induction we merely know that there is a finite amount of calls for X 𝐴, but not for Q → 𝐴. This makes those two types different in some contexts. For instance, if we instantiate SetTT by a presheaf model where propositions are interpreted as opens of R, with I := N and O 𝑖 := ]0, 1 𝑖 [, we have Q 0 so Q → 𝐴 is always trivial but X 𝐴 is not in general because 𝑖 ∈𝐼 O 𝑖 is non-empty for any finite 𝐼 .

We believe that this is the fundamental mismatch between ShTT and AxTT. Fortunately for us, what a strict axiom taketh, a strict axiom giveth. Such a mismatch between a higher-order function and a finite tree is a well-known phenomenon, which has a well-known solution, bar induction provided by the fan functional.

The historical presentation of bar induction is somewhat confusing. We will follow the modern presentation of Sterling [START_REF] Sterling | Higher order functions and Brouwer's thesis[END_REF], which is very easy to convey in a type-theoretic setting. We define at Figure 3 the Q-continuity predicate C : Π{𝐴 : Type}. (Q → 𝐴) → SProp. Note that this predicate does not require O to be proposition.

Intuitively, this predicate captures the fact that a higher-order function has been obtained by the evaluation of a call tree. As expected, one can easily show the following in SetTT. What is missing, and as already explained not true in an arbitrary presheaf model, is that all functions are Q-continuous. A modern way to phrase Brouwer's bar induction is precisely that. The validity of bar induction is a sensitive topic in MLTT, because it can make the theory inconsistent when phrased too proof-relevantly, in particular when expressed as a fan functional that computes the module of continuity of functions [START_REF] Hötzel | The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation[END_REF]. This paradox does not apply here because C is a strict proposition.

We believe that we can bridge the gap between AxTT and ShTT using a similar principle. We know that inductive types in ShTT are intepreted as free sheaves in SetTT. Hence, in theory we could reflect this into AxTT by adding bar induction axioms for every inductive type, i.e. if I is a first-order inductive type we have an axiom bi I : Π(𝑥 : Q → I). C 𝑥.

We do not currently know whether such a set of axioms would be consistent in CIC. If it were the case, since the added axioms are propositional, by virtue of Theorem 10.3 the resulting variant of AxTT would still enjoy canonicity, while behaving essentially as ShTT.

We leave to further investigation the design of a theory that would validate these principles. In any case, the above discussion shows that there is a strong interplay between the nature of Prop and the kind of sheaves it allows. Also, while the use of sheaves to study continuity is folklore [START_REF] Fourman | Sheaf models for analysis[END_REF][START_REF] Peter | On a Topological Topos[END_REF][START_REF] Xu | A continuous computational interpretation of type theories[END_REF], the fact that sheaves are essentially enforcing a generalized continuity property does not seem to have been exposed so clearly.

CONCLUSION AND FUTURE WORK

We gave in this paper a straightforward description of sheaves as a specific kind of interaction trees. This description is internal to a generic type theory and can be written in CIC. By contrast, the existence of free sheaves relies on the availability of a particular quotient inductive type and, as usual for this kind of structures, introduces issues w.r.t. propositional equality. Through this presentation, the quasi-effectful nature of sheafification becomes obvious. Sheaves thus provide yet another insight into ruling out ill-behaved effectful proofs.

We believe that the use of strict propositions can lead to a generalization of ShTT in the style of [START_REF] Coquand | A Note on Forcing and Type Theory[END_REF], using more complex structures for the input and output types. More generally, the interaction of sheaves with definitional equality, and the existence of definitional sheaves is also an important question which deserves further study. We leave this for future work.

  Functional extensionality funext : Π𝐴 𝐵 (𝑓 𝑔 : Π𝑥 : 𝐴. 𝐵 𝑥). (Π𝑥 : 𝐴. 𝑓 𝑥 = 𝑔 𝑥) → 𝑓 = 𝑔 Propositional extensionality propext : Π(𝑃 𝑄 : Prop). (𝑃 → 𝑄) → (𝑄 → 𝑃) → 𝑃 = 𝑄 Proof-irrelevance pi : Π(𝑃 : Prop) (𝑝 𝑞 : 𝑃). 𝑝 = 𝑞 Unique choice uc : Π(𝐴 : Type) (𝑃 : 𝐴 → Prop). (∃!𝑥 : 𝐴. 𝑃 𝑥) → Σ𝑥 : 𝐴. 𝑃 𝑥 Equality reflection Γ ⊢ 𝐸 : 𝑀 = 𝑁 Γ ⊢ 𝑀 ≡ 𝑁 Quotient types . . .

Definition 4 . 1 .

 41 A Lawvere-Tierney topology is a triple• T : Prop → Prop • 𝜂 T : Π𝑃 : Prop. 𝑃 → T 𝑃 • > >= T : Π(𝑃 𝑄 : Prop). T 𝑃 → (𝑃 → T 𝑄) → T 𝑄 Lemma 4.2.Lawvere-Tierney topologies in the presheaf model of CIC are exactly Grothendieck topologies.

Definition 4 . 3 .

 43 We define the record type isSh T as isSh T (𝐴 : Type) : Type := Sh T ϙ : Π(𝑃 : Prop). T 𝑃 → (𝑃 → 𝐴) → 𝐴 e : Π𝑃 (𝑝 : T 𝑃) (𝑥 : 𝐴). ϙ 𝑃 𝑝 (𝜆𝑜 : 𝑃 . 𝑥) = 𝑥

Lemma 4 . 4 .

 44 Assuming funext and pi, isSh T 𝐴 is a mere proposition, i.e. there is a proof Π(𝐴 : Type) (𝑝 𝑞 : isSh T 𝐴). 𝑝 = 𝑞 Lemma 4.5. Let 𝐴 : Type. 𝐴 is a T-sheaf in the sense of Definition 4.3 in the presheaf model exactly when 𝐴 is a T-sheaf in the sense of Definition 2.5.

Definition 4 . 6 .

 46 Let Prop T := Σ𝑃 : Prop. (T 𝑃 → 𝑃) and 𝐴 : Type, we define 𝐴 + := Σ𝑃 : 𝐴 → Prop T . T (∃𝑥 : 𝐴. (Π𝑦 : 𝐴. (𝑃 𝑦).𝜋 1 ↔ T (𝑥 = 𝑦))).

Definition 5. 1 .

 1 We define the record type isSh as isSh (𝐴 : Type) : Type := Sh ϙ : Π𝑖 : I. (O 𝑖 → 𝐴) → 𝐴 e : Π(𝑖 : I) (𝑥 : 𝐴). ϙ 𝑖 (𝜆𝑜 : O 𝑖. 𝑥) = 𝑥 For brevity, we will define □ □ := Σ𝐴 : Type. isSh 𝐴. Lemma 5.2. Up to a trivial curryfication, Definition 4.3 is obtained by setting I := Σ𝑃 : Prop. T 𝑃 O (𝑃, _) := 𝑃.

  rec

Definition 5. 8 .

 8 We define the type of sheaf propositions ⊛ similarly to □ □, i.e. ⊛ := Σ𝑃 : Prop. (Π𝑖 : I. (O 𝑖 → 𝑃) → 𝑃).

Lemma 5. 9 .

 9 Assuming propext, we define El * : X ⊛ → ⊛ as El * (𝜂 𝑃) := 𝑃 El * (ϙ 𝑖 𝐾) := (Π𝑜 : O 𝑖. El * (𝐾 𝑜).𝜋 1 , 𝜑 𝑖 𝐾) where 𝜑 : Π(𝑖 : I) (𝐾 : O 𝑖 → X ⊛ ) ( 𝑗 : I). (Π(𝑞 : O 𝑗) (𝑜 : O 𝑖). (El * (𝐾 𝑜)).𝜋 1 ) → Π(𝑜 : O 𝑖). (El * (𝐾 𝑜)).𝜋 1 𝜑 := 𝜆(𝑖 : I) 𝐾 ( 𝑗 : I) 𝑘 (𝑜 : O 𝑖). (El * (𝐾 𝑜)).𝜋 2 𝑗 (𝜆(𝑞 : O 𝑗). 𝑘 𝑞 𝑜).

Definition 9 . 1 .

 91 Let isSh E (𝐴 : Type) := Π𝑖 : I. (O 𝑖 → 𝐴) → 𝐴. We will define the type of effectful sheaves as □ □ E := Σ𝐴 : Type. isSh E 𝐴. Contrarily to usual sheaves, this structure need not be a mere proposition. But it is an intensionally well-behaved way to define algebras of the dialogue monad Inductive D (𝐴 : Type) : Type := 𝜂 E : 𝐴 → D 𝐴 | ϙ E : Π𝑖 : I. (O 𝑖 → 𝐴) → 𝐴.

10. 1

 1 Admit It Topologically, sheaves are a way to force locally true properties to become globally true. Rephrased type-theoretically, T-sheaves allow one to consider T-true propositions as if they were actually true, i.e. ShTT morally 2 validates the axiom Π(𝑃 : Prop). T 𝑃 → 𝑃. In our generalized case, this literally corresponds to forcing Q := Π(𝑖 : I). O 𝑖 to hold up to curryfication. More formally, in SetTT one can write an evaluation function 𝜀 : Π{𝐴 : Type}. X 𝐴 → Q → 𝐴 𝜀 (𝜂 𝑥) 𝛼 := 𝑥 𝜀 (ϙ 𝑖 𝑘) 𝛼 := 𝜀 (𝑘 (𝛼 𝑖)) 𝛼

Lemma 10 . 4 .Fig. 3 .

 1043 Fig. 3. Inductive characterization of Q-continuity

Definition 10 . 5 .

 105 Let us locally pose I := N and O := 𝜆(_ : I). N. We define Brouwer's bar induction to be the principle bi := Π(𝑓 : (N → N) → N). C 𝑓 .

  𝐴 𝑃 𝑝 𝜂 𝑝 ϙ 𝑝 e (𝜂 𝑥) ≡ 𝑝 𝜂 𝑥 rec X 𝐴 𝑃 𝑝 𝜂 𝑝 ϙ 𝑝 e (ϙ 𝑖 𝑘) ≡ 𝑝 ϙ 𝑖 𝑘 (𝜆𝑜 : O 𝑖. rec X 𝐴 𝑃 𝑝 𝜂 𝑝 ϙ 𝑝 e (𝑘 𝑜)) ap (rec X 𝐴 𝑃 𝑝 𝜂 𝑝 ϙ 𝑝 e ) (e 𝑖 x) ≡ 𝑝 e 𝑖 x (rec X 𝐴 𝑃 𝑝 𝜂 𝑝 ϙ 𝑝 e ) x

		𝑝).
		𝑃
	Π( x : X 𝐴). 𝑃	x
	rec X Fig. 2. Recursor for the X type

X : Π(𝐴 : Type) (𝑃 : X 𝐴 → Type). Π(𝑝 𝜂 : Π𝑥 : 𝐴. 𝑃 (𝜂 𝑥)). Π(𝑝 ϙ : Π(𝑖 : I) (𝑘 : Π𝑜 : O 𝑖. X 𝐴). (Π𝑜 : O 𝑖. 𝑃 (𝑘 𝑜)) → 𝑃 (ϙ 𝑖 𝑘)). Π(𝑝 e : Π(𝑖 : I) ( x : X 𝐴) (𝑝 : 𝑃 x). 𝑝 ϙ 𝑖 (𝜆𝑜 : O 𝑖. x) (𝜆𝑜 : O 𝑖. 𝑝) = e 𝑖 x

We insist that these arrows are not functors, but instead interpretations of a theory into another theory.

Assuming T can be reflected from SetTT to ShTT.