Search for blocks/addresses/...
Proofgold Address
address
PUUZvQgByP78kmc7R8m6QRmXrcMPSqEA4q3
total
0
mg
-
conjpub
-
current assets
fb51a..
/
bd849..
bday:
9727
doc published by
PrCx1..
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
)
Param
MetaCat
MetaCat
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
struct_b
struct_b
:
ι
→
ο
Param
unpack_b_o
unpack_b_o
:
ι
→
(
ι
→
(
ι
→
ι
→
ι
) →
ο
) →
ο
Param
explicit_Group
explicit_Group
:
ι
→
(
ι
→
ι
→
ι
) →
ο
Definition
Group
Group
:=
λ x0 .
and
(
struct_b
x0
)
(
unpack_b_o
x0
explicit_Group
)
Param
MagmaHom
Hom_struct_b
:
ι
→
ι
→
ι
→
ο
Known
125f1..
MetaCat_struct_b_gen
:
∀ x0 :
ι → ο
.
(
∀ x1 .
x0
x1
⟶
struct_b
x1
)
⟶
MetaCat
x0
MagmaHom
(
λ x1 .
lam_id
(
ap
x1
0
)
)
(
λ x1 x2 x3 .
lam_comp
(
ap
x1
0
)
)
Theorem
d87b9..
MetaCat_struct_b_group
:
MetaCat
Group
MagmaHom
struct_id
struct_comp
(proof)
Param
MetaFunctor
MetaFunctor
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
) →
ο
Param
True
True
:
ο
Param
HomSet
SetHom
:
ι
→
ι
→
ι
→
ο
Known
79957..
MetaCat_struct_b_Forgetful_gen
:
∀ x0 :
ι → ο
.
(
∀ x1 .
x0
x1
⟶
struct_b
x1
)
⟶
MetaFunctor
x0
MagmaHom
(
λ 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
e0977..
MetaCat_struct_b_group_Forgetful
:
MetaFunctor
Group
MagmaHom
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
8e7ab..
MetaCat_struct_b_group_initial
:
∀ x0 : ο .
(
∀ x1 .
(
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
MetaCat_initial_p
Group
MagmaHom
struct_id
struct_comp
x1
x3
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_terminal_p
terminal_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ι
→
(
ι
→
ι
) →
ο
Conjecture
4ce24..
MetaCat_struct_b_group_terminal
:
∀ x0 : ο .
(
∀ x1 .
(
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
MetaCat_terminal_p
Group
MagmaHom
struct_id
struct_comp
x1
x3
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_coproduct_constr_p
coproduct_constr_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
7abd1..
MetaCat_struct_b_group_coproduct_constr
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_coproduct_constr_p
Group
MagmaHom
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
05bdf..
MetaCat_struct_b_group_product_constr
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_product_constr_p
Group
MagmaHom
struct_id
struct_comp
x1
x3
x5
x7
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_coequalizer_buggy_struct_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
df3fd..
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι →
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_coequalizer_buggy_struct_p
Group
MagmaHom
struct_id
struct_comp
x1
x3
x5
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_equalizer_buggy_struct_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
7619f..
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι →
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_equalizer_buggy_struct_p
Group
MagmaHom
struct_id
struct_comp
x1
x3
x5
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_pushout_buggy_constr_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
fc8d8..
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_pushout_buggy_constr_p
Group
MagmaHom
struct_id
struct_comp
x1
x3
x5
x7
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
Param
MetaCat_pullback_buggy_struct_p
:
(
ι
→
ο
) →
(
ι
→
ι
→
ι
→
ο
) →
(
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
) →
ο
Conjecture
12f90..
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_pullback_buggy_struct_p
Group
MagmaHom
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
01a47..
MetaCat_struct_b_group_product_exponent
:
∀ x0 : ο .
(
∀ x1 :
ι →
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι →
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι →
ι →
ι →
ι →
ι → ι
.
(
∀ x8 : ο .
(
∀ x9 :
ι →
ι → ι
.
(
∀ x10 : ο .
(
∀ x11 :
ι →
ι → ι
.
(
∀ x12 : ο .
(
∀ x13 :
ι →
ι →
ι →
ι → ι
.
MetaCat_exp_constr_p
Group
MagmaHom
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
13d0c..
:
∀ x0 : ο .
(
∀ x1 .
(
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 .
(
∀ x6 : ο .
(
∀ x7 .
(
∀ x8 : ο .
(
∀ x9 :
ι →
ι →
ι → ι
.
(
∀ x10 : ο .
(
∀ x11 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_subobject_classifier_buggy_p
Group
MagmaHom
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
b8f7d..
MetaCat_struct_b_group_nno
:
∀ x0 : ο .
(
∀ x1 .
(
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 .
(
∀ x6 : ο .
(
∀ x7 .
(
∀ x8 : ο .
(
∀ x9 .
(
∀ x10 : ο .
(
∀ x11 :
ι →
ι →
ι → ι
.
MetaCat_nno_p
Group
MagmaHom
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
2570d..
MetaCat_struct_b_group_left_adjoint_forgetful
:
∀ x0 : ο .
(
∀ x1 :
ι → ι
.
(
∀ x2 : ο .
(
∀ x3 :
ι →
ι →
ι → ι
.
(
∀ x4 : ο .
(
∀ x5 :
ι → ι
.
(
∀ x6 : ο .
(
∀ x7 :
ι → ι
.
MetaAdjunction_strict
(
λ x8 .
True
)
HomSet
lam_id
(
λ x8 x9 x10 .
lam_comp
x8
)
Group
MagmaHom
struct_id
struct_comp
x1
x3
(
λ x8 .
ap
x8
0
)
(
λ x8 x9 x10 .
x10
)
x5
x7
⟶
x6
)
⟶
x6
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
)
⟶
x0
)
⟶
x0
previous assets