proposition: Theorem ispullback_objectclassifier_square {A : Type} (P : A -> Type) : IsPullback (objectclassifier_square P).
proof: 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.
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations