Definition. We define struct_p_nonempty to be λX ⇒ struct_p X ∧ unpack_p_o X (λX' p ⇒ ∃x ∈ X', p x) of type set → prop.
In Proofgold the corresponding term root is 8ef0c9... and object id is 00081f...
Theorem. (MetaCat_struct_p_nonempty)
MetaCat struct_p_nonempty Hom_struct_p struct_id struct_comp
In Proofgold the corresponding term root is f74def... and proposition id is aef2e9...
Proof:
We prove the intermediate claim L1: ∀X, struct_p_nonempty X → struct_p X.
Let X be given.
Assume HX.
Apply HX to the current goal.
Assume H _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is MetaCat_struct_p_gen struct_p_nonempty L1.
∎
Theorem. (MetaCat_struct_p_nonempty_Forgetful)
MetaFunctor struct_p_nonempty Hom_struct_p struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)
In Proofgold the corresponding term root is 996d2c... and proposition id is 0322a2...
Proof:
We prove the intermediate claim L1: ∀X, struct_p_nonempty X → struct_p X.
Let X be given.
Assume HX.
Apply HX to the current goal.
Assume H _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is MetaCat_struct_p_Forgetful_gen struct_p_nonempty L1.
∎
Proposition. (MetaCat_struct_p_nonempty_initial)
∃Y : set, ∃uniqa : set → set, initial_p struct_p_nonempty Hom_struct_p struct_id struct_comp Y uniqa
In Proofgold the corresponding term root is 343f3e... and proposition id is da2c17...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_terminal)
∃Y : set, ∃uniqa : set → set, terminal_p struct_p_nonempty Hom_struct_p struct_id struct_comp Y uniqa
In Proofgold the corresponding term root is a3d382... and proposition id is 128d6c...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_coproduct_constr)
∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p struct_p_nonempty Hom_struct_p struct_id struct_comp coprod i0 i1 copair
In Proofgold the corresponding term root is dc308e... and proposition id is 0e8077...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_product_constr)
∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p struct_p_nonempty Hom_struct_p struct_id struct_comp prod pi0 pi1 pair
In Proofgold the corresponding term root is 27a094... and proposition id is 456586...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_coequalizer_constr)
∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_p struct_p_nonempty Hom_struct_p struct_id struct_comp quot canonmap fac
In Proofgold the corresponding term root is 05e388... and proposition id is 5f5ea3...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_equalizer_constr)
∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, equalizer_constr_p struct_p_nonempty Hom_struct_p struct_id struct_comp quot canonmap fac
In Proofgold the corresponding term root is 6e85da... and proposition id is e3112c...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_pushout_constr)
∃po : set → set → set → set → set → set, ∃i0 : set → set → set → set → set → set, ∃i1 : set → set → set → set → set → set, ∃copair : set → set → set → set → set → set → set → set → set, pushout_constr_p struct_p_nonempty Hom_struct_p struct_id struct_comp po i0 i1 copair
In Proofgold the corresponding term root is f9e1f6... and proposition id is 77ee96...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_pullback_constr)
∃pb : set → set → set → set → set → set, ∃pi0 : set → set → set → set → set → set, ∃pi1 : set → set → set → set → set → set, ∃pair : set → set → set → set → set → set → set → set → set, pullback_constr_p struct_p_nonempty Hom_struct_p struct_id struct_comp pb pi0 pi1 pair
In Proofgold the corresponding term root is 36c11b... and proposition id is ebc637...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_product_exponent)
∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, ∃exp : set → set → set, ∃a : set → set → set, ∃lm : set → set → set → set → set, product_exponent_constr_p struct_p_nonempty Hom_struct_p struct_id struct_comp prod pi0 pi1 pair exp a lm
In Proofgold the corresponding term root is 9bd4d5... and proposition id is e25fa0...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_subobject_classifier)
∃one : set, ∃uniqa : set → set, ∃Omega : set, ∃tru : set, ∃ch : set → set → set → set, ∃constr : set → set → set → set → set → set → set, subobject_classifier_p struct_p_nonempty Hom_struct_p struct_id struct_comp one uniqa Omega tru ch constr
In Proofgold the corresponding term root is ed4e1f... and proposition id is 7aaf37...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_nno)
∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_p_nonempty Hom_struct_p struct_id struct_comp one uniqa N zer suc rec
In Proofgold the corresponding term root is 8dadcf... and proposition id is b8863f...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_p_nonempty_left_adjoint_forgetful)
∃F0 : set → set, ∃F1 : set → set → set → set, ∃eta eps : set → set, MetaAdjunction_strict (λ_ ⇒ True) SetHom (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_p_nonempty Hom_struct_p struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps
In Proofgold the corresponding term root is ee112f... and proposition id is 57ed90...
Proof:
The rest of the proof is missing.

Proposition. (MetaFunctor_struct_e_struct_p_nonempty)
MetaFunctor struct_e Hom_struct_e (λX ⇒ (lam_id (X 0))) (λX Y Z f g ⇒ (lam_comp (X 0) f g)) struct_p_nonempty Hom_struct_p (λX ⇒ (lam_id (X 0))) (λX Y Z f g ⇒ (lam_comp (X 0) f g)) (λX ⇒ unpack_e_i X (λX' e ⇒ pack_p X' (λx ⇒ x = e))) (λX Y f ⇒ f)
In Proofgold the corresponding term root is f195ff... and proposition id is 1f2a9b...
Proof:
The rest of the proof is missing.