`{Univalence} (A : Type) : fracture_glue_uncurried (fracture_unglue A) = A. Proof. apply path_universe_uncurried, equiv_inverse. exact (Build_Equiv _ _ (pullback_corec (fracture_square A)) (ispullback_fracture_square A)). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.