Search for blocks/addresses/...

Proofgold Address

address
PUgEpCLq92CKMjuWgpnriqb2smVgnqjt3Sz
total
0
mg
-
conjpub
-
current assets
2171e../eac97.. bday: 9725 doc published by PrCx1..
Param lam_idlam_id : ιι
Param apap : ιιι
Definition struct_idstruct_id := λ x0 . lam_id (ap x0 0)
Param lam_complam_comp : ιιιι
Definition struct_compstruct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Param MetaCat_initial_pinitial_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ο
Param struct_pstruct_p : ιο
Param UnaryPredHomHom_struct_p : ιιιο
Conjecture 1615b..MetaCat_struct_p_initial : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p struct_p UnaryPredHom struct_id struct_comp x1 x3x2)x2)x0)x0
Param MetaCat_terminal_pterminal_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ο
Conjecture 14bd1..MetaCat_struct_p_terminal : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p struct_p UnaryPredHom struct_id struct_comp x1 x3x2)x2)x0)x0
Param MetaCat_coproduct_constr_pcoproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture 09ba2..MetaCat_struct_p_coproduct_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_product_constr_pproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture 4f9ac..MetaCat_struct_p_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_coequalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture 98a5f.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_equalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture aa945.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_pushout_buggy_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture 8a34f.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_pullback_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture b5697.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_exp_constr_pproduct_exponent_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιιιι) → ο
Conjecture 592be..MetaCat_struct_p_product_exponent : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7 x9 x11 x13x12)x12)x10)x10)x8)x8)x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_subobject_classifier_buggy_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ιι(ιιιι) → (ιιιιιιι) → ο
Conjecture 109e8.. : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7 x9 x11x10)x10)x8)x8)x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_nno_pnno_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ιιι(ιιιι) → ο
Conjecture dcba1..MetaCat_struct_p_nno : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p struct_p UnaryPredHom struct_id struct_comp x1 x3 x5 x7 x9 x11x10)x10)x8)x8)x6)x6)x4)x4)x2)x2)x0)x0
Param MetaAdjunction_strictMetaAdjunction_strict : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → (ιι) → (ιιιι) → (ιι) → (ιι) → ο
Param TrueTrue : ο
Param HomSetSetHom : ιιιο
Conjecture c3ca2..MetaCat_struct_p_left_adjoint_forgetful : ∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) struct_p UnaryPredHom struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7x6)x6)x4)x4)x2)x2)x0)x0

previous assets