So in reading I have come across the terms "InLeft" and "InRight" and I am unable to find a concrete definition for it.
I have found it used in the specification for COQ, and in some notes on compilers (there it was refered to as INL and INR).
As far as I am able to ascertain it is to do with making a difference between two options. However the seems like a weird nomenclature for something so simple.
The page you reference for Coq defines inLeft and inRight as constructors of the inductive type sumor. The names themselves come from "left/right injection", as in the left/right injection into a sum type. Other names commonly used are inl/inr, Left/Right, $\iota_0$/$\iota_1$, and variations on these (e.g. that Coq file also defines left/right in the definition of sumbool). It also defines inl/inr as the constructors of the general sum type. sum, sumor, and sumbool are minor, technical variations of each other.
Which terms are used depends on the author, but they are most commonly used for injections into a sum type, particularly in a type theory/category theory context. Of course, an author is always free to use them for something else if they provide a definition.
There is no accepted definition for this. You'll presumably need to infer what the authors had in mind based on all of the available context (e.g., all of the code), in which case it might not be a suitable question here.
