Created
August 13, 2011 16:31
-
-
Save msakai/1144008 to your computer and use it in GitHub Desktop.
Lawvere's fixed-point theorem formalized in Coq with ConCaT
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment