Most presentations of (dependent) constructive type theory present introduction and elimination rules for $0,1,+,\times$, which via Curry-Howard-Lambek corresponds to the initial object, terminal object, coproduct, and product, respectively.
It is well known (for example) that with dependent types one can construct some of the other common categorical constructions in type theory, for example: $\sum_{x:X} f(x) = g(x)$ is the equalizer.
However, I am interested in seeing equalizers/coequalizers/etc... specifically constructed as types via their own introduction and elimination rules. Is this possible, and has it been done explicitly anywhere?
More generally, I will ask:
Is there a procedure for giving explicit introduction and elimination rules in constructive type theory characterizing all small (co)limits? (when the type theory in question is viewed as a category)
For example, such a procedure (for limits) would take the product diagram $A \leftarrow A \times B \rightarrow B$ and return the usual introduction and elimination rules for products in type theory.
I suspect that given the close correspondence between (for example) the two elimination rules for products and the projection morphisms in a product diagram, there must be some way of doing this in general for small (co)limits, but I am unsure if this has explicitly been done anywhere.
My answer here gives an indication of what equalizers might look like in the internal language: https://math.stackexchange.com/a/1707284/305738 Combined with finite products, this gives all finite limits. NuPRL's subset types and quotient types give an idea of another presentation of equalizers and coequalizers.
To get arbitrary (co)limits you'd then "just" need to articulate arbitrary, set-indexed, (co)products. Ultimately, the result is going to look something like the dependent product/sum or, perhaps more accurately, $\Pi$ and $\Sigma$ types in a Pure Type System.
The problem is: what is a "set"? what is a "set-indexed product" or, more importantly, a "set-indexed family"? what is a "small" diagram? How do we specify any of these things in our type theory?
If you can embed set-theoretic reasoning into your type theory, e.g. as HoTT can do, then you can just restrict the dependent product/sum to "sets" and you're done. Otherwise, it starts getting awkward. Naively, the introduction rule for an arbitrary, set-indexed product would have an arbitrary set of premises. In general, a derivation wouldn't even be able to be written down, let alone checked. Time to retreat and regroup.
A set indexed product would look like the following: $\prod_{s\in S}E(s)$ where $S$ is a set and $E$ is a $S$-indexed family of objects of our category. More precisely, $S$ is a set-valued expression. In a nutshell, we have a type theory with two sorts: $\mathsf{set}$ and $\mathsf{obj}$. We'll then need to actually formally spell out whichever set theory we're using as that will be the sublanguage for expressions of sort $\mathsf{set}$. If our category is locally small, we'll have a type constructor $\mathsf{hom} : \mathsf{obj} \times \mathsf{obj} \to \mathsf{set}$ and similar operations for identity and composition. Elements of $\mathsf{hom}$ sets will be (convertible to) terms of sort $\mathsf{obj}$ with the appropriate types. If our category is well-powered, we'll have $\mathsf{sub} : \mathsf{obj} \to \mathsf{set}$. If our category is concrete, we'll have $U : \mathsf{obj} \to \mathsf{set}$. In this context, we could instead represent a concrete category by making the sort $\mathsf{set}$ depend on the sort $\mathsf{obj}$. This would mean that we allow $\mathsf{obj}$ indexed families of sets, i.e. given a type, $T$, of sort $\mathsf{obj}$, we can consider families of sets parameterized by a variable of type $T$.
So what do I mean by "family"? One natural answer in ZF(C) is a $S$-indexed family of $X$s for sets $S$ and $X$ is a function $S \to X$. Unfortunately, this doesn't work for us as the objects of a category often form a proper class. Fortunately, if we can articulate a "class function" with domain $S$ into the class of objects, the Axiom of Replacement states that the image is then a set from which we can form a set function. The introduction rule for these products would then take a $S$-indexed product of terms, i.e. $\mathsf{tuple}_{S,E} : \prod_{s\in S}\mathsf{hom}(\Gamma,E(s)) \to \prod_{s\in S}E(s)$. The input of $\mathsf{tuple}$ would be a term of sort $\mathsf{set}$ which would be an expression in ZFC, say.
It's unlikely that the specific structure of ZFC is important to capture the general idea. To be clear, as we vary our set theory, whether a category is (co)complete and what that means will vary, but we should be able to abstract from the particular details of our chosen set theory to establish some general principles. Luckily, categorists have considered this problem for a while and the solution is to use a tool already in common use in categorical logic, fibered categories. Fibered Categories and the Foundations of Naive Category Theory discusses how you might formulate category theory without needing to reference set theory. Section 13 of Set Theory for Category Theory also discusses what "small" and "complete" mean for an arbitrary category serving as "the category of sets". While the latter focuses on indexed products as I have here, it also mentions that (co)limits of diagrams can be formulated by using category objects in our "category of sets" and then formulating what a functor from such category objects would be. As far as I can tell, this would be way less pleasant to use than reducing to (co)products and (co)equalizers. What this all amounts to is instead of exploring the internal language of a particular category, we view that category as a fiber of a fibered category and we explore the internal language of that fibration. The base of that fibration will be the "category of sets". Of course, we'll likely want additional structure, e.g. the $\mathsf{hom}$ operations, and we'll want our "category of sets" to be something like an elementary topos with NNO.