Proofgold Proposition

∀ 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)))

type
prop

theory
HotG

name
-

proof
PUcag..

Megalodon
MetaCatSet_subobject_classifier_gen

proofgold address
TMLy4..^{MetaCatSet_subobject_classifier_gen}

creator
11547 PrEBh../7d014..

owner
11561 PrEBh../11fbd..

term root
37cca..