$\P_{\mathsf{ext}}\to\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbb{I}\cong\mathbf{1}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbb{I}\cong\mathbf{1}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbb{I}\cong\mathbf{1}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbb{I}\cong\mathbf{1}$}\mathclose{}{)}}$
holds. The purpose of this axiom is as follows: if $\mathbb{I}$ is
$\P_{\mathsf{ext}}$-connected in the above sense, any path $\mathbb{I}\to A$
restricts to a _constant_ function under $\P_{\mathsf{ext}}$; thus we always
have $\P_{\mathsf{ext}}\land x\sqsubseteq_{A}y\to x=y$. Thus in the presence
of this axiom, any synthetic preorder is “partially discrete” in the sense of
being discrete as soon as $\P_{\mathsf{ext}}=\top$.

We now summarize the axiomatics of _synthetic partially discrete preorder
theory_ for an arbitrary elementary QWI-topos $\mathscr{E}$.

###### Axiom 4.27.

We assume a proposition $\P_{\mathsf{ext}}:\Omega$.

###### Axiom 4.28.

We assume a type $\mathbb{I}$ together with two elements $0,1:\mathbb{I}$.

###### Axiom 4.29.

The interval object $\mathbb{I}$ of Axiom 4.28 is
$\P_{\mathsf{ext}}$-connected.

###### Axiom 4.30.

The interval object $\mathbb{I}$ of Axiom 4.28 satisfies the Phoa principle
(Definition 4.18).

###### Definition 4.31.

Let $\mathscr{E}$ be an elementary QWI-topos.

  1. (1)

We say that $\mathscr{E}$ is a _model of synthetic preorder theory_ when it
satisfies Axioms 4.28 and 4.30.

  2. (2)

If $\mathscr{E}$ additionally satisfies Axioms 4.27 and 4.29, then we call it
a _model of synthetic partially discrete preorder theory_.

Given a model of synthetic partially discrete preorder theory $\mathscr{E}$,
we say that $\mathscr{E}$ is _well-adapted_ when there is a fully faithful
functor $\mathbf{Preord}\hookrightarrow\mathscr{E}$ whose image lies within
the $\P_{\mathsf{ext}}$-connected types, _i.e_. those that restrict under
$\P_{\mathsf{ext}}$ to a singleton. This terminology is inspired by an
analogous situation in _synthetic differential geometry_ where a topos model
$\mathscr{E}$ is called well-adapted (Dubuc, 1979) when there is an embedding
of ordinary manifolds into $\mathscr{E}$ that preserves the differential
geometry structure.

###  4.4. Algebra models of decalf in synthetic partially discrete preorder
theory

In this section, we describe how to instantiate the constructs of decalf in
any model $\mathscr{E}$ of synthetic partially discrete preorder theory in the
sense of Definition 4.31. To construct our model, we fix universes
$\mathcal{U}\in\mathcal{V}$ in $\mathscr{E}$; judgments of calf are intepreted
in the outer universe $\mathcal{V}$. We will write
$\mathcal{U}_{\mathsf{P}}\subseteq\mathcal{U}$ for the subuniverse of
$\mathcal{U}$ spanned by synthetic preorders, _i.e_. path-transitive and
boundary separated types.

####  4.4.1. Cost structure

The theory of decalf is parameterized by a cost monoid
$\mathbb{C}:\mathcal{U}_{\mathsf{P}}$ that is $\P_{\mathsf{ext}}$-connected,
_i.e_. becomes a singleton when $\P_{\mathsf{ext}}$ is true. In a well-adapted
model of synthetic preorder theory $\mathscr{E}$ in the sense of Section 4.3,
we may take an ordinary preordered monoid $P$ and define $\mathbb{C}$ as the
image of $P$ under the full embedding
$\mathbf{Preord}\hookrightarrow\mathscr{E}$. An alternative method would be to
define the cost monoid $\mathbb{C}$ as a quotient inductive type that builds
in the expected order structure. For instance, we may define the synthetic
preorder $\omega$ that can be thought of as the colimit of the inclusions of
finite chains $\mathbb{I}_{0}\to\mathbb{I}_{1}\to\dots$ by means of a quotient
inductive type:

  * ${\textbf{data}}~{}\omega:\mathcal{U}_{\mathsf{P}}~{}{\textbf{where}}$

    * $\mathsf{zero}:\omega$

    * $\mathsf{suc}:\omega\to\omega$

    * $\mathsf{rel}:\omega\to\mathbb{I}\to\omega$

    * $\\_:\mathchoice{\mathopen{}{(}\hbox{$\displaystyle n:\omega$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle n:\omega$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle n:\omega$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle n:\omega$}\mathclose{}{)}}\to\mathsf{rel}\,n\,0=n$

    * $\\_:\mathchoice{\mathopen{}{(}\hbox{$\displaystyle n:\omega$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle n:\omega$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle n:\omega$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle n:\omega$}\mathclose{}{)}}\to\mathsf{rel}\,n\,1=\mathsf{suc}\,n$

Note that this is _not_ the natural numbers type of the synthetic preorders as
the latter is discrete. It can be seen, however, that $\omega$ as defined
above is $\P_{\mathsf{ext}}$-connected, since in that case we would have
$n=\mathsf{rel}\,n\,0=\mathsf{rel}\,n\,1=\mathsf{suc}(n)$.

####  4.4.2. Monads for effects

Let $M$ be a (strong) monad on $\mathcal{U}$. The monad $M$ may not preserve
the property of being a synthetic preorder, but we may adapt it to a monad
$M_{\mathsf{P}}$ on $\mathcal{U}_{\mathsf{P}}$ by postprocessing with the
synthetic preorder reflection, sending $A:\mathcal{U}_{\mathsf{P}}$ to
$\mathsf{P}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
MA$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
MA$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
MA$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
MA$}\mathclose{}{)}}$.999If $M$ does preserve synthetic preorders, then we
have $M_{\mathsf{P}}\cong M$ as reflections are idempotent. We can then adapt
$M_{\mathsf{P}}$ to support a cost effect using the _cost monad transformer_
corresponding to the writer monad $\mathbb{C}\times-$. In particular, we
define a new monad $T$ on $\mathcal{U}_{\mathsf{P}}$ by the assignment
$TA\coloneq
M_{\mathsf{P}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbb{C}\times-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbb{C}\times-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbb{C}\times-$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbb{C}\times-$}\mathclose{}{)}}$.

  1. (1)

For verifying pure code (as in calf), we can let $M$ be the identity monad.

  2. (2)

For nondeterminism (as in Section 3.2.1), we can let $M$ be the _free
semilattice_ monad, which can be defined by a quotient inductive type.

  3. (3)

For probabilistic choice (as in Section 3.2.2), we can let $M$ be the _free
convex space_ monad, which is likewise (constructively) definable by a
quotient inductive type.101010Classically this is equivalent to the finite
distribution monad; in our definitions we must be careful to give constructive
definitions because the logic of $\mathscr{E}$ is not classical.

  4. (4)

For global state (as in Section 3.2.3), we let $M$ be the state monad $S\to
S\times-$ for a given synthetic preorder $S$.

As an alternative to defining $T$ using the cost monad transformer as above,
we can also treat the effect signatures of Section 3.2 as specifications of an
algebraic effect, where for each $c:\mathbb{C}$ we have a generating operation
$\mathsf{step}^{c}$. In such cases, we can simply define $T$ as the _free_
monad for these effect signature using a quotient inductive type.

####  4.4.3. Universes of positive and negative types

We then define $\mathsf{tp}^{+}$ to be $\mathcal{U}_{\mathsf{P}}$ itself,
letting $\mathsf{tm}^{+}(A):\mathsf{tp}^{+}\to\mathbf{Jdg}$ be the image of
$A:\mathcal{U}_{\mathsf{P}}$ under the inclusion
$\mathcal{U}_{\mathsf{P}}\hookrightarrow\mathcal{V}$, which we shall leave
implicit in our informal notations. We interpret $\mathsf{tp}^{\ominus}$ by
the type of $T$-algebras where $T$ is the application of the cost monad
transformer to a monad $M$ from Section 4.4.2, which we may equip, as we
please, with the structure of the Eilenberg–Moore category. Then
$\mathsf{tm}^{\ominus}(X)$ is interpreted the same as
$\mathsf{tm}^{+}(\mathsf{U}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
X$}\mathclose{}{)}})$. Thus we have a free-forgetful adjunction
$\mathsf{F}\dashv\mathsf{U}:\mathsf{tp}^{\ominus}\to\mathsf{tp}^{+}$
interpreting the call-by-push-value adjunctive structure of decalf.

####  4.4.4. Inequality relation

For any type $A:\mathsf{tp}^{+}$ and elements $x,y:\mathsf{tm}^{+}(A)$, the
inequality $x\leq y$ is interpreted by the path relation
$x\sqsubseteq_{\mathsf{tm}^{+}(A)}y$, which is transitive because $A$ lies in
$\mathcal{U}_{\mathsf{P}}$. The $\leq_{\textsf{ext}}$ axiom is a consequence
of the partial discreteness axiom (Axiom 4.29) that we have assumed of
$\mathscr{E}$; the $\leq_{\textsf{mono}}$ axiom holds by definition. The
$\leq_{\textsf{pi}}$ axiom holds by Lemma 4.15, as every synthetic preorder is
boundary separated.

###  4.5. A presheaf model of decalf in augmented simplicial sets

####  4.5.1. Simplicial sets for synthetic preorders

To model synthetic preorders in a QWI-topos, we take a cue from higher
category theory and consider _simplicial sets_ , which are presheaves on the
simplex category defined below.

###### Definition 4.32 (Simplex category).

We will write $\mathbf{\Delta}$ for the _simplex category_ , _i.e_. the
category of inhabited finite ordinals
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
n$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
n$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
n$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
n$}\mathclose{}{]}}$ and order-preserving maps between them. By convention,
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
0$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
0$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
0$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
0$}\mathclose{}{]}}$ will denote the singleton ordinal, _i.e_. the terminal
object of $\mathbf{\Delta}$.

What do simplicial sets have to do with preorders? Every preorder can be
reconstructed by gluing simplices together in a canonical way; this is the
_density_ of the embedding $I:\mathbf{\Delta}\hookrightarrow\mathbf{Preord}$,
which implies that the corresponding nerve functor
$N:\mathbf{Preord}\to\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}$
sending a preorder $P$ to the restricted hom presheaf
$\hom_{\mathbf{Preord}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
I-,P$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
I-,P$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
I-,P$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
I-,P$}\mathclose{}{)}}$ is fully faithful. In this way, simplicial sets are an
appropriate place to study concrete preorders; this is the content of a well-
adapted model as defined in Section 4.3. The synthetic preorder theory of
simplicial sets, then, studies sufficient conditions in the internal language
for arbitrary simplicial sets to “behave like” those that arise from actual
preorders via the nerve functor $N$.

###### Theorem 4.33.

The category
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}$
of simplicial sets forms a non-trivial model of _synthetic preorder theory_ in
the sense of Definition 4.31 in which the interval is given by the
representable presheaf
$\mathbf{y}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}$ and its two global points.

####  4.5.2. Augmented simplicial sets for synthetic partially discrete
preorders

