proposition: Lemma path_pmap_compose : ∀ I (q r : I * I → Type) (f : q :→ r) i j k (z : Path q (i,j)) (s : Path q (j,k)), path_compose I r (path_pmap f z) (path_pmap f s) = path_pmap f (path_compose I q z s).
proof: Proof. dependent induction z; auto. dependent destruction s; auto. simpl in *. f_equal. rewrite <- (IHz r f k). f_equal. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple