-------------------------------------------------------------------------------- Path Sequences library Ettore Aldrovandi, ealdrovandi@fsu.edu Begun November 2022 October 2023 -------------------------------------------------------------------------------- This is a port of the PathSeq path manipulation library found in the HoTT-Agda library at https://github.com/HoTT/HoTT-Agda \begin{code} {-# OPTIONS --without-K --safe --auto-inline #-} module PathSequences.index where import PathSequences.Type import PathSequences.Concat import PathSequences.Split import PathSequences.Reasoning import PathSequences.Ap import PathSequences.Inversion import PathSequences.Rotations import PathSequences.Cancel \end{code}