From 7dce99e1f86c2aff0d17285a36974081d6c6b2bd Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Mon, 9 Dec 2024 22:10:51 -0800
Subject: [PATCH] some category theory

---
 examples/category.pg | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/examples/category.pg b/examples/category.pg
index 87c5102..c95a458 100644
--- a/examples/category.pg
+++ b/examples/category.pg
@@ -18,6 +18,12 @@ section Category
     def initial  (A : Obj) := forall (B : Obj), exists_uniq_t (Hom A B);
     def terminal (A : Obj) := forall (B : Obj), exists_uniq_t (Hom B A);
 
+    def product (A B C : Obj) (piA : Hom C A) (piB : Hom C B) :=
+        forall (D : Obj) (f : Hom D A) (g : Hom D B),
+            exists_uniq (Hom D C) (fun (fxg : Hom D C) =>
+                and (eq (Hom D A) (comp D C A fxg piA) f)
+                    (eq (Hom D B) (comp D C B fxg piB) g));
+
     section Inverses
         variable
             (A B : Obj)
@@ -48,4 +54,19 @@ section Category
                         (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)))))))));
+
+    def terminal_uniq (A B : Obj) (hA : terminal A) (hB : terminal B) : isomorphic A B :=
+        exists_uniq_t_elim (Hom A B) (isomorphic A B) (hB A) (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) (hA B) (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