(X : Type@{u}) := { Z : Type@{u} & merely (Z = X) }.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations. Require Import ObjectClassifier Homotopy.ExactSequence Pointed.