{ B : Type_ O1 & { C : Type_ O2 & C -> O2 B }} -> Type := fun BCf => Pullback BCf.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.