fact: Definition objectclassifier_square {A : Type} (P : A -> Type) : P o pr1 == pointed_type o (topmap P) := fun e : sig P => idpath (P e.1).
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Pointed Truncations