1. Paths¶
This is a literate rzk file:
Path induction¶
We define path induction in terms of the built-in J rule, so that we can apply it like any other function.
#define ind-path
( A : U)
( a : A)
( C : (x : A) → (a = x) → U)
( d : C a refl)
( x : A)
( p : a = x)
: C x p
:= idJ (A , a , C , d , x , p)
To emphasize the fact that this version of path induction is biased towards
paths with fixed starting point, we introduce the synonym ind-path-start.
Later we will construct the analogous path induction ind-path-end, for paths
with fixed end point.
#define ind-path-start
( A : U)
( a : A)
( C : (x : A) → (a = x) → U)
( d : C a refl)
( x : A)
( p : a = x)
: C x p
:=
ind-path A a C d x p
Some basic path algebra¶
Path reversal¶
#def rev
( p : x = y)
: y = x
:= ind-path (A) (x) (\ y' p' → y' = x) (refl) (y) (p)
Path concatenation¶
We take path concatenation defined by induction on the second path variable as our main definition.
#def concat
( p : x = y)
( q : y = z)
: ( x = z)
:= ind-path (A) (y) (\ z' q' → (x = z')) (p) (z) (q)
We also introduce a version defined by induction on the first path variable, for situations where it is easier to induct on the first path.
#def concat'
( p : x = y)
: ( y = z) → (x = z)
:= ind-path (A) (x) (\ y' p' → (y' = z) → (x = z)) (\ q' → q') (y) (p)
#end path-algebra
Some basic coherences in path algebra¶
#section basic-path-coherence
#variable A : U
#variables w x y z : A
#def rev-rev
( p : x = y)
: ( rev A y x (rev A x y p)) = p
:=
ind-path
( A) (x) (\ y' p' → (rev A y' x (rev A x y' p')) = p') (refl) (y) (p)
Left unit law for path concatenation¶
The left unit law for path concatenation does not hold definitionally due to our choice of definition.
#def left-unit-concat
( p : x = y)
: ( concat A x x y refl p) = p
:= ind-path (A) (x) (\ y' p' → (concat A x x y' refl p') = p') (refl) (y) (p)
Associativity of path concatenation¶
#def associative-concat
( p : w = x)
( q : x = y)
( r : y = z)
: ( concat A w y z (concat A w x y p q) r)
= ( concat A w x z p (concat A x y z q r))
:=
ind-path
( A)
( y)
( \ z' r' →
concat A w y z' (concat A w x y p q) r'
= concat A w x z' p (concat A x y z' q r'))
( refl)
( z)
( r)
#def rev-associative-concat
( p : w = x)
( q : x = y)
( r : y = z)
: ( concat A w x z p (concat A x y z q r))
= ( concat A w y z (concat A w x y p q) r)
:=
ind-path
( A)
( y)
( \ z' r' →
concat A w x z' p (concat A x y z' q r')
= concat A w y z' (concat A w x y p q) r')
( refl)
( z)
( r)
#def right-inverse-concat
( p : x = y)
: ( concat A x y x p (rev A x y p)) = refl
:=
ind-path
( A)
( x)
( \ y' p' → concat A x y' x p' (rev A x y' p') = refl)
( refl)
( y)
( p)
#def left-inverse-concat
( p : x = y)
: ( concat A y x y (rev A x y p) p) = refl
:=
ind-path
( A)
( x)
( \ y' p' → concat A y' x y' (rev A x y' p') p' = refl)
( refl)
( y)
( p)
Concatenation of two paths with common codomain¶
Concatenation of two paths with common codomain; defined using concat
and rev.
#def zig-zag-concat
( p : x = y)
( q : z = y)
: ( x = z)
:= concat A x y z p (rev A z y q)
Concatenation of two paths with common domain¶
Concatenation of two paths with common domain; defined using concat and
rev.
#def zag-zig-concat
( p : y = x)
( q : y = z)
: ( x = z)
:= concat A x y z (rev A y x p) q
#def right-cancel-concat
( p q : x = y)
( r : y = z)
: ( ( concat A x y z p r) = (concat A x y z q r)) → (p = q)
:=
ind-path
( A)
( y)
( \ z' r' → ((concat A x y z' p r') = (concat A x y z' q r')) → (p = q))
( \ H → H)
( z)
( r)
#end basic-path-coherence
Some derived coherences in path algebra¶
The statements or proofs of the following path algebra coherences reference one of the path algebra coherences defined above.
#section derived-path-coherence
#variable A : U
#variables x y z : A
#def rev-concat
( p : x = y)
( q : y = z)
: ( rev A x z (concat A x y z p q))
= ( concat A z y x (rev A y z q) (rev A x y p))
:=
ind-path
( A)
( y)
( \ z' q' →
( rev A x z' (concat A x y z' p q'))
= ( concat A z' y x (rev A y z' q') (rev A x y p)))
( rev
( y = x)
( concat A y y x refl (rev A x y p))
( rev A x y p)
( left-unit-concat A y x (rev A x y p)))
( z)
( q)
Postwhiskering paths of paths¶
#def concat-eq-left
( p q : x = y)
( H : p = q)
( r : y = z)
: ( concat A x y z p r) = (concat A x y z q r)
:=
ind-path
( A)
( y)
( \ z' r' → (concat A x y z' p r') = (concat A x y z' q r'))
( H)
( z)
( r)
Prewhiskering paths of paths¶
Prewhiskering paths of paths is much harder.
#def concat-eq-right
( p : x = y)
: ( q : y = z)
→ ( r : y = z)
→ ( H : q = r)
→ ( concat A x y z p q) = (concat A x y z p r)
:=
ind-path
( A)
( x)
( \ y' p' →
( q : y' = z)
→ ( r : y' = z)
→ ( H : q = r)
→ ( concat A x y' z p' q) = (concat A x y' z p' r))
( \ q r H →
concat
( x = z)
( concat A x x z refl q)
( r)
( concat A x x z refl r)
( concat (x = z) (concat A x x z refl q) q r (left-unit-concat A x z q) H)
( rev (x = z) (concat A x x z refl r) r (left-unit-concat A x z r)))
( y)
( p)
Identifying the two definitions of path concatenation¶
#def concat-concat'
( p : x = y)
: ( q : y = z)
→ ( concat A x y z p q) = (concat' A x y z p q)
:=
ind-path
( A)
( x)
( \ y' p' →
( q' : y' =_{A} z)
→ ( concat A x y' z p' q') =_{x =_{A} z} concat' A x y' z p' q')
( \ q' → left-unit-concat A x z q')
( y)
( p)
#def concat'-concat
( p : x = y)
( q : y = z)
: concat' A x y z p q = concat A x y z p q
:=
rev
( x = z)
( concat A x y z p q)
( concat' A x y z p q)
( concat-concat' p q)
This is easier to prove for concat' than for concat.
#def alt-triangle-rotation
( p : x = z)
( q : x = y)
: ( r : y = z)
→ ( H : p = concat' A x y z q r)
→ ( concat' A y x z (rev A x y q) p) = r
:=
ind-path
( A)
( x)
( \ y' q' →
( r' : y' =_{A} z)
→ ( H' : p = concat' A x y' z q' r')
→ ( concat' A y' x z (rev A x y' q') p) = r')
( \ r' H' → H')
( y)
( q)
The following needs to be outside the previous section because of the usage of
concat-concat' A y x.
#end derived-path-coherence
#def triangle-rotation
( A : U)
( x y z : A)
( p : x = z)
( q : x = y)
( r : y = z)
( H : p = concat A x y z q r)
: ( concat A y x z (rev A x y q) p) = r
:=
concat
( y = z)
( concat A y x z (rev A x y q) p)
( concat' A y x z (rev A x y q) p)
( r)
( concat-concat' A y x z (rev A x y q) p)
( alt-triangle-rotation
( A) (x) (y) (z) (p) (q) (r)
( concat
( x = z)
( p)
( concat A x y z q r)
( concat' A x y z q r)
( H)
( concat-concat' A x y z q r)))
A special case of this is sometimes useful
#def cancel-left-path
( A : U)
( x y : A)
( p q : x = y)
: ( p = q) → (concat A y x y (rev A x y q) p) = refl
:= triangle-rotation A x y y p q refl
Concatenation with a path and its reversal¶
#def retraction-preconcat
( A : U)
( x y z : A)
( p : x = y)
( q : y = z)
: concat A y x z (rev A x y p) (concat A x y z p q) = q
:=
ind-path (A) (y)
( \ z' q' → concat A y x z' (rev A x y p) (concat A x y z' p q') = q') (left-inverse-concat A x y p) (z) (q)
#def section-preconcat
( A : U)
( x y z : A)
( p : x = y)
( r : x = z)
: concat A x y z p (concat A y x z (rev A x y p) r) = r
:=
ind-path (A) (x)
( \ z' r' → concat A x y z' p (concat A y x z' (rev A x y p) r') = r') (right-inverse-concat A x y p) (z) (r)
#def retraction-postconcat
( A : U)
( x y z : A)
( q : y = z)
( p : x = y)
: concat A x z y (concat A x y z p q) (rev A y z q) = p
:=
ind-path (A) (y)
( \ z' q' → concat A x z' y (concat A x y z' p q') (rev A y z' q') = p)
( refl) (z) (q)
#def section-postconcat
( A : U)
( x y z : A)
( q : y = z)
( r : x = z)
: concat A x y z (concat A x z y r (rev A y z q)) q = r
:=
concat
( x = z)
( concat A x y z (concat A x z y r (rev A y z q)) q)
( concat A x z z r (concat A z y z (rev A y z q) q))
( r)
( associative-concat A x z y z r (rev A y z q) q)
( concat-eq-right A x z z r
( concat A z y z (rev A y z q) q)
( refl)
( left-inverse-concat A y z q))
Application of functions to paths¶
#def ap
( A B : U)
( x y : A)
( f : A → B)
( p : x = y)
: ( f x = f y)
:= ind-path (A) (x) (\ y' p' → (f x = f y')) (refl) (y) (p)
#def ap-rev
( A B : U)
( x y : A)
( f : A → B)
( p : x = y)
: ( ap A B y x f (rev A x y p)) = (rev B (f x) (f y) (ap A B x y f p))
:=
ind-path
( A)
( x)
( \ y' p' →
ap A B y' x f (rev A x y' p') = rev B (f x) (f y') (ap A B x y' f p'))
( refl)
( y)
( p)
#def ap-concat
( A B : U)
( x y z : A)
( f : A → B)
( p : x = y)
( q : y = z)
: ( ap A B x z f (concat A x y z p q))
= ( concat B (f x) (f y) (f z) (ap A B x y f p) (ap A B y z f q))
:=
ind-path
( A)
( y)
( \ z' q' →
( ap A B x z' f (concat A x y z' p q'))
= ( concat B (f x) (f y) (f z') (ap A B x y f p) (ap A B y z' f q')))
( refl)
( z)
( q)
#def rev-ap-rev
( A B : U)
( x y : A)
( f : A → B)
( p : x = y)
: ( rev B (f y) (f x) (ap A B y x f (rev A x y p))) = (ap A B x y f p)
:=
ind-path
( A)
( x)
( \ y' p' →
( rev B (f y') (f x) (ap A B y' x f (rev A x y' p')))
= ( ap A B x y' f p'))
( refl)
( y)
( p)
The following is for a specific use.
#def concat-ap-rev-ap-id
( A B : U)
( x y : A)
( f : A → B)
( p : x = y)
: ( concat
( B) (f y) (f x) (f y)
( ap A B y x f (rev A x y p))
( ap A B x y f p))
= ( refl)
:=
ind-path
( A)
( x)
( \ y' p' →
( concat
( B) (f y') (f x) (f y')
( ap A B y' x f (rev A x y' p')) (ap A B x y' f p'))
= ( refl))
( refl)
( y)
( p)
#def ap-id
( A : U)
( x y : A)
( p : x = y)
: ( ap A A x y (identity A) p) = p
:= ind-path (A) (x) (\ y' p' → (ap A A x y' (\ z → z) p') = p') (refl) (y) (p)
Application of a function to homotopic paths yields homotopic paths.
#def ap-eq
( A B : U)
( x y : A)
( f : A → B)
( p q : x = y)
( H : p = q)
: ( ap A B x y f p) = (ap A B x y f q)
:=
ind-path
( x = y)
( p)
( \ q' H' → (ap A B x y f p) = (ap A B x y f q'))
( refl)
( q)
( H)
#def ap-comp
( A B C : U)
( x y : A)
( f : A → B)
( g : B → C)
( p : x = y)
: ( ap A C x y (comp A B C g f) p)
= ( ap B C (f x) (f y) g (ap A B x y f p))
:=
ind-path
( A)
( x)
( \ y' p' →
( ap A C x y' (\ z → g (f z)) p')
= ( ap B C (f x) (f y') g (ap A B x y' f p')))
( refl)
( y)
( p)
#def rev-ap-comp
( A B C : U)
( x y : A)
( f : A → B)
( g : B → C)
( p : x = y)
: ( ap B C (f x) (f y) g (ap A B x y f p))
= ( ap A C x y (comp A B C g f) p)
:=
rev
( g (f x) = g (f y))
( ap A C x y (\ z → g (f z)) p)
( ap B C (f x) (f y) g (ap A B x y f p))
( ap-comp A B C x y f g p)
Transport¶
Transport in a type family along a path in the base¶
#def transport
( x y : A)
( p : x = y)
( u : B x)
: B y
:= ind-path (A) (x) (\ y' p' → B y') (u) (y) (p)
The lift of a base path to a path from a term in the total space to its transport¶
#def transport-lift
( x y : A)
( p : x = y)
( u : B x)
: ( x , u) =_{Σ (z : A) , B z} (y , transport x y p u)
:=
ind-path
( A)
( x)
( \ y' p' → (x , u) =_{Σ (z : A) , B z} (y' , transport x y' p' u))
( refl)
( y)
( p)
Transport along concatenated paths¶
#def transport-concat
( x y z : A)
( p : x = y)
( q : y = z)
( u : B x)
: ( transport x z (concat A x y z p q) u)
= ( transport y z q (transport x y p u))
:=
ind-path
( A)
( y)
( \ z' q' →
( transport x z' (concat A x y z' p q') u)
= ( transport y z' q' (transport x y p u)))
( refl)
( z)
( q)
#def transport-concat-rev
( x y z : A)
( p : x = y)
( q : y = z)
( u : B x)
: ( transport y z q (transport x y p u))
= ( transport x z (concat A x y z p q) u)
:=
ind-path
( A)
( y)
( \ z' q' →
( transport y z' q' (transport x y p u))
= ( transport x z' (concat A x y z' p q') u))
( refl)
( z)
( q)
Transport along homotopic paths¶
#def transport2
( x y : A)
( p q : x = y)
( H : p = q)
( u : B x)
: ( transport x y p u) = (transport x y q u)
:=
ind-path
( x = y)
( p)
( \ q' H' → (transport x y p u) = (transport x y q' u))
( refl)
( q)
( H)
Transport along a loop¶
#def transport-loop
( a : A)
( b : B a)
: ( a = a) → B a
:= \ p → (transport a a p b)
Substitution law for transport¶
#def transport-substitution
( A' A : U)
( B : A → U)
( f : A' → A)
( x y : A')
( p : x = y)
( u : B (f x))
: transport A' (\ x → B (f x)) x y p u
= transport A B (f x) (f y) (ap A' A x y f p) u
:=
ind-path
( A')
( x)
( \ y' p' →
transport A' (\ x → B (f x)) x y' p' u
= transport A B (f x) (f y') (ap A' A x y' f p') u)
( refl)
( y)
( p)
Path induction¶
Using rev we can deduce a path induction principle with fixed end point.
#def ind-path-end
( A : U)
( a : A)
( C : (x : A) → (x = a) → U)
( d : C a refl)
( x : A)
( p : x = a)
: C x p
:=
transport (x = a) (\ q → C x q) (rev A a x (rev A x a p)) p
( rev-rev A x a p)
( ind-path A a (\ y q → C y (rev A a y q)) d x (rev A x a p))
Dependent application¶
#def apd
( A : U)
( B : A → U)
( x y : A)
( f : (z : A) → B z)
( p : x = y)
: ( transport A B x y p (f x)) = f y
:=
ind-path
( A)
( x)
( ( \ y' p' → (transport A B x y' p' (f x)) = f y'))
( refl)
( y)
( p)
Higher-order concatenation¶
For convenience, we record lemmas for higher-order concatenation here.
#section higher-concatenation
#variable A : U
#def triple-concat
( a0 a1 a2 a3 : A)
( p1 : a0 = a1)
( p2 : a1 = a2)
( p3 : a2 = a3)
: a0 = a3
:= concat A a0 a1 a3 p1 (concat A a1 a2 a3 p2 p3)
#def quadruple-concat
( a0 a1 a2 a3 a4 : A)
( p1 : a0 = a1)
( p2 : a1 = a2)
( p3 : a2 = a3)
( p4 : a3 = a4)
: a0 = a4
:= triple-concat a0 a1 a2 a4 p1 p2 (concat A a2 a3 a4 p3 p4)
#def quintuple-concat
( a0 a1 a2 a3 a4 a5 : A)
( p1 : a0 = a1)
( p2 : a1 = a2)
( p3 : a2 = a3)
( p4 : a3 = a4)
( p5 : a4 = a5)
: a0 = a5
:= quadruple-concat a0 a1 a2 a3 a5 p1 p2 p3 (concat A a3 a4 a5 p4 p5)
#def alternating-quintuple-concat
( a0 : A)
( a1 : A) (p1 : a0 = a1)
( a2 : A) (p2 : a1 = a2)
( a3 : A) (p3 : a2 = a3)
( a4 : A) (p4 : a3 = a4)
( a5 : A) (p5 : a4 = a5)
: a0 = a5
:= quadruple-concat a0 a1 a2 a3 a5 p1 p2 p3 (concat A a3 a4 a5 p4 p5)
#def 12ary-concat
( a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 : A)
( p1 : a0 = a1)
( p2 : a1 = a2)
( p3 : a2 = a3)
( p4 : a3 = a4)
( p5 : a4 = a5)
( p6 : a5 = a6)
( p7 : a6 = a7)
( p8 : a7 = a8)
( p9 : a8 = a9)
( p10 : a9 = a10)
( p11 : a10 = a11)
( p12 : a11 = a12)
: a0 = a12
:=
quintuple-concat
a0 a1 a2 a3 a4 a12
p1 p2 p3 p4
( quintuple-concat
a4 a5 a6 a7 a8 a12
p5 p6 p7 p8
( quadruple-concat
a8 a9 a10 a11 a12
p9 p10 p11 p12))
The following is the same as above but with alternating arguments.
#def alternating-12ary-concat
( a0 : A)
( a1 : A) (p1 : a0 = a1)
( a2 : A) (p2 : a1 = a2)
( a3 : A) (p3 : a2 = a3)
( a4 : A) (p4 : a3 = a4)
( a5 : A) (p5 : a4 = a5)
( a6 : A) (p6 : a5 = a6)
( a7 : A) (p7 : a6 = a7)
( a8 : A) (p8 : a7 = a8)
( a9 : A) (p9 : a8 = a9)
( a10 : A) (p10 : a9 = a10)
( a11 : A) (p11 : a10 = a11)
( a12 : A) (p12 : a11 = a12)
: a0 = a12
:=
12ary-concat
a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12
#end higher-concatenation
Higher-order coherences¶
#def rev-refl-id-triple-concat
( A : U)
( x y : A)
( p : x = y)
: triple-concat A y x x y (rev A x y p) refl p = refl
:=
ind-path
( A)
( x)
( \ y' p' → triple-concat A y' x x y' (rev A x y' p') refl p' = refl)
( refl)
( y)
( p)
#def ap-rev-refl-id-triple-concat
( A B : U)
( x y : A)
( f : A → B)
( p : x = y)
: ( ap A B y y f (triple-concat A y x x y (rev A x y p) refl p)) = refl
:=
ind-path
( A)
( x)
( \ y' p' →
( ap A B y' y' f (triple-concat A y' x x y' (rev A x y' p') refl p'))
= ( refl))
( refl)
( y)
( p)
#def ap-triple-concat
( A B : U)
( w x y z : A)
( f : A → B)
( p : w = x)
( q : x = y)
( r : y = z)
: ( ap A B w z f (triple-concat A w x y z p q r))
= ( triple-concat
( B)
( f w)
( f x)
( f y)
( f z)
( ap A B w x f p)
( ap A B x y f q)
( ap A B y z f r))
:=
ind-path
( A)
( y)
( \ z' r' →
( ap A B w z' f (triple-concat A w x y z' p q r'))
= ( triple-concat
( B)
( f w) (f x) (f y) (f z')
( ap A B w x f p)
( ap A B x y f q)
( ap A B y z' f r')))
( ap-concat A B w x y f p q)
( z)
( r)
#def triple-concat-eq-first
( A : U)
( w x y z : A)
( p q : w = x)
( r : x = y)
( s : y = z)
( H : p = q)
: ( triple-concat A w x y z p r s) = (triple-concat A w x y z q r s)
:= concat-eq-left A w x z p q H (concat A x y z r s)
#def triple-concat-eq-second
( A : U)
( w x y z : A)
( p : w = x)
( q r : x = y)
( s : y = z)
( H : q = r)
: ( triple-concat A w x y z p q s) = (triple-concat A w x y z p r s)
:=
ind-path
( x = y)
( q)
( \ r' H' →
triple-concat A w x y z p q s = triple-concat A w x y z p r' s)
( refl)
( r)
( H)
The function below represents a somewhat special situation, which nevertheless arises when dealing with certain naturality diagrams. One has a commutative square and a path that cancels that top path. Then the type below witnesses the equivalence between the right side of the square (in blue) and a particular zig-zag of paths, the red zig-zag. We choose the assocativity order for the triple compostion for ease of use in a later proof.
#def eq-top-cancel-commutative-square
( A : U)
( v w y z : A)
( p : v = w)
( q : w = v)
( s : w = y)
( r : v = z)
( t : y = z)
( H : (concat A w v z q r) = (concat A w y z s t))
( H' : (concat A v w v p q) = refl)
: r = (concat A v w z p (concat A w y z s t))
:=
( concat
( v = z)
( r)
( concat A v v z refl r)
( concat A v w z p (concat A w y z s t))
( rev
( v = z)
( concat A v v z refl r)
( r)
( left-unit-concat A v z r))
( concat
( v = z)
( concat A v v z refl r)
( concat A v v z (concat A v w v p q) r)
( concat A v w z p (concat A w y z s t))
( rev
( v = z)
( concat A v v z (concat A v w v p q) r)
( concat A v v z refl r)
( concat-eq-left
( A)
( v)
( v)
( z)
( concat A v w v p q)
( refl)
( H')
( r)))
( concat
( v = z)
( concat A v v z (concat A v w v p q) r)
( concat A v w z p (concat A w v z q r))
( concat A v w z p (concat A w y z s t))
( associative-concat A v w v z p q r)
( concat-eq-right
( A)
( v)
( w)
( z)
( p)
( concat A w v z q r)
( concat A w y z s t)
( H)))))
It is also convenient to have a a version with the opposite associativity.
#def eq-top-cancel-commutative-square'
( A : U)
( v w y z : A)
( p : v = w)
( q : w = v)
( s : w = y)
( r : v = z)
( t : y = z)
( H : (concat A w v z q r) = (concat A w y z s t))
( H' : (concat A v w v p q) = refl)
: r = (concat A v y z (concat A v w y p s) t)
:=
concat
( v = z)
( r)
( concat A v w z p (concat A w y z s t))
( concat A v y z (concat A v w y p s) t)
( eq-top-cancel-commutative-square A v w y z p q s r t H H')
( rev-associative-concat A v w y z p s t)
And a reversed version.
#def rev-eq-top-cancel-commutative-square'
( A : U)
( v w y z : A)
( p : v = w)
( q : w = v)
( s : w = y)
( r : v = z)
( t : y = z)
( H : (concat A w v z q r) = (concat A w y z s t))
( H' : (concat A v w v p q) = refl)
: ( concat A v y z (concat A v w y p s) t) = r
:=
rev
( v = z)
( r)
( concat A v y z (concat A v w y p s) t)
( eq-top-cancel-commutative-square' A v w y z p q s r t H H')
Given a homotopy between paths H : p = q, then we can cancel on the left to
get a homotopy between concat (rev p) q and refl.
#def htpy-id-cancel-left-concat-left-eq
( A : U)
( a b : A)
( p : a = b)
( q : a = b)
( H : p = q)
( r : b = a)
( H' : (concat A a b a q r) = refl)
: ( concat A a b a p r) = refl
:=
concat
( a = a)
( concat A a b a p r)
( concat A a b a q r)
( refl)
( concat-eq-left A a b a p q H r)
( H')