(V_empty ∈ V_omega) * (forall x, x ∈ V_omega -> V_succ x ∈ V_omega). Proof. split. - apply tr; exists 0; auto. - intro. apply (Trunc_functor (-1)). intros [n p]. exists (S n). rewrite p; auto. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.