Proofgold Address

Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Param struct_e^struct_e : ι → ο
Param PtdSetHom^Hom_struct_e : ι → ι → ι → ο
Param lam_id^lam_id : ι → ι
Param ap^ap : ι → ι → ι
Definition struct_id^struct_id := λ x0 . lam_id (ap x0 0)
Param lam_comp^lam_comp : ι → ι → ι → ι
Definition struct_comp^struct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Known 1c0e1..^{MetaCat_struct_e_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_e x1) ⟶ MetaCat x0 PtdSetHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem 5aae9..^{MetaCat_struct_e} : MetaCat struct_e PtdSetHom struct_id struct_comp (proof)
Param MetaFunctor^MetaFunctor : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → ο
Param True^True : ο
Param HomSet^SetHom : ι → ι → ι → ο
Known 0f4ef..^{MetaCat_struct_e_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_e x1) ⟶ MetaFunctor x0 PtdSetHom (λ 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)
Theorem a6c49..^{MetaCat_struct_e_Forgetful} : MetaFunctor struct_e PtdSetHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param struct_p^struct_p : ι → ο
Param UnaryPredHom^Hom_struct_p : ι → ι → ι → ο
Known 5387a..^{MetaCat_struct_p_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_p x1) ⟶ MetaCat x0 UnaryPredHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem caa5e..^{MetaCat_struct_p} : MetaCat struct_p UnaryPredHom struct_id struct_comp (proof)
Known 57ba0..^{MetaCat_struct_p_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_p x1) ⟶ MetaFunctor x0 UnaryPredHom (λ 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)
Theorem 40bbd..^{MetaCat_struct_p_Forgetful} : MetaFunctor struct_p UnaryPredHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param struct_u^struct_u : ι → ο
Param UnaryFuncHom^Hom_struct_u : ι → ι → ι → ο
Known 7ce95..^{MetaCat_struct_u_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_u x1) ⟶ MetaCat x0 UnaryFuncHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem 73eab..^{MetaCat_struct_u} : MetaCat struct_u UnaryFuncHom struct_id struct_comp (proof)
Known 6eadb..^{MetaCat_struct_u_Forgetful_gen} : ∀ 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)
Theorem 0032d..^{MetaCat_struct_u_Forgetful} : MetaFunctor struct_u UnaryFuncHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param struct_r^struct_r : ι → ο
Param BinRelnHom^Hom_struct_r : ι → ι → ι → ο
Known 62658..^{MetaCat_struct_r_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_r x1) ⟶ MetaCat x0 BinRelnHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem 6955f..^{MetaCat_struct_r} : MetaCat struct_r BinRelnHom struct_id struct_comp (proof)
Known 45945..^{MetaCat_struct_r_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_r x1) ⟶ MetaFunctor x0 BinRelnHom (λ 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)
Theorem 07626..^{MetaCat_struct_r_Forgetful} : MetaFunctor struct_r BinRelnHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param struct_b^struct_b : ι → ο
Param MagmaHom^Hom_struct_b : ι → ι → ι → ο
Known 125f1..^{MetaCat_struct_b_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b x1) ⟶ MetaCat x0 MagmaHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem c55c1..^{MetaCat_struct_b} : MetaCat struct_b MagmaHom struct_id struct_comp (proof)
Known 79957..^{MetaCat_struct_b_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b x1) ⟶ MetaFunctor x0 MagmaHom (λ 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)
Theorem dda03..^{MetaCat_struct_b_Forgetful} : MetaFunctor struct_b MagmaHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param struct_c^struct_c : ι → ο
Param PreContinuousHom^Hom_struct_c : ι → ι → ι → ο
Known dd75c..^{MetaCat_struct_c_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_c x1) ⟶ MetaCat x0 PreContinuousHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem ed6b5..^{MetaCat_struct_c} : MetaCat struct_c PreContinuousHom struct_id struct_comp (proof)
Known 58a40..^{MetaCat_struct_c_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_c x1) ⟶ MetaFunctor x0 PreContinuousHom (λ 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)
Theorem 803c1..^{MetaCat_struct_c_Forgetful} : MetaFunctor struct_c PreContinuousHom struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param struct_b_b_e^struct_b_b_e : ι → ο
Param Hom_b_b_e^{Hom_struct_b_b_e} : ι → ι → ι → ο
Known 5f5c5..^{MetaCat_struct_b_b_e_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_e x1) ⟶ MetaCat x0 Hom_b_b_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem 8af1e..^{MetaCat_struct_b_b_e} : MetaCat struct_b_b_e Hom_b_b_e struct_id struct_comp (proof)
Known 9c6b9..^{MetaCat_struct_b_b_e_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_e x1) ⟶ MetaFunctor x0 Hom_b_b_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)
Theorem 0a59e..^{MetaCat_struct_b_b_e_Forgetful} : MetaFunctor struct_b_b_e Hom_b_b_e struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param struct_b_b_e_e^{struct_b_b_e_e} : ι → ο
Param Hom_b_b_e_e^{Hom_struct_b_b_e_e} : ι → ι → ι → ο
Known 936d9..^{MetaCat_struct_b_b_e_e_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_e_e x1) ⟶ MetaCat x0 Hom_b_b_e_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem e84d1..^{MetaCat_struct_b_b_e_e} : MetaCat struct_b_b_e_e Hom_b_b_e_e struct_id struct_comp (proof)
Known 72690..^{MetaCat_struct_b_b_e_e_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_e_e x1) ⟶ MetaFunctor x0 Hom_b_b_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)
Theorem 4b8c9..^{MetaCat_struct_b_b_e_e_Forgetful} : MetaFunctor struct_b_b_e_e Hom_b_b_e_e struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)
Param struct_b_b_r_e_e^{struct_b_b_r_e_e} : ι → ο
Param Hom_b_b_r_e_e^{Hom_struct_b_b_r_e_e} : ι → ι → ι → ο
Known dc6cf..^{MetaCat_struct_b_b_r_e_e_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_r_e_e x1) ⟶ MetaCat x0 Hom_b_b_r_e_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))
Theorem d5a62..^{MetaCat_struct_b_b_r_e_e} : MetaCat struct_b_b_r_e_e Hom_b_b_r_e_e struct_id struct_comp (proof)
Known 49006..^{MetaCat_struct_b_b_r_e_e_Forgetful_gen} : ∀ 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)
Theorem e9786..^{MetaCat_struct_b_b_r_e_e_Forgetful} : MetaFunctor struct_b_b_r_e_e Hom_b_b_r_e_e struct_id struct_comp (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (λ x0 . ap x0 0) (λ x0 x1 x2 . x2) (proof)