+(* initial objects are unique up to iso *)
+Lemma initial_unique_up_to_iso `{C:Category}{io1:C}(i1:InitialObject C io1){io2:C}(i2:InitialObject C io2) : io1 ≅ io2.
+ refine {| iso_backward := bottom(InitialObject:=i2) io1 ; iso_forward := bottom(InitialObject:=i1) io2 |}.
+ setoid_rewrite (bottom_unique(InitialObject:=i1)); reflexivity.
+ setoid_rewrite (bottom_unique(InitialObject:=i2)); reflexivity.
+ Qed.
+
+(* terminal objects are unique up to iso *)
+Lemma terminal_unique_up_to_iso `{C:Category}{to1:C}(t1:TerminalObject C to1){to2:C}(t2:TerminalObject C to2) : to1 ≅ to2.
+ refine {| iso_backward := drop(TerminalObject:=t1) to2 ; iso_forward := drop(TerminalObject:=t2) to1 |}.
+ setoid_rewrite (drop_unique(TerminalObject:=t1)); reflexivity.
+ setoid_rewrite (drop_unique(TerminalObject:=t2)); reflexivity.
+ Qed.