Proofgold Term Root Disambiguation

∀ x0 : ι → ο . x0 1 ⟶ x0 2 ⟶ MetaCat_subobject_classifier_p x0 HomSet lam_id (λ x1 x2 x3 . lam_comp x1) 1 (λ x1 . lam x1 (λ x2 . 0)) 2 (lam 1 (λ x1 . 1)) (λ x1 x2 x3 . lam x2 (λ x4 . If_i (∀ x5 : ο . (∀ x6 . and (x6 ∈ x1) (ap x3 x6 = x4) ⟶ x5) ⟶ x5) 1 0)) (λ x1 x2 x3 x4 x5 x6 . lam x4 (λ x7 . inv x1 (ap x3) (ap x6 x7)))

as obj
-

as prop
bd9cd..^{MetaCatSet_subobject_classifier_gen}

theory
HotG

stx
c80b6..

address
TMaqc..^{MetaCatSet_subobject_classifier_gen}