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