Definition. We define struct_b_b_r_e_e_ordered_field to be λR ⇒ struct_b_b_r_e_eR ∧ unpack_b_b_r_e_e_oR(λR plus mult leq zero one ⇒ explicit_OrderedFieldRzerooneplusmultleq) of type set → prop.
In Proofgold the corresponding term root is 98aa98... and object id is 1de6a1...
MetaFunctorstruct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_comp(λ_ ⇒ True)SetHom(λX ⇒ lam_idX)(λX Y Z f g ⇒ (lam_compXfg))(λX ⇒ X0)(λX Y f ⇒ f)
In Proofgold the corresponding term root is 3151a0... and proposition id is e3e2f3...
∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_pstruct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_compcoprodi0i1copair
In Proofgold the corresponding term root is 4f754f... and proposition id is d2d4c3...
∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_pstruct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_compprodpi0pi1pair
In Proofgold the corresponding term root is 1b5210... and proposition id is 79bf31...
∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_pstruct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_compquotcanonmapfac
In Proofgold the corresponding term root is b2851a... and proposition id is 9d5c1a...
∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, equalizer_constr_pstruct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_compquotcanonmapfac
In Proofgold the corresponding term root is f0fafa... and proposition id is 7479e8...
∃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_pstruct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_comppoi0i1copair
In Proofgold the corresponding term root is a00d98... and proposition id is 03b598...
∃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_pstruct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_comppbpi0pi1pair
In Proofgold the corresponding term root is f9f68c... and proposition id is f53f5e...
∃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_pstruct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_compprodpi0pi1pairexpalm
In Proofgold the corresponding term root is 6e43cd... and proposition id is 6fb85e...
∃one : set, ∃uniqa : set → set, ∃Omega : set, ∃tru : set, ∃ch : set → set → set → set, ∃constr : set → set → set → set → set → set → set, subobject_classifier_pstruct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_componeuniqaOmegatruchconstr
In Proofgold the corresponding term root is d1a11f... and proposition id is 098413...
∃F0 : set → set, ∃F1 : set → set → set → set, ∃eta eps : set → set, MetaAdjunction_strict(λ_ ⇒ True)SetHom(λX ⇒ (lam_idX))(λX Y Z f g ⇒ (lam_compXfg))struct_b_b_r_e_e_ordered_fieldHom_struct_b_b_r_e_estruct_idstruct_compF0F1(λX ⇒ X0)(λX Y f ⇒ f)etaeps
In Proofgold the corresponding term root is a63581... and proposition id is 7c52e6...