`{Univalence} : IsEquiv fracture_unglue := isequiv_adjointify fracture_unglue fracture_glue_uncurried fracture_unglue_isretr fracture_unglue_issect.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.