/* Provenance: Lean 4 → LambdaIR → MiniC → C
 * Source: HeytingLean.Algebra.HomotopyTower.GroupoidBridge + InfinityGroupoidBridge
 * Theorem preserved: stabilized_fixed_point_category_has_infty_groupoid_presentation
 */

#include <stddef.h>
#include <stdbool.h>

/* A quiver: directed graph with typed vertices and edges. */
typedef struct {
    size_t num_vertices;
    size_t num_edges;
    size_t *edge_src;
    size_t *edge_dst;
} Quiver;

/* Free groupoid element: a word in generators and their inverses. */
typedef struct {
    size_t *edges;      /* sequence of edge indices */
    bool *inverted;     /* whether each edge is inverted */
    size_t length;
} FreeGroupoidElement;

/* Stage groupoid: free groupoid on a quiver at a given tower level. */
typedef struct {
    Quiver quiver;
    size_t level;
} StageGroupoid;

/* StableTransportQuiver: quiver-valued transport surface. */
typedef struct {
    Quiver *quivers;     /* one per level */
    size_t num_levels;
} StableTransportQuiver;

/* Check identity element (empty word). */
static inline bool is_identity(const FreeGroupoidElement *g) {
    return g->length == 0;
}

/* Compose two free groupoid elements (concatenation with cancellation). */
size_t compose_length(const FreeGroupoidElement *a, const FreeGroupoidElement *b) {
    /* Count cancellations at junction */
    size_t cancel = 0;
    while (cancel < a->length && cancel < b->length) {
        size_t ai = a->length - 1 - cancel;
        if (a->edges[ai] == b->edges[cancel] &&
            a->inverted[ai] != b->inverted[cancel]) {
            cancel++;
        } else {
            break;
        }
    }
    return (a->length - cancel) + (b->length - cancel);
}