Lawvere's fixed-point theorem formalized in Coq with ConCaT

LawvereFixedPointTheorem.v

(*
Lawvere's fixed point theorem.

References:
F. W. Lawvere and S. H. Schanuel, Conceptual Mathematics: A First Introduction to Categories.
Cambridge University Press, Nov. 1997.
*)

Require Export Category.
Require Export CCC.
Require Export CatProperty.
Set Implicit Arguments.
Unset Strict Implicit.

Section lawvere.

Variable (C : Category).
Variable (C1 : IsCartesian C).
Variable (Y : C).

Definition FixedPointProperty :=
  forall alpha : Y --> Y,
    exists y : Terminal_ob C1 --> Y,
      y o alpha =_S y.

Variable (T : C).
Variable (f : (H_obj_prod C1 T T) --> Y).

Let delta (X : C) : X --> H_obj_prod C1 X X
  := H_together C1 (Id X) (Id X).

Lemma lem1 :
  forall (X Y1 Y2 Z1 Z2 : C) (f1 : X --> Y1) (f2 : X --> Y2) (g1 : Y1 --> Z1) (g2 : Y2 --> Z2),
    H_together C1 f1 f2 o (Mor_prod C1 g1 g2) =_S
    H_together C1 (f1 o g1) (f2 o g2).
intros.
unfold Mor_prod.
apply Trans with
(H_together C1
  (H_together C1 f1 f2 o H_proj1_prod C1 Y1 Y2 o g1)
  (H_together C1 f1 f2 o H_proj2_prod C1 Y1 Y2 o g2)
).
apply Eq3_prod.
apply Prf_map2_cong.

apply Trans with ((H_together C1 f1 f2 o H_proj1_prod C1 Y1 Y2) o g1).
apply Ass.
apply Comp_r.
apply Prf_eq1_prod.

apply Trans with ((H_together C1 f1 f2 o H_proj2_prod C1 Y1 Y2) o g2).
apply Ass.
apply Comp_r.
apply Prf_eq2_prod.

Qed.

Lemma lem2 : forall (p q : Terminal_ob C1 --> Terminal_ob C1), p =_S q.
intros.
apply Trans with (MorT C1 (Terminal_ob C1)).
apply Prf_isTerminal.
apply Sym.
apply Prf_isTerminal.
Qed.

Lemma lem3 :
  forall (A : C) (p : Terminal_ob C1 --> A),
    p o delta A =_S p o delta A o (Mor_prod C1 (MorT C1 A o p) (Id A)).
intros.
unfold delta.
apply Sym.

apply Trans with (p o H_together C1 (Id A o MorT C1 A o p) (Id A o Id A)).
apply Comp_l.
apply lem1.

apply Trans with (H_together C1 (p o Id A o MorT C1 A o p) (p o Id A o Id A)).
apply Eq3_prod.

apply Trans with (H_together C1 (p o Id A) (p o Id A)).
apply Prf_map2_cong.

apply Trans with ((p o Id A) o MorT C1 A o p).
apply Ass.
apply Trans with (((p o Id A) o MorT C1 A) o p).
apply Ass.
apply Trans with (Id (Terminal_ob C1) o p).
apply Comp_r.
apply lem2.

apply Trans with p.
apply Prf_idl.
apply Prf_idr.

apply Comp_l.
apply Prf_idl.

apply Sym.
apply Eq3_prod.
Qed.

Variable (H : forall (g : T --> Y),
              exists p : Terminal_ob C1 --> T,
              g =_S delta T o Mor_prod C1 (MorT C1 T o p) (Id T) o f).

Theorem FixedPointTheorem : FixedPointProperty.
intro.

set (g := delta T o f o alpha).
destruct (H g).
set (p := x).
set (y := p o g).
exists y.
apply Sym.

apply Trans with ((x o delta T) o f o alpha).
apply Ass.

apply Trans with (((x o delta T) o f) o alpha).
apply Ass.

apply Comp_r.

apply Trans with ((x o (delta T o (Mor_prod C1 (MorT C1 T o x) (Id T)))) o f).
apply Comp_r.
apply lem3.

apply Trans with (x o ((delta T o (Mor_prod C1 (MorT C1 T o x) (Id T))) o f)).
apply Ass1.

apply Trans with (x o delta T o Mor_prod C1 (MorT C1 T o x) (Id T) o f).
apply Comp_l.
apply Ass1.

apply Trans with (x o g).
apply Comp_l.
apply Sym.
apply H0.

apply Refl.

Qed.

End lawvere.