{-
=======================================================================
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