wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

proved initial objects unique

Browse source
This commit is contained in:
William Ball 2024-12-08 20:17:34 -08:00
parent fbfd8891bb
commit 6f34793ba2
2 changed files with 24 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
examples/category.pg
View file

@ -15,8 +15,8 @@ section Category
(comp A B D f (comp B C D g h)) (comp A B D f (comp B C D g h))
(comp A C D (comp A B C f g) h)); (comp A C D (comp A B C f g) h));
def initial (A : Obj) := forall (B : Obj), exists_uniq (Hom A B) (fun (f : Hom A B) => true); def initial (A : Obj) := forall (B : Obj), exists_uniq_t (Hom A B);
def terminal (A : Obj) := forall (B : Obj), exists_uniq (Hom B A) (fun (f : Hom B A) => true); def terminal (A : Obj) := forall (B : Obj), exists_uniq_t (Hom B A);
section Inverses section Inverses
variable variable
@ -32,6 +32,20 @@ section Category
def isomorphic (A B : Obj) := def isomorphic (A B : Obj) :=
exists (Hom A B) (fun (f : Hom A B) => exists (Hom A B) (fun (f : Hom A B) =>
exists (Hom B A) (fun (g : Hom B A) => exists (Hom B A) (inv A B f));
inv A B f g));
def initial_uniq (A B : Obj) (hA : initial A) (hB : initial B) : isomorphic A B :=
exists_uniq_t_elim (Hom A B) (isomorphic A B) (hA B) (fun (f : Hom A B) (f_uniq : forall (y : Hom A B), eq (Hom A B) f y) =>
exists_uniq_t_elim (Hom B A) (isomorphic A B) (hB A) (fun (g : Hom B A) (g_uniq : forall (y : Hom B A), eq (Hom B A) g y) =>
exists_uniq_t_elim (Hom A A) (isomorphic A B) (hA A) (fun (a : Hom A A) (a_uniq : forall (y : Hom A A), eq (Hom A A) a y) =>
exists_uniq_t_elim (Hom B B) (isomorphic A B) (hB B) (fun (b : Hom B B) (b_uniq : forall (y : Hom B B), eq (Hom B B) b y) =>
exists_intro (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (inv A B f)) f
(exists_intro (Hom B A) (inv A B f) g
(and_intro (inv_l A B f g) (inv_r A B f g)
(eq_trans (Hom A A) (comp A B A f g) a (id A)
(eq_sym (Hom A A) a (comp A B A f g) (a_uniq (comp A B A f g)))
(a_uniq (id A)))
(eq_trans (Hom B B) (comp B A B g f) b (id B)
(eq_sym (Hom B B) b (comp B A B g f) (b_uniq (comp B A B g f)))
(b_uniq (id B)))))))));
end Category end Category

6
examples/logic.pg
View file

@ -131,6 +131,12 @@ def exists_uniq_elim (A B : *) (P : A -> *) (ex_a : exists_uniq A P) (h : forall
h a (and_elim_l (P a) (forall (y : A), P y -> eq A a y) h2) h a (and_elim_l (P a) (forall (y : A), P y -> eq A a y) h2)
(and_elim_r (P a) (forall (y : A), P y -> eq A a y) h2)); (and_elim_r (P a) (forall (y : A), P y -> eq A a y) h2));
def exists_uniq_t (A : *) : * :=
exists A (fun (x : A) => forall (y : A), eq A x y);
def exists_uniq_t_elim (A B : *) (ex_a : exists_uniq_t A) (h : forall (a : A), (forall (y : A), eq A a y) -> B) : B :=
exists_elim A B (fun (x : A) => forall (y : A), eq A x y) ex_a (fun (a : A) (h2 : forall (y : A), eq A a y) => h a h2);
-- -------------------------------------------------------------------------------------------------------------- -- --------------------------------------------------------------------------------------------------------------
-- Some logic theorems -- Some logic theorems