# 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 :-)