Synthetic topology in Homotopy Type Theory for probabilistic programming

The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial σ-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies, we define valuations and lower integrals on sets and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed.

A Topology on a Hyper BCI-algebra Generated by a Hyper-order

In this paper, we introduce an operator on a hyper BCI-algebra via application of aleft hyper-order. The family consisting of the images of subsets under the operator turns out to be a base for some topology on the hyper BCI-algebra. We investigate some important properties of the induced topology on certain hyper BCI-algebras. In particular, we show that the generated topology on a non-trivial hyper subalgebra of an ordered hyper BCI-algebra coincides with the relative topology on this hyper subalgebra.

Metric spaces related to Abelian groups

<p>When working with a metric space, we are dealing with the additive group (R, +). Replacing (R, +) with an Abelian group (G, ∗), offers a new structure of a metric space. We call it a G-metric space and the induced topology is called the G-metric topology. In this paper, we are studying G-metric spaces based on L-groups (i.e., partially ordered groups which are lattices). Some results in G-metric spaces are obtained. The G-metric topology is defined which is further studied for its topological properties. We prove that if G is a densely ordered group or an infinite cyclic group, then every G-metric space is Hausdorff. It is shown that if G is a Dedekind-complete densely ordered group, (X, d) a G-metric space, A ⊆ X and d is bounded, then f : X → G with f(x) = d(x, A) := inf{d(x, a) : a ∈ A} is continuous and further x ∈ cl_XA if and only if f(x) = e (the identity element in G). Moreover, we show that if G is a densely ordered group and further a closed subset of R, K(X) is the family of nonempty compact subsets of X, e &lt; g ∈ G and d is bounded, then d′ (A, B) &lt; g if and only if A ⊆ N_d(B, g) and B ⊆ N_d(A, g), where N_d(A, g) = {x ∈ X : d(x, A) &lt; g}, d_B(A) = sup{d(a, B) : a ∈ A} and d′ (A, B) = sup{d_A(B), d_B(A)}.</p>

Some Remarks on Fuzzy sb-Metric Spaces

Fuzzy strong b-metrics called here by fuzzy sb-metrics, were introduced recently as a fuzzy version of strong b-metrics. It was shown that open balls in fuzzy sb-metric spaces are open in the induced topology (as different from the case of fuzzy b-metric spaces) and thanks to this fact fuzzy sb-metrics have many useful properties common with fuzzy metric spaces which generally may fail to be in the case of fuzzy b-metric spaces. In the present paper, we go further in the research of fuzzy sb-metric spaces. It is shown that the class of fuzzy sb-metric spaces lies strictly between the classes of fuzzy metric and fuzzy b-metric spaces. We prove that the topology induced by a fuzzy sb-metric is metrizable. A characterization of completeness in terms of diameter zero sets in these structures is given. We investigate products and coproducts in the naturally defined category of fuzzy sb-metric spaces.

On Metric-Type Spaces Based on Extended T-Conorms

Kirk and Shahzad introduced the class of strong b-metric spaces lying between the class of b-metric spaces and the class of metric spaces. As compared with b-metric spaces, strong b-metric spaces have the advantage that open balls are open in the induced topology and, hence, they have many properties that are similar to the properties of classic metric spaces. Having noticed the advantages of strong b-metric spaces Kirk and Shahzad complained about the absence of non-trivial examples of such spaces. It is the main aim of this paper to construct a series of strong b-metric spaces that fail to be metric. Realizing this programme, we found it reasonable to consider these metric-type spaces in the context when the ordinary sum operation is replaced by operation ⊕, where ⊕ is an extended t-conorm satisfying certain conditions.