Proofgold Term Root Disambiguation

∀ x0 : ι → ο . x0 1 ⟶ x0 2 ⟶ ∃ x1 . ∃ x3 : ι → ι . ∃ x5 x7 . ∃ x9 : ι → ι → ι → ι . ∃ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p x0 HomSet lam_id (λ x13 x14 x15 . lam_comp x13) x1 x3 x5 x7 x9 x11

as obj
-

as prop
e5b47..^{MetaCatSet_subobject_classifier_gen_ex}

theory
HotG

stx
c80b6..

address
TMZLT..^{MetaCatSet_subobject_classifier_gen_ex}