Definition. We define struct_u_inj to be λX ⇒ struct_u X ∧ unpack_u_o X (λX' h ⇒ inj X' X' (λx ⇒ h x)) of type set → prop.

In Proofgold the corresponding term root is b72369... and object id is c2d02a...

Theorem. (MetaCat_struct_u_inj)

MetaCat struct_u_inj Hom_struct_u struct_id struct_comp

In Proofgold the corresponding term root is a7df09... and proposition id is 6bcb57...

Proof:
Proof not loaded.

L10

Theorem. (MetaCat_struct_u_inj_Forgetful)

MetaFunctor struct_u_inj Hom_struct_u 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 d826f3... and proposition id is 1687de...

Proof:
Proof not loaded.

L20

Proposition. (MetaCat_struct_u_inj_initial)

∃Y : set, ∃uniqa : set → set, initial_p struct_u_inj Hom_struct_u struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is 8f462c... and proposition id is bdf9a2...

Proof:
Proof not loaded.

L24

Proposition. (MetaCat_struct_u_inj_terminal)

∃Y : set, ∃uniqa : set → set, terminal_p struct_u_inj Hom_struct_u struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is ff70ce... and proposition id is 883bd9...

Proof:
Proof not loaded.

L28

Proposition. (MetaCat_struct_u_inj_coproduct_constr)

∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p struct_u_inj Hom_struct_u struct_id struct_comp coprod i0 i1 copair

In Proofgold the corresponding term root is 1c7f4e... and proposition id is d74c33...

Proof:
Proof not loaded.

L35

Proposition. (MetaCat_struct_u_inj_product_constr)

∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p struct_u_inj Hom_struct_u struct_id struct_comp prod pi0 pi1 pair

In Proofgold the corresponding term root is d16054... and proposition id is 501bf4...

Proof:
Proof not loaded.

L42

Proposition. (MetaCat_struct_u_inj_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_u_inj Hom_struct_u struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is 12ca82... and proposition id is 3807d8...

Proof:
Proof not loaded.

L49

Proposition. (MetaCat_struct_u_inj_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_u_inj Hom_struct_u struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is c671ed... and proposition id is 0ba1a5...

Proof:
Proof not loaded.

L56

Proposition. (MetaCat_struct_u_inj_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_u_inj Hom_struct_u struct_id struct_comp po i0 i1 copair

In Proofgold the corresponding term root is 7ae3ec... and proposition id is abb6af...

Proof:
Proof not loaded.

L64

Proposition. (MetaCat_struct_u_inj_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_u_inj Hom_struct_u struct_id struct_comp pb pi0 pi1 pair

In Proofgold the corresponding term root is 73858b... and proposition id is 40b2c0...

Proof:
Proof not loaded.

L72

Proposition. (MetaCat_struct_u_inj_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_u_inj Hom_struct_u struct_id struct_comp prod pi0 pi1 pair exp a lm

In Proofgold the corresponding term root is 59f543... and proposition id is 02f51b...

Proof:
Proof not loaded.

L82

Proposition. (MetaCat_struct_u_inj_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_u_inj Hom_struct_u struct_id struct_comp one uniqa Omega tru ch constr

In Proofgold the corresponding term root is 67602a... and proposition id is e753ae...

Proof:
Proof not loaded.

L90

Proposition. (MetaCat_struct_u_inj_nno)

∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_u_inj Hom_struct_u struct_id struct_comp one uniqa N zer suc rec

In Proofgold the corresponding term root is 23ecf0... and proposition id is fc83dc...

Proof:
Proof not loaded.

L99

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

In Proofgold the corresponding term root is 9cef1d... and proposition id is 8822b0...

Proof:
Proof not loaded.