Toward a Type-Theoretic Framework for Linear Mode Connectivity: Univalence and Path-Finding in Weight Spaces

Linear Mode Connectivity (LMC) reveals that independently trained networks can be connected by low-loss linear paths after permutation alignment, yet why discrete symmetry matching implies continuous topological connectivity remains theoretically unresolved. We propose a framework grounded in Homotopy Type Theory (HoTT), conjecturing that neural symmetry orbits as Higher Inductive Types allow the Univalence Axiom to lift permutation equivalences into continuous identity paths under cohesive semantics. Multi-trial experiments on MNIST MLPs demonstrate consistent barrier collapse (peak loss reduced by $>$98\%), and ResNet20 experiments on CIFAR-10 show that activation renormalization (REPAIR) is necessary to realize low-loss paths in architectures with batch normalization. We position this univalent framework as a principled foundation for formal verification of model merging algorithms.