Proofgold Proposition

∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_r_e_e x1) ⟶ MetaFunctor x0 Hom_b_b_r_e_e (λ 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)

type
prop

theory
HotG

name
-

proof
PUdXV..

Megalodon
MetaCat_struct_b_b_r_e_e_Forgetful_gen

proofgold address
TMLzy..^{MetaCat_struct_b_b_r_e_e_Forgetful_gen}

creator
9630 PrCx1../8ba66..

owner
9630 PrCx1../8ba66..

term root
de2d1..