Search for blocks/addresses/...

Proofgold Asset

asset id
ab329fa70ca03ada85b9207b866e47232ddf0dc85ef099cc4f97fe29b45081ea
asset hash
a69ec68301e5f3a2b2bdde7cc47fb50c08e7ad3db33cd952a12958864c0d7331
bday / block
9730
tx
85d60..
preasset
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_b_b_estruct_b_b_e : ιο
Param Hom_b_b_eHom_struct_b_b_e : ιιιο
Conjecture 2d772..MetaCat_struct_b_b_e_initial : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p struct_b_b_e Hom_b_b_e struct_id struct_comp x1 x3x2)x2)x0)x0
Param MetaCat_terminal_pterminal_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ο
Conjecture df1ca..MetaCat_struct_b_b_e_terminal : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p struct_b_b_e Hom_b_b_e struct_id struct_comp x1 x3x2)x2)x0)x0
Param MetaCat_coproduct_constr_pcoproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture 121ce..MetaCat_struct_b_b_e_coproduct_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_b_b_e Hom_b_b_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_product_constr_pproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture c5905..MetaCat_struct_b_b_e_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_b_b_e Hom_b_b_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_coequalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture e9456.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p struct_b_b_e Hom_b_b_e struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_equalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture 6b1b1.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p struct_b_b_e Hom_b_b_e struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_pushout_buggy_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture c1382.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p struct_b_b_e Hom_b_b_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_pullback_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture ce41c.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p struct_b_b_e Hom_b_b_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_exp_constr_pproduct_exponent_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιιιι) → ο
Conjecture ce6a2..MetaCat_struct_b_b_e_product_exponent : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p struct_b_b_e Hom_b_b_e 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 22e04.. : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p struct_b_b_e Hom_b_b_e 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 2edf3..MetaCat_struct_b_b_e_nno : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p struct_b_b_e Hom_b_b_e 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 5f551..MetaCat_struct_b_b_e_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_b_b_e Hom_b_b_e struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7x6)x6)x4)x4)x2)x2)x0)x0