Definition zig_zag_in_grpd_to_mor {G : groupoid} {x y : G} (gs : zig_zag x y) : x --> y := zig_zag_of_length_in_grpd_to_mor (pr2 gs).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Groupoids.