Definition. We define struct_r_partialord to be λX ⇒ struct_r Xunpack_r_o X (λX' r ⇒ (∀xX', ¬ r x x)(∀x y zX', r x yr y zr x z)) of type setprop.
Theorem. (MetaCat_struct_r_partialord)
MetaCat struct_r_partialord Hom_struct_r struct_id struct_comp
Proof:
We prove the intermediate claim L1: ∀X, struct_r_partialord Xstruct_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_partialord L1.
Theorem. (MetaCat_struct_r_partialord_Forgetful)
MetaFunctor struct_r_partialord 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)
Proof:
We prove the intermediate claim L1: ∀X, struct_r_partialord Xstruct_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_partialord L1.
Proposition. (MetaCat_struct_r_partialord_initial)
∃Y : set, ∃uniqa : setset, initial_p struct_r_partialord Hom_struct_r struct_id struct_comp Y uniqa
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_terminal)
∃Y : set, ∃uniqa : setset, terminal_p struct_r_partialord Hom_struct_r struct_id struct_comp Y uniqa
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_coproduct_constr)
∃coprod : setsetset, ∃i0 i1 : setsetset, ∃copair : setsetsetsetsetset, coproduct_constr_p struct_r_partialord Hom_struct_r struct_id struct_comp coprod i0 i1 copair
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_product_constr)
∃prod : setsetset, ∃pi0 pi1 : setsetset, ∃pair : setsetsetsetsetset, product_constr_p struct_r_partialord Hom_struct_r struct_id struct_comp prod pi0 pi1 pair
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_coequalizer_constr)
∃quot : setsetsetsetset, ∃canonmap : setsetsetsetset, ∃fac : setsetsetsetsetsetset, coequalizer_constr_p struct_r_partialord Hom_struct_r struct_id struct_comp quot canonmap fac
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_equalizer_constr)
∃quot : setsetsetsetset, ∃canonmap : setsetsetsetset, ∃fac : setsetsetsetsetsetset, equalizer_constr_p struct_r_partialord Hom_struct_r struct_id struct_comp quot canonmap fac
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_pushout_constr)
∃po : setsetsetsetsetset, ∃i0 : setsetsetsetsetset, ∃i1 : setsetsetsetsetset, ∃copair : setsetsetsetsetsetsetsetset, pushout_constr_p struct_r_partialord Hom_struct_r struct_id struct_comp po i0 i1 copair
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_pullback_constr)
∃pb : setsetsetsetsetset, ∃pi0 : setsetsetsetsetset, ∃pi1 : setsetsetsetsetset, ∃pair : setsetsetsetsetsetsetsetset, pullback_constr_p struct_r_partialord Hom_struct_r struct_id struct_comp pb pi0 pi1 pair
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_product_exponent)
∃prod : setsetset, ∃pi0 pi1 : setsetset, ∃pair : setsetsetsetsetset, ∃exp : setsetset, ∃a : setsetset, ∃lm : setsetsetsetset, product_exponent_constr_p struct_r_partialord Hom_struct_r struct_id struct_comp prod pi0 pi1 pair exp a lm
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_subobject_classifier)
∃one : set, ∃uniqa : setset, ∃Omega : set, ∃tru : set, ∃ch : setsetsetset, ∃constr : setsetsetsetsetsetset, subobject_classifier_p struct_r_partialord Hom_struct_r struct_id struct_comp one uniqa Omega tru ch constr
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_nno)
∃one : set, ∃uniqa : setset, ∃N : set, ∃zer suc : set, ∃rec : setsetsetset, nno_p struct_r_partialord Hom_struct_r struct_id struct_comp one uniqa N zer suc rec
Proof:
The rest of the proof is missing.

Proposition. (MetaCat_struct_r_partialord_left_adjoint_forgetful)
∃F0 : setset, ∃F1 : setsetsetset, ∃eta eps : setset, MetaAdjunction_strict (λ_ ⇒ True) SetHom (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_r_partialord Hom_struct_r struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps
Proof:
The rest of the proof is missing.