Proofgold Address

Param lam_id^lam_id : ι → ι
Param ap^ap : ι → ι → ι
Definition struct_id^struct_id := λ x0 . lam_id (ap x0 0)
Param lam_comp^lam_comp : ι → ι → ι → ι
Definition struct_comp^struct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param struct_r^struct_r : ι → ο
Param unpack_r_o^unpack_r_o : ι → (ι → (ι → ι → ο) → ο) → ο
Param not^not : ο → ο
Param or^or : ο → ο → ο
Definition 8b17e..^{struct_r_wellord} := λ x0 . and (struct_r x0) (unpack_r_o x0 (λ x1 . λ x2 : ι → ι → ο . and (and (and (∀ x3 . x3 ∈ x1 ⟶ not (x2 x3 x3)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ or (x2 x3 x4) (x2 x4 x3))) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x5 ⟶ x2 x3 x5)) (∀ x3 : ι → ο . (∀ x4 . x4 ∈ x1 ⟶ (∀ x5 . x5 ∈ x1 ⟶ x2 x5 x4 ⟶ x3 x5) ⟶ x3 x4) ⟶ ∀ x4 . x4 ∈ x1 ⟶ x3 x4)))
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Param BinRelnHom^Hom_struct_r : ι → ι → ι → ο
Known 62658..^{MetaCat_struct_r_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_r x1) ⟶ MetaCat x0 BinRelnHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem 85435..^{MetaCat_struct_r_wellord} : MetaCat 8b17e.. BinRelnHom struct_id struct_comp (proof)
Param MetaFunctor^MetaFunctor : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → ο
Param True^True : ο
Param HomSet^SetHom : ι → ι → ι → ο
Known 45945..^{MetaCat_struct_r_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_r x1) ⟶ MetaFunctor x0 BinRelnHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3)
Theorem 3315e..^{MetaCat_struct_r_wellord_Forgetful} : MetaFunctor 8b17e.. BinRelnHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param MetaCat_initial_p^initial_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Conjecture 105dd..^{MetaCat_struct_r_wellord_initial} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_terminal_p^terminal_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Conjecture 49763..^{MetaCat_struct_r_wellord_terminal} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_coproduct_constr_p^{coproduct_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture 17458..^{MetaCat_struct_r_wellord_coproduct_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_product_constr_p^{product_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Conjecture 71d59..^{MetaCat_struct_r_wellord_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_coequalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 69725.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_equalizer_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture d6008.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_pushout_buggy_constr_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture d3e44.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_pullback_buggy_struct_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 4916b.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_exp_constr_p^{product_exponent_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι) → ο
Conjecture 9460d..^{MetaCat_struct_r_wellord_product_exponent} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 x13 ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_subobject_classifier_buggy_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → (ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Conjecture 1e983.. : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaCat_nno_p^nno_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ι → ι → ι → (ι → ι → ι → ι) → ο
Conjecture d6d09..^{MetaCat_struct_r_wellord_nno} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p 8b17e.. BinRelnHom struct_id struct_comp x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Param MetaAdjunction_strict^{MetaAdjunction_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
Conjecture 538f6..^{MetaCat_struct_r_wellord_left_adjoint_forgetful} : ∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) 8b17e.. BinRelnHom struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0