(** * Factorizations and factorization systems. *)

Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Extensions Homotopy.IdentitySystems.
Local Open Scope path_scope.


(** ** Factorizations *)

Section Factorization.
  Universes ctxi.
  Context {class1 class2 : forall (X Y : Type@{ctxi}), (X -> Y) -> Type@{ctxi}}
          `{forall (X Y : Type@{ctxi}) (g:X->Y), IsHProp (class1 _ _ g)}
          `{forall (X Y : Type@{ctxi}) (g:X->Y), IsHProp (class2 _ _ g)}
          {A B : Type@{ctxi}} {f : A -> B}.

  (** A factorization of [f] into a first factor lying in [class1] and a second factor lying in [class2]. *)
  Record Factorization :=
    { intermediate : Type@{ctxi} ;
      factor1 : A -> intermediate ;
      factor2 : intermediate -> B ;
      fact_factors : factor2 o factor1 == f ;
      inclass1 : class1 _ _ factor1 ;
      inclass2 : class2 _ _ factor2
    }.

  Lemma issig_Factorization :
    { I : Type & { g : A -> I & { h : I -> B & { p : h o g == f &
      { gin1 : class1 _ _ g & class2 _ _ h }}}}}
      <~> Factorization.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
{I : Type &
{g : A -> I &
{h : I -> B &
{_ : h o g == f & {_ : class1 A I g & class2 I B h}}}}} <~>
Factorization
  Proof.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
{I : Type &
{g : A -> I &
{h : I -> B &
{_ : h o g == f & {_ : class1 A I g & class2 I B h}}}}} <~>
Factorization
    issig.
  Defined.

  (** A path between factorizations is equivalent to a structure of the following sort. *)
  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
    }.
  Arguments PathFactorization fact fact' : clear implicits.

  Lemma issig_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 &
       forall a, path_factor2 (factor1 fact a)
                              @ ap (factor2 fact') (path_factor1 a)
                              @ fact_factors fact' a
                 = fact_factors fact a }}}
      <~> PathFactorization fact fact'.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
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 : A,
(path_factor2 (factor1 fact a) @
 ap (factor2 fact') (path_factor1 a)) @
fact_factors fact' a = fact_factors fact a}}} <~>
PathFactorization fact fact'
  Proof.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
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 : A,
(path_factor2 (factor1 fact a) @
 ap (factor2 fact') (path_factor1 a)) @
fact_factors fact' a = fact_factors fact a}}} <~>
PathFactorization fact fact'
    issig.
  Defined.

  Definition equiv_path_factorization `{Univalence}
             (fact fact' : Factorization)
    : PathFactorization fact fact' <~> fact = fact'.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
fact, fact': Factorization
PathFactorization fact fact' <~> fact = fact'
  Proof.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
fact, fact': Factorization
PathFactorization fact fact' <~> fact = fact'
    refine (_ oE (issig_PathFactorization fact fact')^-1).
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
fact, fact': Factorization
{path_intermediate
: intermediate fact <~> intermediate fact' &
{path_factor1
: (fun x : A => path_intermediate (factor1 fact x)) ==
  factor1 fact' &
{path_factor2
: factor2 fact ==
  (fun x : intermediate fact =>
   factor2 fact' (path_intermediate x)) &
forall a : A,
(path_factor2 (factor1 fact a) @
 ap (factor2 fact') (path_factor1 a)) @
fact_factors fact' a = fact_factors fact a}}} <~>
fact = fact'
    revert fact fact'; apply (equiv_path_issig_contr issig_Factorization).
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
forall
b : {I : Type &
    {g : A -> I &
    {h : I -> B &
    {_ : (fun x : A => h (g x)) == f &
    {_ : class1 A I g & class2 I B h}}}}},
{path_intermediate
: intermediate (issig_Factorization b) <~>
  intermediate (issig_Factorization b) &
{path_factor1
: (fun x : A =>
   path_intermediate
     (factor1 (issig_Factorization b) x)) ==
  factor1 (issig_Factorization b) &
{path_factor2
: factor2 (issig_Factorization b) ==
  (fun x : intermediate (issig_Factorization b) =>
   factor2 (issig_Factorization b)
     (path_intermediate x)) &
forall a : A,
(path_factor2 (factor1 (issig_Factorization b) a) @
 ap (factor2 (issig_Factorization b)) (path_factor1 a)) @
fact_factors (issig_Factorization b) a =
fact_factors (issig_Factorization b) a}}}
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
forall
b1 : {I : Type &
     {g : A -> I &
     {h : I -> B &
     {_ : (fun x : A => h (g x)) == f &
     {_ : class1 A I g & class2 I B h}}}}},
Contr
  {b2
  : {I : Type &
    {g : A -> I &
    {h : I -> B &
    {_ : (fun x : A => h (g x)) == f &
    {_ : class1 A I g & class2 I B h}}}}} &
  {path_intermediate
  : intermediate (issig_Factorization b1) <~>
    intermediate (issig_Factorization b2) &
  {path_factor1
  : (fun x : A =>
     path_intermediate
       (factor1 (issig_Factorization b1) x)) ==
    factor1 (issig_Factorization b2) &
  {path_factor2
  : factor2 (issig_Factorization b1) ==
    (fun x : intermediate (issig_Factorization b1) =>
     factor2 (issig_Factorization b2)
       (path_intermediate x)) &
  forall a : A,
  (path_factor2 (factor1 (issig_Factorization b1) a) @
   ap (factor2 (issig_Factorization b2))
     (path_factor1 a)) @
  fact_factors (issig_Factorization b2) a =
  fact_factors (issig_Factorization b1) a}}}}
    {
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
forall
b : {I : Type &
    {g : A -> I &
    {h : I -> B &
    {_ : (fun x : A => h (g x)) == f &
    {_ : class1 A I g & class2 I B h}}}}},
{path_intermediate
: intermediate (issig_Factorization b) <~>
  intermediate (issig_Factorization b) &
{path_factor1
: (fun x : A =>
   path_intermediate
     (factor1 (issig_Factorization b) x)) ==
  factor1 (issig_Factorization b) &
{path_factor2
: factor2 (issig_Factorization b) ==
  (fun x : intermediate (issig_Factorization b) =>
   factor2 (issig_Factorization b)
     (path_intermediate x)) &
forall a : A,
(path_factor2 (factor1 (issig_Factorization b) a) @
 ap (factor2 (issig_Factorization b)) (path_factor1 a)) @
fact_factors (issig_Factorization b) a =
fact_factors (issig_Factorization b) a}}} intros [I [f1 [f2 [ff [oc1 oc2]]]]].
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
{path_intermediate
: intermediate
    (issig_Factorization (I; f1; f2; ff; oc1; oc2)) <~>
  intermediate
    (issig_Factorization (I; f1; f2; ff; oc1; oc2)) &
{path_factor1
: (fun x : A =>
   path_intermediate
     (factor1
        (issig_Factorization (I; f1; f2; ff; oc1; oc2))
        x)) ==
  factor1
    (issig_Factorization (I; f1; f2; ff; oc1; oc2)) &
{path_factor2
: factor2
    (issig_Factorization (I; f1; f2; ff; oc1; oc2)) ==
  (fun
     x : intermediate
           (issig_Factorization
              (I; f1; f2; ff; oc1; oc2)) =>
   factor2
     (issig_Factorization (I; f1; f2; ff; oc1; oc2))
     (path_intermediate x)) &
forall a : A,
(path_factor2
   (factor1
      (issig_Factorization (I; f1; f2; ff; oc1; oc2))
      a) @
 ap
   (factor2
      (issig_Factorization (I; f1; f2; ff; oc1; oc2)))
   (path_factor1 a)) @
fact_factors
  (issig_Factorization (I; f1; f2; ff; oc1; oc2)) a =
fact_factors
  (issig_Factorization (I; f1; f2; ff; oc1; oc2)) a}}}
      exists (equiv_idmap I); cbn.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
{path_factor1 : (fun x : A => f1 x) == f1 &
{path_factor2 : f2 == (fun x : I => f2 x) &
forall a : A,
(path_factor2 (f1 a) @ ap f2 (path_factor1 a)) @ ff a =
ff a}}
      exists (fun x:A => 1%path); cbn.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
{path_factor2 : f2 == (fun x : I => f2 x) &
forall a : A, (path_factor2 (f1 a) @ 1) @ ff a = ff a}
      exists (fun x:I => 1%path); cbn.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
forall a : A, 1 @ ff a = ff a
      intros; apply concat_1p. }
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
forall
b1 : {I : Type &
     {g : A -> I &
     {h : I -> B &
     {_ : (fun x : A => h (g x)) == f &
     {_ : class1 A I g & class2 I B h}}}}},
Contr
  {b2
  : {I : Type &
    {g : A -> I &
    {h : I -> B &
    {_ : (fun x : A => h (g x)) == f &
    {_ : class1 A I g & class2 I B h}}}}} &
  {path_intermediate
  : intermediate (issig_Factorization b1) <~>
    intermediate (issig_Factorization b2) &
  {path_factor1
  : (fun x : A =>
     path_intermediate
       (factor1 (issig_Factorization b1) x)) ==
    factor1 (issig_Factorization b2) &
  {path_factor2
  : factor2 (issig_Factorization b1) ==
    (fun x : intermediate (issig_Factorization b1) =>
     factor2 (issig_Factorization b2)
       (path_intermediate x)) &
  forall a : A,
  (path_factor2 (factor1 (issig_Factorization b1) a) @
   ap (factor2 (issig_Factorization b2))
     (path_factor1 a)) @
  fact_factors (issig_Factorization b2) a =
  fact_factors (issig_Factorization b1) a}}}}
    intros [I [f1 [f2 [ff [oc1 oc2]]]]].
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
Contr
  {b2
  : {I : Type &
    {g : A -> I &
    {h : I -> B &
    {_ : (fun x : A => h (g x)) == f &
    {_ : class1 A I g & class2 I B h}}}}} &
  {path_intermediate
  : intermediate
      (issig_Factorization (I; f1; f2; ff; oc1; oc2)) <~>
    intermediate (issig_Factorization b2) &
  {path_factor1
  : (fun x : A =>
     path_intermediate
       (factor1
          (issig_Factorization
             (I; f1; f2; ff; oc1; oc2)) x)) ==
    factor1 (issig_Factorization b2) &
  {path_factor2
  : factor2
      (issig_Factorization (I; f1; f2; ff; oc1; oc2)) ==
    (fun
       x : intermediate
             (issig_Factorization
                (I; f1; f2; ff; oc1; oc2)) =>
     factor2 (issig_Factorization b2)
       (path_intermediate x)) &
  forall a : A,
  (path_factor2
     (factor1
        (issig_Factorization (I; f1; f2; ff; oc1; oc2))
        a) @
   ap (factor2 (issig_Factorization b2))
     (path_factor1 a)) @
  fact_factors (issig_Factorization b2) a =
  fact_factors
    (issig_Factorization (I; f1; f2; ff; oc1; oc2)) a}}}}
    contr_sigsig I (equiv_idmap I); cbn.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
Contr
  {y
  : {g : A -> I &
    {h : I -> B &
    {_ : (fun x : A => h (g x)) == f &
    {_ : class1 A I g & class2 I B h}}}} &
  {path_factor1 : (fun x : A => f1 x) == y.1 &
  {path_factor2 : f2 == (fun x : I => (y.2).1 x) &
  forall a : A,
  (path_factor2 (f1 a) @ ap (y.2).1 (path_factor1 a)) @
  ((y.2).2).1 a = ff a}}}
    contr_sigsig f1 (fun x:A => idpath (f1 x)); cbn.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
Contr
  {y
  : {h : I -> B &
    {_ : (fun x : A => h (f1 x)) == f &
    {_ : class1 A I f1 & class2 I B h}}} &
  {path_factor2 : f2 == (fun x : I => y.1 x) &
  forall a : A,
  (path_factor2 (f1 a) @ 1) @ (y.2).1 a = ff a}}
    contr_sigsig f2 (fun x:I => idpath (f2 x)); cbn.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
Contr
  {y
  : {_ : (fun x : A => f2 (f1 x)) == f &
    {_ : class1 A I f1 & class2 I B f2}} &
  forall a : A, 1 @ y.1 a = ff a}
    refine (contr_equiv' {ff' : f2 o f1 == f & ff == ff'} _).
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
{ff' : (fun x : A => f2 (f1 x)) == f & ff == ff'} <~>
{y
: {_ : (fun x : A => f2 (f1 x)) == f &
  {_ : class1 A I f1 & class2 I B f2}} &
forall a : A, 1 @ y.1 a = ff a}
    symmetry; srefine (equiv_functor_sigma' (equiv_sigma_contr _) _).
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
forall a : (fun x : A => f2 (f1 x)) == f,
Contr
  ((fun _ : (fun x : A => f2 (f1 x)) == f =>
    {_ : class1 A I f1 & class2 I B f2}) a)
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
forall
a : {_ : (fun x : A => f2 (f1 x)) == f &
    {_ : class1 A I f1 & class2 I B f2}},
(fun
   y : {_ : (fun x : A => f2 (f1 x)) == f &
       {_ : class1 A I f1 & class2 I B f2}} =>
 forall a0 : A, 1 @ y.1 a0 = ff a0) a <~>
(fun ff' : (fun x : A => f2 (f1 x)) == f => ff == ff')
  (equiv_sigma_contr
     (fun _ : (fun x : A => f2 (f1 x)) == f =>
      {_ : class1 A I f1 & class2 I B f2}) a)
    {
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
forall a : (fun x : A => f2 (f1 x)) == f,
Contr
  ((fun _ : (fun x : A => f2 (f1 x)) == f =>
    {_ : class1 A I f1 & class2 I B f2}) a) intros h; cbn.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
h: (fun x : A => f2 (f1 x)) == f
Contr {_ : class1 A I f1 & class2 I B f2}
      srefine (@istrunc_sigma _ _ _ _ _); [ | intros a];
        apply contr_inhabited_hprop; try exact _; assumption. }
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
forall
a : {_ : (fun x : A => f2 (f1 x)) == f &
    {_ : class1 A I f1 & class2 I B f2}},
(fun
   y : {_ : (fun x : A => f2 (f1 x)) == f &
       {_ : class1 A I f1 & class2 I B f2}} =>
 forall a0 : A, 1 @ y.1 a0 = ff a0) a <~>
(fun ff' : (fun x : A => f2 (f1 x)) == f => ff == ff')
  (equiv_sigma_contr
     (fun _ : (fun x : A => f2 (f1 x)) == f =>
      {_ : class1 A I f1 & class2 I B f2}) a)
    intros [ff' [oc1' oc2']]; cbn.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
ff': (fun x : A => f2 (f1 x)) == f
oc1': class1 A I f1
oc2': class2 I B f2
(forall a : A, 1 @ ff' a = ff a) <~> ff == ff'
    refine (equiv_functor_forall' (equiv_idmap _) _); intros a.
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
ff': (fun x : A => f2 (f1 x)) == f
oc1': class1 A I f1
oc2': class2 I B f2
a: A
1 @ ff' (1%equiv a) = ff (1%equiv a) <~> ff a = ff' a
    refine (equiv_path_inverse _ _ oE _).
class1, class2: forall X Y : Type, (X -> Y) -> Type
H: forall (X Y : Type) (g : X -> Y),
IsHProp (class1 X Y g)
H0: forall (X Y : Type) (g : X -> Y),
IsHProp (class2 X Y g)
A, B: Type
f: A -> B
H1: Univalence
I: Type
f1: A -> I
f2: I -> B
ff: (fun x : A => f2 (f1 x)) == f
oc1: class1 A I f1
oc2: class2 I B f2
ff': (fun x : A => f2 (f1 x)) == f
oc1': class1 A I f1
oc2': class2 I B f2
a: A
1 @ ff' (1%equiv a) = ff (1%equiv a) <~> ff' a = ff a
    apply equiv_concat_l; symmetry; apply concat_1p.
  Defined.

  Definition path_factorization `{Univalence} (fact fact' : Factorization)
    : PathFactorization fact fact' -> fact = fact'
    := equiv_path_factorization fact fact'.

End Factorization.

Arguments Factorization class1 class2 {A B} f.
Arguments PathFactorization {class1 class2 A B f} fact fact'.

(* This enables us to talk about "the image of a map" as a factorization but also as the intermediate object appearing in it, as is common in informal mathematics. *)
Coercion intermediate : Factorization >-> Sortclass.

(** ** Factorization Systems *)

(** A ("unique" or "orthogonal") factorization system consists of a couple of classes of maps, closed under composition, such that every map admits a unique factorization. *)
Record FactorizationSystem@{i j k} :=
  { class1 : forall {X Y : Type@{i}}, (X -> Y) -> Type@{j} ;
    ishprop_class1 :: forall {X Y : Type@{i}} (g:X->Y), IsHProp (class1 g) ;
    class1_isequiv : forall {X Y : Type@{i}} (g:X->Y) {geq:IsEquiv g}, class1 g ;
    class1_compose : forall {X Y Z : Type@{i}} (g:X->Y) (h:Y->Z),
                       class1 g -> class1 h -> class1 (h o g) ;
    class2 : forall {X Y : Type@{i}}, (X -> Y) -> Type@{k} ;
    ishprop_class2 :: forall {X Y : Type@{i}} (g:X->Y), IsHProp (class2 g) ;
    class2_isequiv : forall {X Y : Type@{i}} (g:X->Y) {geq:IsEquiv g}, class2 g ;
    class2_compose : forall {X Y Z : Type@{i}} (g:X->Y) (h:Y->Z),
                       class2 g -> class2 h -> class2 (h o g) ;
    (** Morally, the uniqueness of factorizations says that [Factorization class1 class2 f] is contractible.  However, in practice we always *prove* that by way of [path_factorization], and we frequently want to *use* the components of a [PathFactorization] as well.  Thus, as data we store the canonical factorization and a [PathFactorization] between any two such, and prove in a moment that this implies contractibility of the space of factorizations. *)
    factor : forall {X Y : Type@{i}} (f:X->Y), Factorization@{i} (@class1) (@class2) f ;
    path_factor : forall {X Y : Type@{i}} (f:X->Y)
                         (fact : Factorization@{i} (@class1) (@class2) f)
                         (fact' : Factorization@{i} (@class1) (@class2) f),
                    PathFactorization@{i} fact fact'
  }.

(** The type of factorizations is, as promised, contractible. *)
Theorem contr_factor `{Univalence} (factsys : FactorizationSystem)
        {X Y : Type} (f : X -> Y)
  : Contr (Factorization (@class1 factsys) (@class2 factsys) f).
H: Univalence
factsys: FactorizationSystem
X, Y: Type
f: X -> Y
Contr
  (Factorization (@class1 factsys) (@class2 factsys) f)
Proof.
H: Univalence
factsys: FactorizationSystem
X, Y: Type
f: X -> Y
Contr
  (Factorization (@class1 factsys) (@class2 factsys) f)
  apply contr_inhabited_hprop.
H: Univalence
factsys: FactorizationSystem
X, Y: Type
f: X -> Y
IsHProp
  (Factorization (@class1 factsys) (@class2 factsys) f)
H: Univalence
factsys: FactorizationSystem
X, Y: Type
f: X -> Y
Factorization (@class1 factsys) (@class2 factsys) f
  -
H: Univalence
factsys: FactorizationSystem
X, Y: Type
f: X -> Y
IsHProp
  (Factorization (@class1 factsys) (@class2 factsys) f) apply hprop_allpath.
H: Univalence
factsys: FactorizationSystem
X, Y: Type
f: X -> Y
forall
x
 y : Factorization (@class1 factsys) (@class2 factsys)
       f, x = y
    intros fact fact'.
H: Univalence
factsys: FactorizationSystem
X, Y: Type
f: X -> Y
fact, fact': Factorization (@class1 factsys)
  (@class2 factsys) f
fact = fact'
    apply path_factorization; try exact _.
H: Univalence
factsys: FactorizationSystem
X, Y: Type
f: X -> Y
fact, fact': Factorization (@class1 factsys)
  (@class2 factsys) f
PathFactorization fact fact'
    apply path_factor.
  -
H: Univalence
factsys: FactorizationSystem
X, Y: Type
f: X -> Y
Factorization (@class1 factsys) (@class2 factsys) f apply factor.
Defined.

Section FactSys.

  Context (factsys : FactorizationSystem).

  Definition Build_Factorization' {X Y}
    := @Build_Factorization (@class1 factsys) (@class2 factsys) X Y.

  Definition Build_PathFactorization' {X Y}
    := @Build_PathFactorization (@class1 factsys) (@class2 factsys) X Y.

  (** The left class is right-cancellable and the right class is left-cancellable. *)
  Definition cancelR_class1 `{Funext} {X Y Z} (f : X -> Y) (g : Y -> Z)
  : class1 factsys f -> class1 factsys (g o f) -> class1 factsys g.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
class1 factsys f ->
class1 factsys (g o f) -> class1 factsys g
  Proof.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
class1 factsys f ->
class1 factsys (g o f) -> class1 factsys g
    intros c1f c1gf.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c1f: class1 factsys f
c1gf: class1 factsys (g o f)
class1 factsys g
    destruct (factor factsys g) as [I g1 g2 gf c1g1 c2g2].
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c1f: class1 factsys f
c1gf: class1 factsys (g o f)
I: Type
g1: Y -> I
g2: I -> Z
gf: (fun x : Y => g2 (g1 x)) == g
c1g1: class1 factsys g1
c2g2: class2 factsys g2
class1 factsys g
    pose (fact  := Build_Factorization' (g o f) Z (g o f) (idmap)
                     (fun x => 1) c1gf (class2_isequiv factsys idmap)).
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c1f: class1 factsys f
c1gf: class1 factsys (g o f)
I: Type
g1: Y -> I
g2: I -> Z
gf: (fun x : Y => g2 (g1 x)) == g
c1g1: class1 factsys g1
c2g2: class2 factsys g2
fact:= Build_Factorization' (g o f) Z 
  (g o f) idmap (fun x : X => 1) c1gf
  (class2_isequiv factsys idmap): Factorization (@class1 factsys)
  (@class2 factsys) (g o f)
class1 factsys g
    pose (fact' := Build_Factorization' (g o f) I (g1 o f) g2
                     (fun x => gf (f x))
                     (class1_compose factsys f g1 c1f c1g1) c2g2).
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c1f: class1 factsys f
c1gf: class1 factsys (g o f)
I: Type
g1: Y -> I
g2: I -> Z
gf: (fun x : Y => g2 (g1 x)) == g
c1g1: class1 factsys g1
c2g2: class2 factsys g2
fact:= Build_Factorization' (g o f) Z 
  (g o f) idmap (fun x : X => 1) c1gf
  (class2_isequiv factsys idmap): Factorization (@class1 factsys)
  (@class2 factsys) (g o f)
fact':= Build_Factorization' (g o f) I 
  (g1 o f) g2 (fun x : X => gf (f x))
  (class1_compose factsys f g1 c1f c1g1) c2g2: Factorization (@class1 factsys)
  (@class2 factsys) (g o f)
class1 factsys g
    destruct (path_factor factsys (g o f) fact' fact)
             as [q q1 q2 qf]; simpl in *.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c1f: class1 factsys f
c1gf: class1 factsys (fun x : X => g (f x))
I: Type
g1: Y -> I
g2: I -> Z
gf: (fun x : Y => g2 (g1 x)) == g
c1g1: class1 factsys g1
c2g2: class2 factsys g2
fact:= Build_Factorization' (fun x : X => g (f x)) Z
  (fun x : X => g (f x)) idmap 
  (fun x : X => 1) c1gf
  (class2_isequiv factsys idmap): Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
fact':= Build_Factorization' (fun x : X => g (f x)) I
  (fun x : X => g1 (f x)) g2
  (fun x : X => gf (f x))
  (class1_compose factsys f g1 c1f c1g1) c2g2: Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
q: I <~> Z
q1: (fun x : X => q (g1 (f x))) ==
(fun x : X => g (f x))
q2: g2 == (fun x : I => q x)
qf: forall a : X,
(q2 (g1 (f a)) @ ap idmap (q1 a)) @ 1 = gf (f a)
class1 factsys g
    refine (transport (class1 factsys) (path_arrow _ _ gf) _).
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c1f: class1 factsys f
c1gf: class1 factsys (fun x : X => g (f x))
I: Type
g1: Y -> I
g2: I -> Z
gf: (fun x : Y => g2 (g1 x)) == g
c1g1: class1 factsys g1
c2g2: class2 factsys g2
fact:= Build_Factorization' (fun x : X => g (f x)) Z
  (fun x : X => g (f x)) idmap 
  (fun x : X => 1) c1gf
  (class2_isequiv factsys idmap): Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
fact':= Build_Factorization' (fun x : X => g (f x)) I
  (fun x : X => g1 (f x)) g2
  (fun x : X => gf (f x))
  (class1_compose factsys f g1 c1f c1g1) c2g2: Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
q: I <~> Z
q1: (fun x : X => q (g1 (f x))) ==
(fun x : X => g (f x))
q2: g2 == (fun x : I => q x)
qf: forall a : X,
(q2 (g1 (f a)) @ ap idmap (q1 a)) @ 1 = gf (f a)
class1 factsys (fun x : Y => g2 (g1 x))
    refine (class1_compose factsys g1 g2 c1g1 _).
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c1f: class1 factsys f
c1gf: class1 factsys (fun x : X => g (f x))
I: Type
g1: Y -> I
g2: I -> Z
gf: (fun x : Y => g2 (g1 x)) == g
c1g1: class1 factsys g1
c2g2: class2 factsys g2
fact:= Build_Factorization' (fun x : X => g (f x)) Z
  (fun x : X => g (f x)) idmap 
  (fun x : X => 1) c1gf
  (class2_isequiv factsys idmap): Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
fact':= Build_Factorization' (fun x : X => g (f x)) I
  (fun x : X => g1 (f x)) g2
  (fun x : X => gf (f x))
  (class1_compose factsys f g1 c1f c1g1) c2g2: Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
q: I <~> Z
q1: (fun x : X => q (g1 (f x))) ==
(fun x : X => g (f x))
q2: g2 == (fun x : I => q x)
qf: forall a : X,
(q2 (g1 (f a)) @ ap idmap (q1 a)) @ 1 = gf (f a)
class1 factsys g2
    apply class1_isequiv.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c1f: class1 factsys f
c1gf: class1 factsys (fun x : X => g (f x))
I: Type
g1: Y -> I
g2: I -> Z
gf: (fun x : Y => g2 (g1 x)) == g
c1g1: class1 factsys g1
c2g2: class2 factsys g2
fact:= Build_Factorization' (fun x : X => g (f x)) Z
  (fun x : X => g (f x)) idmap 
  (fun x : X => 1) c1gf
  (class2_isequiv factsys idmap): Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
fact':= Build_Factorization' (fun x : X => g (f x)) I
  (fun x : X => g1 (f x)) g2
  (fun x : X => gf (f x))
  (class1_compose factsys f g1 c1f c1g1) c2g2: Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
q: I <~> Z
q1: (fun x : X => q (g1 (f x))) ==
(fun x : X => g (f x))
q2: g2 == (fun x : I => q x)
qf: forall a : X,
(q2 (g1 (f a)) @ ap idmap (q1 a)) @ 1 = gf (f a)
IsEquiv g2
    exact (isequiv_homotopic _ (fun i => (q2 i)^)).
  Defined.

  Definition cancelL_class2 `{Funext} {X Y Z} (f : X -> Y) (g : Y -> Z)
  : class2 factsys g -> class2 factsys (g o f) -> class2 factsys f.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
class2 factsys g ->
class2 factsys (g o f) -> class2 factsys f
  Proof.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
class2 factsys g ->
class2 factsys (g o f) -> class2 factsys f
    intros c2g c2gf.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c2g: class2 factsys g
c2gf: class2 factsys (g o f)
class2 factsys f
    destruct (factor factsys f) as [I f1 f2 ff c1f1 c2f2].
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c2g: class2 factsys g
c2gf: class2 factsys (g o f)
I: Type
f1: X -> I
f2: I -> Y
ff: (fun x : X => f2 (f1 x)) == f
c1f1: class1 factsys f1
c2f2: class2 factsys f2
class2 factsys f
    pose (fact  := Build_Factorization' (g o f) X (idmap) (g o f)
                     (fun x => 1) (class1_isequiv factsys idmap) c2gf).
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c2g: class2 factsys g
c2gf: class2 factsys (g o f)
I: Type
f1: X -> I
f2: I -> Y
ff: (fun x : X => f2 (f1 x)) == f
c1f1: class1 factsys f1
c2f2: class2 factsys f2
fact:= Build_Factorization' (g o f) X idmap 
  (g o f) (fun x : X => 1)
  (class1_isequiv factsys idmap) c2gf: Factorization (@class1 factsys)
  (@class2 factsys) (g o f)
class2 factsys f
    pose (fact' := Build_Factorization' (g o f) I f1 (g o f2)
                     (fun x => ap g (ff x))
                     c1f1 (class2_compose factsys f2 g c2f2 c2g)).
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c2g: class2 factsys g
c2gf: class2 factsys (g o f)
I: Type
f1: X -> I
f2: I -> Y
ff: (fun x : X => f2 (f1 x)) == f
c1f1: class1 factsys f1
c2f2: class2 factsys f2
fact:= Build_Factorization' (g o f) X idmap 
  (g o f) (fun x : X => 1)
  (class1_isequiv factsys idmap) c2gf: Factorization (@class1 factsys)
  (@class2 factsys) (g o f)
fact':= Build_Factorization' (g o f) I f1 
  (g o f2) (fun x : X => ap g (ff x)) c1f1
  (class2_compose factsys f2 g c2f2 c2g): Factorization (@class1 factsys)
  (@class2 factsys) (g o f)
class2 factsys f
    destruct (path_factor factsys (g o f) fact fact')
             as [q q1 q2 qf]; simpl in *.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c2g: class2 factsys g
c2gf: class2 factsys (fun x : X => g (f x))
I: Type
f1: X -> I
f2: I -> Y
ff: (fun x : X => f2 (f1 x)) == f
c1f1: class1 factsys f1
c2f2: class2 factsys f2
fact:= Build_Factorization' (fun x : X => g (f x)) X
  idmap (fun x : X => g (f x)) 
  (fun x : X => 1)
  (class1_isequiv factsys idmap) c2gf: Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
fact':= Build_Factorization' (fun x : X => g (f x)) I
  f1 (fun x : I => g (f2 x))
  (fun x : X => ap g (ff x)) c1f1
  (class2_compose factsys f2 g c2f2 c2g): Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
q: X <~> I
q1: (fun x : X => q x) == f1
q2: (fun x : X => g (f x)) ==
(fun x : X => g (f2 (q x)))
qf: forall a : X,
(q2 a @ ap (fun x : I => g (f2 x)) (q1 a)) @
ap g (ff a) = 1
class2 factsys f
    refine (transport (class2 factsys) (path_arrow _ _ ff) _).
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c2g: class2 factsys g
c2gf: class2 factsys (fun x : X => g (f x))
I: Type
f1: X -> I
f2: I -> Y
ff: (fun x : X => f2 (f1 x)) == f
c1f1: class1 factsys f1
c2f2: class2 factsys f2
fact:= Build_Factorization' (fun x : X => g (f x)) X
  idmap (fun x : X => g (f x)) 
  (fun x : X => 1)
  (class1_isequiv factsys idmap) c2gf: Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
fact':= Build_Factorization' (fun x : X => g (f x)) I
  f1 (fun x : I => g (f2 x))
  (fun x : X => ap g (ff x)) c1f1
  (class2_compose factsys f2 g c2f2 c2g): Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
q: X <~> I
q1: (fun x : X => q x) == f1
q2: (fun x : X => g (f x)) ==
(fun x : X => g (f2 (q x)))
qf: forall a : X,
(q2 a @ ap (fun x : I => g (f2 x)) (q1 a)) @
ap g (ff a) = 1
class2 factsys (fun x : X => f2 (f1 x))
    refine (class2_compose factsys f1 f2 _ c2f2).
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c2g: class2 factsys g
c2gf: class2 factsys (fun x : X => g (f x))
I: Type
f1: X -> I
f2: I -> Y
ff: (fun x : X => f2 (f1 x)) == f
c1f1: class1 factsys f1
c2f2: class2 factsys f2
fact:= Build_Factorization' (fun x : X => g (f x)) X
  idmap (fun x : X => g (f x)) 
  (fun x : X => 1)
  (class1_isequiv factsys idmap) c2gf: Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
fact':= Build_Factorization' (fun x : X => g (f x)) I
  f1 (fun x : I => g (f2 x))
  (fun x : X => ap g (ff x)) c1f1
  (class2_compose factsys f2 g c2f2 c2g): Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
q: X <~> I
q1: (fun x : X => q x) == f1
q2: (fun x : X => g (f x)) ==
(fun x : X => g (f2 (q x)))
qf: forall a : X,
(q2 a @ ap (fun x : I => g (f2 x)) (q1 a)) @
ap g (ff a) = 1
class2 factsys f1
    apply class2_isequiv.
factsys: FactorizationSystem
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
c2g: class2 factsys g
c2gf: class2 factsys (fun x : X => g (f x))
I: Type
f1: X -> I
f2: I -> Y
ff: (fun x : X => f2 (f1 x)) == f
c1f1: class1 factsys f1
c2f2: class2 factsys f2
fact:= Build_Factorization' (fun x : X => g (f x)) X
  idmap (fun x : X => g (f x)) 
  (fun x : X => 1)
  (class1_isequiv factsys idmap) c2gf: Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
fact':= Build_Factorization' (fun x : X => g (f x)) I
  f1 (fun x : I => g (f2 x))
  (fun x : X => ap g (ff x)) c1f1
  (class2_compose factsys f2 g c2f2 c2g): Factorization (@class1 factsys)
  (@class2 factsys) (fun x : X => g (f x))
q: X <~> I
q1: (fun x : X => q x) == f1
q2: (fun x : X => g (f x)) ==
(fun x : X => g (f2 (q x)))
qf: forall a : X,
(q2 a @ ap (fun x : I => g (f2 x)) (q1 a)) @
ap g (ff a) = 1
IsEquiv f1
    exact (isequiv_homotopic _ q1).
  Defined.

  (** The two classes of maps are automatically orthogonal, i.e. any commutative square from a [class1] map to a [class2] map has a unique diagonal filler.  For now, we only bother to define the lift; in principle we ought to show that the type of lifts is contractible. *)
  Universe ctxi.
  Context {A B X Y : Type@{ctxi}}
          (i : A -> B) (c1i : class1 factsys i)
          (p : X -> Y) (c2p : class2 factsys p)
          (f : A -> X) (g : B -> Y) (h : p o f == g o i).

  (** First we factor [f] *)
  Let C  : Type         := intermediate (factor factsys f).
  Let f1 : A -> C       := factor1      (factor factsys f).
  Let f2 : C -> X       := factor2      (factor factsys f).
  Let ff : f2 o f1 == f := fact_factors (factor factsys f).

  (** and [g] *)
  Let D  : Type         := intermediate (factor factsys g).
  Let g1 : B -> D       := factor1      (factor factsys g).
  Let g2 : D -> Y       := factor2      (factor factsys g).
  Let gf : g2 o g1 == g := fact_factors (factor factsys g).

  (** Now we observe that [p o f2] and [f1], and [g2] and [g1 o i], are both factorizations of the common diagonal of the commutative square (for which we use [p o f], but we could equally well use [g o i]. *)
  Let fact  : Factorization (@class1 factsys) (@class2 factsys) (p o f)
            := Build_Factorization' (p o f) C f1 (p o f2)
                 (fun a => ap p (ff a))
                 (inclass1 (factor factsys f))
                 (class2_compose factsys f2 p
                                 (inclass2 (factor factsys f))
                                 c2p).
  Let fact' : Factorization (@class1 factsys) (@class2 factsys) (p o f)
            := Build_Factorization' (p o f) D (g1 o i) g2
                 (fun a => gf (i a) @ (h a)^)
                 (class1_compose factsys i g1 c1i
                                 (inclass1 (factor factsys g)))
                 (inclass2 (factor factsys g)).

  (** Therefore, by the uniqueness of factorizations, we have an equivalence [q] relating them. *)
  Let q  : C <~> D          := path_intermediate
                                 (path_factor factsys (p o f) fact fact').
  Let q1 : q o f1 == g1 o i := path_factor1
                                 (path_factor factsys (p o f) fact fact').
  Let q2 : p o f2 == g2 o q := path_factor2
                                 (path_factor factsys (p o f) fact fact').

  (** Using this, we can define the lift. *)
  Definition lift_factsys : B -> X
    := f2 o q^-1 o g1.

  (** And the commutative triangles making it a lift *)
  Definition lift_factsys_tri1 : lift_factsys o i == f.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
lift_factsys o i == f
  Proof.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
lift_factsys o i == f
    intros x.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
lift_factsys (i x) = f x
    refine (ap (f2 o q^-1) (q1 x)^ @ _).
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
f2 (q^-1 (q (f1 x))) = f x
    transitivity (f2 (f1 x)).
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
f2 (q^-1 (q (f1 x))) = f2 (f1 x)
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
f2 (f1 x) = f x
    +
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
f2 (q^-1 (q (f1 x))) = f2 (f1 x) apply ap, eissect.
    +
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
f2 (f1 x) = f x apply ff.
  Defined.

  Definition lift_factsys_tri2 : p o lift_factsys == g.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
p o lift_factsys == g
  Proof.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
p o lift_factsys == g
    intros x.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: B
p (lift_factsys x) = g x
    refine (q2 _ @ _).
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: B
g2 (q (q^-1 (g1 x))) = g x
    transitivity (g2 (g1 x)).
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: B
g2 (q (q^-1 (g1 x))) = g2 (g1 x)
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: B
g2 (g1 x) = g x
    +
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: B
g2 (q (q^-1 (g1 x))) = g2 (g1 x) apply ap, eisretr.
    +
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: B
g2 (g1 x) = g x apply gf.
  Defined.

  (** And finally prove that these two triangles compose to the given commutative square. *)
  Definition lift_factsys_square (x : A)
  : ap p (lift_factsys_tri1 x)^ @ lift_factsys_tri2 (i x) = h x.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p (lift_factsys_tri1 x)^ @ lift_factsys_tri2 (i x) =
h x
  Proof.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p (lift_factsys_tri1 x)^ @ lift_factsys_tri2 (i x) =
h x
    unfold lift_factsys_tri1, lift_factsys_tri2.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a) @ (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p
  (ap (fun x : D => f2 (q^-1 x)) (q1 x)^ @
   (ap f2 (eissect q (f1 x)) @ ff x))^ @
(q2 (q^-1 (g1 (i x))) @
 (ap g2 (eisretr q (g1 (i x))) @ gf (i x))) = h x
    Open Scope long_path_scope.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p
  (ap (fun x : D => f2 (q^-1 x)) (q1 x)^
   @' (ap f2 (eissect q (f1 x))
       @' ff x))^
@' (q2 (q^-1 (g1 (i x)))
    @' (ap g2 (eisretr q (g1 (i x)))
        @' gf (i x))) = h x
    (* First we use the one aspect of the uniqueness of factorizations that we haven't mentioned yet. *)
    pose (r := path_fact_factors (path_factor factsys (p o f) fact fact') x
            : q2 (f1 x) @ ap g2 (q1 x) @ (gf (i x) @ (h x)^) = ap p (ff x)).
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
r:= path_fact_factors
  (path_factor factsys (p o f) fact fact') x
:
q2 (f1 x)
@' ap g2 (q1 x)
@' (gf (i x)
    @' (h x)^) = ap p (ff x): q2 (f1 x)
@' ap g2 (q1 x)
@' (gf (i x)
    @' (h x)^) = ap p (ff x)
ap p
  (ap (fun x : D => f2 (q^-1 x)) (q1 x)^
   @' (ap f2 (eissect q (f1 x))
       @' ff x))^
@' (q2 (q^-1 (g1 (i x)))
    @' (ap g2 (eisretr q (g1 (i x)))
        @' gf (i x))) = h x
    rewrite concat_p_pp in r.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
r: q2 (f1 x)
@' ap g2 (q1 x)
@' gf (i x)
@' (h x)^ = ap p (ff x)
ap p
  (ap (fun x : D => f2 (q^-1 x)) (q1 x)^
   @' (ap f2 (eissect q (f1 x))
       @' ff x))^
@' (q2 (q^-1 (g1 (i x)))
    @' (ap g2 (eisretr q (g1 (i x)))
        @' gf (i x))) = h x
    apply moveL_pM, moveR_Vp in r.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
r: (ap p (ff x))^
@' (q2 (f1 x)
    @' ap g2 (q1 x)
    @' gf (i x)) = h x
ap p
  (ap (fun x : D => f2 (q^-1 x)) (q1 x)^
   @' (ap f2 (eissect q (f1 x))
       @' ff x))^
@' (q2 (q^-1 (g1 (i x)))
    @' (ap g2 (eisretr q (g1 (i x)))
        @' gf (i x))) = h x
    refine (_ @ r); clear r.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p
  (ap (fun x : D => f2 (q^-1 x)) (q1 x)^
   @' (ap f2 (eissect q (f1 x))
       @' ff x))^
@' (q2 (q^-1 (g1 (i x)))
    @' (ap g2 (eisretr q (g1 (i x)))
        @' gf (i x))) =
(ap p (ff x))^
@' (q2 (f1 x)
    @' ap g2 (q1 x)
    @' gf (i x))
    (* Now we can cancel some whiskered paths on both sides. *)
    repeat rewrite inv_pp; repeat rewrite ap_pp; rewrite ap_V.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
(ap p (ff x))^
@' ap p (ap f2 (eissect q (f1 x)))^
@' ap p (ap (fun x : D => f2 (q^-1 x)) (q1 x)^)^
@' (q2 (q^-1 (g1 (i x)))
    @' (ap g2 (eisretr q (g1 (i x)))
        @' gf (i x))) =
(ap p (ff x))^
@' (q2 (f1 x)
    @' ap g2 (q1 x)
    @' gf (i x))
    repeat rewrite concat_pp_p; apply whiskerL.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p (ap f2 (eissect q (f1 x)))^
@' (ap p (ap (fun x : D => f2 (q^-1 x)) (q1 x)^)^
    @' (q2 (q^-1 (g1 (i x)))
        @' (ap g2 (eisretr q (g1 (i x)))
            @' gf (i x)))) =
q2 (f1 x)
@' (ap g2 (q1 x)
    @' gf (i x))
    repeat rewrite concat_p_pp; apply whiskerR.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p (ap f2 (eissect q (f1 x)))^
@' ap p (ap (fun x : D => f2 (q^-1 x)) (q1 x)^)^
@' q2 (q^-1 (g1 (i x)))
@' ap g2 (eisretr q (g1 (i x))) =
q2 (f1 x)
@' ap g2 (q1 x)
    (* Next we set up for a naturality. *)
    rewrite (ap_compose q^-1 f2), <- ap_pp, <- inv_pp.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p
  (ap f2 (ap q^-1 (q1 x)^)
   @' ap f2 (eissect q (f1 x)))^
@' q2 (q^-1 (g1 (i x)))
@' ap g2 (eisretr q (g1 (i x))) =
q2 (f1 x)
@' ap g2 (q1 x)
    (* The next line appears to do nothing, but in fact it is necessary for the subsequent [rewrite] to succeed, because [lift_factsys] appears in the invisible implicit point-arguments of [paths].  One way to discover issues of that sort is to turn on printing of all implicit arguments with [Set Printing All]; another is to use [Set Debug Tactic Unification] and inspect the output to see what [rewrite] is trying and failing to unify. *)
    unfold lift_factsys.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p
  (ap f2 (ap q^-1 (q1 x)^)
   @' ap f2 (eissect q (f1 x)))^
@' q2 (q^-1 (g1 (i x)))
@' ap g2 (eisretr q (g1 (i x))) =
q2 (f1 x)
@' ap g2 (q1 x)
    rewrite <- ap_pp.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap p (ap f2 (ap q^-1 (q1 x)^
             @' eissect q (f1 x)))^
@' q2 (q^-1 (g1 (i x)))
@' ap g2 (eisretr q (g1 (i x))) =
q2 (f1 x)
@' ap g2 (q1 x)
    rewrite <- ap_V, <- ap_compose.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap (fun x : C => p (f2 x))
  (ap q^-1 (q1 x)^
   @' eissect q (f1 x))^
@' q2 (q^-1 (g1 (i x)))
@' ap g2 (eisretr q (g1 (i x))) =
q2 (f1 x)
@' ap g2 (q1 x)
    rewrite (concat_Ap q2).
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
q2 (f1 x)
@' ap (fun x : C => g2 (q x))
     (ap q^-1 (q1 x)^
      @' eissect q (f1 x))^
@' ap g2 (eisretr q (g1 (i x))) =
q2 (f1 x)
@' ap g2 (q1 x)
    (* Now we can cancel another path *)
    rewrite concat_pp_p; apply whiskerL.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap (fun x : C => g2 (q x))
  (ap q^-1 (q1 x)^
   @' eissect q (f1 x))^
@' ap g2 (eisretr q (g1 (i x))) = ap g2 (q1 x)
    (* And set up for an application of [ap]. *)
    rewrite ap_compose.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap g2 (ap q (ap q^-1 (q1 x)^
             @' eissect q (f1 x))^)
@' ap g2 (eisretr q (g1 (i x))) = ap g2 (q1 x)
    rewrite <- ap_pp.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap g2
  (ap q (ap q^-1 (q1 x)^
         @' eissect q (f1 x))^
   @' eisretr q (g1 (i x))) = ap g2 (q1 x)
    apply ap.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap q (ap q^-1 (q1 x)^
      @' eissect q (f1 x))^
@' eisretr q (g1 (i x)) = q1 x
    (* Now we apply the triangle identity [eisadj]. *)
    rewrite inv_pp, ap_pp, ap_V.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
(ap q (eissect q (f1 x)))^
@' ap q (ap q^-1 (q1 x)^)^
@' eisretr q (g1 (i x)) = q1 x
    rewrite <- eisadj.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
(eisretr q (q (f1 x)))^
@' ap q (ap q^-1 (q1 x)^)^
@' eisretr q (g1 (i x)) = q1 x
    (* Finally, we rearrange and it becomes a naturality square. *)
    rewrite concat_pp_p; apply moveR_Vp.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap q (ap q^-1 (q1 x)^)^
@' eisretr q (g1 (i x)) = eisretr q (q (f1 x))
                          @' q1 x
    rewrite <- ap_V, inv_V, <- ap_compose.
factsys: FactorizationSystem
A, B, X, Y: Type
i: A -> B
c1i: class1 factsys i
p: X -> Y
c2p: class2 factsys p
f: A -> X
g: B -> Y
h: p o f == g o i
C:= factor factsys f: Type
f1:= factor1 (factor factsys f): A -> C
f2:= factor2 (factor factsys f): C -> X
ff:= fact_factors (factor factsys f): f2 o f1 == f
D:= factor factsys g: Type
g1:= factor1 (factor factsys g): B -> D
g2:= factor2 (factor factsys g): D -> Y
gf:= fact_factors (factor factsys g): g2 o g1 == g
fact:= Build_Factorization' (p o f) C f1 
  (p o f2) (fun a : A => ap p (ff a))
  (inclass1 (factor factsys f))
  (class2_compose factsys f2 p
     (inclass2 (factor factsys f)) c2p): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
fact':= Build_Factorization' (p o f) D 
  (g1 o i) g2 (fun a : A => gf (i a)
                      @' (h a)^)
  (class1_compose factsys i g1 c1i
     (inclass1 (factor factsys g)))
  (inclass2 (factor factsys g)): Factorization (@class1 factsys)
  (@class2 factsys) (p o f)
q:= path_intermediate
  (path_factor factsys (p o f) fact fact'): C <~> D
q1:= path_factor1
  (path_factor factsys (p o f) fact fact'): q o f1 == g1 o i
q2:= path_factor2
  (path_factor factsys (p o f) fact fact'): p o f2 == g2 o q
x: A
ap (fun x : D => q (q^-1 x)) (q1 x)
@' eisretr q (g1 (i x)) = eisretr q (q (f1 x))
                          @' q1 x
    exact (concat_A1p (eisretr q) (q1 x)).
    Close Scope long_path_scope.
  Qed.

End FactSys.

Section FactsysExtensions.
  Context {factsys : FactorizationSystem}.

  (** We can deduce the lifting property in terms of extensions fairly easily from the version in terms of commutative squares. *)
  Definition extension_factsys {A B : Type}
             (f : A -> B) {c1f : class1 factsys f}
             (P : B -> Type) (c2P : class2 factsys (@pr1 B P))
             (d : forall a:A, P (f a))
  : ExtensionAlong f P d.
factsys: FactorizationSystem
A, B: Type
f: A -> B
c1f: class1 factsys f
P: B -> Type
c2P: class2 factsys pr1
d: forall a : A, P (f a)
ExtensionAlong f P d
  Proof.
factsys: FactorizationSystem
A, B: Type
f: A -> B
c1f: class1 factsys f
P: B -> Type
c2P: class2 factsys pr1
d: forall a : A, P (f a)
ExtensionAlong f P d
    pose (e := lift_factsys factsys f c1f pr1 c2P
                            (fun a => (f a ; d a)) idmap
                            (fun a => 1)).
factsys: FactorizationSystem
A, B: Type
f: A -> B
c1f: class1 factsys f
P: B -> Type
c2P: class2 factsys pr1
d: forall a : A, P (f a)
e:= lift_factsys factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): B -> {x : _ & P x}
ExtensionAlong f P d
    pose (e2 := lift_factsys_tri2 factsys f c1f pr1 c2P
                            (fun a => (f a ; d a)) idmap
                            (fun a => 1)).
factsys: FactorizationSystem
A, B: Type
f: A -> B
c1f: class1 factsys f
P: B -> Type
c2P: class2 factsys pr1
d: forall a : A, P (f a)
e:= lift_factsys factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): B -> {x : _ & P x}
e2:= lift_factsys_tri2 factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): pr1
o lift_factsys factsys f c1f pr1 c2P
    (fun a : A => (f a; d a)) idmap
    (fun a : A => 1) == idmap
ExtensionAlong f P d
    exists (fun a => (e2 a) # (e a).2).
factsys: FactorizationSystem
A, B: Type
f: A -> B
c1f: class1 factsys f
P: B -> Type
c2P: class2 factsys pr1
d: forall a : A, P (f a)
e:= lift_factsys factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): B -> {x : _ & P x}
e2:= lift_factsys_tri2 factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): pr1
o lift_factsys factsys f c1f pr1 c2P
    (fun a : A => (f a; d a)) idmap
    (fun a : A => 1) == idmap
forall x : A, transport P (e2 (f x)) (e (f x)).2 = d x
    intros a.
factsys: FactorizationSystem
A, B: Type
f: A -> B
c1f: class1 factsys f
P: B -> Type
c2P: class2 factsys pr1
d: forall a : A, P (f a)
e:= lift_factsys factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): B -> {x : _ & P x}
e2:= lift_factsys_tri2 factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): pr1
o lift_factsys factsys f c1f pr1 c2P
    (fun a : A => (f a; d a)) idmap
    (fun a : A => 1) == idmap
a: A
transport P (e2 (f a)) (e (f a)).2 = d a
    pose (e1 := lift_factsys_tri1 factsys f c1f pr1 c2P
                            (fun a => (f a ; d a)) idmap
                            (fun a => 1) a
                : e (f a) = (f a ; d a)).
factsys: FactorizationSystem
A, B: Type
f: A -> B
c1f: class1 factsys f
P: B -> Type
c2P: class2 factsys pr1
d: forall a : A, P (f a)
e:= lift_factsys factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): B -> {x : _ & P x}
e2:= lift_factsys_tri2 factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): pr1
o lift_factsys factsys f c1f pr1 c2P
    (fun a : A => (f a; d a)) idmap
    (fun a : A => 1) == idmap
a: A
e1:= lift_factsys_tri1 factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1) a
:
e (f a) = (f a; d a): e (f a) = (f a; d a)
transport P (e2 (f a)) (e (f a)).2 = d a
    pose (e3 := moveL_M1 _ _ (((ap_V _ _)^ @@ 1)
                @ lift_factsys_square factsys f c1f pr1 c2P
                            (fun a => (f a ; d a)) idmap
                            (fun a => 1) a)
                : e2 (f a) = pr1_path e1).
factsys: FactorizationSystem
A, B: Type
f: A -> B
c1f: class1 factsys f
P: B -> Type
c2P: class2 factsys pr1
d: forall a : A, P (f a)
e:= lift_factsys factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): B -> {x : _ & P x}
e2:= lift_factsys_tri2 factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): pr1
o lift_factsys factsys f c1f pr1 c2P
    (fun a : A => (f a; d a)) idmap
    (fun a : A => 1) == idmap
a: A
e1:= lift_factsys_tri1 factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1) a
:
e (f a) = (f a; d a): e (f a) = (f a; d a)
e3:= moveL_M1
  (lift_factsys_tri2 factsys f c1f pr1 c2P
     (fun a : A => (f a; d a)) idmap
     (fun a : A => 1) (f a))
  (ap pr1
     (lift_factsys_tri1 factsys f c1f pr1 c2P
        (fun a : A => (f a; d a)) idmap
        (fun a : A => 1) a))
  (((ap_V pr1
       (lift_factsys_tri1 factsys f c1f pr1 c2P
          (fun a : A => (f a; d a)) idmap
          (fun a : A => 1) a))^ @@ 1) @
   lift_factsys_square factsys f c1f pr1 c2P
     (fun a : A => (f a; d a)) idmap
     (fun a : A => 1) a)
:
e2 (f a) = e1 ..1: e2 (f a) = e1 ..1
transport P (e2 (f a)) (e (f a)).2 = d a
    refine (ap (fun p => transport P p (e (f a)).2) e3 @ _).
factsys: FactorizationSystem
A, B: Type
f: A -> B
c1f: class1 factsys f
P: B -> Type
c2P: class2 factsys pr1
d: forall a : A, P (f a)
e:= lift_factsys factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): B -> {x : _ & P x}
e2:= lift_factsys_tri2 factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1): pr1
o lift_factsys factsys f c1f pr1 c2P
    (fun a : A => (f a; d a)) idmap
    (fun a : A => 1) == idmap
a: A
e1:= lift_factsys_tri1 factsys f c1f pr1 c2P
  (fun a : A => (f a; d a)) idmap 
  (fun a : A => 1) a
:
e (f a) = (f a; d a): e (f a) = (f a; d a)
e3:= moveL_M1
  (lift_factsys_tri2 factsys f c1f pr1 c2P
     (fun a : A => (f a; d a)) idmap
     (fun a : A => 1) (f a))
  (ap pr1
     (lift_factsys_tri1 factsys f c1f pr1 c2P
        (fun a : A => (f a; d a)) idmap
        (fun a : A => 1) a))
  (((ap_V pr1
       (lift_factsys_tri1 factsys f c1f pr1 c2P
          (fun a : A => (f a; d a)) idmap
          (fun a : A => 1) a))^ @@ 1) @
   lift_factsys_square factsys f c1f pr1 c2P
     (fun a : A => (f a; d a)) idmap
     (fun a : A => 1) a)
:
e2 (f a) = e1 ..1: e2 (f a) = e1 ..1
transport P e1 ..1 (e (f a)).2 = d a
    exact (pr2_path e1).
  Defined.

End FactsysExtensions.