Definition. We define struct_b_b_e_crng to be λR ⇒ struct_b_b_e R ∧ unpack_b_b_e_o R (λR plus mult zero ⇒ explicit_Rng R zero plus mult ∧ (∀x y ∈ R, mult x y = mult y x)) of type set → prop.

In Proofgold the corresponding term root is a27cd8... and object id is 72966a...

Theorem. (MetaCat_struct_b_b_e_crng)

MetaCat struct_b_b_e_crng Hom_struct_b_b_e struct_id struct_comp

In Proofgold the corresponding term root is 8ccfb9... and proposition id is 2eee93...

Proof:
Proof not loaded.

L14

Theorem. (MetaCat_struct_b_b_e_crng_Forgetful)

MetaFunctor struct_b_b_e_crng Hom_struct_b_b_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 367b3e... and proposition id is d5d286...

Proof:
Proof not loaded.

L24

Proposition. (MetaCat_struct_b_b_e_crng_initial)

∃Y : set, ∃uniqa : set → set, initial_p struct_b_b_e_crng Hom_struct_b_b_e struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is 37f6f7... and proposition id is 0e3a37...

Proof:
Proof not loaded.

L28

Proposition. (MetaCat_struct_b_b_e_crng_terminal)

∃Y : set, ∃uniqa : set → set, terminal_p struct_b_b_e_crng Hom_struct_b_b_e struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is 68df42... and proposition id is 23816c...

Proof:
Proof not loaded.

L32

Proposition. (MetaCat_struct_b_b_e_crng_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_crng Hom_struct_b_b_e struct_id struct_comp coprod i0 i1 copair

In Proofgold the corresponding term root is 98f1e6... and proposition id is 5d66b3...

Proof:
Proof not loaded.

L39

Proposition. (MetaCat_struct_b_b_e_crng_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_crng Hom_struct_b_b_e struct_id struct_comp prod pi0 pi1 pair

In Proofgold the corresponding term root is 8843e1... and proposition id is 256257...

Proof:
Proof not loaded.

L46

Proposition. (MetaCat_struct_b_b_e_crng_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_crng Hom_struct_b_b_e struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is aa6332... and proposition id is 64e778...

Proof:
Proof not loaded.

L53

Proposition. (MetaCat_struct_b_b_e_crng_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_crng Hom_struct_b_b_e struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is df3c36... and proposition id is 6b4e01...

Proof:
Proof not loaded.

L60

Proposition. (MetaCat_struct_b_b_e_crng_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_crng Hom_struct_b_b_e struct_id struct_comp po i0 i1 copair

In Proofgold the corresponding term root is 721f79... and proposition id is 406b91...

Proof:
Proof not loaded.

L68

Proposition. (MetaCat_struct_b_b_e_crng_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_crng Hom_struct_b_b_e struct_id struct_comp pb pi0 pi1 pair

In Proofgold the corresponding term root is c78a61... and proposition id is de7c82...

Proof:
Proof not loaded.

L76

Proposition. (MetaCat_struct_b_b_e_crng_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_crng Hom_struct_b_b_e struct_id struct_comp prod pi0 pi1 pair exp a lm

In Proofgold the corresponding term root is d5ef5c... and proposition id is da9ac3...

Proof:
Proof not loaded.

L86

Proposition. (MetaCat_struct_b_b_e_crng_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_crng Hom_struct_b_b_e struct_id struct_comp one uniqa Omega tru ch constr

In Proofgold the corresponding term root is ea2298... and proposition id is 60634a...

Proof:
Proof not loaded.

L94

Proposition. (MetaCat_struct_b_b_e_crng_nno)

∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_b_b_e_crng Hom_struct_b_b_e struct_id struct_comp one uniqa N zer suc rec

In Proofgold the corresponding term root is 83b532... and proposition id is dbe72a...

Proof:
Proof not loaded.

L103

Proposition. (MetaCat_struct_b_b_e_crng_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_crng Hom_struct_b_b_e struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps

In Proofgold the corresponding term root is 3918b6... and proposition id is ea9f0f...

Proof:
Proof not loaded.