Definition append_graph_zig_zag {g : graph} {x y z : vertex g} (fs : graph_zig_zag x y) (gs : graph_zig_zag y z) : graph_zig_zag x z := length_of_graph_zig_zag fs + length_of_graph_zig_zag gs ,, append_graph_zig_zag_of_length (pr2 fs) (pr2 gs).
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core.