Concrete description of (co)limits in elementary toposes via internal language?

In the category of sets, limits and colimits can be concrete described respectively as subobjects of products and quotients of coproducts.

It seems like these descriptions make sense in any elementary topos. I was wondering whether they actually describe the corresponding limits and colimits, and how to see this.

Clarification. I'm asking about concrete element-based formulas we can give to limits and colimits, i.g compatible strings of elements.

I'll be using the definition of an elementary topos as a finitely complete cartesian closed category with a subobject classifier as this definition fits most nicely with type theoretic notions. While I'll formulate the syntax and rules for limits, it doesn't make sense to ask what they are concretely since the are part of the assumed structure. You can show that they are isomorphic to other things that are defined in terms of that structure if you want.

Moving on, finite products and cartesian closure means our internal language contains a simply typed lambda calculus with products. I won't spell out that structure. Finite completeness also means we have equalizers for which I'll use the following type formation, introduction, and elimination rules: $$\frac{\Gamma, x:A \vdash M(x) : B \qquad \Gamma, x:A \vdash N(x) : B}{\Gamma \vdash \{ x \in A\ |\ M(x) =_B N(x)\}}$$ $$\frac{\Gamma \vdash E : A \qquad \Gamma \vdash M(E)\equiv N(E)}{\Gamma \vdash \iota_{M,N}(E) : \{x\in A\ |\ M(x) =_B N(x)\}}\qquad \frac{\Gamma \vdash E : \{ x\in A\ |\ M(x)=_B N(x)\}}{\Gamma \vdash \pi_{M,N}(E) : A}$$ $$\frac{\Gamma \vdash E : \{ x\in A\ |\ M(x) =_B N(x)\}}{\Gamma \vdash M(\pi_{M,N}(E)) \equiv N(\pi_{M,N}(E))}$$ $$\frac{\Gamma \vdash E :\{ x\in A\ |\ M(x)=_B N(x)\}}{\Gamma \vdash \iota_{M,N}(\pi_{M,N}(E)) \equiv E}\qquad \frac{\Gamma \vdash E : A \qquad \Gamma \vdash M(E) \equiv N(E)}{\Gamma \vdash \pi_{M,N}(\iota_{M,N}(E)) \equiv E}$$

Here $\Gamma \vdash M \equiv N$ means $M$ and $N$ are definitionally equal. When two things are definitionally equal then we treat them exactly the same everywhere (i.e. definitional equality is a congruence in our type theory). For our purposes, every definitional equality we need to check we'll be able to check by simply reducing both sides to a normal form and then checking syntactic equality (up to alpha equivalence, i.e. modulo renaming of bound variables). The reduction rules of the lambda calculus that we need come from the triangle identities for the adjunctions defining cartesian closure. Also, the subscripts on $\iota$ and $\pi$ can usually be inferred from context, so I'll be loose with them, using something to suggest the appropriate equalizer.

The existence of a subobject classifier (and equalizers) immediately implies that all monomorphisms are regular, so I'll cheat a bit and assume that as well. Then a subobject classifier just means for every equalizer we have a (unique) characteristic morphism. Formally, we have a type $\Omega$ and a point $\top : \Omega$ and, using the short-hand $E_{A,B}(M,N)$ for $\{ x \in A\ |\ M(x)=_B N(x)\}$, $$\frac{\Gamma \vdash \{ x\in A\ |\ M(x) =_B N(x)\}}{\Gamma, x : A \vdash \chi_{E_{A,B}(M,N)}(x) : \Omega} \quad \frac{\Gamma \vdash E : \{ x\in A\ |\ M(x) =_B N(x)\}}{\Gamma \vdash \chi_{E_{A,B}(M,N)}(\pi_{M,N}(E))\equiv \top}\quad \frac{\Gamma \vdash E : \{ x\in A\ |\ \chi_{E_{A,B}(M,N)}(x) =_\Omega \top\}}{\Gamma \vdash M(\pi_{\chi}(E))\equiv N(\pi_{\chi}(E))}$$

The above implies that every equalizer $\{ x\in A\ |\ M(x)=_B N(x)\}$ is isomorphic to an equalizer of the form $\{ x\in A\ |\ P(x) =_\Omega \top\}$ which I'll abbreviate as $\{ x\in A\ |\ P(x)\}$. There are other ways of formulating all of this, and I haven't used the fully elaborated form of even the rules provided.

That was a whole lot of setup to even start answering the question. Time to build the arsenal. For any type $A$, we have $= : A\times A \to \Omega$ via $\chi_{E_{A\times A,A}(\pi_1,\pi_2)}$. This gives singletons via $\{M\}\equiv(\lambda x.x =_A M) : \Omega^A$. A critical step is we have two values of type $\Omega^\Omega$, namely $\lambda x.x$ and $\lambda x.\top$. The whole category collapses if these are equal. We define the initial object $0_A$ via $\{ t \in A\ |\ (\lambda x.x) =_{\Omega^\Omega} (\lambda x.\top)\}$. This lets us define $\bot \equiv \chi_{0_1}(\langle\rangle) : \Omega$ and $\emptyset_A \equiv (\lambda x.\bot) : \Omega^A$. (As an aside, if you want you can define $\in_A \equiv (\lambda\langle x,p \rangle.p(x)) : A\times\Omega^A \to \Omega$.)

Fleshing out the Heyting algebra structure of $\Omega$ a bit more, we have: $$\begin{align} \land \equiv (\lambda p.p = \langle\top,\top\rangle) \qquad &\Rightarrow \equiv (\lambda\langle x,y \rangle. x\land y = x) \\ \lor \equiv (\lambda p.p \neq \langle\bot,\bot\rangle) \qquad &\lnot \equiv (\lambda x. x\Rightarrow\bot) \end{align}$$

(I'm not quite sure of these definitions. I'm trying to skirt needing to talk about monomorphisms and the Sub functor. See Toposes, Triples, and Theories for a more standard and authoritative account.)

We also have the quantifiers $$ \forall_A \equiv (\lambda p. p = \lambda x.\top) : \Omega^A\to\Omega \qquad \exists_A \equiv (\lambda p. p\neq \emptyset_A) : \Omega^A\to\Omega \\ \exists!_A \equiv (\lambda p. \exists_A (\lambda x. p = \{x\})) : \Omega^A\to\Omega$$ which leads to the image, $\text{im}(f) \equiv \{ y \in B\ |\ \exists_A(\lambda x. y = f(x)) \}$ and the direct image $f_* \equiv \lambda p.\lambda y.\exists_A(\lambda x.p(x)\land f(x) = y) : \Omega^A\to\Omega^B$ if $f : A\to B$. $\exists!$ is key for being able to go from power objects back to plain objects because it shows that the singleton map is an equalizer.

For the coproduct, guided by $C^{A+B}\cong C^A\times C^B$ and set theoretic intuitions, we make the following definitions $$A+B \equiv \{ \langle p,q\rangle \in \Omega^A\times\Omega^B\ |\ (\exists!_A(p)\land q = \emptyset_B) \lor (p = \emptyset_A \land \exists!_B(q))\} \\ \mathtt{inl} \equiv \lambda x.\iota(\langle\{x\},\emptyset_B\rangle) \qquad \mathtt{inr} \equiv \lambda y.\iota(\langle\emptyset_A,\{y\}\rangle) \\ f+g \equiv \lambda s.\iota_{A'+B'}((f_*\times g_*)(\pi_{A+B}(s)))\text{ where } f : A\to A'\text{ and }g : B\to B' \\ \varepsilon \equiv (\lambda s.\pi_{\exists!_C}(\cup_C(\pi_{A+B}(s)))) : C+C \to C\text{ where }\cup_C \equiv \lambda\langle p,q \rangle.\lambda c.p(c)\lor q(c)$$

Finally, to get all finite colimits we need either coequalizers or pushouts. I'll do coequalizers. Going from the set theoretic intuition, the object part is relatively easy. If we want to find the coequalizer of $f,g : A \to B$, we first define the relation $$\sim \equiv (\lambda b_1.\lambda b_2.\exists_A(\lambda a. f(a) = b_1 \land g(a) = b_2)) : B \to \Omega^B$$ and its reflexive, symmetric, transitive closure $\sim^*$. How to do the transitive closure part I'll cover later. The reflexive and symmetric part is easy. $\sim^*$ coequalizes $f$ and $g$, and $q : B \to \text{im}(\sim^*)$ will be the coequalizer. Notice that the image corresponds to the set of equivalence classes. We need to show that given $h : B \to C$ which coequalizes $f$ and $g$, there's a unique arrow $\text{im}(\sim^*)\to C$. We'll use the same trick as before: if we can show that the image of $h_* \circ \pi: \text{im}(\sim^*)\to\Omega^C$ is always a singleton, then we can use the fact that the singleton map is an equalizer to get a map $\pi_{(\exists!_C \circ h_*)} : \text{im}(\sim^*)\to C$. For this to happen, $h$ needs to send every element of an equivalence class to a single element. Specifically, the formula is $$h_*(\lambda b.b_1\sim^* b) = \lambda c.\exists_B(\lambda b_2. b_1\sim^* b_2 \land h(b_2) = c)$$ It's easy enough to show that this is a singleton, in particular $\{h(b_1)\}$. This also shows that $h = \pi_{(\exists!_C \circ h_*)} \circ q$.

All that remains now is showing that we can make the transitive closure of a relation. It would be straight-forward if we had a natural numbers object, but we haven't assumed that. Instead, we'll carve up the type of binary relations until we're left with what we want. To start, we can make the type of all reflexive, symmetric, transitive relations that contain $\sim$. $$\begin{align} P_\sim(S) & \equiv \forall_B(\lambda b_1. \forall_B(\lambda b_2. b_1 \sim b_2 \Rightarrow S(\langle b_1, b_2 \rangle))) \\ & \land \forall_B(\lambda b. S(\langle b, b \rangle)) \\ & \land \forall_B(\lambda b_1. \forall_B(\lambda b_2. S(\langle b_1, b_2 \rangle) \Rightarrow S(\langle b_2, b_1 \rangle))) \\ & \land \forall_B(\lambda b_1. \forall_B(\lambda b_2. (\exists_B(\lambda b. S(\langle b_1, b \rangle) \land S(\langle b, b_2 \rangle)) \Rightarrow S(\langle b_1, b_2 \rangle))) \\ \\ T_\sim & \equiv \{ S \in \Omega^{B\times B}\ |\ P_\sim(S)\} \end{align}$$

$T_\sim$ is the type of all reflexive, symmetric, transitive relations containing $\sim$, including, e.g. $B\times B$. Next, we carve down to a minimal element. $$M_{\sim} \equiv \{ S \in T_\sim\ |\ \forall_{T_{\sim}}(\lambda R. \forall_{B\times B}(\lambda\langle b_1, b_2 \rangle. \pi(S)(b_1, b_2) \Rightarrow \pi(R)(b_1, b_2)))\}$$

If we can show $M_{\sim} \cong 1$, then the equalizer would pick out $\sim^*$. Let's just assume it does and call it a day though. There are many more proof obligations in the above than this. For example, any use of $\iota$ or verifying that the operations for coproducts satisfy all the laws, e.g. $f+g$ is functorial.

I've been mostly making this up as I go along with vague recollections of the more standard, categorical (i.e. not internal language based) run down in Toposes, Triples, and Theories, which I recommend reading the toposes sections. They start from power objects. Nevertheless, while I'm not 100% sure about some definitions and I'd be surprised if there are not errors, I'm reasonably confident about the broad strokes particularly for the parts most relevant to your question.