{A : Type} (P : A -> Type) : IsPullback (objectclassifier_square P). Proof. srapply isequiv_adjointify. - intros [a [F p]]. exact (a; transport idmap p^ (point F)). - intros [a [[T t] p]]; cbn in p. refine (path_sigma' _ (idpath a) _). by induction p. - reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations.