Global elements in categories with no terminal object?

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

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