Theorem. (MetaCat_struct_b_b_e_e_cring)

MetaCat CRing Hom_struct_b_b_e_e struct_id struct_comp

In Proofgold the corresponding term root is ca4007... and proposition id is f41f4d...

Proof:

We prove the intermediate claim L1: ∀X, CRing X → struct_b_b_e_e 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_b_b_e_e_gen CRing L1.

∎

Theorem. (MetaCat_struct_b_b_e_e_cring_Forgetful)

MetaFunctor CRing 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 e3fd93... and proposition id is 5aa862...

Proof:

We prove the intermediate claim L1: ∀X, CRing X → struct_b_b_e_e 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_b_b_e_e_Forgetful_gen CRing L1.

∎

Proposition. (MetaCat_struct_b_b_e_e_cring_initial)

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

In Proofgold the corresponding term root is 339087... and proposition id is e9603a...

Proof:

The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_cring_terminal)

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

In Proofgold the corresponding term root is 4286c0... and proposition id is 323c3c...

Proof:

The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_cring_coproduct_constr)

∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p CRing Hom_struct_b_b_e_e struct_id struct_comp coprod i0 i1 copair

In Proofgold the corresponding term root is 800c7b... and proposition id is c63e16...

Proof:

The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_cring_product_constr)

∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p CRing Hom_struct_b_b_e_e struct_id struct_comp prod pi0 pi1 pair

In Proofgold the corresponding term root is 15e72e... and proposition id is 82d73b...

Proof:

The rest of the proof is missing.

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

In Proofgold the corresponding term root is 2b3958... and proposition id is a936dd...

Proof:

The rest of the proof is missing.

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

In Proofgold the corresponding term root is fee504... and proposition id is 764c08...

Proof:

The rest of the proof is missing.

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

In Proofgold the corresponding term root is eddad9... and proposition id is affbb3...

Proof:

The rest of the proof is missing.

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

In Proofgold the corresponding term root is 231194... and proposition id is 06b407...

Proof:

The rest of the proof is missing.

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

In Proofgold the corresponding term root is e9b3fd... and proposition id is 67a9fa...

Proof:

The rest of the proof is missing.

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

In Proofgold the corresponding term root is 98a8d5... and proposition id is ef408a...

Proof:

The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_cring_nno)

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

In Proofgold the corresponding term root is 03d4c4... and proposition id is f54cc0...

Proof:

The rest of the proof is missing.

Proposition. (MetaCat_struct_b_b_e_e_cring_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)) CRing 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 3379e3... and proposition id is c7343a...

Proof:

The rest of the proof is missing.