Definition. We define struct_b_b_e_e_semiring to be λR ⇒ struct_b_b_e_e R ∧ unpack_b_b_e_e_o R (λR plus mult zero one ⇒ (∀x y z ∈ R, plus (plus x y) z = plus x (plus y z)) ∧ (∀x y ∈ R, plus x y = plus y x) ∧ (∀x ∈ R, plus x zero = x) ∧ (∀x y z ∈ R, mult (mult x y) z = mult x (mult y z)) ∧ (∀x ∈ R, mult x one = x ∧ mult one x = x) ∧ (∀x y z ∈ R, mult x (plus y z) = plus (mult x y) (mult x z)) ∧ (∀x y z ∈ R, mult (plus x y) z = plus (mult x z) (mult y z)) ∧ (∀x ∈ R, mult x zero = zero) ∧ (∀x ∈ R, mult zero x = zero)) of type set → prop.

In Proofgold the corresponding term root is bde844... and object id is 5b4ddd...

L15

Theorem. (MetaCat_struct_b_b_e_e_semiring)

MetaCat struct_b_b_e_e_semiring Hom_struct_b_b_e_e struct_id struct_comp

In Proofgold the corresponding term root is 847b73... and proposition id is 37e9ff...

Proof:
Proof not loaded.

L21

Theorem. (MetaCat_struct_b_b_e_e_semiring_Forgetful)

MetaFunctor struct_b_b_e_e_semiring 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 2b3fcd... and proposition id is f402bf...

Proof:
Proof not loaded.

L31

Proposition. (MetaCat_struct_b_b_e_e_semiring_initial)

∃Y : set, ∃uniqa : set → set, initial_p struct_b_b_e_e_semiring Hom_struct_b_b_e_e struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is d09938... and proposition id is 869d4a...

Proof:
Proof not loaded.

L35

Proposition. (MetaCat_struct_b_b_e_e_semiring_terminal)

∃Y : set, ∃uniqa : set → set, terminal_p struct_b_b_e_e_semiring Hom_struct_b_b_e_e struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is 372152... and proposition id is 674c6b...

Proof:
Proof not loaded.

L39

Proposition. (MetaCat_struct_b_b_e_e_semiring_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_semiring Hom_struct_b_b_e_e struct_id struct_comp coprod i0 i1 copair

In Proofgold the corresponding term root is b06d26... and proposition id is 8d77da...

Proof:
Proof not loaded.

L46

Proposition. (MetaCat_struct_b_b_e_e_semiring_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_semiring Hom_struct_b_b_e_e struct_id struct_comp prod pi0 pi1 pair

In Proofgold the corresponding term root is 242a90... and proposition id is 56fbd7...

Proof:
Proof not loaded.

L53

Proposition. (MetaCat_struct_b_b_e_e_semiring_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_semiring Hom_struct_b_b_e_e struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is da036b... and proposition id is 21d064...

Proof:
Proof not loaded.

L60

Proposition. (MetaCat_struct_b_b_e_e_semiring_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_semiring Hom_struct_b_b_e_e struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is 31c95e... and proposition id is dca6f7...

Proof:
Proof not loaded.

L67

Proposition. (MetaCat_struct_b_b_e_e_semiring_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_semiring Hom_struct_b_b_e_e struct_id struct_comp po i0 i1 copair

In Proofgold the corresponding term root is 3167f8... and proposition id is 9b9a38...

Proof:
Proof not loaded.

L75

Proposition. (MetaCat_struct_b_b_e_e_semiring_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_semiring Hom_struct_b_b_e_e struct_id struct_comp pb pi0 pi1 pair

In Proofgold the corresponding term root is 513a36... and proposition id is e6262e...

Proof:
Proof not loaded.

L83

Proposition. (MetaCat_struct_b_b_e_e_semiring_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_semiring Hom_struct_b_b_e_e struct_id struct_comp prod pi0 pi1 pair exp a lm

In Proofgold the corresponding term root is b2ca42... and proposition id is 6b4675...

Proof:
Proof not loaded.

L93

Proposition. (MetaCat_struct_b_b_e_e_semiring_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_semiring Hom_struct_b_b_e_e struct_id struct_comp one uniqa Omega tru ch constr

In Proofgold the corresponding term root is fc2754... and proposition id is 419d29...

Proof:
Proof not loaded.

L101

Proposition. (MetaCat_struct_b_b_e_e_semiring_nno)

∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_b_b_e_e_semiring Hom_struct_b_b_e_e struct_id struct_comp one uniqa N zer suc rec

In Proofgold the corresponding term root is 550304... and proposition id is 5669f1...

Proof:
Proof not loaded.

L110

Proposition. (MetaCat_struct_b_b_e_e_semiring_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_semiring 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 8e575a... and proposition id is 29f18b...

Proof:
Proof not loaded.