diff --git a/examples/category.pg b/examples/category.pg
index 5bb5f72..87c5102 100644
--- a/examples/category.pg
+++ b/examples/category.pg
@@ -15,8 +15,8 @@ section Category
                 (comp A B D f (comp B C D 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 terminal (A : Obj) := forall (B : Obj), exists_uniq (Hom B A) (fun (f : Hom B A) => true);
+    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);
 
     section Inverses
         variable
@@ -32,6 +32,20 @@ section Category
 
     def isomorphic (A B : Obj) :=
         exists (Hom A B) (fun (f : Hom A B) =>
-            exists (Hom B A) (fun (g : Hom B A) => 
-                inv A B f g));
+            exists (Hom B A) (inv A B f));
+
+    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
diff --git a/examples/logic.pg b/examples/logic.pg
index d90a909..c549769 100644
--- a/examples/logic.pg
+++ b/examples/logic.pg
@@ -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)
             (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