Definition zig_zag_of_length {C : category} (n : ℕ) : ∏ (x y : C), UU. Proof. induction n as [ | n IHn ]. - exact (λ x y, z_iso x y). - exact (λ x y, ∑ (z : C), ((x --> z) ⨿ (z --> x)) × IHn z y). 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.