In fact,
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}$
also forms a (highly degenerate) model of _synthetic partially discrete
preorder theory_ in the sense of Definition 4.31, setting
$\P_{\mathsf{ext}}\coloneq\bot$. Our goal is to find a _non-trivial_ model
$\mathscr{E}$, _i.e_. where the slice $\mathscr{E}/\P_{\mathsf{ext}}$ is not
the terminal category. The most canonical choice for such a topos is obtained
by _freely extending_
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}$
with a maximal topos-theoretic point by forming an “inverted Sierpiński cone”,
_i.e_. the Artin gluing (Artin et al., 1972) of the constant presheaves
functor
${\textbf{Set}}\to\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}$.
This gluing can also be presented equivalently by presheaves on a different
category, as adding a maximal point to a presheaf topos corresponds (dually)
to freely extending the base category by an initial object — which amounts in
the case of $\mathbf{\Delta}$ to the use of _augmented simplicial sets_. These
two perspectives on the same topos are both useful, and play a role in our
results.

###### Definition 4.34 (Augmented simplex category).

We will write $\mathbf{\Delta}_{\bot}$ for the _augmented simplex category_ ,
the free extension of $\mathbf{\Delta}$ by an initial object
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-1$}\mathclose{}{]}}$.
Concretely, $\mathbf{\Delta}_{\bot}$ can be thought of as the category of
_arbitrary_ finite ordinals and order-preserving maps between them; under this
interpretation,
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-1$}\mathclose{}{]}}$
corresponds to the empty ordinal.

###### Theorem 4.35.

The category
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$
of _augmented simplicial sets_ forms a non-trivial well-adapted model of
_synthetic partially discrete preorder theory_ in the sense of Definition 4.31
in which:

  1. (1)

the interval is given by the representable presheaf
$\mathbb{I}\coloneq\mathbf{y}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}$;

  2. (2)

and the phase distinction is given by the representable subterminal presheaf
$\P_{\mathsf{ext}}\coloneq\mathbf{y}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-1$}\mathclose{}{]}}$.

####  4.5.3. Soundness of decalf

The following soundness theorem is a corollary of Theorem 4.35 via the
description of algebra models of decalf in Section 4.4.

###### Theorem 4.36 (Soundness).

For any of the notions of computational effect considered in Section 3.2, we
have a non-trivial model of the decalf theory in
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$.

##  5\. Conclusion

In this work, we presented decalf, an inequational extension of calf (Niu et
al., 2022a) that supports precise and approximate bounds on the cost and
effect structure of programs. Throughout the development, our guiding
principle has been that a _cost bound for an effectful program should be
another effectful program._

In Section 3, we demonstrated this methodology through a variety of case
studies. For pure, first-order algorithms, we were able to provide simple
proofs of combined cost and correctness. Such proofs in decalf are more
streamlined than their calf counterparts and can be carried out without
reference to any separable notion of recurrence. Instead, the code itself
serves the role of the recurrence, which we then solve for a closed form,
either exactly using equality or loosely using inequality. Then, using the
extensional modality, we were able to extract extensional equalities from both
equality and inequality program bounds. For example, from the cost and
correctness proofs of various sorting algorithms, we may determine immediately
that all the given sorting algorithms are extensionally equal. This approach
scaled naturally to support more complex classes of programs, including
higher-order programs with non-cost effects.

In Section 4, we justified this style of reasoning using the notion of a
_synthetic partially discrete preorder theory_ , a novel formulation of an
_intrinsic_ theory of preorders that smoothly integrates with the existing
intension-extension phase distinction of calf. To obtain a model of this new
theory, we draw inspiration from both work in directed type theory and
synthetic domain theory and characterize the synthetic preorders using simple
orthogonality conditions, which furnish a well-behaved subuniverse that
supports the structures for workaday program verification.

Ab initio, the theory of decalf has been forged and guided by the pragmatic
struggles encountered in cost analysis and program verification. Building on
the work of Niu et al. (2022b), the definition of decalf and the examples
presented have been partially mechanized in the Agda proof assistant (Norell,
2009), and we are working on improving the development of the existing case
studies in calf by adapting them to the decalf setting.

###  5.1. Future Work

We see these decalf perspectives as a starting point for deeper investigations
into related ideas.

##### Amortized analysis via coinduction

As discussed in Section 1.5, our approach draws inspiration from Grodin and
Harper (2023), who perform amortized analyses in calf for programs whose only
effect is cost. However, we do not in this work consider connecting amortized
analysis to our story involving effects and inexact bounds due to the lack of
negative sums in decalf. We anticipate that the techniques developed here
could be combined with those of _op. cit_. to perform a broader class of
amortized analyses.

##### Advanced probabilistic reasoning

In Section 3.2.2, we implement a simple probabilistic program and show an
exact bound on its cost. However, many algorithms in practice do not have
well-behaved distributions, so one may instead wish to analyze expected and
high probability bounds. We believe that the techniques presented here will
scale to support such reasoning in future work.

##### Parallelism and effects

As mentioned in Section 3.4, while parallelism is compatible with pure
algorithms in decalf, we leave a proper theory of the interaction between
parallelism and other effects to future work.

##### More sophisticated effects

It would be useful to consider a semantics for decalf that goes beyond the
simple, non-enriched algebraic effects we have considered here, allowing for
constructs like control or unbounded recursion.

##### Abstraction and specification implementations

One drawback of decalf, inherited from calf, is that in order to describe a
concise cost bound for a program, one must be able to compute the result of
the computation as a complex value (Levy, 2003, §3) via a “specification”
implementation. Unfortunately, this puts abstraction at odds with cost
analysis: in order to export a bound of an abstract computation, one must also
specify the return value, allowing a client to compute results cost-free if
desired. We observe a similarity to frameworks based on program logics, in
which one sometimes verifies an effectful (there, imperative; here, costly)
algorithm by first providing a functional specification (for instance, see the
case study on list fold in Iris (Birkedal and Bizjak, 2022)). We hope this
tension can be resolved in future iterations of decalf.

###### Acknowledgements.

We are grateful to Marcelo Fiore, Runming Li, and Parth Shastri for many
insightful discussions. This work was supported in part by Sponsor AFOSR
https://www.afrl.af.mil/AFOSR/ (Tristan Nguyen, program manager) under grants
Grant #MURI FA9550-15-1-0053, Grant #FA9550-19-1-0216, and Grant
#FA9550-21-0009, and in part by the Sponsor National Science Foundation
https://nsf.gov under award number Grant #CCF-1901381, and by Sponsor AFRL
https://afresearchlab.com/ through the Grant #NDSEG fellowship. This work was
co-funded by the European Union under the Sponsor Marie Skłodowska-Curie
Actions https://cordis.europa.eu/programme/id/HORIZON.1.2/en Postdoctoral
Fellowship grant agreement Grant #101065303. Any opinions, findings and
conclusions or recommendations expressed in this material are those of the
authors and do not necessarily reflect the views of the AFOSR, NSF, AFRL, the
European Union, or the European Commission. Neither the European Union nor the
granting authority can be held responsible for them.

## References

  * (1)
  * Artin et al. (1972) Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier. 1972\.  _Théorie des topos et cohomologie étale des schémas_. Lecture Notes in Mathematics, Vol. 269, 270, 305.  Springer-Verlag, Berlin.  Séminaire de Géométrie Algébrique du Bois-Marie 1963–1964 (SGA 4), Dirigé par M. Artin, A. Grothendieck, et J.-L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat.
  * Awodey et al. (2021) Steve Awodey, Nicola Gambino, and Sina Hazratpour. 2021\.  Kripke-Joyal forcing for type theory and uniform fibrations. (2021).  arXiv:2110.14576 [math.LO]  Unpublished manuscript.
  * Birkedal and Bizjak (2022) Lars Birkedal and Aleš Bizjak. 2022.  Lecture Notes on Iris: Higher-Order Concurrent Separation Logic.  https://iris-project.org/tutorial-material.html
  * Christansen et al. (2020) J. Daniel Christansen, Morgan Opie, Egbert Rijke, and Luis Scoccola. 2020.  Localization in Homotopy Type Theory.  _Higher Structures_ 4 (Feb. 2020), 1–32.  Issue 1. https://higher-structures.math.cas.cz/api/files/issues/Vol4Iss1/ChrOpiRijSco
  * Dubuc (1979) Eduardo J. Dubuc. 1979\.  Sur les modèles de la géométrie différentielle synthétique.  _Cahiers de Topologie et Géométrie Différentielle Catégoriques_ 20, 3 (1979), 231–279.  http://eudml.org/doc/91216
  * Fiore (1997) Marcelo P. Fiore. 1997\.  An Enrichment Theorem for an Axiomatisation of Categories of Domains and Continuous Functions.  _Mathematical Structures in Computer Science_ 7, 5 (Oct. 1997), 591–618.  https://doi.org/10.1017/S0960129597002429
  * Fiore et al. (2021) Marcelo P. Fiore, Andrew M. Pitts, and S. C. Steenkamp. 2021\.  Quotients, inductive types, and quotient inductive types. (2021).  arXiv:2101.02994 [cs.LO]
  * Fiore and Rosolini (1997) Marcelo P. Fiore and Giuseppe Rosolini. 1997.  The category of cpos from a synthetic viewpoint. In _Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, MFPS 1997, Carnegie Mellon University, Pittsburgh, PA, USA, March 23-26, 1997_ _(Electronic Notes in Theoretical Computer Science, Vol. 6)_ , Stephen D. Brookes and Michael W. Mislove (Eds.). Elsevier, 133–150.  https://doi.org/10.1016/S1571-0661(05)80165-3
  * Fiore and Rosolini (2001) Marcelo P. Fiore and Giuseppe Rosolini. 2001.  Domains in H.  _Theoretical Computer Science_ 264, 2 (Aug. 2001), 171–193.  https://doi.org/10.1016/S0304-3975(00)00221-8
  * Gratzer and Sterling (2020) Daniel Gratzer and Jonathan Sterling. 2020.  Syntactic categories for dependent type theory: sketching and adequacy. (2020).  arXiv:2012.10783 [cs.LO]  Unpublished manuscript.
  * Grodin and Harper (2023) Harrison Grodin and Robert Harper. 2023.  Amortized Analysis via Coinduction. In _10th Conference on Algebra and Coalgebra in Computer Science_ _(LIPIcs)_. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
  * Harper et al. (1990) Robert Harper, John C. Mitchell, and Eugenio Moggi. 1990\.  Higher-Order Modules and the Phase Distinction. In _Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. Association for Computing Machinery, San Francisco, California, USA, 341–354.  https://doi.org/10.1145/96709.96744
  * Hoare (1961) C. A. R. Hoare. 1961\.  Algorithm 64: Quicksort.  _Commun. ACM_ 4, 7 (July 1961), 321\.  https://doi.org/10.1145/366622.366644
  * Hoare (1962) C. A. R. Hoare. 1962\.  Quicksort.  _Comput. J._ 5, 1 (Jan. 1962), 10–16.  https://doi.org/10.1093/comjnl/5.1.10
  * Hofmann (1995) Martin Hofmann. 1995\.  _Extensional concepts in intensional type theory_.  Ph. D. Dissertation. University of Edinburgh, Edinburgh.
  * Hyland (1991) J. M. E. Hyland. 1991\.  First steps in synthetic domain theory. In _Category Theory_ , Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 131–156.
  * Kaposi et al. (2019) Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. 2019\.  Constructing Quotient Inductive-inductive Types.  _Proceedings of the ACM on Programming Languages_ 3, POPL (Jan. 2019), 2:1–2:24.  https://doi.org/10.1145/3290315
  * Kavvos et al. (2019) G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner. 2019.  Recurrence Extraction for Functional Programs through Call-by-Push-Value.  _Proceedings of the ACM on Programming Languages_ 4, POPL (Dec. 2019).  https://doi.org/10.1145/3371083
  * Levy (2003) Paul Blain Levy. 2003\.  _Call-by-Push-Value: A Functional/Imperative Synthesis_.  Kluwer, Semantic Structures in Computation, 2.
  * Licata and Harper (2011) Daniel R. Licata and Robert Harper. 2011.  2-Dimensional Directed Type Theory.  _Electronic Notes in Theoretical Computer Science_ 276 (2011), 263–289.  https://doi.org/10.1016/j.entcs.2011.09.026 Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII).
  * Maietti (2005) Maria Emilia Maietti. 2005\.  Modular correspondence between dependent type theories and categories including pretopoi and topoi.  _Mathematical Structures in Computer Science_ 15, 6 (2005), 1089–1149.  https://doi.org/10.1017/S0960129505004962
  * Martin-Löf (1984) Per Martin-Löf. 1984\.  _Intuitionistic type theory_. Studies in Proof Theory, Vol. 1.  Bibliopolis. iv+91 pages.
  * Niu et al. (2022a) Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper. 2022a.  A Cost-Aware Logical Framework.  _Proceedings of the ACM on Programming Languages_ 6, POPL (Jan. 2022).  https://doi.org/10.1145/3498670 arXiv:2107.04663 [cs.PL]
  * Niu et al. (2022b) Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper. 2022b.  _agda-calf_.  https://doi.org/10.1145/3462303
  * Norell (2009) Ulf Norell. 2009\.  Dependently Typed Programming in Agda. In _Proceedings of the 4th International Workshop on Types in Language Design and Implementation_ _(TLDI ’09)_. Association for Computing Machinery, Savannah, GA, USA, 1–2.
  * Pédrot and Tabareau (2019) Pierre-Marie Pédrot and Nicolas Tabareau. 2019.  The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects.  _Proceedings of the ACM on Programming Languages_ 4, POPL (Dec. 2019).  https://doi.org/10.1145/3371126
  * Phoa (1991) Wesley Phoa. 1991\.  _Domain Theory in Realizability Toposes_.  Ph. D. Dissertation. University of Edinburgh.
  * Plotkin and Power (2002) Gordon D. Plotkin and John Power. 2002.  Notions of Computation Determine Monads. In _Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures_. Springer-Verlag, Berlin, Heidelberg, 342–356.
  * Radiček et al. (2017) Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger. 2017.  Monadic Refinements for Relational Cost Analysis.  _Proc. ACM Program. Lang._ 2, POPL, Article 36 (dec 2017), 32 pages.  https://doi.org/10.1145/3158124
  * Rajani et al. (2021) Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2021.  A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis.  _Proceedings of the ACM on Programming Languages_ 5, POPL (Jan. 2021).  https://doi.org/10.1145/3434308
  * Riehl and Shulman (2017) Emily Riehl and Michael Shulman. 2017.  A type theory for synthetic $\infty$-categories.  _Higher Structures_ 1 (2017), 147–224.  Issue 1. arXiv:1705.07442 [math.CT] https://journals.mq.edu.au/index.php/higher_structures/article/view/36
  * Rijke (2019) Egbert Rijke. 2019\.  _Classifying Types_.  Ph. D. Dissertation. Carnegie Mellon University.  arXiv:1906.09435
  * Rijke et al. (2020) Egbert Rijke, Michael Shulman, and Bas Spitters. 2020\.  Modalities in homotopy type theory.  _Logical Methods in Computer Science_ Volume 16, Issue 1 (Jan. 2020).  https://doi.org/10.23638/LMCS-16(1:2)2020 arXiv:1706.07526 [math.CT]
  * Sterling (2021) Jonathan Sterling. 2021\.  _First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory_.  Ph. D. Dissertation. Carnegie Mellon University.  https://doi.org/10.5281/zenodo.6990769 Version 1.1, revised May 2022.
  * Sterling et al. (2019) Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. 2019\.  Cubical Syntax for Reflection-Free Extensional Equality. In _4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 131)_ , Herman Geuvers (Ed.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 31:1–31:25.  https://doi.org/10.4230/LIPIcs.FSCD.2019.31 arXiv:1904.08562 [cs.LO]
  * Sterling et al. (2022) Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. 2022\.  A Cubical Language for Bishop Sets.  _Logical Methods in Computer Science_ 18 (March 2022).  Issue 1. https://doi.org/10.46298/lmcs-18(1:43)2022 arXiv:2003.01491 [cs.LO]
  * Sterling and Harper (2021) Jonathan Sterling and Robert Harper. 2021.  Logical Relations as Types: Proof-Relevant Parametricity for Program Modules.  _J. ACM_ 68, 6 (Oct. 2021).  https://doi.org/10.1145/3474834 arXiv:2010.08599 [cs.PL]
  * Uemura (2019) Taichi Uemura. 2019\.  A General Framework for the Semantics of Type Theory. (2019).  arXiv:1904.04097 [math.CT]
  * Vákár (2017) Matthijs Vákár. 2017\.  _In Search of Effectful Dependent Types_.  Ph. D. Dissertation. University of Oxford.  https://doi.org/10.48550/arXiv.1706.07997 arXiv:1706.07997 [cs.LO]

##  Appendix A Complete definition of decalf

$\displaystyle\mathsf{tp}^{+}$ $\displaystyle:\mathbf{Jdg}$
$\displaystyle\mathsf{tm}^{+}$ $\displaystyle:\mathsf{tp}^{+}\to\mathbf{Jdg}$
$\displaystyle\mathsf{tp}^{\ominus}$ $\displaystyle:\mathbf{Jdg}$
$\displaystyle\mathsf{tm}^{\ominus}$
$\displaystyle:\mathsf{tp}^{\ominus}\to\mathbf{Jdg}$
$\displaystyle\mathsf{tm}^{\ominus}(X)$
$\displaystyle\coloneq\mathsf{tm}^{+}(\mathsf{U}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
X$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
X$}\mathclose{}{)}})$ $\displaystyle\mathsf{U}$
$\displaystyle:\mathsf{tp}^{\ominus}\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{F}$
$\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{\ominus}$
$\displaystyle\mathsf{ret}$
$\displaystyle:(A:\mathsf{tp}^{+},a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})$ $\displaystyle\mathsf{bind}$
$\displaystyle:\,\mathrel{\\{A:\mathsf{tp}^{+},X:\mathsf{tp}^{\ominus}\\}}\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}})\to(\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(X))\to\mathsf{tm}^{\ominus}(X)$
$\displaystyle\mathsf{bind}/\mathsf{ret}$
$\displaystyle:\,\mathrel{\\{A,X\\}}(a:\mathsf{tm}^{+}(A))\to(f:\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(X))\to$
$\displaystyle{\mathsf{bind}(\mathsf{ret}(a);f)}=_{\mathsf{tm}^{\ominus}(X)}{f(a)}$
$\displaystyle\mathsf{bind}/\mathsf{assoc}$
$\displaystyle:\,\mathrel{\\{A,B,X\\}}(e:\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}))\to$
$\displaystyle(f:\mathsf{tm}^{+}(A)\to\mathsf{tm}^{\ominus}(\mathsf{F}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
B$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
B$}\mathclose{}{)}}))\to(g:\mathsf{tm}^{+}(B)\to\mathsf{tm}^{\ominus}(X))\to$
$\displaystyle{\mathsf{bind}(\mathsf{bind}(e;f);g)}=_{\mathsf{tm}^{\ominus}(X)}{\mathsf{bind}(e;\lambda
a.\,\mathsf{bind}(f(a);g))}$ $\displaystyle\leq$
$\displaystyle:(A:\mathsf{tp}^{+})\to\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(A)\to\mathbf{Jdg}$
$\displaystyle\mathsf{pord}$
$\displaystyle:A:\mathsf{tp}^{+}\to\mathsf{isPartialOrder}(A,\leq^{+})$
$\displaystyle\leq_{\textsf{ext}}$ $\displaystyle:\P_{\mathsf{ext}}\to a\leq
a^{\prime}\to a=a^{\prime}$ $\displaystyle\leq_{\textsf{mono}}$
$\displaystyle:\,\mathrel{\\{A,B,a,a^{\prime}\\}}(f:\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(B))\to
a\leq a^{\prime}\to f(a)\leq f(a^{\prime})$ $\displaystyle\leq_{\textsf{pi}}$
$\displaystyle:\,\mathrel{\\{A,B,f,f^{\prime}\\}}((a:\mathsf{tm}^{+}(A))\to
f(a)\leq f^{\prime}(a))\to\textsf{lam}(f)\leq\textsf{lam}(f^{\prime})$ Figure
14. Core decalf calculus. $\displaystyle\begin{aligned}
\mathbb{C}&:\mathsf{tp}^{+}\\\ 0&:\mathsf{tm}^{+}(\mathbb{C})\\\
+&:\mathsf{tm}^{+}(\mathbb{C})\to\mathsf{tm}^{+}(\mathbb{C})\to\mathsf{tm}^{+}(\mathbb{C})\\\
\mathsf{costMon}&:\mathsf{isMonoid}(\mathbb{C},0,+)\end{aligned}$
$\displaystyle\begin{aligned}
\mathsf{step}&:\,\mathrel{\\{X:\mathsf{tp}^{\ominus}\\}}\mathsf{tm}^{+}(\mathbb{C})\to\mathsf{tm}^{\ominus}(X)\to\mathsf{tm}^{\ominus}(X)\\\
\mathsf{step}_{0}&:\,\mathrel{\\{X,e\\}}\mathsf{step}^{0}(e)=e\\\
\mathsf{step}_{+}&:\,\mathrel{\\{X,c_{1},c_{2},e\\}}\mathsf{step}^{c_{1}}(\mathsf{step}^{c_{2}}(e))=\mathsf{step}^{c_{1}+c_{2}}(e)\end{aligned}$
$\displaystyle\begin{aligned}
\mathsf{bind}_{\mathsf{step}}&:\,\mathrel{\\{A,X,e,f,c\\}}\mathsf{bind}(\mathsf{step}^{c}(e);f)=\mathsf{step}^{c}(\mathsf{bind}(e;f))\\\
\mathsf{lam}_{\mathsf{step}}&:\,\mathrel{\\{A,X,c\\}}(f:(a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(a)))\to\mathsf{step}^{c}(\mathsf{lam}(f))=\mathsf{lam}(\mathsf{step}^{c}(f))\end{aligned}$
Figure 15. Cost structure and cost effect. $\displaystyle\P_{\mathsf{ext}}$
$\displaystyle:\mathbf{Jdg}$ $\displaystyle\P_{\mathsf{ext}}/{\mathsf{uni}}$
$\displaystyle:\,\mathrel{\\{u,v:\P_{\mathsf{ext}}\\}}u=v$
$\displaystyle\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
A$}\mathclose{}{)}}$ $\displaystyle\coloneqq\P_{\mathsf{ext}}\to A$
$\displaystyle\mathbb{C}/{\P_{\mathsf{ext}}}$
$\displaystyle:\,\mathrel{\\{X,e,c\\}}\mathchoice{\mbox{\normalshape\fullmoon}}{\mbox{\normalshape\fullmoon}}{\scalebox{0.8}{\normalshape\fullmoon}}{\scalebox{0.6}{\normalshape\fullmoon}}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathsf{tm}^{+}(\mathbb{C})\cong\textbf{1}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathsf{tm}^{+}(\mathbb{C})\cong\textbf{1}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathsf{tm}^{+}(\mathbb{C})\cong\textbf{1}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathsf{tm}^{+}(\mathbb{C})\cong\textbf{1}$}\mathclose{}{)}}$
Figure 16. Open modality for extensional phase. $\displaystyle\Pi$
$\displaystyle:(A:\mathsf{tp}^{+},X:\mathsf{tm}^{+}(A)\to\mathsf{tp}^{\ominus})\to\mathsf{tp}^{\ominus}$
$\displaystyle(\mathsf{ap},\mathsf{lam})$
$\displaystyle:\,\mathrel{\\{A,X\\}}\mathsf{tm}^{\ominus}(\Pi(A;X))\cong(a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{\ominus}(X(a))$
$\displaystyle\Pi^{+}$
$\displaystyle:(A:\mathsf{tp}^{+},B:\mathsf{tm}^{+}(A)\to\mathsf{tp}^{+})\to\mathsf{tp}^{+}$
$\displaystyle(\mathsf{ap}^{+},\mathsf{lam}^{+})$
$\displaystyle:\,\mathrel{\\{A,B\\}}\mathsf{tm}^{\ominus}(\Pi^{+}(A;B))\cong(a:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{+}(B(a))$
$\displaystyle\times$
$\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{+}\to\mathsf{tp}^{+}$
$\displaystyle(\mathsf{unpair},\mathsf{pair})$
$\displaystyle:\,\mathrel{\\{A,B\\}}\mathsf{tm}^{+}(A\times B)\cong
a:\mathsf{tm}^{+}(A)\times\mathsf{tm}^{+}(B)$ $\displaystyle\mathsf{eq}$
$\displaystyle:(A:\mathsf{tp}^{+})\to\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(A)\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{self}$
$\displaystyle:\,\mathrel{\\{A\\}}(a,b:\mathsf{tm}^{+}(A))\to
a=b\to\mathsf{tm}^{+}(\mathsf{eq}_{A}(a,b))$ $\displaystyle\mathsf{ref}$
$\displaystyle:\,\mathrel{\\{A\\}}(a,b:\mathsf{tm}^{+}(A))\to\mathsf{tm}^{+}(\mathsf{eq}_{A}(a,b))\to
a=b$ $\displaystyle\mathsf{uni}$
$\displaystyle:\,\mathrel{\\{A,a,b\\}}(p,q:\mathsf{tm}^{+}(\mathsf{eq}_{A}(a,b)))\to
p=q$ $\displaystyle 1$ $\displaystyle:\mathsf{tp}^{+}$ $\displaystyle\star$
$\displaystyle:\mathsf{tm}^{+}(1)$ $\displaystyle\eta_{1}$
$\displaystyle:\,\mathrel{\\{u,v\\}}u=_{\mathsf{tm}^{+}(1)}v$ $\displaystyle+$
$\displaystyle:\mathsf{tp}^{+}\to\mathsf{tp}^{+}\to\mathsf{tp}^{+}$
$\displaystyle\mathsf{inl}$
$\displaystyle:\,\mathrel{\\{A,B\\}}\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(A+B)$
$\displaystyle\mathsf{inr}$
$\displaystyle:\,\mathrel{\\{A,B\\}}\mathsf{tm}^{+}(B)\to\mathsf{tm}^{+}(A+B)$
$\displaystyle\mathsf{case}$
$\displaystyle:\,\mathrel{\\{A,B\\}}(s:\mathsf{tm}^{+}(A+B))\to(F:\mathsf{tm}^{+}(A+B)\to\mathbf{Jdg})\to$
$\displaystyle((a:\mathsf{tm}^{+}(A))\to F(\mathsf{inl}(a)))\to$
$\displaystyle((b:\mathsf{tm}^{+}(B))\to F(\mathsf{inl}(b)))\to F(s)$
$\displaystyle\mathsf{case}_{\mathsf{inl}}$
$\displaystyle:\,\mathrel{\\{A,B,F,e_{0},e_{1}\\}}(a:\mathsf{tm}^{+}(A))\to\mathsf{case}(\mathsf{inl}(a);F;e_{0};e_{1})=e_{0}(a)$
$\displaystyle\mathsf{case}_{\mathsf{inr}}$
$\displaystyle:\,\mathrel{\\{A,B,F,e_{0},e_{1}\\}}(b:\mathsf{tm}^{+}(B))\to\mathsf{case}(\mathsf{inr}(b);F;e_{0};e_{1})=e_{1}(b)$
$\displaystyle\mathsf{case}_{\eta}$
$\displaystyle:\,\mathrel{\\{A,B,F,a,b\\}}(s:\mathsf{tm}^{+}(A+B))\to\mathsf{case}(s;F;\lambda
x.F(\mathsf{inl}(x));\lambda y.F(\mathsf{inr}(y)))=F(s)$ Figure 17. Types
$\displaystyle\mathsf{nat}$ $\displaystyle:\mathsf{tp}^{+}$
$\displaystyle\mathsf{zero}$ $\displaystyle:\mathsf{tm}^{+}(\mathsf{nat})$
$\displaystyle\mathsf{suc}$
$\displaystyle:\mathsf{tm}^{+}(\mathsf{nat})\to\mathsf{tm}^{+}(\mathsf{nat})$
$\displaystyle\mathsf{rec}$
$\displaystyle:(n:\mathsf{tm}^{+}(\mathsf{nat}))\to(F:\mathsf{tm}^{+}(\mathsf{nat})\to{\mathbf{Jdg}})\to{F(\mathsf{zero})}\to$
$\displaystyle((n:\mathsf{tm}^{+}(\mathsf{nat}))\to{F(n)}\to{F(\mathsf{suc}(n))})\to
F(n)$ $\displaystyle\mathsf{rec}/\mathsf{zero}$
$\displaystyle:\,\mathrel{\\{F,e_{0},e_{1}\\}}\mathsf{rec}(\mathsf{zero};F;e_{0};e_{1})=e_{0}$
$\displaystyle\mathsf{rec}/\mathsf{suc}$
$\displaystyle:\,\mathrel{\\{n,F,e_{0},e_{1}\\}}\mathsf{rec}(\mathsf{suc}(n);F;e_{0};e_{1})=e_{1}(n)(\mathsf{rec}(n;F;e_{0};e_{1}))$
$\displaystyle\mathsf{L}$
$\displaystyle:{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}\mathbb{C}}\to\mathsf{tp}^{+}\to\mathsf{tp}^{+}$
$\displaystyle[]$ $\displaystyle:\,\mathrel{\\{c,A\\}}\mathsf{L}^{c}(A)$
$\displaystyle\mathsf{cons}$
$\displaystyle:\,\mathrel{\\{c,A\\}}\mathsf{tm}^{+}(A)\to\mathsf{tm}^{+}(\mathsf{L}^{c}(A))\to\mathsf{tm}^{+}(\mathsf{L}^{c}(A))$
$\displaystyle\mathsf{rec}$
$\displaystyle:\,\mathrel{\\{c,A\\}}(l:\mathsf{tm}^{+}(\mathsf{L}^{c}(A)))\to(F:\mathsf{tm}^{+}(\mathsf{L}^{c}(A))\to\mathbf{Jdg})\to$
$\displaystyle({F([])})\to$
$\displaystyle((a:\mathsf{tm}^{+}(A))\to(l:\mathsf{tm}^{+}(\mathsf{L}^{c}(A)))\to{F(l)}\to{F({a}\mathrel{\mathchoice{\vbox{\hbox{$\displaystyle:$}}}{\vbox{\hbox{$\textstyle:$}}}{\vbox{\hbox{$\scriptstyle:$}}}{\vbox{\hbox{$\scriptscriptstyle:$}}}\mathchoice{\vbox{\hbox{$\displaystyle:$}}}{\vbox{\hbox{$\textstyle:$}}}{\vbox{\hbox{$\scriptstyle:$}}}{\vbox{\hbox{$\scriptscriptstyle:$}}}}{l})})\to$
$\displaystyle{F(l)}$ $\displaystyle\mathsf{rec}/\mathsf{nil}$
$\displaystyle:\,\mathrel{\\{c,A,F,e_{0},e_{1}\\}}\mathsf{rec}_{\mathsf{L}}([];F;e_{0};e_{1})=e_{0}$
$\displaystyle\mathsf{rec}/\mathsf{cons}$
$\displaystyle:\,\mathrel{\\{c,A,a,e_{0},e_{1}\\}}(F:\mathsf{tm}^{+}(\mathsf{L}^{c}(A))\to\mathsf{tp}^{\ominus})\to(l:\mathsf{tm}^{+}(\mathsf{L}^{c}(A)))\to$
$\displaystyle\mathsf{rec}_{\mathsf{L}}({a}\mathrel{\mathchoice{\vbox{\hbox{$\displaystyle:$}}}{\vbox{\hbox{$\textstyle:$}}}{\vbox{\hbox{$\scriptstyle:$}}}{\vbox{\hbox{$\scriptscriptstyle:$}}}\mathchoice{\vbox{\hbox{$\displaystyle:$}}}{\vbox{\hbox{$\textstyle:$}}}{\vbox{\hbox{$\scriptstyle:$}}}{\vbox{\hbox{$\scriptscriptstyle:$}}}}{l};F;e_{0};e_{1})={\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}\mathsf{step}^{c}}(e_{1}(a)(l)(\mathsf{rec}_{\mathsf{L}}(l;F;e_{0};e_{1})))$
Figure 18. Types, continued

##  Appendix B Proofs of theorems

See 4.10

###### Proof.

Let $\alpha:\mathbb{I}\to A$ and $\beta:\mathbb{I}\to A$ with $\alpha 1=\beta
0$; we wish to construct a path from $\alpha 0$ to $\beta 1$. With these data,
we may define a map $\gamma:\mathbb{I}\lor\mathbb{I}\to A$ using the universal
property of the pushout:

$\mathbf{1}$$\mathbb{I}$$0$$\mathbb{I}$$\mathbb{I}\lor\mathbb{I}$$1$$\mathsf{in}_{1}$$\mathsf{in}_{0}$$A$$\beta$$\alpha$$\gamma$

Because $A$ is orthogonal to $\tau:\mathbb{I}\lor\mathbb{I}\to\mathbb{I}_{2}$,
we have the following unique lift:

$\mathbb{I}\lor\mathbb{I}$$A$$\mathbb{I}_{2}$$\tau$$\gamma$$\hat{\gamma}$

We define a new path $\phi
i\coloneq\hat{\gamma}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
i,i$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
i,i$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
i,i$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
i,i$}\mathclose{}{)}}$ restricting $\hat{\gamma}$ along the diagonal, and we
compute:

$\displaystyle\phi 0$
$\displaystyle=\hat{\gamma}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
0,0$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
0,0$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
0,0$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
0,0$}\mathclose{}{)}}=\alpha 0$ $\displaystyle\phi 1$
$\displaystyle=\hat{\gamma}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
1,1$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
1,1$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
1,1$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
1,1$}\mathclose{}{)}}=\beta 1\qed$

See 4.13

###### Proof.

A map $\mathbb{S}\mathbf{2}\to A$ is a pair of paths between two fixed
elements of $A$; a map $\mathbb{S}\mathbf{1}\to A$ is a single path between
two fixed elements. Thus orthogonality to the suspension
$\mathbb{S}\mathbf{2}\to\mathbb{S}\mathbf{1}$ means precisely that any two
paths between the same elements are equal, which is precisely suborthogonality
to $i:\mathbf{2}\to\mathbb{I}$. ∎

See 4.15

###### Proof.

The forward direction is trivial, and holds even for non–boundary separated
types. In the backwards direction, suppose that we have $\forall
x:A.fx\sqsubseteq_{Bx}gx$; because $Bx$ is boundary separated, paths therein
are uniquely determined by their endpoints, so we may use the topos-valid
principle of _unique_ choice to obtain a family of paths
$\beta:A\to\mathbb{I}\to B$ such that $\beta x$ is in each case a path from
$fx$ to $gx$. By permuting arguments, we thus have a path from $f$ to $g$ and
so we have $f\sqsubseteq_{\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
x:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
x:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
x:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
x:A$}\mathclose{}{)}}\to Bx}g$. ∎

See 4.20

###### Proof.

Let $\alpha:\mathbb{I}\to A$ be such that $\alpha 0=x$ and $\alpha 1=y$, and
fix an observation $\phi:A\to\mathbb{I}$. The Phoa principle ensures that the
composite $\phi\circ\alpha$ is monotone in the implication order, and so we
have $\phi\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\alpha
0$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\alpha
0$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\alpha
0$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\alpha
0$}\mathclose{}{)}}\to_{\mathbb{I}}\phi\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\alpha
1$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\alpha
1$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\alpha
1$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\alpha
1$}\mathclose{}{)}}$ and thus $\phi x\to_{\mathbb{I}}\phi y$. ∎

See 4.22

###### Proof.

To show that $A$ is discrete, suppose that $a_{0}\sqsubseteq_{A}a_{1}$ such
that $a_{0}\not=a_{1}$; it follows from $a_{0}\sqsubseteq_{A}a_{1}$ via Lemma
4.20 and the Phoa principle that for any $\phi:A\to\mathbb{I}$ we have $\phi
a_{0}\to_{\mathbb{I}}\phi a_{1}$. Define $\phi:A\to\mathbb{I}$ as follows,
using the fact that $A$ has decidable equality:

$\phi x\coloneq\begin{cases}1&\text{if }x=a_{0}\\\
0&\text{otherwise}\end{cases}$

By assumption, we have $1=\phi a_{0}\to_{\mathbb{I}}\phi a_{1}=0$, _i.e_. we
have $1\to_{\mathbb{I}}0$; because the ordering on $\mathbb{I}$ is
antisymmetric, we have $1=0$. Because we have assumed a path $\mathbb{I}\to A$
from $a_{0}$ to $a_{1}$, from $1=0$ we may conclude that $a_{0}=a_{1}$, which
is a contradiction. ∎

See 4.23

###### Proof.

Boundary separation is obviously preserved by dependent pair types, so we will
consider only path-transitivity. We fix an orthogonal lifting scenario as
follows:

$\mathbb{I}\lor\mathbb{I}$$\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
x:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
x:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
x:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
x:A$}\mathclose{}{)}}\times Bx$$\mathbb{I}_{2}$$\tau$$\psi$

We must construct a unique lift
$\hat{\psi}:\mathbb{I}_{2}\to\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
x:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
x:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
x:A$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
x:A$}\mathclose{}{)}}\times Bx$ with $\psi=\hat{\psi}\circ\tau$. Because $A$
is discrete, it follows that the restriction
$\pi_{1}\circ\psi:\mathbb{I}\lor\mathbb{I}\to A$ is constant on some element
$a:A$, and so the restriction $\pi_{2}\circ\psi$ is a non-dependent function
$\mathbb{I}\lor\mathbb{I}\to Ba$. Therefore, it suffices to solve the
following simpler orthogonal lifting problem:

$\mathbb{I}\lor\mathbb{I}$$Ba$$\mathbb{I}_{2}$$\tau$$\psi\circ\pi_{2}$$\exists!$

The unique lift above exists because we have assumed each $Ba$ is path-
transitive. ∎

See 4.33

###### Proof.

To see that Axiom 4.30 is satisfied, observe that the ordinal
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}=\mathchoice{\mathopen{}{\\{}\hbox{$\displaystyle
0<1$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\textstyle
0<1$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptstyle
0<1$}\mathclose{}{\\}}}{\mathopen{}{\\{}\hbox{$\scriptscriptstyle
0<1$}\mathclose{}{\\}}}$ satisfies the Phoa principle in the category of
preorders. In particular, the exponential preorder
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}^{\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}}$ can indeed be seen to be isomorphic to the subobject of
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}\times\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}$ spanned by pairs of the form
$\mathchoice{\mathopen{}{(}\hbox{$\displaystyle i\leq
j$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle i\leq
j$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle i\leq
j$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle i\leq
j$}\mathclose{}{)}}$. We finally observe that this fact corresponds under the
$N:\mathbf{Preord}\hookrightarrow\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}$
to the Phoa principle. ∎

See 4.35

###### Proof.

Let
$i_{*}:\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}\hookrightarrow\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$
be the directed image functor of the _closed immersion_ corresponding to the
view of
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$
as the _inverted scone_ of
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}$;
the essential image of $i_{*}$ in
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$
consists precisely of the $\P_{\mathsf{ext}}$-connected objects, _i.e_. those
that contract to a singleton when restricted into
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}/{\P_{\mathsf{ext}}}$.
The embedding
$N_{\bot}:\mathbf{Preord}\hookrightarrow\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$
obtained by composing the nerve
$N:\mathbf{Preord}\hookrightarrow\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}$
with
$i_{*}:\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}$}\mathclose{}{)}}\hookrightarrow\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$
renders
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$
well-adapted, noting that the image of $i_{*}$ is precisely the
$\P_{\mathsf{ext}}$-connected objects of
$\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$.
This embedding is not only fully faithful, but also continuous and cartesian
closed. Moreover, $N_{\bot}$ restricts on augmented simplices to the Yoneda
embedding
$\mathbf{y}:\mathbf{\Delta}_{\bot}\hookrightarrow\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$.

To check that $\mathbb{I}$ is $\P_{\mathsf{ext}}$-connected (Axiom 4.29), it
suffices to prove that $\mathbb{I}^{\P_{\mathsf{ext}}}$ is the terminal
object; we compute using our observations above:

$\displaystyle\mathbb{I}^{\P_{\mathsf{ext}}}\cong\mathbf{y}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}^{\mathbf{y}{\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-1$}\mathclose{}{]}}}}\cong\mathchoice{\mathopen{}{(}\hbox{$\displaystyle
N_{\bot}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle
N_{\bot}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle
N_{\bot}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle
N_{\bot}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}$}\mathclose{}{)}}^{N_{\bot}\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-1$}\mathclose{}{]}}}\cong
N_{\bot}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}^{\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-1$}\mathclose{}{]}}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}^{\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-1$}\mathclose{}{]}}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}^{\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-1$}\mathclose{}{]}}}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}^{\mathchoice{\mathopen{}{[}\hbox{$\displaystyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle-1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle-1$}\mathclose{}{]}}}$}\mathclose{}{)}}\cong
N_{\bot}\mathbf{1}\cong\mathbf{1}$

