Proofgold Term Root Disambiguation

∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ (∃ x4 x6 : ι → ι → ι → ι → ι . ∃ x8 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x4 x6 x8) ⟶ (∃ x4 x6 x8 : ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x4 x6 x8 x10) ⟶ ∃ x4 x6 x8 : ι → ι → ι → ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x4 x6 x8 x10

as obj
-

as prop
ed2b0..^{product_equalizer_pullback_constr_ex}

theory
HotG

stx
0c7a5..

address
TMSRG..^{product_equalizer_pullback_constr_ex}