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