The Phoa principle (Axiom 4.30) follows in roughly the same way as for
simplicial sets (Theorem 4.33): first we see that
$\mathchoice{\mathopen{}{[}\hbox{$\displaystyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\textstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptstyle
1$}\mathclose{}{]}}{\mathopen{}{[}\hbox{$\scriptscriptstyle
1$}\mathclose{}{]}}$ satisfies the Phoa principle in $\mathbf{Preord}$, and
then we observe that this fact is preserved by the cartesian closed embedding
$N_{\bot}:\mathbf{Preord}\hookrightarrow\mathrm{Pr}\mathchoice{\mathopen{}{(}\hbox{$\displaystyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\textstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}{\mathopen{}{(}\hbox{$\scriptscriptstyle\mathbf{\Delta}_{\bot}$}\mathclose{}{)}}$.
∎


# Magnetic field structure in the vicinity of a super-massive black hole in
low luminosity galaxies: the case of Sgr A*

Antonios Nathanail1,5 , Prasun Dhang2,3 and Christian M. Fromm4,5,6
1 Department of Physics, National and Kapodistrian University of Athens,
Panepistimiopolis, GR 15783 Zografos, Greece
2Institute for Advanced Study, Tsinghua University, Beijing-100084, China
3Department of Astronomy, Tsinghua University, Beijing-100084, China
4 Institut für Theoretische Physik und Astrophysik, Universität Würzburg,
Emil-Fischer-Strasse 31, 97074 Würzburg, Germany
5Institut für Theoretische Physik, Goethe Universität Frankfurt, Max-von-Laue-
Str.1, 60438 Frankfurt am Main, Germany
6Max-Planck-Institut für Radioastronomie, Auf dem Hügel 69, D-53121 Bonn,
Germany E-mail<EMAIL_ADDRESS>
###### Abstract

Observations of $\rm SgrA^{*}$ have provided a lot of insight on low-
luminosity accretion, with a handful of bright flares accompanied with orbital
motion close to the horizon. It has been proposed that gas supply comes from
stellar winds in the neighborhood of the supermassive black hole. We here
argue that the flow at the vicinity of the black hole has a low magnetization
and a structure of alternating polarity totally dictated by the well studied
and long-ago proposed MRI turbulent process. This can be the case, provided
that in larger distances from the black hole magnetic diffusivity is dominant
and thus the magnetic field will never reach equipartition values. For $\rm
SgrA^{*}$, we show the immediate consequences of this specific magnetic field
geometry, which are: (i) an intermittent flow that passes from quiescent
states to flaring activity, (ii) no quasi-steady-state jet, (iii) no
possibility of a magnetically arrested configuration. Moreover a further
distinctive feature of this geometry is the intense magnetic reconnection
events, occurring as layers of opposite magnetic polarity are accreted, in the
vicinity of the black hole. Finally, we argue that the absence of a jet
structure in such case will be a smoking gun in 43 & 86 GHz observations.

###### keywords:

Black hole physics, Sgr A*, Magnetohydrodynamics

##  1 Introduction

The supermassive black hole (BH) in the Galactic center, Sgr A*, is the
closest of its kind and is the subject of several campaigns of multi-
wavelength observations, since it is an excellent probe for accretion physics
in the extreme gravity regime. Over the years unparalleled insight on the
accretion flow in the immediate environment of the central BH has been
obtained (Falcke et al., 1998; Doeleman et al., 2008). Sgr A* is one of the
primary sources for the Event Horizon Telescope (EHT) and GRAVITY
collaborations yielding extraordinary results the last years and more expected
to come (Johnson et al., 2015; GRAVITY collaboration et al., 2018).

Multi-wavelength observations have revealed a low accretion rate with an
extremely low bolometric luminosity $L_{\rm bol}\sim 10^{-9}L_{\rm Edd}$,
where $L_{\rm Edd}$ is the Eddington Luminosity (Baganoff et al., 2003; Bower
et al., 2019), which places the accretion flow of $\rm SgrA^{*}$ in the regime
of a radiatively inefficient accretion flow (Yuan & Narayan, 2014).

Observations have hinted that around 80 massive stars reside in a rotating
disk inside the parsec neighborhood of the Galactic center(Martins et al.,
2007).It has been suggested that 30 of these massive stars, identified as
Wolf-Rayet (WR) magnetized stars could source the accretion flow around the
Galactic center (Quataert, 2004; Loeb, 2004; Shcherbakov & Baganoff, 2009;
Ressler et al., 2020b). This scenario has been studied in a multi-scale
simulation (Ressler et al., 2020a) and suggested that the accretion flow
around Sgr A* is in a magnetically arrested (MAD) state, moreover, its
dynamics differ significantly from the rotationally supported tori usually
used in the general-relativistic magnetohydrodynamic (GRMHD) community (Porth
et al., 2019).

Table 1: Consequences of the two different assumptions that (i) magnetic field dragging and flux-freezing is effective and (ii) that magnetic diffusion is dominant | flux-freezing effective | diffusion dominant
---|---|---
| MAD | not MAD (FLARE model)
MRI | suppressed | active
jet | MAD jet | no steady jet
expected outflow power | huge and steady | intermittent
43 & 86 GHz image | extended jet base | non-extended (when non-flaring)111See Section 4.
|  | maybe extended when flaring

This novel multi-scale approach assumes ideal magnetohydrodynamics, which has
as a consequence, coherent magnetic field from large radii to be continuously
advected, to form a MAD flow in the vicinity of the black hole (Ressler et
al., 2020b).

In what follows, we present a comprehensive description of what would be
different assuming a dominant magnetic diffusivity in the process of accretion
generated through the stellar winds. To this end, we describe two MHD
simulations, one that monitors the evolution of the magnetic field in an
accretion disk where the MRI has fully developed, and another one where the
magnetic field of different polarity is advected on the low density region
above the BH and results in flaring activity, which we call the FLARE model.
Estimations of the overall energy of the produced flares are presented and
discussed.

This letter is organised as follows: in Section 2 we discuss in detail the
different implications that follow from these assumptions, in Section 3 we
present results from numerical simulations of MRI turbulence and the magnetic
field structure in the close-by accretion disk. In Section 4 we present a
GRMHD simulation (FLARE model) that mimics the MRI turbulent state and where
plasmoids are generated above the black hole, and then compare ray-traced
images from this simulation. Finally, we summarize and conclude in Section 5.

##  2 Diffusion versus flux-freezing assumption and magnetic field reversals

The flow generated by stellar winds around SgrA* continuously accrete magnetic
field, but as the field lines are dragged, they tend to diffuse out. This may
limit any effective process of magnetic field dragging (Heyvaerts et al.,
1996). As the flow and magnetic field are generated far from the BH, it needs
to be advected all the way to its vicinity. However, at distances of $300\ -\
10000\ r_{g}$ a diffusive accretion disk may form as MRI is triggered. This
argument will hold if the MRI linear growth time scale is smaller than the
viscous advection timescale, a robust estimation of this is not easy to be
calculated.

The discussion about the efficiency of the magnetic flux-freezing assumption
is not new, also MRI turbulent discs and the effect of magnetic diffusion have
been studied for decades. However, to interpret EHT and GRAVITY results, such
discussions are not put forward as relevant. In this short study we highlight
the importance of these effects and propose that such long-studied effects are
crucial in interpreting SgrA∗ results.

In the case that turbulent viscosity is of the same order of magnetic
diffusivity, then the magnetic field is not dragged effectively. This is set
by the magnetic Reynolds number, in its simplest form $R_{\rm m}=uL/\eta$,
where $u$ is the velocity of the flow, $L$ is the length scale and $\eta$ the
resistivity/magnetic diffusivity. The value of the magnetic Reynolds number
can set the process along the way from the ejection of the magnetized stellar
winds, all the way to the central suppermassive BH (Balbus & Henri, 2008). For
high $R_{\rm m}$ magnetic field dragging is highly efficient, whereas for
values closer to unity and below this is not the case (Contopoulos et al.,
2015). A transition of $R_{\rm m}$ from low to high, if it occurs at all, will
occur in the inner disk regions $R_{\rm
m}\propto\left(\frac{L}{1000R_{g}}\right)\left(\frac{u}{0.001c}\right)<<1$
(Faghei & Mollatayefeh, 2012). We need to note that in the simulations
reported here, no physical resistivity was used and only numerical diffusion
is present.

Thus, any flux-freezing argument will fail to produce a dynamically important
magnetic field at the vicinity of the BH. The situation will be different
(from the MAD configuration) with a turbulent inner-region accretion disk,
which will be weakly magnetized and MRI is fully operating from the seed
poloidal field that came from the stellar winds. Now if the magnetic field is
not strong enough to suppress the MRI, the field reversals will occur with a
predetermined period. From recent sheering box simulations we can extract that
magnetic field reversals occur in around 10 local orbital periods, where local
refers to $\approx 10R_{g}$ (extracted from the simulation (Dhang & Sharma,
2019), also see (Hogg & Reynolds, 2018)). As was pointed out previously, the
accretion disk could be MRI unstable from a radius of $300\ -\ 10000\ r_{g}$,
however, this will not set the scale of the changing of magnetic field
polarity as is shown in the simulations (Dhang & Sharma, 2019; Hogg &
Reynolds, 2018).

This will set the length scale and the timescale of field reversals, assuming
that the local orbital period is $T_{\rm local}=2\pi(R_{g}/c)(R_{\rm
local}/R_{g})^{3/2}$, assuming a Keplerian orbital period. Thus, for $R_{\rm
local}=10R_{g}$ the corresponding period is $T_{\rm local}\approx 200R_{g}/c$,
and then the corresponding timescale for magnetic field reversals is $t_{\rm
mag}\approx 2\times 10^{3}R_{g}/c$, which to length scale of $l_{\rm
mag}\approx 10^{3}R_{g}$ (Giannios & Uzdensky, 2019). This length could hint
also to the transition radius and maybe important for the particular case of
SgrA* (Quataert & Narayan, 1999; Xu, 2013). It is important to note here that
our estimations are based on the simulations of Dhang & Sharma (2019) and thus
the influence of the spin of the black hole is not taken into account this
could potentially affect the resulting timescale.

In order to clearly differentiate the consequences for each assumption we list
them respectively, to show the important implications that each assumption
leads to. At this point we take the two different assumptions (i) dragging of
magnetic field is effective and the flux-freezing argument holds and (ii) that
magnetic diffusivity is dominant at some point of the flow through the
millions of gravitational radii that travels from the stellar winds to the BH.
The discussion for the two different cases is summarized in Table 1.

For case (i) multi-scale simulations have shown that the accretion flow
becomes magnetically arrested and a MAD state is established. The dynamically
important magnetic field suppresses the MRI which is no longer important for
the evolution of the inner-region flow (Ressler et al., 2020a). A narrow disk-
like structure is produced around the central BH due to the impact of the
strong magnetic field (Ressler et al., 2020b). A MAD configuration is always
accompanied with a magnetized jet along the axis of the angular momentum of
the BH (for a spinning BH, tilted disks excluded), MAD jets are expected to
have huge power and this is yet to be observed for SgrA*. This has also a
straight consequence in the compact radio image of the source (Anantua et al.,
2020), which however may not be so strong in the frequency that EHT is
observing, the 230 GHz, but rather in 43 and 86 GHz where any extended
emission from the jet base with strongly affect and enlarge the image size
(Davelaar et al., 2018). Also a MAD configuration has certain restrictions
when applied to the whole spectrum of SgrA*, in order to fit both the standard
flux in quiescence and when flaring occurs (Chatterjee et al., 2020).

The last point to touch, is about the ability of a MAD state accretion for
SgrA* to provide the observed flaring activity together with the
characteristics, like the observed orbital motion during flares as observed by
GRAVITY collaboration et al. (2018). Reconnection events and flux eruptions
that periodically occur in MAD simulations were put in place to explain the
flares together with their detailed characteristics (Dexter et al., 2020). The
computed near-infrared (NIR) lightcurve are promising, however the flux
centroid motion from the simulation NIR flares is much more restricted than
the observed one. Moreover, the orbiting flux tubes that can potentially
explain the flares show a sub-keplerian motion (Porth et al., 2021), whereas
hot spot models of the flux centroid motion during the flares hint to a super-
keplerian motion (Matsumoto et al., 2020). Another important observational
feature that we could potentially distinguish models is polarization, previous
results have hinted to a rather significant polarization fraction (Johnson et
al., 2015), however to analyze polarization measurements from numerical
simulations is not a trivial step (Gold et al., 2017).

Figure 1: Time evolution of the volume averaged magnetic field energy for each
component. Volume average is done over the region $r\in[6,40]$,
$\theta\in[50^{\circ},130^{\circ}]$ and $\phi\in[0,2\pi]$. The timescale is
normalized for SgrA*.  Figure 2: Butterfly diagram: Variation of azimuthally
averaged radial ($\bar{B}_{r}$) and toroidal ($\bar{B}_{\phi}$) fields with
latitude ($90^{\circ}-\theta$) and time. Time is rescaled appropriately for
Sgr A*.

In the second case (ii), the whole picture of the inner disc accretion flow
close the central BH, is different. The magnetic field is not so strong and
MRI is not suppressed, thus is active and may dictate the field accretion. A
well-known and deeply studied phenomenon in accretion discs with a
stratification is an oscillating mean toroidal magnetic field. Toroidal
magnetic field buoyantly rises from the mid-plane to the upper coronal
regions. This unique feature is commonly referred to as the butterfly diagram,
and is has been seen from local (Brandenburg et al., 1995; Hawley et al.,
1996) but also in global simulations (Beckwith et al., 2011; Sorathia et al.,
2012). In the scale-free simulations, the oscillating toroidal magnetic field
changes sign approximately every 10 local orbits, which scaled for SgrA*
yields a 6-8 hour periodicity at around $\approx 20\,r_{g}$ from the BH.
However, it must be pointed out that unlike a geometrically thin disc, for a
geometrical thick radiatively inefficient accretion flow (RIAF), the dynamo
cycle is intermittent, both poloidal and toroidal fields flip sign irregularly
(Hogg & Reynolds 2018; Dhang & Sharma 2019; Dhang et al. 2020, also see Fig.
2). These dynamo generated large-scale magnetic fields tend to be affected by
the turbulent pumping (an effect which transports large-scale magnetic field
from the turbulent region to the laminar region) resulting in transport of
large-scale magnetic fields from the turbulent disc region to the less
turbulent coronal region (Dhang et al., 2020). Hence this alternating polarity
magnetic field can reconnect either inside the high $\beta$ disk giving rise
to heating of the inner disk, or at the low density and low $\beta$ (highly
magnetized) polar region above the BH and eventually form hot spots/ plasmoids
that can become unbound and fly away from the black hole.

Reconnection in the vicinity of the black hole is operating and gives rise to
plasmoid formation (Parfrey et al., 2015; Mahlmann et al., 2020; Nathanail et
al., 2020; Ripperda et al., 2020). In the next Section we will present results
from such a simulation and give estimates on the energy that such flares have.
Such conditions could give a similar radio image in the 230GHz, but there will
be a significant difference in the 43 & 86 GHZ. During a quiescent state the
radio image in those frequencies will be less extended than the MAD case due
to the absence of a jet. On the other, a radio image at these observed
simultaneously with a flare, would be expected to have several larger scale
features, which would imply an extended size, maybe similar to the MAD case.
In this case models for flares accompanied with orbiting motion in horizon
scales can be expected as the ones found in GRMHD simulations Nathanail et al.
(2020) and will be also discussed in Section 4. These models would be similar
to the plasmoid model from Ball et al. (2020).

##  3 MRI-turbulence

The problem of angular momentum transport in accretion flows and the source of
turbulence can be addressed through the action of the MRI which was studied by
Velikhov (1959); Chandrasekhar (1960), but put into play to resolve this long-
standing problem by Balbus & Hawley (1991). The linear and the non-linear
regimes of the MRI have been studied in local shearing box simulations,
recently also in global simulations (Beckwith et al., 2011; Hogg & Reynolds,
2018; Dhang & Sharma, 2019; Dhang et al., 2020) and GRMHD high resolution
simulations (Liska et al., 2018). How a large-scale magnetic field is
generated in an accretion flow is still debatable. The advection of the
magnetic field from large radii has been proposed (Lubow et al., 1994;
Lovelace et al., 2009) or the in situ production of a large scale magnetic
field by a dynamo process (Brandenburg & Nordlund, 2011). The production in
the vicinity of the BH has been also proposed to be dictated by a battery
process that has distinctive observational signatures (Contopoulos & Kazanas,
1998), however for an AGN with luminosity as low as that one of SgrA* would
require an extremely long timescale to build such a field (Contopoulos et al.,
2015, 2018).

Table 2: Energetics of the reported flares in Fig. 3 at $4620\ M$ in the upper panel and at $7800\ M$ in the lower panel. The assumption on the accretion rate is reported in the first column, then the simulation time, the magnetic and total energy and the ratio between the magnetic field components. $\dot{m}$ | time | magnetic energy | total energy | $Bz/B_{\phi}$
---|---|---|---|---
${\rm[M_{\odot}/year]}$ | ${\rm[M]}$ | ${\rm[erg]}$ | ${\rm[erg]}$ |
$10^{-7}$ | 4620 | $8.9\times 10^{38}$ | $3\times 10^{39}$ | 1.14
$10^{-8}$ | 4620 | $8.9\times 10^{37}$ | $3\times 10^{38}$ | 1.14
$10^{-7}$ | 7800 | $1.4\times 10^{38}$ | $5\times 10^{38}$ | 1.46
$10^{-8}$ | 7800 | $1.4\times 10^{37}$ | $5\times 10^{37}$ | 1.46

We are particularly interested in the generation of a large scale magnetic
field by the MRI driven dynamo in a weakly magnetised RIAF (Beckwith et al.,
2011). Here we will describe the results from the global 3D MHD simulation
that investigates such generation of magnetic fields and the self-sustained
dynamo process in a geometrically thick radiatively inefficient (RIAF)
accretion disk (model M-2P of Dhang & Sharma (2019)). The simulation has an
inner/ outer radius of $4R_{g}/140R_{g}$ respectively and a resolution of
($r,\theta,\phi)=(296,128,512)$ It is important to note that to have such a
high resolution in the disk and also close to the event horizon is costly and
forbiden for present simulations, for this reason we employ one simulation
that focuses in the disk evolution and another that focuses on the black hole
activity. The simulation is initialised to an equilibrium torus (Papaloizou &
Pringle, 1984) threaded by the poloidal magnetic field loops of plasma
$\beta\sim 800$, such that the magnetically, RIAF remains in the regime of
standard and normal evolution (SANE) type of accretion disk in the quasi-
stationary state.

Fig. 1 shows the evolution of the magnetic energy in the accretion flow. Time
evolution follows this path: initially both poloidal ($B_{r}$ and
$B_{\theta}$) and toroidal ($B_{\phi}$) components of the magnetic field grow
exponentially. The poloidal components are amplified by the linear MRI, while
shear generates the toroidal components with different sign above and below
the equatorial plane. In due time the system enters the non-linear regime and
parasitic instabilities become important (Goodman & Xu, 1994), leading to the
full development of turbulence throughout the accretion disk. Here it is to be
noted that the initial zero toroidal magnetic component evolves in time to
increase significantly comprising of almost eighty percent of the total
magnetic energy in the quasi-steady state.

Fig. 2 shows the evolution of the azimuthally averaged radial ($\bar{B}_{r}$)
and toroidal ($\bar{B}_{\phi}$) magnetic fields with latitude
($90^{\circ}-\theta$) and time at a radius $r=20\ r_{g}$. While the strong
shear transforms the poloidal fields into the toroidal fields, the poloidal
fields can be regenerated by an $\alpha$-effect out of the toroidal fields
(Brandenburg et al., 1995; Dhang & Sharma, 2019; Dhang et al., 2020). This
cycle goes on resulting in large-scale magnetic fields (both poloidal and
toroidal) of alternate polarity in time and develops a butterfly diagram. This
is a phenomenon widely known and found in local and global simulations of
accretion disks that study the MRI, moreover several studies hint to a certain
periodicity, which for SgrA* would be a matter of hours (Brandenburg et al.,
1995; Hawley et al., 1996; Sorathia et al., 2012; Hogg & Reynolds, 2018; Dhang
& Sharma, 2019).

Figure 3: Different states during the evolution of the accretion flow with a
bright flare (upper panel), a state of quiescence (middle panel) and another
flare (lower panel). In both flares an orbiting plasmoid/hot spot can be
identified. The time lapse from the upper to the middle panel is 10 hours and
from the middle to the lower 7.5 hours (for SgrA* scales). The first column
shows the magnetization $\sigma$, the middle column the criterion for unbound
matter $-hu_{t}$ (where $-hu_{t}>1$ means unbound) and the last column the
toroidal magnetic field $B_{\phi}$. The reported snapshots are from the 2D
FLARE simulation. Figure 4: GRRT images for SgrA⋆ computed for three different
frequencies $43$ GHz (left column), $86$ GHz (middle column) and $230{\rm
GHz}$ (right column). The top row displays the images generated from a MAD
GRMHD model with spin, a${}^{\star}=0.9375$ (Cruz-Osorio et al., 2022; Fromm
et al., 2021) and the bottom row shows images obtained from a 3D FLARE model
with spin $a^{\star}=0.9375$ (Nathanail et al., 2021).

A strong turbulent pumping is present in the MRI driven dynamo giving rise to
transport of the large-scale fields from the turbulent region close to the
mid-plane to the less turbulent coronal region (Dhang et al., 2020). Accretion
of the large-scale magnetic fields is found to be more efficient in the
coronal region compared to that in the disc (Guilet & Ogilvie, 2013). As these
alternating polarity magnetic fields are advected onto the black hole, they
reconnect and produce structures, such as plasmoids. In some cases the
plasmoids fall onto the BH but they may also become energised and eventually
become unbound and responsible for flaring activity.

##  4 The Different states of $\rm SgrA^{*}$ and image differences

In this section we first discuss how the accretion of the butterfly diagram
onto the BH may give rise to distinctive flaring features and present a
qualitative description of the results discussed thoroughly in (Nathanail et
al., 2020, 2021) called the FLARE model, and then show results of ray traced
images in general relativity (GRRT) in order to show the size of the image
changes for MAD models and the FLARE models we have discussed here. These
features can account for the different states observed in the compact region
at the center of our galaxy, $\rm SgrA^{*}$. We report high resolution, 2D
(Nathanail et al., 2020) and 3D (Nathanail et al., 2021) GRMHD simulations
performed with the BHAC code Porth et al. (2017), a logarithmic grid is
employed with $4096\times 2048$ in $r$ and $\theta$ for the 2D simulation,
whereas an effective resolution of $1050\times 768\times 384$ in $r,\ \theta$
and $\phi$ for the 3D, an outer boundary at $2500\,r_{g}$ and $500\,r_{g}$
respectively, and a Kerr spacetime with a dimensionless spin parameter of
$a=0.9375$ for both 2D and 3D. The inner and outer radii of the torus are at
$r_{\rm in}=6\,r_{g}$ and $r_{\rm out}=12\,r_{g}$. When the simulation reaches
a steady state the average normalized magnetic flux at the horizon is
$\Phi_{BH}/\sqrt{\dot{m}}\approx 0.5$. This magnetic flux fluctuates, as the
loops anninhilate, but never approach the MAD value. The setup for the MAD
simulation has an effective resolution of $384^{3}$ in $r,\ \theta$ and
$\phi$, an outer boundary at $2500\,r_{g}$, the same Kerr spacetime and inner
and outer radii of the torus are at $r_{\rm in}=20\,r_{g}$ and $r_{\rm
out}=41\,r_{g}$. Apart from the disk size, the major difference between MAD
and FLARE simulations are the initial magnetic field configuration, for MAD
this is a nested loop embedded in the initial torus and for FLARE the initial
torus configuration is seeded with loops of alternating polarity.

In the FLARE model loops of alternating polarity are advected with the flow to
the BH. This setup does not yield a persistent jet structure, but may produce
striped jets (Giannios & Uzdensky, 2019). The evolution of such an accretion
flow together with its characteristics was presented in detail in Nathanail et
al. (2020, 2021). Here, we restrict into a consideration of these simulation
with a comparison to the activity of $\rm SgrA^{*}$. Our focus is to find,
during the evolution of the accretion disk and the advection of the magnetic
loops, times that the whole system is radically changing behavior. At the
point that two layers of different magnetic field polarity merge in the low
density region above the BH, plasma gets energy and forms plasmoids through
magnetic reconnection, these features become unbound and leave the BH in a
spiral outward orbit, as seen in the upper panel of Fig. 3.

After a major reconnection event, we usually observe a quiescent state for
some time (middle panel of Fig. 3), till the flow builds a considerable
magnetic flux of one polarity. This structure is subsequently annihilated by
the advection of magnetic flux of different polarity and another flare
(unbound plasmoids, identified through a cutoff in magnetization) is
generated, as in the lower panel of Fig. 3, with a recurring timescale of
$\approx 1200\ {\rm M}$. Flare from flare may differ in overall energy, which
depends on the amount of magnetic flux that reconnects at the reconnection
site. To estimate the energy of each flare we assume a mass accretion rate of
$10^{-8}\ -\ 10^{-7}\ M_{\odot}/year$, for the two boundary values of this
range we estimate the energy in the flares and report them in Table 2. Since
our simulations are 2D, we assume an angular size of $\pi/10$ for the
plasmoids. The resulting energetics acquire enough energy to explain bright
flares from SgrA* (Bouffard et al., 2019). Another important point is that the
magnetic field in the flares is predominantly poloidal, as seen in the last
column of Table 2, and thus could explain the linear polarisation reported
(GRAVITY collaboration et al., 2018), note that this does not hold inside the
dense accretion disk where the field is mostly toroidal due to the MRI and the
differential rotation.

To further compare the standard MAD GRMHD simulations (see, e.g., Cruz-Osorio
et al., 2022; Fromm et al., 2021) with the ones reported in this work we
performed general relativistic radiative transfer (GRRT) calculations. Given
that the GRMHD simulations are scale free (except for the spin and initial
magnetic field topology) we adjusted to the galactic centre during the GRRT by
setting the mass and distance. We used a black hole mass of $4.14\times
10^{6}\,M_{\sun}$ and a distance of 8.14 kpc (Gravity Collaboration et al.,
2019). We iterate the mass accretion rate222The resulting mass accretion rate
is consistent with the values used in Table 2. until we obtain a flux of
$\sim$3 Jy at 230 GHz in agreement with the SgrA⋆ observations of Bower et al.
(2019). During the radiative transfer we exclude regions in the jet funnel
with large magnetisation $\sigma>1$ to avoid contamination from floor values
introduced during the simulations to ensure numerical stability. The radiative
calculation is performed using the well tested GRRT code BHOSS (Younsi et al.,
2012; Younsi et al., 2020). Since your GRMHD simulations do not evolve the
radiating electrons we need to reconstruct their properties, e.g., temperature
and number density, from the ions. Therefore, we applied the so-called
$R-\beta$ model (Mościbrodzka et al., 2016) relating the ion temperature,
$T_{\rm i}$ together with the plasma beta, $\beta=p_{\rm gas}/p_{\rm mag}$ via
a free parameter labeled as $R_{\rm high}$ to the electron temperature:

$\Theta_{\rm e}=\frac{pm_{\rm p}/m_{\rm e}}{\rho T_{\rm ratio}},\,\quad T_{\rm
ratio}\equiv\frac{T_{\rm p}}{T_{\rm e}}=\frac{1+R_{\rm
high}\beta^{2}}{1+\beta^{2}},$ (1)

with $m_{\rm p}$ and $m_{\rm e}$ the proton and electron masses, respectively.
During the GRRT we assumed a thermal distribution electrons while we fixed the
inclination angle to 50∘ and used a $R_{\rm high}=5$333The values are chosen
to highlight the launched jet in the MAD models. The result of the radiative
transport can be seen in Fig. 4. The differences between the MAD model (top
row) and the FLARE model (bottom row) are clearly visible and most striking
one is the missing jet feature in the FLARE images. Another feature of the MAD
model are bright arcs, connected to flux tubes anchored mainly in the
accretion disk scale (Porth et al., 2021). In contrast, the FLARE images do
not show a permanent jet444as mentioned above jets are produced as transient
feature in the FLARE model. The flux is concentrated to the innermost disk
regions $r\sim 100\,\rm{\mu as}$ with a steep decay with decreasing frequency
as compared to the MAD model. Given these significant differences in the
images and in the spectral behaviour the two models should be distinguishable
in recent and future observations of the Event Horizon Telescope.

##  5 Conclusions

In this letter we stress out the importance of using well-studied MRI
turbulent discs for the interpretation of EHT and GRAVITY results. We discuss
the possibility that the magnetic field structure in the vicinity of the super
massive BH at the center of our galaxy, SgrA*, may be totally dictated by the
action of the MRI. This would have as a consequence that the inner accretion
flow will never become magnetically arrested (MAD). We present in detail the
different ways to distinguish the two scenarios, mainly by the images in 43
and 86 GHz that will uncover an extended structure at the base, close to the
BH, but also the polarization signatures. These can be tested by near future
observations.

Results from global simulations of the MRI in accretion disks, provide
evidence for the action of the MRI and its impact to the magnetic field
geometry showing an alternating polarity in an 6-8 hours periodicity. When
poloidal field of different polarity is accreted, it reconnects and provides
an energy release to produce plasmoid/hot spots that can further be observed
as flares for SgrA*.

Lastly, we describe a specific GRMHD simulation that tries to mimic this
behavior for the production of plasmoids interchanging with states of
quiescence in the vicinity of the BH and we estimate the magnetic energy in
the range of $\approx 10^{35-38}\ {\rm erg}$ for the flares, assuming a decent
mass accretion rate of $\approx 10^{-8}\ M_{\odot}/year$ for SgrA*, and show
that the intrinsic poloidal magentic field in these flares can also explain
the observed polarization imprint (GRAVITY collaboration et al., 2018).

Acknowledgements.  The simulations were performed on GOETHE at CSC-Frankfurt.
AN was supported by the Hellenic Foundation for Research and Innovation
(H.F.R.I.) under the 2nd Call for H.F.R.I. Research Projects to support Post-
Doctoral Researchers (Project Number: 00634) This research is supported by the
DFG research grant “Jet physics on horizon scales and beyond" (Grant No. FR
4069/2-1) and the ERC synergy grant “BlackHoleCam: Imaging the Event Horizon
of Black Holes" (Grant No. 610058)
Data Availability.  The data underlying this article will be shared on
reasonable request to the corresponding author.

##

## References

  * Anantua et al. (2020) Anantua R., Ressler S., Quataert E., 2020, Mon. Not. R. Astron. Soc., 493, 1404
  * Baganoff et al. (2003) Baganoff F. K., et al., 2003, Astrophys. J., 591, 891
  * Balbus & Hawley (1991) Balbus S. A., Hawley J. F., 1991, Astrophys. J., 376, 214
  * Balbus & Henri (2008) Balbus S. A., Henri P., 2008, Astrophys. J., 674, 408
  * Ball et al. (2020) Ball D., Özel F., Christian P., Chan C.-K., Psaltis D., 2020, arXiv e-prints, p. arXiv:2005.14251
  * Beckwith et al. (2011) Beckwith K., Armitage P. J., Simon J. B., 2011, Mon. Not. R. Astron. Soc., 416, 361
  * Bouffard et al. (2019) Bouffard É., Haggard D., Nowak M. A., Neilsen J., Markoff S., Baganoff F. K., 2019, Astrophys. J., 884, 148
  * Bower et al. (2019) Bower G. C., et al., 2019, Astrophys. J. Lett., 881, L2
  * Brandenburg & Nordlund (2011) Brandenburg A., Nordlund Åke., 2011, Reports on Progress in Physics, 74, 046901
  * Brandenburg et al. (1995) Brandenburg A., Nordlund A., Stein R. F., Torkelsson U., 1995, Astrophys. J., 446, 741
  * Chandrasekhar (1960) Chandrasekhar S., 1960, Proc. Natl. Acad. Sci., 46, 253
  * Chatterjee et al. (2020) Chatterjee K., et al., 2020, arXiv e-prints, p. arXiv:2011.08904
  * Contopoulos & Kazanas (1998) Contopoulos I., Kazanas D., 1998, Astrophys. J., 508, 859
  * Contopoulos et al. (2015) Contopoulos I., Nathanail A., Katsanikas M., 2015, Astrophys. J., 805, 105
  * Contopoulos et al. (2018) Contopoulos I., Nathanail A., Sa̧dowski A., Kazanas D., Narayan R., 2018, Mon. Not. R. Astron. Soc., 473, 721
  * Cruz-Osorio et al. (2022) Cruz-Osorio A., et al., 2022, Nature Astronomy, 6, 103
  * Davelaar et al. (2018) Davelaar J., Mościbrodzka M., Bronzwaer T., Falcke H., 2018, Astron. Astrophys., 612, A34
  * Dexter et al. (2020) Dexter J., et al., 2020, Mon. Not. R. Astron. Soc., 494, 4168
  * Dhang & Sharma (2019) Dhang P., Sharma P., 2019, Mon. Not. R. Astron. Soc., 482, 848
  * Dhang et al. (2020) Dhang P., Bendre A., Sharma P., Subramanian K., 2020, Mon. Not. R. Astron. Soc., 494, 4854
  * Doeleman et al. (2008) Doeleman S. S., et al., 2008, Nature, 455, 78
  * Faghei & Mollatayefeh (2012) Faghei K., Mollatayefeh A., 2012, Mon. Not. R. Astron. Soc., 422, 672
  * Falcke et al. (1998) Falcke H., Goss W. M., Matsuo H., Teuben P., Zhao J.-H., Zylka R., 1998, Astrophys. J., 499, 731
  * Fromm et al. (2021) Fromm C. M., et al., 2021, Astron. Astrophys., 649, A116
  * GRAVITY collaboration et al. (2018) GRAVITY collaboration Abuter R., et al., 2018, Astron. Astrophys., 618, L10
  * Giannios & Uzdensky (2019) Giannios D., Uzdensky D. A., 2019, Mon. Not. R. Astron. Soc., 484, 1378
  * Gold et al. (2017) Gold R., McKinney J. C., Johnson M. D., Doeleman S. S., 2017, Astrophys. J., 837, 180
  * Goodman & Xu (1994) Goodman J., Xu G., 1994, Astrophys. J., 432, 213
  * Gravity Collaboration et al. (2019) Gravity Collaboration et al., 2019, Astron. Astrophys., 625, L10
  * Guilet & Ogilvie (2013) Guilet J., Ogilvie G. I., 2013, Mon. Not. R. Astron. Soc., 430, 822
  * Hawley et al. (1996) Hawley J. F., Gammie C. F., Balbus S. A., 1996, Astrophys. J., 464, 690
  * Heyvaerts et al. (1996) Heyvaerts J., Priest E. R., Bardou A., 1996, Astrophys. J., 473, 403
  * Hogg & Reynolds (2018) Hogg J. D., Reynolds C. S., 2018, Astrophys. J., 861, 24
  * Johnson et al. (2015) Johnson M. D., et al., 2015, Science, 350, 1242
  * Liska et al. (2018) Liska M. T. P., Tchekhovskoy A., Quataert E., 2018, arXiv e-prints, p. arXiv:1809.04608
  * Loeb (2004) Loeb A., 2004, Mon. Not. R. Astron. Soc., 350, 725
  * Lovelace et al. (2009) Lovelace R. V. E., Rothstein D. M., Bisnovatyi-Kogan G. S., 2009, Astrophys. J., 701, 885
  * Lubow et al. (1994) Lubow S. H., Papaloizou J. C. B., Pringle J. E., 1994, Mon. Not. R. Astron. Soc., 268, 1010
  * Mahlmann et al. (2020) Mahlmann J. F., Levinson A., Aloy M. A., 2020, Mon. Not. R. Astron. Soc., 494, 4203
  * Martins et al. (2007) Martins F., Genzel R., Hillier D. J., Eisenhauer F., Paumard T., Gillessen S., Ott T., Trippe S., 2007, Astron. Astrophys., 468, 233
  * Matsumoto et al. (2020) Matsumoto T., Chan C.-H., Piran T., 2020, Mon. Not. R. Astron. Soc., 497, 2385
  * Mościbrodzka et al. (2016) Mościbrodzka M., Falcke H., Shiokawa H., 2016, Astron. Astrophys., 586, A38
  * Nathanail et al. (2020) Nathanail A., Fromm C. M., Porth O., Olivares H., Younsi Z., Mizuno Y., Rezzolla L., 2020, MNRAS, 495, 1549
  * Nathanail et al. (2021) Nathanail A., Mpisketzis V., Porth O., Fromm C. M., Rezzolla L., 2021, arXiv e-prints, p. arXiv:2111.03689
  * Papaloizou & Pringle (1984) Papaloizou J. C. B., Pringle J. E., 1984, Mon. Not. R. Astron. Soc., 208, 721
  * Parfrey et al. (2015) Parfrey K., Giannios D., Beloborodov A. M., 2015, Mon. Not. R. Astron. Soc., 446, L61
  * Porth et al. (2017) Porth O., Olivares H., Mizuno Y., Younsi Z., Rezzolla L., Moscibrodzka M., Falcke H., Kramer M., 2017, Computational Astrophysics and Cosmology, 4, 1
  * Porth et al. (2019) Porth O., et al., 2019, Astrophys. J. Supp., 243, 26
  * Porth et al. (2021) Porth O., Mizuno Y., Younsi Z., Fromm C. M., 2021, Mon. Not. R. Astron. Soc.,
  * Quataert (2004) Quataert E., 2004, Astrophys. J., 613, 322
  * Quataert & Narayan (1999) Quataert E., Narayan R., 1999, Astrophys. J., 516, 399
  * Ressler et al. (2020a) Ressler S. M., Quataert E., Stone J. M., 2020a, Mon. Not. R. Astron. Soc., 492, 3272
  * Ressler et al. (2020b) Ressler S. M., White C. J., Quataert E., Stone J. M., 2020b, Astrophys. J. Lett., 896, L6
  * Ripperda et al. (2020) Ripperda B., Bacchini F., Philippov A. A., 2020, Astrophys. J., 900, 100
  * Shcherbakov & Baganoff (2009) Shcherbakov R. V., Baganoff F. K., 2009, ArXiv.0912.3255,
  * Sorathia et al. (2012) Sorathia K. A., Reynolds C. S., Stone J. M., Beckwith K., 2012, Astrophys. J., 749, 189
  * Velikhov (1959) Velikhov E. P., 1959, Sov. Phys. JETP, 9, 995
  * Xu (2013) Xu Y.-D., 2013, Astrophys. J., 763, 75
  * Younsi et al. (2012) Younsi Z., Wu K., Fuerst S. V., 2012, Astron. Astrophys., 545, A13
  * Younsi et al. (2020) Younsi Z., Porth O., Mizuno Y., Fromm C. M., Olivares H., 2020, in Asada K., de Gouveia Dal Pino E., Giroletti M., Nagai H., Nemmen R., eds, IAU Symposium Vol. 342, Perseus in Sicily: From Black Hole to Cluster Outskirts. pp 9–12 (arXiv:1907.09196), doi:10.1017/S1743921318007263
  * Yuan & Narayan (2014) Yuan F., Narayan R., 2014, Annual Review of Astronomy and Astrophysics, 52, 529