There are (at least) two different sort of things you can do, roughly corresponding to syntax and semantics.
You can study the internal logic of a category, which lets you use a logical language as a convenient tool for doing calculations with in a category. e.g. objects are types, propositions are subobjects, et cetera.
Conversely, given a suitable language, we can construct its syntactic category consisting of all the types you can construct in the language and the functions you can define between them, and satisfying all of the relations you can prove hold between them. And thus we can use category theory to help us think of type theories.
On the semantic side we can think of a category $T$ (possibly with extra structure; e.g. a sketch) as being a theory. Then models of this theory in a category $C$ will be functors $F : T \to C$ of a certain type.
Of course, these aren't unrelated; if we have the theory of a group, we might then construct $T$ to be its syntactic category, and require the functors defining models of $T$ to be of the sort that preserves the logic used.
Conversely, if we're in the habit of studying functors out of some category $T$, it may be worth considering the theory given by internal language of $T$ and view functors as being models of that theory.
A common type of this construction is one we can do with universal algebra (e.g. the theory of groups, given as operations and equations). If we have some variety of universal algebra, we can take $T$ to be the opposite category of the category of finitely presented algebras, and then models will be functors from $T$ that preserve finite limits.
I'm in a hurry but will try to answer a couple of your questions:
Is it correct that the omission of LEM is the distinguishing characteristic of constructive logic as opposed to classical?
Yes!
Is it correct that the Curry-Howard correspondence is conditioned on the omission of LEM?
In a basic version of the Curry–Howard correspondence, you are quite right: There is no program of the type corresponding to LEM. That would be a kind of oracle which is able, for any type $A$, to either produce a value of $A$ or else produce a procedure $A \to \bot$. In particular, with such an oracle there would be an algorithm deciding the halting problem.
Astoundingly, there are more refined versions of the Curry–Howard correspondence which interpret LEM just fine. Every constructive proof gives rise to a pure program while every classical proof gives rise to a program with side effects. Which side effects exactly, depends on the amount of classical axioms used. For interpreting LEM, to have continuations as side effects is enough. For interpreting countable or dependent choice, other side effects are required. You find some references in these slides.
Is it correct that were LEM used in the heart of CoQ and LEAN that in turn these proof checkers would not be proven to halt?
Literally speaking: No. Coq and Lean support LEM just fine as an unproven assumption and still their proof checking terminates.
Is it correct that therefore to conclude that it is LEM that is at the heart of the halting problem?
Yes in some sense and no in some other.
Yes: Without LEM, it becomes possible for all functions $\mathbb{N} \to \mathbb{N}$ to be computable (by a Turing machine or equivalently by an untyped lambda term). The halting function, which maps a number $n$ to $0$ or $1$ depending on whether the $n$-th Turing machine terminates, is no longer a total function $\mathbb{N} \to \mathbb{N}$ in such a world. (Instead, its domain of definition is the subset consisting of those numbers $n$ such that the $n$-th Turing machine terminates or does not terminate.) Accordingly, the question whether there is a Turing machine computing this no-longer-existing gadget loses a bit of its relevance. There are lots of worlds like this, for instance the "effective topos", I tried to give an introduction here.
No: There is a metatheorem stating that every PA-proof of termination of a Turing machine can be mechanically transformed into a HA-proof, and similarly with ZFC and IZF. (PA is Peano Arithmetic, HA is its constructive cousin without LEM; ZFC is Zermelo–Fraenkel set theory with the axiom of choice, IZF is its constructive cousin without LEM and without choice.) So LEM will never be crucial in proving termination of a Turing machine. LEM might be crucial for abstract tools helping with termination proofs, but in the end LEM can always be eliminated from concrete termination results. Keywords to lookup are "Friedman's trick", "continuation trick" or "Barr's theorem".
Best Answer
There are no particular challenges about defining categories in an intuitionistic logic/type theory. Some results are not constructively valid and thus don't hold, or they motivate some modifications to allow them to hold. One major one is the characterization of equivalence of categories as a full, faithful, and essentially surjective functor. To show that this is equivalent to the definition in terms of a unit and counit requires the Axiom of Choice and so isn't constructively valid. One solution is instead of talking about functors, you can talk about anafunctors. There are reasons to do this even in classical mathematics. That said, in my experience, constructive definitions of categories don't usually use anafunctors, and they just don't particularly care about full, faithful, and essentially surjective functors.
To your main question, I think what Rydeheard and Burstall mean is simply that you'd like to define a notion of product-in-a-category, say, and then be able to apply it to a category of categories to get the notion of a product category. The problem is a definition of product in a $\mathcal U_1$-category won't apply to the category of $\mathcal U_1$-categories which is a $\mathcal U_2$-category.
Forming a "true" "category of all categories" seems like it will lead to inconsistency pretty quickly. In a traditional set theory, you could define a class of all categories and give it some categorical structure via class functions, but it would be a different thing than the sets it classifies. It's also somewhat awkward to formulate definitions entirely as predicates. Regardless, the upshot is that you end up with two (or more) definitions of concepts: one for "class-level" notions and one for set-level notions. This is more or less the problem Rydeheard and Burstall wanted to avoid.
The typical solution for this in set theory is to assume the existence of Grothendieck universes, which do produce this stratification, but then you can at least parameterize definitions by universes. For type theory, the solution is the same. Type theoretic universes serve much the same purpose as Grothendieck universes, and the way to resolve Rydeheard and Burstall's issue is to support universe polymorphism which modern implementations of intuitionistic type theory, such as Agda, do. It's still possible to run into situations where you need superuniverses, but this won't come up for the vast majority of what people want to do with categories. (One place it can come up is when you try to formalize certain $\infty$-categories.)