# A Paragraph Proof

Say an arrow in a category is βconstantβ if it's post-composition with any two arbitrary compatible
arrows is indistinguishable.

In the case that there's a terminal object π, an arrow $f : a βΆ b$ is constant precisely when it
factors through the unique arrow $!β : a βΆ π$. This is not terribly difficult to see provided
that β$a$ is non-emptyβ, i.e., it has a βpointβ, call it $Β‘ : π βΆ a$.
Indeed, if `f`

is constant then the factorization is witness by `f β Β‘`

since $(f β Β‘) β !β = f β (Β‘ β !β) = f β id = f$, where the second equality holds since `f`

is constant. Conversely, if $f$ factorizes through the unique arrow $!β : a βΆ π$ by some arrow $Ξ΅$
then, for any composable maps $x,y$ we have $f β x = Ξ΅ β !β β x = Ξ΅ β !β β y = f β y$
and so `f`

is constant; where the second equality holds since $!β β x$ and $!β β y$ have the same
type going to π but such arrows are unique.

(Challenge: is the factorisation of constants $a βΆ b$ via the unique arrow $a βΆ π$ itself unique?)

# A Calculational Proof

Below is the originally posted answer, but with the requested notational preliminaries.

β’ The Booleans are denoted πΉ and have values `{true, false}`

.

β’ Functions, in type theory or set theory, of the form `X β πΉ`

are called βpredicatesβ.

β’ Unlike any other equality in mathematics, the equality on πΉ is **associative**!
Due to the special statues of this equality, it has a few notations: β‘ and β being the
most popular, with = receiving less usage in this context.
βͺ I do not use the associativity of boolean equality anywhere in this post;
an nifty example usage can be found in The associativity of equivalence and the Towers of Hanoi problem
β«

β’ Rather than write, for example, $β_{p β β, p \text{ prime}} f(p)$ where the range of the
quantification is made a second-class citizen in the usual 2-dimensional notation, I use
linear notation of Z
and write $(β p : β β prime.p β’ f.p)$.

β’ More generally, we can define this quantification notation for any monoid $(M, β, u)$
and write $(β x : X β r.x β’ f.x)$ for the β of the terms `f.x`

where `x β X`

satisfies predicate
$r$.

```
βEmpty rangeβ: (β x : X β false β’ f.x) = u
βFinite rangeβ: (β i : β β 0 β€ i β€ n β’ f.i) = f.0 β f.1 β β― β f.n
βAbbreviationβ: (β x : X β’ f.x) = (β x : X β true β’ f.x)
```

In particular, for the booleans πΉ we have the conjunction β§, βandβ, is associative with unit
being βtrueβ and so this notation applies to `(πΉ, β§, true)`

. It is then conventional to define
a synonym: $(β x : X β r.x β’ f.x) β (β§ x : X β r.x β’ f.x)$. Likewise for the disjunctive monoid
`(πΉ, β¨, false)`

and the βxistential quantifier.

β’ Finally, a proof of an equality can be rendered by a sequence of steps as is done in elementary
school with the justification of each step annotated between the transitions.
Informal βP = Q = R where the first equality follows because of reasonβ and the second follows
because of reasonββ can be rendered in a simpler style as

```
P
=β¨ reasonβ; i.e, a hint explaining why P = Q β©
Q
=β¨ reasonβ; i.e, a hint explaining why Q = R β©
R
```

The conclusion $P = R$ follows by transitivity of equality.

β’ This approach to proofs is very popular among Functional Programmers and computer science
category theorists;
e.g., A Gentle Introduction to Category Theory --- the calculational approach.
It is also used in the popular proof-assistant Agda; where it is
not built-in but is in-fact a user-defined construct! This is possible since Agda allows
mixfix unicode lexemes as identifiers.
I am not using any proof assistant for this post.

Below is my original answer.

Let's start with the second question, then follow up with the first.

# General definition

Definition 0. for any category π, we define the predicate

```
constant : Arr π β πΉ
constant.f β‘ (β x, y β’ f β x = f β y)
```

(Where the bullet ββ’β serves to sepeate the quantifer dummies from the quantifer body).

# Definition reduction

We now show that the above definition reduces to that of OP's when terminal objects exist.

Theorem 1. In any category π with terminal object π,

```
constant.(f : a βΆ b) β‘ (β Ξ΅ : π βΆ b β’ f = Ξ΅ β !β) , provided β Β‘β : π βΆ a
```

where !β denotes the unique morphism to the terminal object:

```
[! characterisation] β x : Obj π β’ β f : Arr π β’ f = !β β‘ f : x βΆ π
```

Proof β·

[β] We have $f : a βΆ b$ and we need to define $Ξ΅ : π βΆ b$ and this can be accomplished
if we only had some element $π βΆ a$. In set theoretical terms, this is tantamount to $a$
being non-empty. βChallenge: in a category with π and π, is it the case that
$x β π β‘ (π βΆ x) β β
$?β Anyhow, we can use our proviso here and so define
$Ξ΅ β f β Β‘β$. It remains to show that we have the property OP uses in his/her definition.

```
Ξ΅ β !β
=β¨ definition of Ξ΅ β©
f β Β‘β β !β
=β¨ constant.f β©
f β idβ
=β¨ identity β©
f
```

[β] Assuming the existence, let $x, y : p βΆ a$ then we prove $f β x = f β y$:

```
f β x
=β¨ assumption β©
Ξ΅ β !β β x
=β¨ !-characterisation since !β β x : p βΆ π β©
Ξ΅ β !β
=β¨ !-characterisation since !β β y : p βΆ π β©
Ξ΅ β !β β y
=β¨ assumption β©
f β y
```

# Constant closure

Finally, we prove the property that OP is interested in, namely:

```
β f,g β’ constant.g β constant.(f β g)
```

Indeed, given arrows $x$ and $y$, we have

```
f β g β x
=β¨ constant.g β©
f β g β y
```

Notice that this is much simpler than a proof using your more particular definition
βless complexity since we avoid existential quantifiers.

It is interesting to note that

```
constant.g β‘ (β f β’ constant.(f β g))
```

# Global elements

Let us say that a global element of an object $b$ is any constant map with target $b$, let's denote such elements by a new predicate:

```
e β¨ββ© b β‘ constant.e β§ tgt.e = b
```

where

```
f : a βΆ b β‘ src.f = a β§ tgt.f = b
```

Let us show that this reduces to the definition of global elements as we know them when
terminals exist. In particular, let's show that there's a correspondence between the two
notions.

[β] given $e β¨ββ© b$, we have some global element $Ξ΅ : π βΆ b$ by the reduction theorem
earlier βof course this relies on us having the same proviso!

[β] conversely, given any global element $Ξ΅ : π βΆ b$, we know it is constant with target
$b$ and so $Ξ΅ β¨ββ© b$.

Neato!

Hope this helps :-)