Let $\mathcal{C}$ be a category. Suppose $\mathcal{C}$ contains a terminal object, which I will denote by $\boldsymbol{1}$. Then for any object $B$ in $\mathcal{C}$, a global element of $B$ is a morphism $\boldsymbol{1}\longrightarrow B$. (In many concrete categories, the terminal object is a singleton set, so this definition picks out something close to what we would normally call an "element" of the object $B$.) Given another object $A$ in $\mathcal{C}$, we can say that a morphism $f:A\longrightarrow B$ is constant if there is some global element $\epsilon:\boldsymbol{1}\longrightarrow B$ such that $f = \epsilon \circ \alpha$, where $\alpha:A\longrightarrow \boldsymbol{1}$ is the (unique) morphism from $A$ to the terminal object $\boldsymbol{1}$.

So far, these definitions are totally standard and well-known. But they require the existence of a terminal object. So my questions are the following:

Suppose $\mathcal{C}$ is a category which does not necessarily have a terminal object. Is there a suitable definition of "global elements" for the objects of $\mathcal{C}$? Is there a suitable definition of "constant morphisms"?

Here, by a "suitable" definition, I mean a definition which reduces to the definitions I gave above in the case when $\mathcal{C}$ has a terminal object. Also a suitable definition of "constant morphism" should have the following property: composing any morphism with a constant morphism yields a constant. (Note that the definition via terminal objects has this property.)


Yes. Instead of working in $C$, you can work in presheaves $[C^{op}, \text{Set}]$ on $C$ using the Yoneda embedding. There is always a terminal presheaf given by sending every object $c \in C$ to $1 \in \text{Set}$ (whether or not it's representable by an object in $C$), and so you can make the following definitions using it.

Definition: A global element of $c \in C$ is a natural transformation $1 \to \text{Hom}(-, c)$ of presheaves.

Definition: A constant morphism $f : c \to d$ is a morphism such that the induced morphism $\text{Hom}(- , f) : \text{Hom}(-, c) \to \text{Hom}(-, d)$ factors through the terminal presheaf.

Because the Yoneda embedding is fully faithful and preserves all limits that exist in $C$, these definitions are guaranteed to reproduce the usual definitions if $C$ does in fact have a terminal object.

Unwinding these definitions, we get the following.

Definition: A global element of $c$ is a choice, for each object $c' \in C$, of a morphism $f_{c'} : c' \to c$ such that, for every morphism $g : c' \to c''$, we have $f_{c''} g = f_{c'}$.

Definition (edited, 7/6/16): A constant morphism $f : c \to d$ is a morphism such that there is a choice $f_{d'} : d' \to d$ of global element of $d$ in the above sense such that, for every morphism $g : c' \to c$, we have $f g = f_{c'}$.

  • 1
    $\begingroup$ Thank you very much, Qiaochu! This is exactly what I was looking for. In fact, I already had in mind something like your second grey box (i.e. below "Unwinding these definitions, we get the following.") But I had not made the connection to the Yoneda embedding. (I am not an expert in category theory.) ----- My remaining question: is this a standard construction, or is it something you just invented? If it is a standard construction, then could you point me to some literature where this construction is defined and its properties are developed? Thanks again! $\endgroup$ – Marcus Pivato Jul 5 '16 at 12:11
  • $\begingroup$ @Marcus: it seems like a pretty natural construction to me, but I don't know a reference for it. $\endgroup$ – Qiaochu Yuan Jul 5 '16 at 18:41
  • 1
    $\begingroup$ I think your "unwound" definition of constant morphism is not exactly what you get by unwinding the definition in terms of the terminal presheaf. The latter would say "we can choose for each object $x$ a morphism $f_x : x \to d$ such that for any $g:y\to x$ we have $f_x g = f_y$ and moreover for any $h:x\to c$ we have $f h = f_x$." They are equivalent if every homset $\mathrm{Hom}(x,c)$ is nonempty, but otherwise the definition using the terminal presheaf is stronger (even if the category does have a terminal object). For instance, consider the identity function on the empty set. $\endgroup$ – Mike Shulman Jul 6 '16 at 15:25
  • $\begingroup$ @Mike: I think you're right, except that if $C$ has a terminal object, then by the fully faithfulness (?) of the Yoneda embedding I still think this definition should reduce to the usual one. What am I missing? (As for your example, by either definition the empty set fails to have a global element and so no function to the empty set is constant.) $\endgroup$ – Qiaochu Yuan Jul 6 '16 at 23:15
  • 3
    $\begingroup$ There really are two different notions of "constant function" even for plain old sets: according to one (factoring through the terminal object) the identity function of the empty set is not constant, while according to the other (the images of any two elements of the domain are equal) it is. See for instance ncatlab.org/nlab/show/constant+morphism, although the second definition there currently needs some fixing (nforum.ncatlab.org/discussion/2689/constant-morphism/…) $\endgroup$ – Mike Shulman Jul 8 '16 at 3:24

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

=⟨ reason₁; i.e, a hint explaining why P = Q ⟩
=⟨ reasonβ‚‚; i.e, a hint explaining why Q = 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 ⟩

[⇐] 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 


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$.


Hope this helps :-)

  • $\begingroup$ What is $\mathbb{B}$? I guess it's some category of "truth values"? $\endgroup$ – Qfwfq Jul 4 '16 at 23:19
  • 3
    $\begingroup$ Nice answer, but it would be quite helpful to add (a) a note explaining what formal language you are writing in, and (b) a translation into ordinary mathematical prose, so that mathematicians not familiar with computer formalisation can read it more easily. $\endgroup$ – Peter LeFanu Lumsdaine Jul 5 '16 at 9:44
  • $\begingroup$ Thank you very much for you response, Musa. However, I must admit that I do not understand most of your notation. I guess it comes from theoretical computer science? Perhaps it would help to answer the following question: once we unpack your notation, is your construction basically the same as Quiaochu's construction via the Yoneda embedding? $\endgroup$ – Marcus Pivato Jul 5 '16 at 12:16
  • $\begingroup$ Could you say please what proof assistant you are using ? $\endgroup$ – Philippe Gaucher Jul 7 '16 at 7:54
  • $\begingroup$ please take another gander $\endgroup$ – Musa Al-hassy Jul 7 '16 at 21:06

Your Answer

By clicking β€œPost Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.