Let Obj be given.
Assume HO.
We use 1 to witness the existential quantifier.
We use (λX ⇒ (λx ∈ X ⇒ 0)) to witness the existential quantifier.
We will prove Obj 1 ∧ ∀X : set, Obj X → SetHom X 1 (λx ∈ X ⇒ 0) ∧ ∀h' : set, SetHom X 1 h' → h' = (λx ∈ X ⇒ 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 X 1 (λx ∈ X ⇒ 0).
We will prove (λx ∈ X ⇒ 0) ∈ ∏x ∈ X, 1.
Apply lam_Pi to the current goal.
Let x be given.
Assume Hx: x ∈ X.
An exact proof term for the current goal is In_0_1.
Let h be given.
Assume Hh: h ∈ ∏x ∈ X, 1.
We will prove h = (λx ∈ X ⇒ 0).
Use transitivity with and (λx ∈ X ⇒ h x).
Use symmetry.
An exact proof term for the current goal is Pi_eta X (λ_ ⇒ 1) h Hh.
Apply lam_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We will prove h x = 0.
Apply SingE 0 (h x) to the current goal.
We will prove h x ∈ {0}.
rewrite the current goal using eq_1_Sing0 (from right to left).
We will prove h x ∈ 1.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ 1) h x Hh Hx.
∎