Theorem. (MetaCat_struct_b_b_e_e)
MetaCat struct_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp
In Proofgold the corresponding term root is feeda8... and proposition id is e84d1b...
Proof:
An exact proof term for the current goal is MetaCat_struct_b_b_e_e_gen struct_b_b_e_e (λX H ⇒ H).
∎
Theorem. (MetaCat_struct_b_b_e_e_Forgetful)
MetaFunctor struct_b_b_e_e Hom_struct_b_b_e_e 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 d90dfc... and proposition id is 4b8c93...
Proof:
An exact proof term for the current goal is MetaCat_struct_b_b_e_e_Forgetful_gen struct_b_b_e_e (λX H ⇒ H).
∎
Proposition. (MetaCat_struct_b_b_e_e_initial)
∃Y : set, ∃uniqa : set → set, initial_p struct_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp Y uniqa
In Proofgold the corresponding term root is 1b00bc... and proposition id is 5cc29e...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_terminal)
∃Y : set, ∃uniqa : set → set, terminal_p struct_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp Y uniqa
In Proofgold the corresponding term root is e0d305... and proposition id is c846f4...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_coproduct_constr)
∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p struct_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp coprod i0 i1 copair
In Proofgold the corresponding term root is 36a25f... and proposition id is 0ab384...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_product_constr)
∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p struct_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp prod pi0 pi1 pair
In Proofgold the corresponding term root is 7a5745... and proposition id is ff8c0a...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_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_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp quot canonmap fac
In Proofgold the corresponding term root is 818ffc... and proposition id is a554cb...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_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_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp quot canonmap fac
In Proofgold the corresponding term root is 0d0281... and proposition id is 916c63...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_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_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp po i0 i1 copair
In Proofgold the corresponding term root is 07b9c5... and proposition id is 8696cc...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_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_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp pb pi0 pi1 pair
In Proofgold the corresponding term root is b090c4... and proposition id is b4381a...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_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_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp prod pi0 pi1 pair exp a lm
In Proofgold the corresponding term root is ca454c... and proposition id is 51d9f2...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_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_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp one uniqa Omega tru ch constr
In Proofgold the corresponding term root is 6df71a... and proposition id is 7af869...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_nno)
∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp one uniqa N zer suc rec
In Proofgold the corresponding term root is 3185a7... and proposition id is 9b2325...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_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_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps
In Proofgold the corresponding term root is 6a0b84... and proposition id is a33bd1...
Proof:
The rest of the proof is missing.