Despite its contested scientific validity, polygraph interviewing is now an established yet opaque practice within criminal justice in England and Wales, with statute law covering polygraph use in the context of probation for released offenders. In this paper, we highlight non-statutory uses of the polygraph by police forces in England and Wales by presenting analysis of responses to freedom of information (FOI) requests. The boundaries around police polygraph use are undefined and potentially elastic. The policies disclosed state that polygraph interviewing is conducted with regard to the Police and Criminal Evidence Act 1984 (PACE) and the Human Rights Act 1998; yet it is denied that a polygraph examination is a criminal interview conducted under PACE. Furthermore, there is a significant risk that the common law may not satisfy the quality of law requirement insofar as it is insufficiently clear who will be subject to polygraph testing, why and in what circumstances. Therefore, we argue that the legal basis for the police’s use of the polygraph is inadequate and imprecise. Without openness and scrutiny regarding the extent of this use, it is difficult to see how the key human rights principle of foreseeability can protect citizens from the risk of arbitrariness.

Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. This higher structure can be captured by finding a homotopy basis for the rewriting system. We show that the basic notions of confluence and wellfoundedness are sufficient to recursively build such a homotopy basis, with a construction reminiscent of an argument by Craig C. Squier. We then go on to translate this construction to the setting of homotopy type theory, where managing equalities between paths is important in order to construct functions which are coherent with respect to higher dimensions. Eventually, we apply the result to approximate a series of open questions in homotopy type theory, such as the characterisation of the homotopy groups of the free group on a set and the pushout of 1-types. This paper expands on our previous conference contribution Coherence via Wellfoundedness by laying out the construction in the language of higher-dimensional rewriting.

Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which are adapted to mechanized computations and include Gray categories as particular cases. We show that a finite rewriting system in precategories admits a finite number of critical pairs, which can be efficiently computed. We also extend Squier’s theorem to our context, showing that a convergent rewriting system is coherent, which means that any two parallel 3-cells are necessarily equal. This allows us to prove coherence results for several well-known structures in the context of Gray categories: monoids, adjunctions, and Frobenius monoids.