/* Provenance: Lean 4 → LambdaIR → MiniC → C
 * Source: HeytingLean.Algebra.HomotopyTower.LimitEquivalence
 * Theorem preserved: mapLimit_id
 * Theorem preserved: mapLimit_comp
 * Theorem preserved: towerLimit_equivalence_of_towerEquivalence
 */

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

/* Discrete category object index. */
typedef size_t ObjId;

/* A levelwise functor between towers: F_n : T.Obj(n) -> U.Obj(n). */
typedef struct {
    ObjId (*map_obj)(size_t level, ObjId x);
    size_t num_levels;
} TowerFunctor;

/* A compatible tower point: a sequence of objects satisfying drop compatibility. */
typedef struct {
    ObjId *obj;      /* obj[n] is the object at level n */
    size_t num_levels;
} TowerLimitPoint;

/* Theorem preserved: mapLimit_id
 * Identity tower functor maps identity on limit points. */
static inline ObjId identity_map(size_t level, ObjId x) {
    (void)level;
    return x;
}

/* Theorem preserved: mapLimit_comp
 * Composition of tower functors composes on limit points. */
static inline ObjId composed_map(const TowerFunctor *F, const TowerFunctor *G,
                                  size_t level, ObjId x) {
    return G->map_obj(level, F->map_obj(level, x));
}

/* Apply tower functor to a limit point. */
void map_limit_point(const TowerFunctor *F, const TowerLimitPoint *src,
                     TowerLimitPoint *dst) {
    for (size_t n = 0; n < src->num_levels && n < F->num_levels; n++) {
        dst->obj[n] = F->map_obj(n, src->obj[n]);
    }
    dst->num_levels = src->num_levels;
}