V := set (fix I n := match n with 0 => V_empty | S n => V_succ (I n) end).
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.