(F : Type) : Subuniverse. Proof. rapply (Build_Subuniverse (fun E => merely (E <~> F))). intros T U mere_eq f iseq_f. strip_truncations. pose (feq:=Build_Equiv _ _ f iseq_f). exact (tr (mere_eq oE feq^-1)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.