Proofgold Term Root Disambiguation

∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_u x1) ⟶ MetaFunctor x0 UnaryFuncHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3)

as obj
-

as prop
6eadb..^{MetaCat_struct_u_Forgetful_gen}

theory
HotG

stx
820be..

address
TMQCL..^{MetaCat_struct_u_Forgetful_gen}