Definition. We define struct_r_wellord to be λX ⇒ struct_r X ∧ unpack_r_o X (λX' r ⇒ (∀x ∈ X', ¬ r x x) ∧ (∀x y ∈ X', r x y ∨ r y x) ∧ (∀x y z ∈ X', r x y → r y z → r x z) ∧ (∀p : set → prop, (∀y ∈ X', (∀x ∈ X', r x y → p x) → p y) → ∀x ∈ X', p x)) of type set → prop.
In Proofgold the corresponding term root is db327c... and object id is 8b17e8...
Theorem. (MetaCat_struct_r_wellord)
MetaCat struct_r_wellord Hom_struct_r struct_id struct_comp
In Proofgold the corresponding term root is 376093... and proposition id is 85435c...
Proof:
We prove the intermediate claim L1: ∀X, struct_r_wellord X → struct_r 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_r_gen struct_r_wellord L1.
∎
Theorem. (MetaCat_struct_r_wellord_Forgetful)
MetaFunctor struct_r_wellord Hom_struct_r 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 716408... and proposition id is 3315e0...
Proof:
We prove the intermediate claim L1: ∀X, struct_r_wellord X → struct_r 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_r_Forgetful_gen struct_r_wellord L1.
∎
Proposition. (MetaCat_struct_r_wellord_initial)
∃Y : set, ∃uniqa : set → set, initial_p struct_r_wellord Hom_struct_r struct_id struct_comp Y uniqa
In Proofgold the corresponding term root is 6b40b8... and proposition id is 105ddf...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_terminal)
∃Y : set, ∃uniqa : set → set, terminal_p struct_r_wellord Hom_struct_r struct_id struct_comp Y uniqa
In Proofgold the corresponding term root is 7e8842... and proposition id is 497636...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_coproduct_constr)
∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p struct_r_wellord Hom_struct_r struct_id struct_comp coprod i0 i1 copair
In Proofgold the corresponding term root is 70ffe1... and proposition id is 174587...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_product_constr)
∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p struct_r_wellord Hom_struct_r struct_id struct_comp prod pi0 pi1 pair
In Proofgold the corresponding term root is 088808... and proposition id is 71d592...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_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_r_wellord Hom_struct_r struct_id struct_comp quot canonmap fac
In Proofgold the corresponding term root is 3692d7... and proposition id is 10b922...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_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_r_wellord Hom_struct_r struct_id struct_comp quot canonmap fac
In Proofgold the corresponding term root is 1016d0... and proposition id is d27a86...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_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_r_wellord Hom_struct_r struct_id struct_comp po i0 i1 copair
In Proofgold the corresponding term root is c1d3de... and proposition id is d4e5cd...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_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_r_wellord Hom_struct_r struct_id struct_comp pb pi0 pi1 pair
In Proofgold the corresponding term root is fced61... and proposition id is ee3b38...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_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_r_wellord Hom_struct_r struct_id struct_comp prod pi0 pi1 pair exp a lm
In Proofgold the corresponding term root is 44f225... and proposition id is 9460db...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_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_r_wellord Hom_struct_r struct_id struct_comp one uniqa Omega tru ch constr
In Proofgold the corresponding term root is 7fa73e... and proposition id is d2cf43...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_nno)
∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_r_wellord Hom_struct_r struct_id struct_comp one uniqa N zer suc rec
In Proofgold the corresponding term root is 75815b... and proposition id is d6d09e...
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_wellord_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_r_wellord Hom_struct_r struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps
In Proofgold the corresponding term root is 7d926b... and proposition id is 538f6b...
Proof:
The rest of the proof is missing.