Definition chain (n : nat) : ∏ (x y:X), Type. Proof. induction n as [|n H]. - intros x y. exact (x = y). - intros x y. exact (∑ s t, H x s × s<t × t=y). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.