`{Univalence} (fact fact' : Factorization) : PathFactorization fact fact' -> fact = fact' := equiv_path_factorization fact fact'.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.