** We develop a constructive theory of finite multisets, defining them as free commutative monoids in Homotopy Type Theory. We formalise two algebraic presentations of this construction using 1-HITs, establishing the universal property for each and thereby their equivalence. These presentations correspond to equational theories including a commutation axiom. In this setting, we prove important structural combinatorial properties of singleton multisets arising from concatenations and projections of multisets. This is done in generality, without assuming decidable equality on the carrier set. Further, as applications, we present a constructive formalisation of the relational model of differential linear logic and use it to characterise the equality type of multisets. This leads us to the introduction of a novel conditional equational presentation of the finite-multiset construction. **

** We present the type theory CaTT, originally introduced by Finster and Mimram to describe globular weak $\omega$-categories, and we formalise this theory in the language of homotopy type theory. Most of the studies about this type theory assume that it is well-formed and satisfy the usual syntactic properties that dependent type theories enjoy, without being completely clear and thorough about what these properties are exactly. We use the formalisation that we provide to list and formally prove all of these meta-properties, thus filling a gap in the foundational aspect. We discuss the key aspects of the formalisation inherent to the theory CaTT, in particular that the absence of definitional equality greatly simplify the study, but also that specific side conditions are challenging to properly model. We present the formalisation in a way that not only handles the type theory CaTT but also all the related type theories that share the same structure, and in particular we show that this formalisation provides a proper ground to the study of the theory MCaTT which describes the globular, monoidal weak $\omega$-categories. The article is accompanied by a development in the proof assistant Agda to actually check the formalisation that we present. **

** Survival outcomes are common in comparative effectiveness studies and require unique handling because they are usually incompletely observed due to right-censoring. A "once for all" approach for causal inference with survival outcomes constructs pseudo-observations and allows standard methods such as propensity score weighting to proceed as if the outcomes are completely observed. For a general class of model-free causal estimands with survival outcomes on user-specified target populations, we develop corresponding propensity score weighting estimators based on the pseudo-observations and establish their asymptotic properties. In particular, utilizing the functional delta-method and the von Mises expansion, we derive a new closed-form variance of the weighting estimator that takes into account the uncertainty due to both pseudo-observation calculation and propensity score estimation. This allows valid and computationally efficient inference without resampling. We also prove the optimal efficiency property of the overlap weights within the class of balancing weights for survival outcomes. The proposed methods are applicable to both binary and multiple treatments. Extensive simulations are conducted to explore the operating characteristics of the proposed method versus other commonly used alternatives. We apply the proposed method to compare the causal effects of three popular treatment approaches for prostate cancer patients. **

** For points $(a,b)$ on an algebraic curve over a field $K$ with height $\mathfrak{h}$, the asymptotic relation between $\mathfrak{h}(a)$ and $\mathfrak{h}(b)$ has been extensively studied in diophantine geometry. When $K=\overline{k(t)}$ is the field of algebraic functions in $t$ over a field $k$ of characteristic zero, Eremenko in 1998 proved the following quasi-equivalence for an absolute logarithmic height $\mathfrak{h}$ in $K$: Given $P\in K[X,Y]$ irreducible over $K$ and $\epsilon>0$, there is a constant $C$ only depending on $P$ and $\epsilon$ such that for each $(a,b)\in K^2$ with $P(a,b)=0$, $$ (1-\epsilon) \deg(P,Y) \mathfrak{h}(b)-C \leq \deg(P,X) \mathfrak{h}(a) \leq (1+\epsilon) \deg(P,Y) \mathfrak{h}(b)+C. $$ In this article, we shall give an explicit bound for the constant $C$ in terms of the total degree of $P$, the height of $P$ and $\epsilon$. This result is expected to have applications in some other areas such as symbolic computation of differential and difference equations. **

** An adjunction is a pair of functors related by a pair of natural transformations, and relating a pair of categories. It displays how a structure, or a concept, projects from each category to the other, and back. Adjunctions are the common denominator of Galois connections, representation theories, spectra, and generalized quantifiers. We call an adjunction nuclear when its categories determine each other. We show that every adjunction can be resolved into a nuclear adjunction. This resolution is idempotent in a strong sense. The nucleus of an adjunction displays its conceptual core, just as the singular value decomposition of an adjoint pair of linear operators displays their canonical bases. The two composites of an adjoint pair of functors induce a monad and a comonad. Monads and comonads generalize the closure and the interior operators from topology, or modalities from logic, while providing a saturated view of algebraic structures and compositions on one side, and of coalgebraic dynamics and decompositions on the other. They are resolved back into adjunctions over the induced categories of algebras and of coalgebras. The nucleus of an adjunction is an adjunction between the induced categories of algebras and coalgebras. It provides new presentations for both, revealing the meaning of constructing algebras for a comonad and coalgebras for a monad. In his seminal early work, Ross Street described an adjunction between monads and comonads in 2-categories. Lifting the nucleus construction, we show that the resulting Street monad on monads is strongly idempotent, and extracts the nucleus of a monad. A dual treatment achieves the same for comonads. Applying a notable fragment of pure 2-category theory on an acute practical problem of data analysis thus led to new theoretical result. **