Search for blocks/addresses/...

Proofgold Asset

asset id
0be5d7c0cd91192216e975cf7dfef309727af09820528fb2cd29b39fc6a53372
asset hash
5b89c038c1ccb1cd2ebde019ad142a65f04bd7cd03a36183cd3f8ad37a5365ba
bday / block
9724
tx
ef27a..
preasset
doc published by PrCx1..
Param lamSigma : ι(ιι) → ι
Definition lam_idlam_id := λ x0 . lam x0 (λ x1 . x1)
Param apap : ιιι
Definition struct_idstruct_id := λ x0 . lam_id (ap x0 0)
Definition lam_complam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition struct_compstruct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition MetaCat_initial_pinitial_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . and (x0 x4) (∀ x6 . x0 x6and (x1 x4 x6 (x5 x6)) (∀ x7 . x1 x4 x6 x7x7 = x5 x6))
Param pack_epack_e : ιιι
Definition struct_estruct_e := λ x0 . ∀ x1 : ι → ο . (∀ x2 x3 . x3x2x1 (pack_e x2 x3))x1 x0
Param PtdSetHomHom_struct_e : ιιιο
Param ordsuccordsucc : ιι
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known pack_struct_e_Ipack_struct_e_I : ∀ x0 x1 . x1x0struct_e (pack_e x0 x1)
Known In_0_1In_0_1 : 01
Known pack_e_1_eq2pack_e_1_eq2 : ∀ x0 x1 . x1 = ap (pack_e x0 x1) 1
Param PiPi : ι(ιι) → ι
Definition setexpsetexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known f65a3..Hom_struct_e_pack : ∀ x0 x1 x2 x3 x4 . PtdSetHom (pack_e x0 x2) (pack_e x1 x3) x4 = and (x4setexp x1 x0) (ap x4 x2 = x3)
Known lam_Pilam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x2 x3x1 x3)lam x0 x2Pi x0 x1
Known betabeta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0ap (lam x0 x1) x2 = x1 x2
Known Pi_etaPi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2Pi x0 x1lam x0 (ap x2) = x2
Known encode_u_extencode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x1 x3 = x2 x3)lam x0 x1 = lam x0 x2
Known cases_1cases_1 : ∀ x0 . x01∀ x1 : ι → ο . x1 0x1 x0
Theorem 11b66..MetaCat_struct_e_initial : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p struct_e PtdSetHom struct_id struct_comp x1 x3x2)x2)x0)x0 (proof)
Param MetaCat_terminal_pterminal_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ο
Conjecture b5447..MetaCat_struct_e_terminal : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p struct_e PtdSetHom struct_id struct_comp x1 x3x2)x2)x0)x0
Param MetaCat_coproduct_constr_pcoproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture 8da75..MetaCat_struct_e_coproduct_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_e PtdSetHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_product_constr_pproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture 8e8d1..MetaCat_struct_e_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p struct_e PtdSetHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_coequalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture 8fa6b.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p struct_e PtdSetHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_equalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture a9707.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p struct_e PtdSetHom struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_pushout_buggy_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture a309a.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p struct_e PtdSetHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_pullback_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture 728ef.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p struct_e PtdSetHom struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_exp_constr_pproduct_exponent_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιιιι) → ο
Conjecture d6977..MetaCat_struct_e_product_exponent : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p struct_e PtdSetHom 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 5a560.. : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p struct_e PtdSetHom 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 99f2c..MetaCat_struct_e_nno : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p struct_e PtdSetHom 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 : ο
Definition HomSetSetHom := λ x0 x1 x2 . x2setexp x1 x0
Param setsumsetsum : ιιι
Param combine_funcscombine_funcs : ιι(ιι) → (ιι) → ιι
Param Inj1Inj1 : ιι
Param Inj0Inj0 : ιι
Param MetaFunctor_strictMetaFunctor_strict : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → ο
Param MetaFunctorMetaFunctor : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → ο
Param MetaNatTransMetaNatTrans : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → (ιι) → (ιιιι) → (ιι) → ο
Param MetaAdjunctionMetaAdjunction : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → (ιι) → (ιιιι) → (ιι) → (ιι) → ο
Known d6aa5..MetaAdjunction_strict_I : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11MetaNatTrans x0 x1 x2 x3 x0 x1 x2 x3 (λ x14 . x14) (λ x14 x15 x16 . x16) (λ x14 . x10 (x8 x14)) (λ x14 x15 x16 . x11 (x8 x14) (x8 x15) (x9 x14 x15 x16)) x12MetaNatTrans x4 x5 x6 x7 x4 x5 x6 x7 (λ x14 . x8 (x10 x14)) (λ x14 x15 x16 . x9 (x10 x14) (x10 x15) (x11 x14 x15 x16)) (λ x14 . x14) (λ x14 x15 x16 . x16) x13MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13MetaAdjunction_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13
Param MetaCatMetaCat : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ο
Known 5cbb4..MetaFunctor_strict_I : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . MetaCat x0 x1 x2 x3MetaCat x4 x5 x6 x7MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
Known e4125..MetaCatSet : MetaCat (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0)
Known 1c0e1..MetaCat_struct_e_gen : ∀ x0 : ι → ο . (∀ x1 . x0 x1struct_e x1)MetaCat x0 PtdSetHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Known 2cb62..MetaFunctorI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . (∀ x10 . x0 x10x4 (x8 x10))(∀ x10 x11 x12 . x0 x10x0 x11x1 x10 x11 x12x5 (x8 x10) (x8 x11) (x9 x10 x11 x12))(∀ x10 . x0 x10x9 x10 x10 (x2 x10) = x6 (x8 x10))(∀ x10 x11 x12 x13 x14 . x0 x10x0 x11x0 x12x1 x10 x11 x13x1 x11 x12 x14x9 x10 x12 (x3 x10 x11 x12 x14 x13) = x7 (x8 x10) (x8 x11) (x8 x12) (x9 x11 x12 x14) (x9 x10 x11 x13))MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known setsum_Inj_invsetsum_Inj_inv : ∀ x0 x1 x2 . x2setsum x0 x1or (∀ x3 : ο . (∀ x4 . and (x4x0) (x2 = Inj0 x4)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4x1) (x2 = Inj1 x4)x3)x3)
Known combine_funcs_eq1combine_funcs_eq1 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known Inj0_0Inj0_0 : Inj0 0 = 0
Known combine_funcs_eq2combine_funcs_eq2 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known ap_Piap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2Pi x0 x1x3x0ap x2 x3x1 x3
Known 0f4ef..MetaCat_struct_e_Forgetful_gen : ∀ x0 : ι → ο . (∀ x1 . x0 x1struct_e x1)MetaFunctor x0 PtdSetHom (λ 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)
Known c1d68..MetaNatTransI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . (∀ x13 . x0 x13x5 (x8 x13) (x10 x13) (x12 x13))(∀ x13 x14 x15 . x0 x13x0 x14x1 x13 x14 x15x7 (x8 x13) (x10 x13) (x10 x14) (x11 x13 x14 x15) (x12 x13) = x7 (x8 x13) (x8 x14) (x10 x14) (x12 x14) (x9 x13 x14 x15))MetaNatTrans x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12
Known Inj1_setsumInj1_setsum : ∀ x0 x1 x2 . x2x1Inj1 x2setsum x0 x1
Known pack_e_0_eq2pack_e_0_eq2 : ∀ x0 x1 . x0 = ap (pack_e x0 x1) 0
Known fd494..MetaAdjunctionI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . (∀ x14 . x0 x14x7 (x8 x14) (x8 (x10 (x8 x14))) (x8 x14) (x13 (x8 x14)) (x9 x14 (x10 (x8 x14)) (x12 x14)) = x6 (x8 x14))(∀ x14 . x4 x14x3 (x10 x14) (x10 (x8 (x10 x14))) (x10 x14) (x11 (x8 (x10 x14)) x14 (x13 x14)) (x12 (x10 x14)) = x2 (x10 x14))MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13
Known Inj0_setsumInj0_setsum : ∀ x0 x1 x2 . x2x0Inj0 x2setsum x0 x1
Theorem 1ffb7..MetaCat_struct_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_e PtdSetHom struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7x6)x6)x4)x4)x2)x2)x0)x0 (proof)