Much has been said already but I'd like to suggest to try and be a bit more careful in the formalization. Stars and underbars are not really used anywhere in the literature I've seen so far and I find them distracting. Also, minimization of the axioms is not always the royal way to clarity.
I'm going to give a detailed categorical definition of groupoids and then indicate how to relate it to the algebraic one you ask about and see that they are equivalent. I'll then briefly address your second question and towards the end I'll try and give some glimpses towards an answer of your broad question 3. I'm making my life a bit more complicated than necessary in that I don't introduce Hom-sets (or only implicitly) but that's because groupoids per se are much more interesting when considered in categories other than $\mathbf{Sets}$ and in order to be able to do so, the following definition is more adequate (view it as a preparation for my attempt at answering your question 3).
So here we go in full detail:
A groupoid $G$ consists of two sets: a set of objects $G_0$ and a set of arrows $G_1$ together with five structure maps $(s,t,u,i,c)$
- source and target $s,t: G_1 \to G_0$ (domain and codomain of arrows).
- unit $u: G_0 \to G_1$ (the unit inclusion mapping an object to its identity morphism)
- composition of arrows $c: G_2 \to G_1$, defined on the fibered product (pullback) $$G_{2} = G_1 {}_s{\times}_{t}\ G_1 = \{(h,g) \in G_1 \times G_1\,:\,s(h)=t(g)\}$$ and written $c(h,g) = hg$. (The set $G_2$ is the set of pairs of composable arrows).
- inversion of arrows $i: G_1 \to G_1$ written $i(g) = g^{-1}$
subject to the following conditions
- compatibility of source and target with composition: for all $(h,g) \in G_2$ we have $s(hg) = s(g)$ and $t(hg) = t(h)$.
- associativity: for all $k,h,g \in G_1$ such that $s(k) = t(h)$ and $s(h)=t(g)$ we have $(kh)g = k(hg)$ (note that this makes sense in view of 1).
- compatibility of unit with source, target and composition:
- For all $x \in G_0$ we have $su(x) = x = tu(x)$
- For all $g \in G_1$ we have $[ut(g)]g = g = g[us(g)]$
- compatibilities of the inverse: For all $g \in G_1$ we have $s(g^{-1}) = t(g)$ and $t(g^{-1}) = s(g)$ as well as $g^{-1}g = us(g)$ and $gg^{-1}=ut(g)$.
All this can be expressed in purely diagrammatic terms and leads to the notion of a groupoid inside a category (and makes sense as soon as there are enough pullbacks). Also when you flesh out the definition of a category on Wikipedia you see that the Hom-sets are simply $G(x,y) = \{g \in G_1:s(g) = x\text{ and }t(g) = y\}$ and that the structure maps above are implicitly built into the formalism.
I'm of the opinion that only this is a reasonable (category-theoretic) definition of groupoids and everything else is just cheating one's way around precision. When saying that one has a (small) category the usual formulation is exactly what is obtained when dropping $i$ and the two points 4. above.
So, when people are saying that "a groupoid is a small category in which every morphism is an isomorphism" then they mean first that they have a category, i.e., two sets $G_0$ and $G_1$ and four structure maps $(s,t,u,c)$ satisfying points 1., 2., and 3. above and 4. is what one ends up with when one thinks about what it really means for a(ll) morphism(s) to be invertible (isomorphisms). So much for the categorical part of your question 1.
Now I should relate this to the definition of algebraic groupoids. From the above it should be clear that given a groupoid in the above sense, $\ast = c$ is a partial operation satisfying associativity, that "inverses are always defined" and that the "identity" axiom is satisfied.
Now we need to check that we can go back from the algebraic definition to the category theoretic definition, so we need to identify the sets $G_1$ and $G_0$ and the structure maps. Here are the details (bear with me and let me drop the star):
- Put $G_1 = G$ and $G_0 = \{g \in G: g^{-1} = g\}$ (idea: objects are the same thing as identity morphisms and they are distinguished by being their own inverses) the unit $u:G_0 \to G_1$ is simply the inclusion and inversion $i: G_1 \to G_1$ is already given.
- Source is $s(g) = g^{-1}g$ and target is $t(g) = gg^{-1}$ these are well-defined because "inverses are always defined" and are maps $s,t: G_1 \to G_0$ because of your "easy and convenient property 2.".
- It remains to identify the domain of definition of multiplication with $G_2$ above (that's already in Arturo's answer). As we already spelled out what source and target are, we need to check that $hg$ is defined whenever $h^{-1}h = s(h) \stackrel{!}{=} t(g) = gg^{-1}$ and conversely.
If $h^{-1}h = gg^{-1}$ then $h = h(h^{-1}h)$ (take $a = b = h$ in the identity axiom) hence $h = h(h^{-1}h) = h(gg^{-1}) = (hg)g^{-1}$. But we can compose the last expression with $g$ from the right and get $(hg)g^{-1}g = hg$, hence $s(h) = t(g)$ implies that $hg$ is defined by the associativity axiom.
Conversely if $hg$ is defined then $hgg^{-1} = h$ hence composing this with $h^{-1}$ from the left we get $s(g) = gg^{-1} = h^{-1}h = t(h)$.
With all this preparation you should now have no trouble verifying the axioms 1. to 4. of the categorical definition.
Question 2 is rather easy to answer:
A morphism $\phi: G \to G'$ between groupoids is just a functor. In the spirit of the above definition let me spell out the details. I'm using primes to denote the structure maps of $G'$:
It consists of two maps $\phi_{1} : G_1 \to G_1^\prime$ and $\phi_{0}: G_{0} \to G_{0}^\prime$ satisfying the following compatibilities with the structure maps:
- source and target: $\phi_0 s = s'\phi_1$ and $\phi_0 t = t' \phi_1$
- unit: $\phi_1 u = u' \phi_0$
- composition: if $s(h) = t(g)$ then $\phi_1(hg) = \phi_1(h)\phi_1(g)$.
A more formal way to express the composition axiom 3. would be to say that $\phi_1$ induces a unique map $\phi_2 = \phi_1 {}_s{\times}_{t}\ \phi_1: G_2 \to G_{2}^{\prime}$ such that $(s',t') \circ \phi_2 = \phi_1 \circ (s,t)$ and the condition then becomes $c' \circ \phi_2 = \phi_1 \circ c$.
Compatibility with inverses is then automatic: $\phi_1 i = i'\phi_1$.
A subgroupoid is usually defined to be a groupoid $H$ together with a functor $\phi: H \to G$ such that $\phi_1$ and $\phi_0$ are injective (embeddings). This means that $\phi_1: H_1 \to \phi_1(H_1)$ is an isomorhpism onto its image and so is $\phi_0: H_0 \to \phi_{0}(H_0)$.
A homomorphism of algebraic groupoids is simply a map $\phi: G \to H$ that is compatible with composition: whenever $hg$ is defined then so is $\phi(h)\phi(g)$ and it is equal to $\phi(hg)$. The description of arrows, objects, source, target unit and composition then yield that a homomorphism of algebraic groupoids yields a functor and vice versa. In particular the categories of algebraic groupoids and homomorphisms and the category of groupoids-as-categories are equivalent.
Note: Starting with an algebraic groupoid and passing to the associated category and going back to the algebraic setting, one gets the algebraic groupoid back. On the other hand, starting with a categorical groupoid and passing to the associated algebraic groupoid and going back one gets an isomorphic categorical groupoid but not necessarily the same one because we didn't insist on $G_0$ being a subset of $G_1$ in the categorical definition. One could add that requirement and get an isomorphism of categories, but neither do I see a compelling reason to do so, nor is it usually done, as far as I can tell.
One should also mention that not only are there functors but there are also natural transformations, so, as the category of (small) categories is not only a category but a $2$-category, so is the category of groupoids. But entering more detail would mean to go too far in this already very long answer. Let me just mention that this allows one to consider groupoids up to equivalence of categories; there is the even weaker notion of Morita equivalence that is of considerable interest from a geometric point of view.
Here are three basic examples of groupoids:
- Groups.
- Equivalence relations.
- Group actions.
A group is a groupoid in which $G_{0}$ is reduced to a singleton. An equivalence relation is a groupoid for which there is at most one morphism between any two objects. Group actions don't have such a handy characterization but to every action of a group $G$ on a set $X$ one can associate the so-called action groupoid (or translation groupoid) $G \ltimes X$.
Many theorems on groupoids had earlier variants for groups, equivalence relations and action groupoids and were then generalized later on. This is one criticism that one often hears: there are few results that go in the other direction, at least not on a basic or immediate level — some people see groupoids as a way of formalizing analogies that were already self-evident before.
As I mentioned in a comment, groupoids on a set-theoretic level are already interesting and the book by Higgins, Categories and Groupoids is a nice introduction to that with e.g. a groupoid version Grushko's theorem and explaining the use in algebraic topology via the fundamental groupoid with the groupoid version of van Kampen as a highlight.
This leads me to my second recommendation: May's Concise course in algebraic topology shows the use of groupoids in a nice formulation of the theory of covering spaces, among other things like van Kampen, of course.
Since you are already aware of Ronald Brown's work, I'm not elaborating on that. However I must say that I think that characterizing Brown as "one of the founders of their study" as was done in one of the comments is a bit unfair considering the earlier and deep work e.g. by Ehresmann and Haefliger upon which Brown's first work on groupoids was built (I don't know Brown personally but from his homage to Ehresmann it seems that he is more than happy to acknowledge that). At some point I should also mention that groupoids were introduced by Heinrich Brandt in 1940.
Your third question
Question 3: (a too broad question, I know, but anything will be useful) Are there any alternate definitions of a groupoid? I'm aiming for one that is used most often throughout mathematics nowadays. How/in what fields are groupoids most often used? Algebraic topology? Are they given topological structure? What are some important theorems regarding groupoids?
is very broad so I'll give a broad answer, just dropping some key-words and giving some links. I should also add the Disclaimer that I'm far from being an expert on groupoids I just happen to have run into them many times already. I'm not aspiring to any sort of comprehensiveness and I'm just mentioning things that came to mind immediately. One further problem is that groupoids are mostly used at a fairly advanced level, so mentioning some scary words is almost unavoidable. Also, the interesting theorems on (or using) groupoids I'm aware of all seem to involve baggage way beyond the scope of this question and this answer.
Briefly: It seems fair to say that in every sufficiently algebraized field there are people considering and using groupoids.
- I'm not aware of significantly different definitions than the two you gave (but see e.g. this PlanetMath article on Brandt groupoids).
- The category-theoretic one is certainly by far more often used than the algebraic one.
- There are many versions of structured groupoids (smooth, topological, measure-theoretic and by means of algebro-geometric methods), as I mention below.
- I can't tell where groupoids are most often used.
A very important, popular and thus highly developed field of investigation is in differential geometry via Lie groupoids. Lie groupoids simultaneously encompass Lie groups and manifolds and on a more advanced level arise from foliations in guise of the holonomy groupoids. This is one of the reasons I spelled out the definition in such painstaking detail above: In order to define a Lie groupoid one needs to be a bit careful on what conditions to impose on $G_1$, $G_0$ and the structure maps. The most straightforward definition ($G_0$ and $G_1$ manifolds and all maps smooth) turns out not to be quite the right one and in order to spell the "good" definition out one needs to do some careful bookkeeping and there's no way around writing down all the structure maps.
Lie groupoids have associated Lie algebroids which are of considerable interest too, very much so in mathematical physics.
As a first step into this direction I recommend the surveys by Alan Weinstein, Groupoids: unifying internal and external symmetry and The geometry of momentum. For a more in-depth view I recommend the book by Weinstein-Canas da Silva, Geometric models of non-commutative algebras for a start. There are several surveys by Moerdijk and Mrčun that you can locate easily if you want to dig deeper.
In representation theory they arise e.g. in the Tannakian formalism (I couldn't find a good and digestible link on that).
In ergodic theory and representation theory of locally compact groups they are used in guise of Mackey's virtual groups, roughly a theory built on a measure-theoretic version of groupoids.
In a topological and operator theoretic setting much has been done, mostly initiated by Jean Renault. For instance, J.-L. Tu used groupoids heavily for proving some forms of the Baum-Connes conjecture.
Not to mention category theory itself and advanced algebraic topology (see e.g. the work by Georges Maltsiniotis and his school elaborating on Grothendieck's approach to stacks), but I'll stop here because I don't like indulging in name-dropping and I've done already too much of it. I didn't mention or link to work on stacks in algebraic geometry (e.g. by Laumon and Moret-Bailly as well as Lurie and Toën, simply because I'm not qualified).
I hope this gave you some impression that there is a lot around and hopefully this answer gives you some leads you can follow.
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.)
Best Answer
I have found the notes you are talking about. The idea of a typing is just that you like to express what kind of thing something is. For example if in a math text someone introduces a new variable n in a proof, then they will also tell you what sort of object n represents. For example they say let n be a natural number or let n be an integer. In the first case the typing of $n$ is for example $n:\mathbb N$. People which are more into set theory will probably want to write $n\in \mathbb N$, but there is a big difference between the two. A type of something is always the answer to the question "What is it?". For example someone might write down the symbol $f$, you might ask "What is $f$?" and they will tell you "Well, $f$ is a morphism from $A$ to $B$ in that category $\mathbb C$ we were talking about." Hence, the type of $f$ in that case is "morphism from $A$ to $B$" and type theorists like to denote this by $f:A\to B$. This explains the terminology in your pdf. It really has not much content, except maybe if you want to formalize category theory in a proof assistant and need to decide if you want to use dependent types for the morphisms or whatever.The only information that the typing tells you is what codomain and domain of a morphism are.
There are some subtleties. Ignore the next paragraph if it confuses you. The thinking of many mathematicians is influenced by material set theories such as ZFC. The formal system of ZFC is single–sorted. There is only type: everything is a set. Instead of $n:\mathbb N$ set theory people would like to write $n\in \mathbb N$, but there is an important difference between the two. The expression $n\in \mathbb N$ is a statement that you can prove are refute. It is something that can be wro g or false. In contrast the information that $n$ is a set is not something you can prove or disprove. (undrr the ssumption that you are working in ZFC at this moment). It something the person has to tell you when they write down the symbol, otherwise they are just talking nonesense. Typing statements $n:\mathbb N$ are not soemthing you can disprove or prove two. They are just extra information that has to be provided when you write down the symbol. If you like to learn more about this difference, then the best setting to observe it is the difference between many–sorted and single–sorted formal first order logic.