{A : pType} {P : pFam A} {f g h k : pForall A P} (p : f ==* g) (q : g ==* h) (r : h ==* k) : p @* (q @* r) ==* (p @* q) @* r. Proof. snrapply Build_pHomotopy. 1: exact (fun x => concat_p_pp (p x) (q x) (r x)). by pelim r q p f g h k. Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.