MetaCat struct_e Hom_struct_e struct_id struct_comp

In Proofgold the corresponding term root is 40d0ba... and proposition id is 5aae9b...

Proof:

An exact proof term for the current goal is MetaCat_struct_e_gen struct_e (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_e_Forgetful)

MetaFunctor struct_e Hom_struct_e struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is 4c2b40... and proposition id is a6c491...

Proof:

An exact proof term for the current goal is MetaCat_struct_e_Forgetful_gen struct_e (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_p)

MetaCat struct_p Hom_struct_p struct_id struct_comp

In Proofgold the corresponding term root is edb0bb... and proposition id is caa5e1...

Proof:

An exact proof term for the current goal is MetaCat_struct_p_gen struct_p (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_p_Forgetful)

MetaFunctor struct_p Hom_struct_p struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is 318901... and proposition id is 40bbd4...

Proof:

An exact proof term for the current goal is MetaCat_struct_p_Forgetful_gen struct_p (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_u)

MetaCat struct_u Hom_struct_u struct_id struct_comp

In Proofgold the corresponding term root is 5de126... and proposition id is 73eabf...

Proof:

An exact proof term for the current goal is MetaCat_struct_u_gen struct_u (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_u_Forgetful)

MetaFunctor struct_u Hom_struct_u struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is b3eb4d... and proposition id is 0032df...

Proof:

An exact proof term for the current goal is MetaCat_struct_u_Forgetful_gen struct_u (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_r)

MetaCat struct_r Hom_struct_r struct_id struct_comp

In Proofgold the corresponding term root is c743d5... and proposition id is 6955f4...

Proof:

An exact proof term for the current goal is MetaCat_struct_r_gen struct_r (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_r_Forgetful)

MetaFunctor struct_r Hom_struct_r struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is 697cf9... and proposition id is 07626c...

Proof:

An exact proof term for the current goal is MetaCat_struct_r_Forgetful_gen struct_r (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_b)

MetaCat struct_b Hom_struct_b struct_id struct_comp

In Proofgold the corresponding term root is cb8d37... and proposition id is c55c1b...

Proof:

An exact proof term for the current goal is MetaCat_struct_b_gen struct_b (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_b_Forgetful)

MetaFunctor struct_b Hom_struct_b struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is 5098f3... and proposition id is dda03f...

Proof:

An exact proof term for the current goal is MetaCat_struct_b_Forgetful_gen struct_b (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_c)

MetaCat struct_c Hom_struct_c struct_id struct_comp

In Proofgold the corresponding term root is 4f44ef... and proposition id is ed6b54...

Proof:

An exact proof term for the current goal is MetaCat_struct_c_gen struct_c (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_c_Forgetful)

MetaFunctor struct_c Hom_struct_c struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is f3e562... and proposition id is 803c1d...

Proof:

An exact proof term for the current goal is MetaCat_struct_c_Forgetful_gen struct_c (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_b_b_e)

MetaCat struct_b_b_e Hom_struct_b_b_e struct_id struct_comp

In Proofgold the corresponding term root is 75b2b1... and proposition id is 8af1e4...

Proof:

An exact proof term for the current goal is MetaCat_struct_b_b_e_gen struct_b_b_e (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_b_b_e_Forgetful)

MetaFunctor struct_b_b_e Hom_struct_b_b_e struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is 209560... and proposition id is 0a59e8...

Proof:

An exact proof term for the current goal is MetaCat_struct_b_b_e_Forgetful_gen struct_b_b_e (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_b_b_e_e)

MetaCat struct_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp

In Proofgold the corresponding term root is feeda8... and proposition id is e84d1b...

Proof:

An exact proof term for the current goal is MetaCat_struct_b_b_e_e_gen struct_b_b_e_e (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_b_b_e_e_Forgetful)

MetaFunctor struct_b_b_e_e Hom_struct_b_b_e_e struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is d90dfc... and proposition id is 4b8c93...

Proof:

An exact proof term for the current goal is MetaCat_struct_b_b_e_e_Forgetful_gen struct_b_b_e_e (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_b_b_r_e_e)

MetaCat struct_b_b_r_e_e Hom_struct_b_b_r_e_e struct_id struct_comp

In Proofgold the corresponding term root is e1b7b4... and proposition id is d5a625...

Proof:

An exact proof term for the current goal is MetaCat_struct_b_b_r_e_e_gen struct_b_b_r_e_e (λX H ⇒ H).

∎

Theorem. (MetaCat_struct_b_b_r_e_e_Forgetful)

MetaFunctor struct_b_b_r_e_e Hom_struct_b_b_r_e_e struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is dcdc54... and proposition id is e97865...

Proof:

An exact proof term for the current goal is MetaCat_struct_b_b_r_e_e_Forgetful_gen struct_b_b_r_e_e (λX H ⇒ H).

∎