A Categorical Construction of the Real Unit Interval

TL;DR

This paper provides a canonical construction of the real unit interval using effect algebras, characterizing it as a unique algebra of a specific monad on bounded posets, with implications for probability theory.

Contribution

It introduces a new categorical construction of the real unit interval via effect algebras and monads, establishing its uniqueness and algebraic properties.

Findings

The real unit interval is the unique non-initial, non-final irreducible algebra of a certain monad.

Categories of omega-complete effect algebras and monoids are monadic over bounded posets.

The construction models operations used in probability theory.

Abstract

The real unit interval is the fundamental building block for many branches of mathematics like probability theory, measure theory, convex sets and homotopy theory. However, a priori the unit interval could be considered an arbitrary choice and one can wonder if there is some more canonical way in which the unit interval can be constructed. In this paper we find such a construction by using the theory of effect algebras. We show that the real unit interval is the unique non-initial, non-final irreducible algebra of a particular monad on the category of bounded posets. The algebras of this monad carry an order, multiplication, addition and complement, and as such model much of the operations we need to do on probabilities. On a technical level, we show that both the categories of omega-complete effect algebras as well as that of omega-complete effect monoids are monadic over the category of bounded posets using Beck's monadicity theorem. The characterisation of the real unit interval then follows easily using a recent representation theorem for omega-complete effect monoids.