{- ======================================================================= A Rewriting Coherence Theorem with Applications in Homotopy Type Theory ======================================================================= Nicolai Kraus and Jakob von Raumer Given a wellfounded and (in some very weak sense) confluent relation, we construct a homotopy basis. This formalises Section 4 of the paper "A Rewriting Coherence Theorem with Applications in Homotopy Type Theory", https://arxiv.org/abs/2107.01594. We use cubical Agda 2.6.2.2, and the current state of the development can be found at https://bitbucket.org/fplab/confluencecoherence/. -} {-# OPTIONS --safe --cubical #-} -- This index file imports everything. module index where -- basic constructions with the transitive and/or symmetric closure -- of a relation, not specific to this project open import squier.graphclosures -- results about Noetherian and wellfounded relations open import squier.accessibility -- definition of generalised 2-polygraphs and basic properties open import squier.polygraphs -- cancelling inverses (auxiliary lemmas) open import squier.cancelInverses -- Important ingredient: The list extension of a wellfounded order -- is wellfounded open import squier.listextension -- generalisations of Newman's lemma open import squier.newman -- the main construction open import squier.homotopybasis -- a consequence in type-theory style: -- "Noetherian induction for closed zig-zags" open import squier.noethercycle