Proofgold Term Root Disambiguation

λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . λ x6 x7 . λ x8 : ι → ι → ι → ι . λ x9 : ι → ι → ι → ι → ι → ι → ι . and (and (and (MetaCat_terminal_p x0 x1 x2 x3 x4 x5) (x0 x6)) (x1 x4 x6 x7)) (∀ x10 x11 x12 . MetaCat_monic_p x0 x1 x2 x3 x10 x11 x12 ⟶ and (x1 x11 x6 (x8 x10 x11 x12)) (MetaCat_pullback_p x0 x1 x2 x3 x4 x11 x6 x7 (x8 x10 x11 x12) x10 (x5 x10) x12 (x9 x10 x11 x12)))

as obj
b2f9d..^{subobject_classifier_p}

as prop
-

theory
HotG

stx
0c7a5..

address
TMPMc..^{subobject_classifier_p}