Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι →
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat
x0
x1
x2
x3
⟶
(
∃ x4 x6 :
ι →
ι →
ι →
ι → ι
.
∃ x8 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_coequalizer_buggy_struct_p
x0
x1
x2
x3
x4
x6
x8
)
⟶
(
∃ x4 x6 x8 :
ι →
ι → ι
.
∃ x10 :
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_coproduct_constr_p
x0
x1
x2
x3
x4
x6
x8
x10
)
⟶
∃ x4 x6 x8 :
ι →
ι →
ι →
ι →
ι → ι
.
∃ x10 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_pushout_buggy_constr_p
x0
x1
x2
x3
x4
x6
x8
x10
as obj
-
as prop
f0f28..
theory
HotG
stx
2772d..
address
TMcre..