(B C : Type) `{HB: In O1 B} `{HC: In O2 C} (f : C -> O2 B) : Type := fracture_glue_uncurried ((B;HB);((C;HC);f)).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.