IsProjective Unit. Proof. apply (isoprojective_ochoice purely Unit). intros P trP S. specialize S with tt. strip_truncations; apply tr. apply Unit_ind. exact S. Defined.
Require Import Basics Types. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Modalities.Modality Modalities.Identity. Require Import Limits.Pullback.