proposition: Lemma path_join_compose : ∀ I (g : I * I → Type) i j k (z : Path (Path g) (i,j)) (s : Path (Path g) (j,k)), path_compose I g (path_join z) (path_join s) = path_join (path_compose I (Path g) z s).
proof: Proof. intros. dependent induction z; auto; dependent destruction s; simpl; auto. rewrite path_right_id. reflexivity. rewrite <- IHz. simpl. repeat rewrite path_comp_assoc. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple