Definition. We define struct_b_loop to be λX ⇒ struct_b X ∧ unpack_b_o X (λX' op ⇒ (∃e ∈ X', ∀x ∈ X', op x e = x ∧ op e x = x) ∧ (∀a ∈ X', bij X' X' (λx ⇒ op a x)) ∧ (∀a ∈ X', bij X' X' (λx ⇒ op x a))) of type set → prop.

In Proofgold the corresponding term root is 10b147... and object id is 6e587c...

Theorem. (MetaCat_struct_b_loop)

MetaCat struct_b_loop Hom_struct_b struct_id struct_comp

In Proofgold the corresponding term root is 0638c3... and proposition id is 8207e8...

Proof:
Proof not loaded.

L15

Theorem. (MetaCat_struct_b_loop_Forgetful)

MetaFunctor struct_b_loop Hom_struct_b 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 1a2bfe... and proposition id is dcd560...

Proof:
Proof not loaded.

L25

Proposition. (MetaCat_struct_b_loop_initial)

∃Y : set, ∃uniqa : set → set, initial_p struct_b_loop Hom_struct_b struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is 2f83cb... and proposition id is b2b2f7...

Proof:
Proof not loaded.

L29

Proposition. (MetaCat_struct_b_loop_terminal)

∃Y : set, ∃uniqa : set → set, terminal_p struct_b_loop Hom_struct_b struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is 7e7e14... and proposition id is 7fbafe...

Proof:
Proof not loaded.

L33

Proposition. (MetaCat_struct_b_loop_coproduct_constr)

∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p struct_b_loop Hom_struct_b struct_id struct_comp coprod i0 i1 copair

In Proofgold the corresponding term root is a6f455... and proposition id is 702de0...

Proof:
Proof not loaded.

L40

Proposition. (MetaCat_struct_b_loop_product_constr)

∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p struct_b_loop Hom_struct_b struct_id struct_comp prod pi0 pi1 pair

In Proofgold the corresponding term root is 8a471b... and proposition id is 6133c4...

Proof:
Proof not loaded.

L47

Proposition. (MetaCat_struct_b_loop_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_loop Hom_struct_b struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is 5ccdcc... and proposition id is 8f14a6...

Proof:
Proof not loaded.

L54

Proposition. (MetaCat_struct_b_loop_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_loop Hom_struct_b struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is 506ac0... and proposition id is f1b36d...

Proof:
Proof not loaded.

L61

Proposition. (MetaCat_struct_b_loop_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_loop Hom_struct_b struct_id struct_comp po i0 i1 copair

In Proofgold the corresponding term root is e40161... and proposition id is 8bacb1...

Proof:
Proof not loaded.

L69

Proposition. (MetaCat_struct_b_loop_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_loop Hom_struct_b struct_id struct_comp pb pi0 pi1 pair

In Proofgold the corresponding term root is 995f89... and proposition id is 2614cb...

Proof:
Proof not loaded.

L77

Proposition. (MetaCat_struct_b_loop_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_loop Hom_struct_b struct_id struct_comp prod pi0 pi1 pair exp a lm

In Proofgold the corresponding term root is 48cc55... and proposition id is 6aef94...

Proof:
Proof not loaded.

L87

Proposition. (MetaCat_struct_b_loop_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_loop Hom_struct_b struct_id struct_comp one uniqa Omega tru ch constr

In Proofgold the corresponding term root is ae76b1... and proposition id is 6f86d4...

Proof:
Proof not loaded.

L95

Proposition. (MetaCat_struct_b_loop_nno)

∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_b_loop Hom_struct_b struct_id struct_comp one uniqa N zer suc rec

In Proofgold the corresponding term root is f70b1c... and proposition id is 26e9f7...

Proof:
Proof not loaded.

L104

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

In Proofgold the corresponding term root is f75c12... and proposition id is 39e48e...

Proof:
Proof not loaded.