(fact fact' : Factorization) : { path_intermediate : intermediate fact <~> intermediate fact' & { path_factor1 : path_intermediate o factor1 fact == factor1 fact' & { path_factor2 : factor2 fact == factor2 fact' o path_intermediate & forall a, path_factor2 (factor1 fact a) @ ap (factor2 fact') (path_factor1 a) @ fact_factors fact' a = fact_factors fact a }}} <~> PathFactorization fact fact'. Proof. issig. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.