fact: Definition equiv_fracture_unglue `{Univalence} : Type <~> { B : Type_ O1 & { C : Type_ O2 & C -> O2 B }} := Build_Equiv _ _ fracture_unglue isequiv_fracture_unglue.
imports: HoTT.Basics HoTT.Types Extensions Limits.Pullback Modality Lex Open Closed Nullification