Require Export SET.
Require Export Single.
Require Export CatProperty.

Set Implicit Arguments.
Unset Strict Implicit.


Section set_terminal.

Variable S : Setoid.

Definition To_Single_fun (x : S) := Elt.

Lemma To_Single_map_law : Map_law To_Single_fun.
Proof.
unfold Map_law in |- ×.
intros; exact I.
Qed.

Definition To_Single := Build_Map To_Single_map_law.

End set_terminal.

Lemma Single_is_Terminal : IsTerminal To_Single.
Proof.
red in |- *; intros a f; simpl in |- *; unfold Ext in |- *; intro x; exact I.
Defined.

Definition SET_Terminal : Terminal SET := Single_is_Terminal.