Definition zig_zag_of_length_in_grpd_to_mor {G : groupoid} {n : ℕ} {x y : G} (gs : zig_zag_of_length n x y) : x --> y. Proof. revert x y gs. induction n as [ | n IHn ]. - intros x y gs. exact (pr1 gs). - intros x y gs. induction gs as [ z gs ]. induction gs as [ g gs ]. induction g as [ g | g ]. + exact (g · IHn _ _ gs). + exact (inv_from_z_iso (g ,, pr2 G _ _ _) · IHn _ _ gs). Defined.
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.