fact: Record PathFactorization {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 ; path_fact_factors : forall a, path_factor2 (factor1 fact a) @ ap (factor2 fact') (path_factor1 a) @ fact_factors fact' a = fact_factors fact a }.
imports: HoTT.Basics HoTT.Types Extensions PathAny