proposition: Corollary isprojective_fin_n (n : nat) : IsProjective (Fin n).
proof: Proof. apply (iff_isoprojective_hasochoice _ (Fin n)). rapply finite_choice. Defined.
imports: Basics Types HSet Spaces.Nat.Core HFiber Factorization Truncations Colimits.Quotient Projective Fin