Search for blocks/addresses/...

Proofgold Asset

asset id
1f696530eda06fe2841c73868c40002a1c8cd6dee14075b1b15f85afb8ff1093
asset hash
26c28355d25cccf4f1584f408933c25864ff0a7d91d7a7d096d65cf342b564bb
bday / block
9730
tx
9caa1..
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)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param struct_b_b_e_estruct_b_b_e_e : ιο
Param unpack_b_b_e_e_ounpack_b_b_e_e_o : ι(ι(ιιι) → (ιιι) → ιιο) → ο
Definition Rigstruct_b_b_e_e_semiring := λ x0 . and (struct_b_b_e_e x0) (unpack_b_b_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . and (and (and (and (and (and (and (and (∀ x6 . x6x1∀ x7 . x7x1∀ x8 . x8x1x2 (x2 x6 x7) x8 = x2 x6 (x2 x7 x8)) (∀ x6 . x6x1∀ x7 . x7x1x2 x6 x7 = x2 x7 x6)) (∀ x6 . x6x1x2 x6 x4 = x6)) (∀ x6 . x6x1∀ x7 . x7x1∀ x8 . x8x1x3 (x3 x6 x7) x8 = x3 x6 (x3 x7 x8))) (∀ x6 . x6x1and (x3 x6 x5 = x6) (x3 x5 x6 = x6))) (∀ x6 . x6x1∀ x7 . x7x1∀ x8 . x8x1x3 x6 (x2 x7 x8) = x2 (x3 x6 x7) (x3 x6 x8))) (∀ x6 . x6x1∀ x7 . x7x1∀ x8 . x8x1x3 (x2 x6 x7) x8 = x2 (x3 x6 x8) (x3 x7 x8))) (∀ x6 . x6x1x3 x6 x4 = x4)) (∀ x6 . x6x1x3 x4 x6 = x4)))
Param MetaCatMetaCat : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ο
Param Hom_b_b_e_eHom_struct_b_b_e_e : ιιιο
Known 936d9..MetaCat_struct_b_b_e_e_gen : ∀ x0 : ι → ο . (∀ x1 . x0 x1struct_b_b_e_e x1)MetaCat x0 Hom_b_b_e_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem 37e9f..MetaCat_struct_b_b_e_e_semiring : MetaCat Rig Hom_b_b_e_e struct_id struct_comp (proof)
Param MetaFunctorMetaFunctor : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → ο
Param TrueTrue : ο
Param HomSetSetHom : ιιιο
Known 72690..MetaCat_struct_b_b_e_e_Forgetful_gen : ∀ x0 : ι → ο . (∀ x1 . x0 x1struct_b_b_e_e x1)MetaFunctor x0 Hom_b_b_e_e (λ 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 f402b..MetaCat_struct_b_b_e_e_semiring_Forgetful : MetaFunctor Rig Hom_b_b_e_e 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_pinitial_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ο
Conjecture 869d4..MetaCat_struct_b_b_e_e_semiring_initial : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p Rig Hom_b_b_e_e struct_id struct_comp x1 x3x2)x2)x0)x0
Param MetaCat_terminal_pterminal_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ι(ιι) → ο
Conjecture 674c6..MetaCat_struct_b_b_e_e_semiring_terminal : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p Rig Hom_b_b_e_e struct_id struct_comp x1 x3x2)x2)x0)x0
Param MetaCat_coproduct_constr_pcoproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture 8d77d..MetaCat_struct_b_b_e_e_semiring_coproduct_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p Rig Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_product_constr_pproduct_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιι) → (ιιι) → (ιιι) → (ιιιιιι) → ο
Conjecture 56fbd..MetaCat_struct_b_b_e_e_semiring_product_constr : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Rig Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_coequalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture db32d.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_buggy_struct_p Rig Hom_b_b_e_e struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_equalizer_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιι) → (ιιιιι) → (ιιιιιιι) → ο
Conjecture 7836a.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_buggy_struct_p Rig Hom_b_b_e_e struct_id struct_comp x1 x3 x5x4)x4)x2)x2)x0)x0
Param MetaCat_pushout_buggy_constr_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture 19b4c.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_buggy_constr_p Rig Hom_b_b_e_e struct_id struct_comp x1 x3 x5 x7x6)x6)x4)x4)x2)x2)x0)x0
Param MetaCat_pullback_buggy_struct_p : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιι) → (ιιιιιιιιι) → ο
Conjecture 9a4e6.. : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_buggy_struct_p Rig Hom_b_b_e_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 6b467..MetaCat_struct_b_b_e_e_semiring_product_exponent : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p Rig Hom_b_b_e_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 059df.. : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_buggy_p Rig Hom_b_b_e_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 5669f..MetaCat_struct_b_b_e_e_semiring_nno : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p Rig Hom_b_b_e_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 : (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιο) → (ιιιο) → (ιι) → (ιιιιιι) → (ιι) → (ιιιι) → (ιι) → (ιιιι) → (ιι) → (ιι) → ο
Conjecture 29f18..MetaCat_struct_b_b_e_e_semiring_left_adjoint_forgetful : ∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) Rig Hom_b_b_e_e struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7x6)x6)x4)x4)x2)x2)x0)x0