Proof that sets with fixed-point operators is closed under binary products.

FPO_products.v

Definition FPO{X}(Y : (X -> X) -> X) :=
  forall f, f (Y f) = Y f.

Section FPOs.

Variables A B : Type.
Variable Y_A : (A -> A) -> A.
Variable Y_B : (B -> B) -> B.

Hypothesis Y_A_FPO : FPO Y_A.
Hypothesis Y_B_FPO : FPO Y_B.

Definition prod_FPO : (A * B -> A * B) -> A * B :=
  fun f =>
    let g : A -> B :=
      fun a => Y_B (fun b => snd (f (a,b))) in
    let h : A -> A :=
      fun a => fst (f (a, g a)) in
    let a : A := Y_A h in
      (a, g a).

Lemma prod_FPO_correct : FPO prod_FPO.
Proof.
  intro f.
  apply injective_projections.
  - unfold prod_FPO at 2; simpl.
    rewrite <- Y_A_FPO.
    reflexivity.
  - unfold prod_FPO at 2; simpl.
    rewrite <- Y_B_FPO.
    reflexivity.
Qed.