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 ∘ ¡ₐ ∘ !ₐ
=⟨ ! characterisation, since ¡ₐ ∘ !ₐ : 𝟙 ⟶ 𝟙 ⟩
f ∘ !₁
=⟨ id₁ : 𝟙 ⟶ 𝟙, so using !-characterisation again ⟩
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 :-)
