Let Obj be given.

Assume HO.

We use 0 to witness the existential quantifier.

We use (λX ⇒ (λx ∈ 0 ⇒ 0)) to witness the existential quantifier.

We will prove Obj 0 ∧ ∀X : set, Obj X → SetHom 0 X (λx ∈ 0 ⇒ 0) ∧ ∀h' : set, SetHom 0 X h' → h' = (λx ∈ 0 ⇒ 0).

Apply andI to the current goal.

An exact proof term for the current goal is HO.

Let X be given.

Assume HX.

Apply andI to the current goal.

We will prove SetHom 0 X (λx ∈ 0 ⇒ 0).

We will prove (λx ∈ 0 ⇒ 0) ∈ ∏x ∈ 0, X.

Apply lam_Pi to the current goal.

Let x be given.

Assume Hx: x ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE x Hx.

Let h be given.

Assume Hh: h ∈ ∏x ∈ 0, X.

We will prove h = (λx ∈ 0 ⇒ 0).

Use transitivity with and (λx ∈ 0 ⇒ h x).

Use symmetry.

An exact proof term for the current goal is Pi_eta 0 (λ_ ⇒ X) h Hh.

Apply lam_ext to the current goal.

Let x be given.

Assume Hx: x ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE x Hx.

∎