  We define a probabilistic programming language for Gaussian random variables
with a first-class exact conditioning construct. We give operational,
denotational and equational semantics for this language, establishing
convenient properties like exchangeability of conditions. Conditioning on
equality of continuous random variables is nontrivial, as the exact observation
may have probability zero; this is Borel's paradox. Using categorical
formulations of conditional probability, we show that the good properties of
our language are not particular to Gaussians, but can be derived from universal
properties, thus generalizing to wider settings. We define the Cond
construction, which internalizes conditioning as a morphism, providing general
compositional semantics for probabilistic programming with exact conditioning.
