/// Provenance: Lean 4 → Safe Rust
/// Source: HeytingLean.Algebra.HomotopyTower.LimitEquivalence
/// Theorem preserved: mapLimit_id
/// Theorem preserved: mapLimit_comp

/// A levelwise functor between towers.
pub trait TowerFunctor {
    fn map_obj(&self, level: usize, x: usize) -> usize;
    fn num_levels(&self) -> usize;
}

/// A compatible tower limit point.
#[derive(Clone, Debug, PartialEq)]
pub struct TowerLimitPoint {
    pub obj: Vec<usize>,
}

/// Theorem preserved: mapLimit_id
pub struct IdentityTowerFunctor {
    pub levels: usize,
}

impl TowerFunctor for IdentityTowerFunctor {
    fn map_obj(&self, _level: usize, x: usize) -> usize { x }
    fn num_levels(&self) -> usize { self.levels }
}

/// Apply tower functor to a limit point.
pub fn map_limit_point(f: &impl TowerFunctor, src: &TowerLimitPoint) -> TowerLimitPoint {
    TowerLimitPoint {
        obj: src.obj.iter().enumerate()
            .map(|(n, &x)| f.map_obj(n, x))
            .collect(),
    }
}

/// Theorem preserved: mapLimit_comp
pub fn compose_map(f: &impl TowerFunctor, g: &impl TowerFunctor,
                   level: usize, x: usize) -> usize {
    g.map_obj(level, f.map_obj(level, x))
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_identity_preserves() {
        let id = IdentityTowerFunctor { levels: 5 };
        let pt = TowerLimitPoint { obj: vec![0, 1, 2, 3, 4] };
        assert_eq!(map_limit_point(&id, &pt), pt);
    }
}