{'fraction_non_alphanumeric': 0.037705446342249434, 'fraction_numerical': 0.01218578794714792, 'mean_word_length': 4.504934028162768, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 11, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism

The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization (the first one to the best of our knowledge) in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a non-trivial interface which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories.


INTRODUCTION
In their ICFP paper "Just do It: Simple Monadic Equational Reasoning" [Gibbons and Hinze 2011], the authors present an axiomatic approach to reason about programs with effects using equational reasoning, thus recovering one of the appeals of pure functional programming. This approach uses monads to encapsulate the effects and is called monadic equational reasoning. In particular, to handle the effects of probability and nondeterminism, Gibbons and Hinze propose a combination of two interfaces: one for monads equipped with an operator for probabilistic choice and one for monads equipped with an operator for nondeterministic choice. It was later observed that in the proposed combination the authors "got [the algebraic properties that characterise their interaction] wrong" [Abou-Saleh et al. 2016]. The problem was that right-distributivity of bind over probabilistic choice is not compatible with distributivity of probabilistic choice over nondeterministic choice. Fortunately, the previous work in question [Gibbons and Hinze 2011] was not relying on this mistake. Yet, this stresses the need for a formal account of combinations of interfaces (representing algebraic theories) and the monads realizing them.
While many sets of axioms have been suggested as axiomatizations of the combination of probabilistic and nondeterministic choice, only few give rise to interesting models [Keimel and Plotkin 2017;Mislove et al. 2004]. We will stick here to Gibbons and Hinze's axiomatization, removing just the incriminated right-distributivity.
We can rely on a large body of work to model formally the combination of probabilistic and nondeterministic choice (e.g., [Beaulieu 2008;Cheung 2017;Gibbons 2012;Keimel and Plotkin 2017;Mislove 2000;Tix et al. 2009;Varacca and Winskel 2006], and much more if we consider concurrency). So what should be a monad modeling this axiomatization? Since we already have the finite powerset monad and the finitely-supported distributions monad for these two choices, one could think of composing them using monadic distributive laws [Beck 1969]. Unfortunately, it has been proved that distributivity between these two monads is impossible [Varacca and Winskel 2006, Proposition 3.2]. We thus have to rethink the construction of a model by looking into what it should be more precisely. The presence of probabilistic choice suggests that sets of distributions might be a model, like it is the case with the probability monad. Yet, the semantics must also be convex-closed because if two distributions d 1 and d 2 are possible outcomes, so is any convex combination pd 1 + (1 − p)d 2 (0 ≤ p ≤ 1) of them [Gibbons 2012, Sect. 5.2]. Convexity is in particular necessary to have idempotence of probabilistic choice. Unfortunately these observations do not readily lead to a formalization, as they leave many technical details unsettled. In his PhD thesis, Cheung derives a monad (called the geometrically convex monad) for the theory resulting from the combination of the effects of probability and nondeterminism [Cheung 2017, Chapter 6]. His pencil-and-paper construction highlights the central role of several technical devices of independent interest: the notion of convex spaces [Fritz 2015;Jacobs 2010;Stone 1949] to formalize convexity without resorting to vector spaces and Beaulieu's operator for infinite nondeterministic choice [Beaulieu 2008, Def. 3.2.3].
But we should not forget that the original incentive for a formalization of a monad that combines probabilistic and nondeterministic choices is monadic equational reasoning. There actually exists a formalization in the C proof assistant [The Coq Development Team 2019a] of the many examples of Gibbons et al. in the form of a library called M [Affeldt et al. 2019]. It comes with concrete monads modeling several interfaces except the one that combines probabilistic and nondeterministic choices, because it is arguably more difficult than the others.
Contributions. In this paper, we provide a formal construction of the geometrically convex monad. To the best of our knowledge, this is the first formalization of a monad that supports probabilistic and nondeterministic choices. It has been carried out in the C proof assistant.
Our formalization of the geometrically convex monad has a direct application: it is used to complete an existing formalization of monadic equational reasoning. The latter was assuming the existence of a such monad without a model; our work improves the trusted base of this practical tool by filling this hole.
Our main contribution (the formalization of the geometrically convex monad) is made possible by a number of technical contributions of independent interest: a formalization of convex spaces (the first formalization to the best of our knowledge), a formalization of semicomplete semilattice structures, an original formalization of concrete categories, and extensions to an existing theory of finitely-supported probability distributions. We will discuss the technical decisions that made it possible to develop these formalizations in such a way that they all fit together to achieve a formalization of the geometrically convex monad.
Paper Outline. In Sect. 2, we clarify our formalization target by reviewing the formalization of monadic equational reasoning we aim at extending. We explain the operators of interest and their properties, and we give an overview of the construction of the geometrically convex monad. In Sect. 3, we give an overview of a formalization of convex spaces, an important ingredient of our construction to represent probabilistic choice, convex sets, hulls, and affine functions. In Sect. 4, we explain the formalization of semicomplete semilattice structures, which provide an operator to represent a nondeterministic choice compatible with the probabilistic choice. In Sect. 5, we explain a formalization of concrete categories to build monads out of adjoint functors. In Sect. 6, we define several adjunctions, from which we derive the geometrically convex monad through composition. Finally, in Sect. 7, we verify that the geometrically convex monad can be equipped with the combined choice and that the latter enjoys the expected properties. We further comment on related work in Sect. 8 and conclude in Sect. 9. About Notations. This paper displays C source code as it is, with some beautification to ease reading using L A T E X symbols instead of ASCII art. When there are too much details we omit parts of the source code and instead provide a paraphrase and indicate to the reader where to look in the formalization. Otherwise, we use standard mathematical notations, sometimes augmented to avoid too much overloading (for example, we note f @(X ) the direct image of the set X by f but F #( ) the application of the functor F to the morphism ).

FORMALIZATION TARGET AND APPROACH
Our goal is to construct a monad that combines probabilistic and nondeterministic choices. This corresponds to the monad intended by Gibbons et al. [Gibbons and Hinze 2011]. We here review a formalization in C of Gibbons et al. 's monads and their interfaces. Our formalization target is a monad of type altProbMonad. Figure 1 provides an excerpt of an existing hierarchy of effects [Affeldt et al. 2019] that includes the ones by Gibbons et al. [Gibbons 2012;Gibbons and Hinze 2011]   We assume given two types functor and monad for endofunctors and monads on Coq's Type universe. The type monad is equipped with a join operator Join and a unit operator Ret. In this section we rather use the bind operator, defined as m ≫= f = Join(M#(f )m) for the monad M. The precise definitions of functor and monad are not relevant at this stage but can be found in related work [Affeldt et al. 2019, Sect. 2.1].

An Existing Hierarchy of Probability-related Monads
Note that these so-called "types" are actually data-structures that provide the same functionality as type classes in Agda [The Agda Team 2020] or Idris [Brady 2013], i.e., providing an implementation for such a type amounts to defining an instance of the corresponding type class. Moreover, thanks to implicit coercions, this implementation itself can be used as a type, so that assuming (M : monad) allows one to write the type M T of computations resulting in a value of type T inside the monad M. The other nodes represent various monad types, that extend monad through the incremental additions of mixins, using the methodology of packed classes [Garillot et al. 2009].
We first extend the type monad into the type of the probability monad probMonad. The interface of probMonad takes the form of a mixin that introduces an operator for probabilistic choice a ◁ p ▷ b, where a and b are computations and p is a probability, i.e., a real number p such that 0 ≤ p ≤ 1. The intuition is that the computation a ◁ p ▷ b represents the computation a with probability p or the computation b with probability 1−p. The properties, or axioms, of the interface are identity axioms (lines 4 and 5), skewed commutativity (line 6), idempotence (line 7), quasi-associativity (line 8), and the fact that bind left-distributes over probabilistic choice (line 11) (see also [Affeldt et al. 2020, file proba_monad.v]). (p = r * s : In C , the type prob is for probabilities. The notation %:pr turns a real number into a probability when possible. The notation p.~is for 1 -p (often written p on paper). Skewed commutativity allows to derive one of the identity axioms from the other; here we are just preserving the original interface from Gibbons and Hinze [Gibbons and Hinze 2011]. The monad type probDrMonad extends probMonad with right-distributivity of bind over probabilistic choice. We do not display its implementation because we do not model this monad in this paper; we mention it for the sake of completeness.
The monad type altMonad introduces an operator ◻ for nondeterministic choice 1 . Besides associativity of nondeterministic choice (line 15 below), it also states that bind left-distributes over nondeterministic choice (line 16) (see also [Affeldt et al. 2020, file fail_monad.v]), as specified by the following mixin: Gibbons and Hinze do not require right-distributivity (i.e., m ≫= (λx . k 1 x ◻ k 2 x) = (m ≫= k 1 ) ◻ (m ≫ = k 2 )) by default, due in particular to undesirable interactions with non-idempotent effects [Gibbons and Hinze 2011, Sect. 4.2]. The monad type altCIMonad extends altMonad with commutativity and idempotence of nondeterministic choice, which we express by the following mixin, where op x y stands for x ◻ y. Finally, in the monad type altProbMonad, probabilistic choice distributes over nondeterministic choice, which we express by another mixin, where op p x y is intended to denote x ◁ p ▷ y. Implementation of Inheritance Relations with Packed Classes. Up to now, we have only shown the mixin part of the inheritance hierarchy. The packed class methodology [Garillot et al. 2009] actually contains three ingredients: mixins, types (implemented as structures), and classes. Here are the class and structure definitions for altProbMonad. The class definition inherits from altCIMonad through its class (line 24), and extends it with two mixins, the one we have seen for probMonad (line 25), and the extra distributivity axiom we have just defined (line 26). The structure then packs together the type operator m which can be implicitly accessed through a coercion, with the above defined class. Finally, the triple mixin-classstructure is completed with extra coercions and unification hints (provided by the Canonical command [Mahboubi and Tassi 2013] of C ) to achieve the inheritance relations depicted in Fig. 1.
Sample Programs. Last, let us reproduce for illustration sample programs by Gibbons [Gibbons 2012, Sect. 5.1] using the operators we have introduced so far in the syntax of M . Here is a biased coin, with probability p of returning true and probability p of returning false: Here is an arbitrary nondeterministic choice between Booleans: Definition arb {M : altMonad} : M bool := Ret true ◻ Ret false.
Using the do notation instead of the bind operator, these two programs can be used to make an arbitrary choice followed by a probabilistic choice:

Alternative Axiomatizations
As we mentioned in the introduction, the axiomatization of combined choice we have followed is not the only possible one. We will consider shortly two other possible axiomatizations for which non-trival models are known.
The first one is obtained by replacing the distributivity axiom added in altProbMonad by the dual one, i.e., distributivity of nondeterministic choice over probabilistic choice.
Keimel et al. [Keimel and Plotkin 2017] have shown that in this case probabilities different from 0 and 1 become undistinguishable (i.e., x ◁ p ▷ y = x ◁ q ▷ y for any 0 < p,q < 1). This means that the algebraic theory of combined choice in this case boils down to a bi-semilattice (two semilattices with their operators mutually distributing over each other), which can be modeled by finite sets of finite sets, easily turned into a monad. While the monad construction is easy, the structure is poor, as all probability information is lost, so we did not try to formalize this axiomatization. This also means that this axiomatization is equivalent to the one with both distributivity axioms, as the original axiom can be derived from the dual one. Another way to reach the same axiomatization is to inherit from probDrMonad rather than probMonad [Abou-Saleh et al. 2016, Sect. 3]. It appears that, while left-distributivity of bind over probabilistic choice is fine alone, right-distributivity can be used to deduce the distributivity of nondeterministic choice over probabilistic choice from its dual, which leads to the same collapse of probability information as above.
The second one is obtained by keeping the same distributivity axiom as in altProdMonad, but removing the idempotence of probabilistic choice from probMonad, i.e., we lose the equality x ◁ p ▷ x = x. Varacca [Varacca and Winskel 2006] has shown that this relaxed probMonad can be modeled by a monad of real quasi-cones, which distributes over the finite powerset monad modeling altCIMonad. As a result, one can use Beck's construction [Beck 1969] to create a monad combining both. While this is a clever approach, the loss of the idempotence axiom is dire, and Varacca presents in the same paper another construction using a convex powerset functor to obtain a model including the idempotence axiom, in a way similar to the geometrically convex powerdomain [Mislove 2000;Tix et al. 2009].
Ultimately, the only way to be sure that our choice of axioms follows our expectations, is to provide a model where we can check that different computations can be properly distinguished (which we will do with the geometrically convex monad in Sect. 7.2).

Formalization of the Geometrically Convex Monad: Overview
As already hinted at in the introduction (Sect. 1), a computation using the monadic operations defined in the type altProbMonad can be modeled by a non-empty convex set of finitely-supported probability distributions. Cheung provides a construction for such a monad and calls the resulting monad the geometrically convex monad [Cheung 2017, Chapter 6]. It is built by composition of adjunctions.
Adjunctions between the categories involved in the construction of the geometrically convex monad Figure 2 depicts four concrete categories related by three adjunctions. Each category is named after a C type to which it corresponds. The category C T corresponds to C 's type Type. The latter actually represents a countably infinite hierarchy of types Type 0 , Type 1 , . . . such that Type i is a subtype of Type i +1 . By default, C hides the indices to the user. We can regard Type as a category by seeing each Type i as a Grothendieck universe [Timany and Jacobs 2016]. The category C C corresponds to types with a choice function. The type choiceType [Garillot et al. 2009, Sect. 3.1] comes from the Mathematical Components library (hereafter, M C ) [Mathematical Components Team 2007]. The category C V corresponds to spaces with a convexity operator (for probabilistic choice) and the category C S corresponds to spaces with a convexity operator and an infinitary operator (for nondeterministic choice); the details of these two categories are one of the purposes of this paper. The three adjunctions are composed of six functors. The unit and counit of F C ⊣ U C are η C and ε C respectively (resp. η 0 , ε 0 for F 0 ⊣ U 0 and η 1 , ε 1 for F 1 ⊣ U 1 ). In particular, U C , U 0 , and U 1 are forgetful functors, which makes F C , F 0 , and F 1 free functors.
Our setting features three adjunctions while Cheung's has only two. The additional adjunction is the one between Type and choiceType. It comes from the fact that the formalization of monadic equational reasoning we build upon [Affeldt et al. 2019] represents monads as endofunctors over Type, whereas our construction requires types to be equipped with a choice function 2 . In practice, the functor F C only amounts to adding a choice function to the type, without changing the values. Note that, since we assume the existence of such a choice function for all types, we are actually adding the axiom of choice to the ambient logic, which is known to be sound in C [The Coq Development Team 2019b]. It is simpler to assume a well known axiom than to try to define all our monads on choiceType, and prove that all the types we use can actually be equipped with a concrete choice function.
The basis of the construction of the geometrically convex monad is easy to explain: by composing adjunctions, we build the adjunction Then we can derive the monad P ∆ = P right ∆ ○P left ∆ directly from this adjunction [Mac Lane 1998]. Yet, the formalization is difficult mostly for two reasons. First, it requires several non-trivial mathematical theories, which, to the best of our knowledge, could not be found in a single formal setting, in particular because some of them (e.g., convex spaces) have never been formalized before. Second, Cheung's construction could not be reproduced directly and we had to come up with some tuning to model nondeterminism (switching from a binary operator to an infinitary one) or to formalize categories (using concrete categories as a solution).

CONVEXITY TOOLBOX
A convex space is an algebraic structure allowing convex combinations of its elements by an operator satisfying several equational axioms. This axiom system can be used to define various related concepts: probabilistic choice, convex sets, convex hulls, affine functions, etc. More precisely, for our application, convex sets are used to represent computations in a monad modeling altProbMonad and convex hulls are used to represent nondeterminism.
In this section, we provide a formal definition of convex space (a.k.a. barycentric calculus [Stone 1949]) as a basis to represent the category C V (and later the category C S ) (both categories have been seen in Sect. 2.3) and we also provide definitions and lemmas to define in particular the functor F 1 . The most relevant file of the accompanying development for this section is [Affeldt et al. 2020, file convex_choice.v].
2 Actually, these choice functions are not used in our development itself, but choiceTypes are required due to our use of the F library [Cohen and Sakaguchi 2015] (which builds upon M C ). See Sect. 6.1 for more details.

Formalization of Convex Spaces
The interface of convex spaces is similar to the interface of the probMonad we saw in Sect. 2.1. It provides a similar operator a ◁ p ▷ b where a and b are elements of the convex space and p is a probability. The axioms about the operator are similar to the ones already explained in Sect. 2.1 (the reader can observe a difference of presentation for the axiom of quasi-associativity but it is not relevant). Of course, contrary to probMonad, convex spaces have no axiom about a bind operator.
Record mixin_of (T : choiceType) : The notation [s_of p, q] stands forpq; the notation [r_of p, q] stands for p pq. Here we assume the carrier type of convex spaces to be a choiceType.
The above mixin is used to define the type convType using the packed classes methodology (that we briefly overviewed in Sect. 2.1).
We can show for example that the real numbers form a convex space by taking the averaging function λp x . px +p to be the operator. Similarly, finitely-supported probability distributions form a convex space with the operator λp d 1 d 2 . pd 1 +pd 2 where d 1 and d 2 are distributions.
We will later need a generalization of the binary operator a ◁ p ▷ b to n points, namely d f , where f consists of n points and d is a distribution of n probabilities whose sum is 1.

Convex Sets and Convex Hulls
We use convex spaces to define convex sets and convex hulls. From now on, we put ourselves in a classical setting, by extending the logic of C with a number of axioms known to be compatible with it. Concretely, we use the axioms provided by M C A , an extension of M C for classical analysis [Affeldt et al. 2018]. In this setting, Prop and bool are equivalent (strong excluded middle), and we can freely embed Prop-valued formulas such as ∀ x, P x into bool using a notation: [<∀ x, P x>] : bool. From M C A , we also reuse a library of sets. Here sets mean sets of elements of a specific type. They are represented by Prop-valued characteristic functions, and thus not necessarily finite. The type set A stands for sets over the type A.
A set D is convex when any convex combination of any two points is still inside D: The hull of a set X is the set of points p such that p is the convex combination of points belonging to X . The notation [set p : T | P p] is for sets defined by comprehension.
We represent the n points to be combined as 0 , 1 , . . ., hence the function g : I_n → T from I_n, the M C type of natural numbers smaller than n. The notation g @ setT is for the direct image g@(setT) where setT is the full set (these are part of the library of sets that comes with the M C A library).

Affine Functions
We are interested in affine functions because they are used for the morphisms of the categories C V and C S (Sect. 2.3). In real analysis, affine functions correspond to the functions of the form x ↦ ax + b. But the real line is just an example of convex space, whose generic operator actually provides an easy, generic definition: If we endow convex spaces with an order, we can also define both convex and concave functions, and alternatively define affine functions as functions that are both convex and concave. As a sample proposition, we can observe that convex hulls are preserved by affine functions: This property will be used to define the functor F 1 , whose action on morphisms defined by the direct image needs to preserve convex hulls.

SEMICOMPLETE SEMILATTICE STRUCTURES
In this section, we define generic structures that provide an operator to represent nondeterministic choice in a way that is compatible with probabilistic choice. The most relevant file in the accompanying development is [Affeldt et al. 2020, file necset.v].
As a prerequisite, we introduce the type of non-empty sets. The type neset T is the type of sets over T that have at least one element. As a convenience, this type comes with a postfix notation %:ne such that s%:ne is the non-empty set corresponding to the set s. This notation infers the proof of non-emptiness in several situations such as when s is a singleton set, the image of a non-empty set, the union of non-empty sets, etc. using C 's canonical structures [Mahboubi and Tassi 2013].

Semicomplete Semila ice
The first structure we introduce provides a unary operator op that turns a non-empty set of elements into a single element (line 53). The first axiom of this structure says that this operator applied to a singleton set returns the sole element of the set (line 54). The second axiom starting at line 55 collapses a non-empty collection (the indexing set itself is not empty) of non-empty sets (f is the collection) into one element: The theory defined by this mixin is similar to Beaulieu's theory for infinite nondeterministic choice [Beaulieu 2008, Def. 3.2.3]. The difference is that the right-hand side of the second axiom in Beaulieu's work is expressed by means of a partition of the indexing set. We prefer to avoid dealing with partitions because in our experience they are heavy to deal with in formal proofs.
Hereafter we denote by ⊔ the operator introduced by the above mixin and use the mixin to define the type semiCompSemiLatt of semicomplete semilattices [Bergman 2015, p. 185].

Combining Semicomplete Semila ice with Convex Space
We now extend the structure of semicomplete semilattices from the previous section (Sect. 4.1) with an axiom that captures the interaction between the operator ⊔ and probabilistic choice. This interaction is akin to a distribution law that can be stated informally as follows: Formally, this axiom is provided as a mixin parameterized by a semicomplete semilattice and a ternary operator op indexed by a probability: We use this mixin to extend the type of semicomplete semilattices to the type of semicomplete semilattice convex spaces (semiCompSemiLattConvType in C scripts) that inherits both the properties of semicomplete semilattices (Sect. 4.1) and the properties of convex spaces (Sect. 3.1). The methodology to achieve this multiple inheritance is again the one of packed classes. We conclude this section with a sample property of the operator ⊔ that is both important and non-trivial: Variable L : semiCompSemiLattConvType. Lemma lub_op_hull (X : neset L) : ⊔ (hull X)%:ne = ⊔ X.
The proof is as follows. First, we lift the operator of convex spaces (◁p▷) from points to sets of points; we denote this lifted operator by (∶◁p▷∶). We use this lifted operator to define a new binary operator X ∶◻∶ Y ∶= ⋃ p∈[0, 1] X ∶◁p▷∶ Y . Second, we show that hull X = ⋃ i ∈N X ∶◻∶ X ∶◻∶ ⋯ ∶◻∶ X i +1 occurrences of X . Then, we show that ⊔(X ) = ⊔(X ∶◻∶ X ∶◻∶ ⋯ ∶◻∶ X ), using the property introduced by semicomplete semilattice convex spaces. Finally, we conclude the proof by appealing to the properties of semicomplete semilattices.
We will later provide a concrete example of use of the lemma lub_op_hull. It can also be used to establish technical results from Beaulieu's work (e.g., [Beaulieu 2008, p. 56, l. 3]) or similar ones as in Varacca and Winskel's work (e.g., [Varacca and Winskel 2006, Lemma 5.6]).

Instances with Non-empty Convex Sets
The definitions of semicomplete semilattices and of semicomplete semilattice convex spaces that we have provided in the previous sections are just interfaces. To instantiate them, it turns out that it suffices to use non-empty convex sets instead of mere non-empty sets. This is this instance that we will use in particular to produce the adjunction F 1 ⊣ U 1 .
Thus we start by extending the type neset of non-empty sets into the type necset of non-empty convex sets, using the definition from the Sect. 3.2 (and again the methodology of packed classes).
We then instantiate the semicomplete semilattice operator on nonempty convex sets using union and hull operators (necset A is the type of nonempty convex sets over a convex space A): This gives us in particular the type necset_semiCompSemiLattConvType A: a generic instance of semiCompSemiLattConvType where the carrier consists of non-empty convex sets over A, a convType.

FORMALIZATION OF CONCRETE CATEGORIES IN COQ
The purpose of this section is to provide a formalization of enough category theory to construct the geometrically convex monad. The interest of this formalization is that it comes as a conservative extension of related work (M [Affeldt et al. 2019]) and that it features an original use of concrete categories to achieve a shallow embedding of categories in the C proof assistant. The most relevant file in the accompanying development is [Affeldt et al. 2020, file category.v].

Formalization of Categories
5.1.1 Definition of Concrete Categories. As we saw in Sect. 2.3, we need to formalize several categories; this is in contrast with M , which could get along with the sole category of sets. Among the various possibilities, we chose to favor a definition (akin to a shallow embedding) that lets us use the typing relation of C to declare elements of an object and apply morphisms to them as if morphisms were ordinary C functions. Our solution is to represent categories with a universe à la Tarski, i.e., a type with an interpretation operation, or realizer, allowing us to regard terms of this type as types (the function el below at line 63). In this setting, we can look at the morphisms of a category through the realizer and identify morphisms as a subset of the function space (via the predicate defining the hom-set at line 64). In the code above, the modifier @ is a C feature to disable implicit arguments. The advantage of this definition is twofold. First, the parameter obj lets us choose how we index our objects and use this index to declare morphisms (e.g., f : el A → el B). Second, we can use morphisms as functions and apply them to elements, as illustrated by the following script: The result is by no way ad hoc: it actually corresponds to the definition of concrete categories. A category C is said to be concrete if it comes with a faithful functor from C to Set, that is, a functor whose action on each hom-set is injective. The indexing type obj and the realizer el together form the object part. The morphism part is directly represented by its images in Set, without specifying its source for which we did not find a use.

Categories to Build the Geometrically Convex Monad.
In this section, we instantiate our definition of concrete categories with the categories that were described in Sect. 2.3.
The Categories C T and C C . To define the category C T , we take the identity function as the realizer and the third argument of @Category.Mixin to be the true predicate fun _ _ _ ⇒ True, so that the faithful functor for the concrete category is full (i.e., surjective on hom-sets): Definition Type_category_mixin : Category.mixin_of Type := @Category.Mixin Type (fun x : Type ⇒ x) (fun _ _ _ ⇒ True) (fun⇒ I) (fun _ _ _ _ _ _ _ ⇒ I).
The command Canonical (that we already mentioned for its use in the packed classes methodology) provides a unification hint to C 's type-checker to automatically endow Type with a structure of category when needed. To define the category C C , we take the function (fun x : choiceType ⇒ Choice.sort x), that returns the carrier type (in Type) of its argument (we make Choice.sort appear explicitly here but it is actually an implicit coercion in C ). As for C T , the faithful functor is full: The Category of Convex Spaces C V . The objects are convex spaces (Sect. 3.1) and the morphisms are affine functions (between convex spaces). In our formalization, the objects are indexed by the type of convex spaces convType, and realized by its coercion into Type. The morphisms are affine functions between convex spaces. Contrary to the previous two examples, being affine is not just a true predicate and requires us to prove that the identity function over a convex space is affine (proof affine_function_id_proof) and that the composition of affine functions is affine (proof affine_function_comp_proof ): Definition convType_category_mixin : Category.mixin_of convType := @Category.Mixin convType (fun A : convType ⇒ A) AffineFunction.axiom affine_function_id_proof affine_function_comp_proof . Canonical convType_category := Category.Pack convType_category_mixin.
The Category of Semicomplete Semilattice Convex Spaces C S . The objects are semicomplete semilattice convex spaces (Sect. 4.2) and the morphisms are affine functions f such that f @(⊔ X ) = ⊔(f @(X )) for any non-empty convex set X . We can show that identity functions are such functions (proof lub_op_affine_id_proof) and that composition preserves these properties (proof lub_op_affine_co leading to the following definition of C S : Definition semiCompSemiLattConvType_category_mixin : Category.mixin_of semiCompSemiLattConvType := @Category.Mixin semiCompSemiLattConvType (fun U : semiCompSemiLattConvType ⇒ U) LubOpAffine.class_of lub_op_affine_id_proof lub_op_affine_comp_proof. Canonical semiCompSemiLattConvType_category := Category.Pack semiCompSemiLattConvType_category_mixin.

Formalization of Functors, Natural Transformations, and Monads
Equipped with the formalization of categories from the previous section, we now formalize functors, natural transformations, and monads. In the following, C and D are two categories. We encode a functor from C to D as an action on objects represented by a function m : C → D It is clear that the new, more general setting introduced above improves on this specialized setting because it makes it possible to talk about morphisms that are, e.g., affine functions. Hereafter, we denote by F # g the application of a functor F to a morphism g. Let F and G be two functors from C to D. We encode a natural transformation from F to G as a family of maps f : ∀ a, {hom F a ,G a} (hereafter, denoted by F / / / o G) such the naturality predicate holds: When F / / / o G is packed together with a proof of naturality, we have a genuine natural transformation that we denote by F ↝ G.
Finally, we define a monad as an endofunctor M equipped with two natural transformations: ret from the identify functor (denoted by We already said that our formalization of functors generalizes the one of M , the formal framework for monadic equational reasoning on which our work is based. Similarly, our formalization of monads generalizes the one of M in a conservative way. Concretely, we provide a function Monad_of_category_monad that given a monad (as defined just above) over the category C T , returns a monad as defined in M (over the category Set). This way, it will be possible to retrofit our formalization of the geometrically convex monad (the topic of the next section) back into M .

Formalization of Adjoint Functors
We use adjoint functors to build the geometrically convex monad. In this section, we recall the lemmas used for this construction and give a brief overview of their formalization. We do not provide all the technical details because these lemmas are well-known lemmas and their formalization follows naturally from the definitions we saw so far (and whose design decisions are more important).
In C , we provide the notation F ⊣ G for the following type (where the categories C and D are implicit arguments): AdjointFunctors.t : ∀ C D : category, functor C D → functor D C → Type To build an adjunction, one needs to provides two natural transformations eta and eps together with the proofs that they satisfy the triangular laws. The corresponding constructors has the following type (where all arguments expect the proofs of the triangular laws are implicit):

Composition of Adjunction.
It is well-known that two adjunction F ⊣ G (with unit/counit η/ε) and F ′ ⊣ G ′ (with unit/counit η ′ /ε ′ ) can be composed to form another adjunction F ′ ○F ⊣ G ○G ′ by taking the unit to be λA. G#(η ′ (F A )) ○ η A ) and the counit to be λA. ε ′ A ○ F ′ #(ε(G ′ A )). Using the constructs we have defined so far, we provide a C function that performs this composition:

Monad Defined by Adjointness.
It is well-known that an adjunction F ⊣ G gives rise to a monad G ○ F by taking η to be the unit and λA. G#(ε(F A )) to be the join operator. In our formalization, this construction takes the form the following function: Monad_of_adjoint : ∀ (C D : category) (F : functor C D) (G : functor D C), F ⊣ G → monad C Observe that contrary to M where all monads are over the category Set, here our monad is over some category C which appears explicitly in the type.

ADJOINT FUNCTORS FOR THE GEOMETRICALLY CONVEX MONAD
At this point, we have explained the formalization of all the elements necessary to construct the geometrically convex monad: convex spaces in Sect. 3, semicomplete semilattice structures in Sect. 4, and category theory in Sect. 5. In this section, we explain the formalization of the adjunctions explained in Sect. 2.3. The most relevant file from the accompanying development is [Affeldt et al. 2020, file gcm_model.v]. 6.1 The Adjunction F C ⊣ U C The existence of the adjunction F C ⊣ U C in our formalization is technical: it comes from the use of the C type Type in M and the need to use a choiceType in the definition of finitely-supported distributions.
Let us first define the functor F C from C T to C C . The action on objects consists in turning a type in Type into a choiceType. This is performed by the function choice_of_Type which relies on an axiom inherited from a M C library and whose validity is explained elsewhere [Affeldt et al. The purpose of the function hom_choiceType is to turn a C function between two choiceTypes into a morphism of the category C C . I from the C standard library is a trivial proof that f is indeed a morphism; it is sufficient here because in this category all functions are morphisms (see the accompanying development [Affeldt et al. 2020] for the notation Hom). The functor laws are trivially proved and together with the definitions above, this leads to the definition of the functor free_choiceType of type functor C T C C . The definition of the corresponding forgetful functor U C is similar. The main difference is that instead of using the function choice_of_Type to augment a type in Type, we use the coercion Choice.sort that retrieved the carrier type of a choiceType (see forget_choiceType in [Affeldt et al. 2020, file gcm_model.v]).
The unit η C ∶ 1 ↝ U C ○ F C and the counit ε c ∶ F C ○ U C ↝ 1 are also essentially identity functions and the proofs of the triangular laws are therefore trivial.
6.2 The Adjunction F 0 ⊣ U 0 The second adjunction F 0 ⊣ U 0 corresponds to the probability monad [Giry 1982]. It relies on an existing formalization of finitely-supported distributions [Affeldt et al. 2019, Sect. 6.2] that we recall briefly. In the definition of FSDist.t below, the first field (line 128) is a finitely-supported function f from the choiceType A to the type of real numbers from the standard C library; this function evaluates to 0 outside its support finsupp f. The second (anonymous) field (line 129) contains proofs that (1) the probability function outputs positive reals and that (2) its outputs sum to 1. It is important to observe that FSDist.t has type choiceType → choiceType and can therefore be used to build an endofunctor and a monad on top of it. Hereafter, {dist A} is a notation for FSDist.t A.
6.2.1 Functors. The action on morphisms of F 0 is the map of the probability monad associated with finitely-supported distributions. Indeed, let ⋅ ◁ ⋅ ▷ ⋅ be the operation of the convex space of finitely-supported distributions (see Sect. 3.1) and let ≫= be the bind operator of the probability monad. We have which is equivalent to the map of the probability monad being affine.
In C , we define the action on morphisms of F 0 as follows, where FSDistfmap is the map operation of the probability monad: The type FSDist_convType A is the type of convex spaces of finitely-supported distributions over A.
We can show that free_convType_mor satisfies the functor laws (proofs free_convType_mor_id and free_convType_mor_comp), leading to the definition of the functor F 0 (recall the definitions of Sect. 5.2): Definition free_convType : functor C C C V := Functor.Pack (Functor.Mixin free_convType_mor_id free_convType_mor_comp).
The constructors Functor.Mixin and Functor.Pack are respectively for the mixin and the type of functors explained in Sect. 5.2. The forgetful functor U 0 of type functor C V C C is just formalized by substituting the category C V by the category C C in morphisms (see forget_convType in [Affeldt et al. 2020, file gcm_model.v]).
6.2.2 Counit / unit. The counit is the natural transformation ε 0 ∶ F 0 ○U 0 ↝ 1 C V essentially defined by the following function: In this definition, C is a convType; the operation ⋅ ⋅ has been explained in Sect. 3.1. Intuitively, ε 0 corresponds to the computation of a barycenter.
The unit is the natural transformation η 0 ∶ 1 C C ↝ U 0 ○ F 0 defined by the point-supported distribution FSDist1.d: The proofs of the triangular laws required us to substantially enrich the theory of finitelysupported distributions of M . The reason can be understood by looking at the proof of the left triangular law triL0. The latter essentially amounts to prove that we have for any probability distribution d: One can observe that this statement involves distributions of distributions Check FSDistfmap (@FSDist1.d C) d : {dist {dist C}}. whose properties called for new lemmas. Comparatively, the proof of the right triangular law triR0 is simpler.
6.3 The Adjunction F 1 ⊣ U 1 6.3.1 Functors. The action on objects of F 1 is necset_semiCompSemiLattConvType, explained in Sect. 4.3. The action on morphisms of F 1 is defined by the direct image f ↦ λX . f @(X ) (where X is non-empty convex set): We can show that the image of a morphism is still a morphism: it is affine and preserves ⊔ (because convex hulls are preserved by taking the direct image along affine functions-Sect. 3.3): Finally, we show that the action on morphisms satisfy the functor laws, leading to the following definition of F 1 : Definition free_semiCompSemiLattConvType : functor C V C S := Functor.Pack (Functor.Mixin free_semiCompSemiLattConvType_mor_id free_semiCompSemiLattConvType_mor_comp).
Like for the adjunction F 0 ⊣ U 0 , the forgetful functor U 1 of type functor C S C V is just formalized by substituting the category C S by the category C V in morphisms (see forget_semiCompSemiLattConvType in [Affeldt et al. 2020, file gcm_model.v]).
6.3.2 Counit / unit. Let us explain how we implement the counit ε 1 ∶ F 1 ○ U 1 ↝ 1 C S . It is exactly the ⊔ operator seen in Sect. 4.3: We need to show that it is natural, that it preserves the operator ⊔, i.e., ε 1 (⊔(X )) = ⊔(ε1@(X )) (for that purpose we use the lemma lub_op_hull from Sect. 4.2), and that it is affine, i.e., ε 1 (X ◁p ▷Y ) = ε 1 X ◁ p ▷ ε 1 Y . The unit η 1 ∶ 1 C V ↝ U 1 ○ F 1 is the singleton map, which is easily shown to be natural and affine.
We call the corresponding triangular laws triL1 and triR1.
The definition of these adjunctions has been given in Sect. 5.3.1. We then build the adjunction resulting from the composition of the three adjunctions we have just defined, using the function of Sect. 5.3.2: Definition Agcm := adj_comp AC (adj_comp A0 A1).
Finally, we obtain the geometrically convex monad from the resulting adjunction using the generic lemma explained at the end of Sect. 5.3.3: The very last step is to use the function Monad_of_category_monad of Sect. 5.2 to recover a monad compatible with the M formal framework of monadic equational reasoning: Definition gcm := Monad_of_category_monad Mgcm.

Informal
Description of the Join of the Monad. At this stage, it is worth taking a step back to check that the join of the monad we have built indeed corresponds to the intuition one can have of the execution of a program mixing probabilistic choice and nondeterministic choice. Provided we ignore the function ε C (the counit of the adjunction F C ⊣ U C , which, as we already explained in Sect. 6.1, is here essentially for technical reasons), the join operator can informally be explained as the following function: ε 1 ○ (λ X . ε 0 @(X )). The input of this function is indeed necset {dist (necset {dist T})}, i.e., it takes non-empty sets of distributions. The function ε 0 (Sect. 6.2.2) computes barycenters, so that when applied the lefthand side of the function composition returns an object of type necset (necset {dist T}). The function ε 1 (Sect. 6.3.2) computes the hull of the union of its input, which results in an object of type necset (dist T), as expected.

THE PROPERTIES OF COMBINED CHOICE OF THE GCM
The very last step of our construction is to show that the geometrically convex monad (that we obtained as a result of the previous section-Sect. 6) satisfies the expected distributivity axioms that we discussed in Sect. 2.1 and to check that it is meaningful, i.e., that it really distinguishes the different choice operators. This corresponds to [Affeldt et al. 2020, file altprob_model.v] in the accompanying development.

The Combined Choice is not a Trivial Theory
We conclude this section with a formal check that probabilistic choice in our axiom system of combined choice is not trivial, meaning that it indeed distinguishes different probabilities. It is sufficient to check that there exists a model which is not trivial in this sense, and our construction of geometrically convex monad serves this purpose nicely: Example gcmAP_choice_nontrivial (p q : prob) : p ≠ q → Ret true ◁p▷ Ret false ≠ Ret true ◁q▷ Ret false :> gcmAP bool. Proof. ... Qed.
Here :> gcmAP bool indicates the type of this inequality, which forces the resolution of monadic operations inside our instance of altProbMonad. The proof just requires to unfold definitions and provides further evidence that the geometrically convex monad is not a trivial model.

RELATED WORK
We have already commented on several related work throughout this paper. We add in this section further comments that are better explained after the presentation of our contributions.
In our formalization of semicomplete semilattices (in Sect. 4), the nondeterministic choice is modeled as an infinitary operator. This is similar to Beaulieu's "infinite nondeterministic choice" [Beaulieu 2008, Def. 3.2.3] and, at first sight, looks different from Cheung's approach, who models nondeterministic choice as a binary operator [Cheung 2017, Sec. 6.3.1]. However, we observe that Cheung also implicitly uses an infinitary version of his operator (e.g., [Cheung 2017, p. 160]).
There is a number of formalizations of category theory in proof assistants (many of which being listed by Gross et al. [Gross et al. 2014]). However, we could not find a readily usable formalization of concrete categories in C . For example, UniMath is a large C library that aims at formalizing mathematics using the univalent point of view [Voevodsky et al. 2014]. It contains a substantial formalization of abstract categories but does not seem to feature a formalization of concrete categories. Since we needed only a handful of theorems about category theory, we formalized concrete categories from scratch and developed their theories as a generalization of M (in Sect. 5). The idea of using categories as a package to handle functions with proofs was already presented by McBride [McBride 1999, Chapter 7, Section 3.1]. He also proposed the use of concrete categories for such a lightweight use of category theory, noting that the convertibility of terms is an easier way than propositional equality to handle the equational laws for morphisms, such as unit and associativity laws. His formal definition of categories differs from ours in that it is also indexing on hom-sets, while in our definition, hom-sets are embedded as predicates. This difference further affects later definitions such as functors. Our definition makes it clearer that concrete categories are shallow embeddings of categories.

CONCLUSIONS AND FUTURE WORK
In this paper, we proposed a formalization in the C proof assistant of the geometrically convex monad, a monad that combines probabilistic and nondeterministic choice. To the best of our knowledge, this is the first formalization of such a monad. A direct application is to complete an existing formalization of monadic equational reasoning which was lacking the model of the combined interface of probabilistic and nondeterministic choices. Our development of this formal model also led us to develop several mathematical theories of broader interest such as a formalization of convex spaces and a formalization of concrete categories. We can now use our model to check the non-triviality of Gibbons et al. 's choice of axioms.
Our experiment is an example of combination of two monads that requires a substantial amount of work. Although they could not be used here, there also exist a number of generic results about the combination of monads such as monad transformers [Jaskelioff 2009] or distributive laws [Zwart and Marsden 2018] that could also deserve formalization. By introducing a formalization of concrete categories to support the construction of the geometrically convex monad, our work also raises the question of the generalization of M from its specialization to the Set category.