Definition. We define struct_r_graph to be λX ⇒ struct_r X ∧ unpack_r_o X (λX' r ⇒ (∀x ∈ X', ¬ r x x) ∧ (∀x y ∈ X', r x y → r y x)) of type set → prop.

In Proofgold the corresponding term root is fa6fca... and object id is 15e29f...

Theorem. (MetaCat_struct_r_graph)

MetaCat struct_r_graph Hom_struct_r struct_id struct_comp

In Proofgold the corresponding term root is 53ea81... and proposition id is 716750...

Proof:
Proof not loaded.

L11

Theorem. (MetaCat_struct_r_graph_Forgetful)

MetaFunctor struct_r_graph Hom_struct_r 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 6c92db... and proposition id is 1299d5...

Proof:
Proof not loaded.

L21

Proposition. (MetaCat_struct_r_graph_initial)

∃Y : set, ∃uniqa : set → set, initial_p struct_r_graph Hom_struct_r struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is bedfac... and proposition id is fc401a...

Proof:
Proof not loaded.

L25

Proposition. (MetaCat_struct_r_graph_terminal)

∃Y : set, ∃uniqa : set → set, terminal_p struct_r_graph Hom_struct_r struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is 1689f2... and proposition id is 891694...

Proof:
Proof not loaded.

L29

Proposition. (MetaCat_struct_r_graph_coproduct_constr)

∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p struct_r_graph Hom_struct_r struct_id struct_comp coprod i0 i1 copair

In Proofgold the corresponding term root is ae33e3... and proposition id is ad517c...

Proof:
Proof not loaded.

L36

Proposition. (MetaCat_struct_r_graph_product_constr)

∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p struct_r_graph Hom_struct_r struct_id struct_comp prod pi0 pi1 pair

In Proofgold the corresponding term root is 3c8643... and proposition id is 709ef9...

Proof:
Proof not loaded.

L43

Proposition. (MetaCat_struct_r_graph_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_r_graph Hom_struct_r struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is 31b820... and proposition id is f97121...

Proof:
Proof not loaded.

L50

Proposition. (MetaCat_struct_r_graph_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_r_graph Hom_struct_r struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is df7a79... and proposition id is 06b274...

Proof:
Proof not loaded.

L57

Proposition. (MetaCat_struct_r_graph_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_r_graph Hom_struct_r struct_id struct_comp po i0 i1 copair

In Proofgold the corresponding term root is 5a5e55... and proposition id is 4a76cf...

Proof:
Proof not loaded.

L65

Proposition. (MetaCat_struct_r_graph_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_r_graph Hom_struct_r struct_id struct_comp pb pi0 pi1 pair

In Proofgold the corresponding term root is ace795... and proposition id is c2d12c...

Proof:
Proof not loaded.

L73

Proposition. (MetaCat_struct_r_graph_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_r_graph Hom_struct_r struct_id struct_comp prod pi0 pi1 pair exp a lm

In Proofgold the corresponding term root is 42c34c... and proposition id is 90b913...

Proof:
Proof not loaded.

L83

Proposition. (MetaCat_struct_r_graph_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_r_graph Hom_struct_r struct_id struct_comp one uniqa Omega tru ch constr

In Proofgold the corresponding term root is cfd776... and proposition id is 3aa348...

Proof:
Proof not loaded.

L91

Proposition. (MetaCat_struct_r_graph_nno)

∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_r_graph Hom_struct_r struct_id struct_comp one uniqa N zer suc rec

In Proofgold the corresponding term root is f251af... and proposition id is 318861...

Proof:
Proof not loaded.

L100

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

In Proofgold the corresponding term root is 682a6e... and proposition id is 1e88dd...

Proof:
Proof not loaded.