let H := NullHomotopy.concat h h'
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
⊢ Homotopy p r
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
H : NullHomotopy (append (append p (inverse q)) (append q (inverse r))) := NullHomotopy.concat h h'
⊢ Homotopy p r