I am trying to understand the semidirect product of groupoids, as defined in this answer by Theo Johnson-Freyd. Part of my difficulty is that although the definition of a 2-group …