Proofgold Address

Definition 28b0a.. := λ x0 . λ x1 : ι → ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 (x1 x2 x3) x4 = x1 x2 (x1 x3 x4)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition 0941b.. := λ x0 . λ x1 : ι → ι → ι . and (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 (x1 x2 x3) x4 = x1 x2 (x1 x3 x4)) (∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ and (x1 x4 x3 = x4) (x1 x3 x4 = x4)) ⟶ x2) ⟶ x2)
Definition explicit_Group^{explicit_Group} := λ x0 . λ x1 : ι → ι → ι . and (and (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)) (∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (and (∀ x4 . x4 ∈ x0 ⟶ and (x1 x3 x4 = x4) (x1 x4 x3 = x4)) (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (and (x1 x4 x6 = x3) (x1 x6 x4 = x3)) ⟶ x5) ⟶ x5)) ⟶ x2) ⟶ x2)
Definition explicit_abelian^{explicit_abelian} := λ x0 . λ x1 : ι → ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 = x1 x3 x2
Definition 127dd.. := λ x0 . λ x1 : ι → ι → ι . and (explicit_Group x0 x1) (explicit_abelian x0 x1)
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem e4946.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ 28b0a.. x0 x2 = 28b0a.. x0 x1 (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem e219d.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ 0941b.. x0 x2 = 0941b.. x0 x1 (proof)
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known prop_ext^prop_ext : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 = x1
Known explicit_Group_repindep^{explicit_Group_repindep} : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ iff (explicit_Group x0 x1) (explicit_Group x0 x2)
Theorem 68b43.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ explicit_Group x0 x2 = explicit_Group x0 x1 (proof)
Known explicit_abelian_repindep^{explicit_abelian_repindep} : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ iff (explicit_abelian x0 x1) (explicit_abelian x0 x2)
Theorem 40a7b.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ 127dd.. x0 x2 = 127dd.. x0 x1 (proof)
Param ordsucc^ordsucc : ι → ι
Definition MetaCat_terminal_p^terminal_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . and (x0 x4) (∀ x6 . x0 x6 ⟶ and (x1 x6 x4 (x5 x6)) (∀ x7 . x1 x6 x4 x7 ⟶ x7 = x5 x6))
Param pack_b^pack_b : ι → CT2 ι
Definition struct_b^struct_b := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ x1 (pack_b x2 x3)) ⟶ x1 x0
Param unpack_b_o^unpack_b_o : ι → (ι → (ι → ι → ι) → ο) → ο
Param MagmaHom^Hom_struct_b : ι → ι → ι → ο
Param struct_id^struct_id : ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param ap^ap : ι → ι → ι
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition struct_comp^struct_comp := λ x0 x1 x2 . lam_comp (ap x0 0)
Known pack_struct_b_I^{pack_struct_b_I} : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ struct_b (pack_b x0 x1)
Known In_0_1^In_0_1 : 0 ∈ 1
Known unpack_b_o_eq^{unpack_b_o_eq} : ∀ x0 : ι → (ι → ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_b_o (pack_b x1 x2) x0 = x0 x1 x2
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known 2cd8d..^{Hom_struct_b_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 . MagmaHom (pack_b x0 x2) (pack_b x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ap x4 (x2 x6 x7) = x3 (ap x4 x6) (ap x4 x7))
Known pack_b_0_eq2^pack_b_0_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . x0 = ap (pack_b x0 x1) 0
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Param Sing^Sing : ι → ι
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known eq_1_Sing0^eq_1_Sing0 : 1 = Sing 0
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Theorem 1e9a4.. : ∀ x0 : ι → (ι → ι → ι) → ο . (∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ∈ x1) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ (∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ 1 ⟶ ∀ x3 . x3 ∈ 1 ⟶ 0 = x1 x2 x3) ⟶ x0 1 x1) ⟶ ∀ x1 : ο . (∀ x2 . (∀ x3 : ο . (∀ x4 : ι → ι . MetaCat_terminal_p (λ x5 . and (struct_b x5) (unpack_b_o x5 x0)) MagmaHom struct_id struct_comp x2 x4 ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Definition Semigroup^{struct_b_semigroup} := λ x0 . and (struct_b x0) (unpack_b_o x0 (λ x1 . λ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 (x2 x3 x4) x5 = x2 x3 (x2 x4 x5)))
Theorem aa3f3..^{MetaCat_struct_b_semigroup_terminal} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p Semigroup MagmaHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition Monoid^{struct_b_monoid} := λ x0 . and (struct_b x0) (unpack_b_o x0 (λ x1 . λ x2 : ι → ι → ι . and (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 (x2 x3 x4) x5 = x2 x3 (x2 x4 x5)) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (∀ x5 . x5 ∈ x1 ⟶ and (x2 x5 x4 = x5) (x2 x4 x5 = x5)) ⟶ x3) ⟶ x3)))
Known cases_1^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Theorem e4b9e..^{MetaCat_struct_b_monoid_terminal} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p Monoid MagmaHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 1a38b.. : ∀ x0 : ι → ι → ι . x0 0 0 = 0 ⟶ explicit_Group 1 x0 (proof)
Definition Group^Group := λ x0 . and (struct_b x0) (unpack_b_o x0 explicit_Group)
Theorem 4ce24..^{MetaCat_struct_b_group_terminal} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p Group MagmaHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition abelian_Group_alt^{struct_b_abelian_group} := λ x0 . and (struct_b x0) (unpack_b_o x0 (λ x1 . λ x2 : ι → ι → ι . and (explicit_Group x1 x2) (explicit_abelian x1 x2)))
Theorem ad386..^{MetaCat_struct_b_abelian_group_terminal} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p abelian_Group_alt MagmaHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param MetaCat_product_constr_p^{product_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Known 97db2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 : ι → ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 x9 . x0 x8 ⟶ x0 x9 ⟶ ∀ x10 : ο . (x0 (x4 x8 x9) ⟶ x1 (x4 x8 x9) x8 (x5 x8 x9) ⟶ x1 (x4 x8 x9) x9 (x6 x8 x9) ⟶ (∀ x11 . x0 x11 ⟶ ∀ x12 x13 . x1 x11 x8 x12 ⟶ x1 x11 x9 x13 ⟶ and (and (and (x1 x11 (x4 x8 x9) (x7 x8 x9 x11 x12 x13)) (x3 x11 (x4 x8 x9) x8 (x5 x8 x9) (x7 x8 x9 x11 x12 x13) = x12)) (x3 x11 (x4 x8 x9) x9 (x6 x8 x9) (x7 x8 x9 x11 x12 x13) = x13)) (∀ x14 . x1 x11 (x4 x8 x9) x14 ⟶ x3 x11 (x4 x8 x9) x8 (x5 x8 x9) x14 = x12 ⟶ x3 x11 (x4 x8 x9) x9 (x6 x8 x9) x14 = x13 ⟶ x14 = x7 x8 x9 x11 x12 x13)) ⟶ x10) ⟶ x10) ⟶ MetaCat_product_constr_p x0 x1 x2 x3 x4 x5 x6 x7
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Param If_i^If_i : ο → ι → ι → ι
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0)
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Known Pi_ext^Pi_ext : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ ∀ x3 . x3 ∈ Pi x0 x1 ⟶ (∀ x4 . x4 ∈ x0 ⟶ ap x2 x4 = ap x3 x4) ⟶ x2 = x3
Known tuple_Sigma_eta^{tuple_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known tuple_2_setprod^{tuple_2_setprod} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ setprod x0 x1
Param unpack_b_i^unpack_b_i : ι → (ι → CT2 ι) → ι
Known unpack_b_i_eq^{unpack_b_i_eq} : ∀ x0 : ι → (ι → ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_b_i (pack_b x1 x2) x0 = x0 x1 x2
Known pack_b_ext^pack_b_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ pack_b x0 x1 = pack_b x0 x2
Theorem 8633f.. : ∀ x0 : ι → (ι → ι → ι) → ο . (∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ∈ x1) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ (∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ∈ x1) ⟶ x0 x1 x2 ⟶ ∀ x3 . ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ∈ x3) ⟶ x0 x3 x4 ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ setprod x1 x3 ⟶ ∀ x7 . x7 ∈ setprod x1 x3 ⟶ lam 2 (λ x9 . If_i (x9 = 0) (x2 (ap x6 0) (ap x7 0)) (x4 (ap x6 1) (ap x7 1))) = x5 x6 x7) ⟶ x0 (setprod x1 x3) x5) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι . (∀ x7 : ο . (∀ x8 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p (λ x9 . and (struct_b x9) (unpack_b_o x9 x0)) MagmaHom struct_id struct_comp x2 x4 x6 x8 ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Theorem 57959.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ 28b0a.. x0 x1 ⟶ ∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ 28b0a.. x2 x3 ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ setprod x0 x2 ⟶ ∀ x6 . x6 ∈ setprod x0 x2 ⟶ lam 2 (λ x8 . If_i (x8 = 0) (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1))) = x4 x5 x6) ⟶ 28b0a.. (setprod x0 x2) x4 (proof)
Theorem 0e909.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ 0941b.. x0 x1 ⟶ ∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ 0941b.. x2 x3 ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ setprod x0 x2 ⟶ ∀ x6 . x6 ∈ setprod x0 x2 ⟶ lam 2 (λ x8 . If_i (x8 = 0) (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1))) = x4 x5 x6) ⟶ 0941b.. (setprod x0 x2) x4 (proof)
Theorem 6bacd.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ explicit_Group x0 x1 ⟶ ∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ explicit_Group x2 x3 ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ setprod x0 x2 ⟶ ∀ x6 . x6 ∈ setprod x0 x2 ⟶ lam 2 (λ x8 . If_i (x8 = 0) (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1))) = x4 x5 x6) ⟶ explicit_Group (setprod x0 x2) x4 (proof)
Theorem 183c5..^{MetaCat_struct_b_semigroup_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Semigroup MagmaHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 64746..^{MetaCat_struct_b_monoid_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Monoid MagmaHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 05bdf..^{MetaCat_struct_b_group_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Group MagmaHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 760b6..^{MetaCat_struct_b_abelian_group_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p abelian_Group_alt MagmaHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param MetaCat_equalizer_struct_p^{equalizer_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Known 500a0.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 : ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ι . (∀ x7 x8 x9 x10 . x0 x7 ⟶ x0 x8 ⟶ x1 x7 x8 x9 ⟶ x1 x7 x8 x10 ⟶ ∀ x11 : ο . (x0 (x4 x7 x8 x9 x10) ⟶ x1 (x4 x7 x8 x9 x10) x7 (x5 x7 x8 x9 x10) ⟶ x3 (x4 x7 x8 x9 x10) x7 x8 x9 (x5 x7 x8 x9 x10) = x3 (x4 x7 x8 x9 x10) x7 x8 x10 (x5 x7 x8 x9 x10) ⟶ (∀ x12 . x0 x12 ⟶ ∀ x13 . x1 x12 x7 x13 ⟶ x3 x12 x7 x8 x9 x13 = x3 x12 x7 x8 x10 x13 ⟶ and (and (x1 x12 (x4 x7 x8 x9 x10) (x6 x7 x8 x9 x10 x12 x13)) (x3 x12 (x4 x7 x8 x9 x10) x7 (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10 x12 x13) = x13)) (∀ x14 . x1 x12 (x4 x7 x8 x9 x10) x14 ⟶ x3 x12 (x4 x7 x8 x9 x10) x7 (x5 x7 x8 x9 x10) x14 = x13 ⟶ x14 = x6 x7 x8 x9 x10 x12 x13)) ⟶ x11) ⟶ x11) ⟶ MetaCat_equalizer_struct_p x0 x1 x2 x3 x4 x5 x6
Param Sep^Sep : ι → (ι → ο) → ι
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Theorem 01619.. : ∀ x0 : ι → (ι → ι → ι) → ο . (∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ∈ x1) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ (∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ∈ x1) ⟶ x0 x1 x2 ⟶ ∀ x3 . ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ∈ x3) ⟶ x0 x3 x4 ⟶ ∀ x5 x6 . MagmaHom (pack_b x1 x2) (pack_b x3 x4) x5 ⟶ MagmaHom (pack_b x1 x2) (pack_b x3 x4) x6 ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ {x9 ∈ x1|ap x5 x9 = ap x6 x9} ⟶ ∀ x9 . x9 ∈ {x10 ∈ x1|ap x5 x10 = ap x6 x10} ⟶ x2 x8 x9 = x7 x8 x9) ⟶ x0 {x8 ∈ x1|ap x5 x8 = ap x6 x8} x7) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p (λ x7 . and (struct_b x7) (unpack_b_o x7 x0)) MagmaHom struct_id struct_comp x2 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Theorem 1dd10.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ 28b0a.. x0 x1 ⟶ ∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ 28b0a.. x2 x3 ⟶ ∀ x4 x5 . MagmaHom (pack_b x0 x1) (pack_b x2 x3) x4 ⟶ MagmaHom (pack_b x0 x1) (pack_b x2 x3) x5 ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ {x8 ∈ x0|ap x4 x8 = ap x5 x8} ⟶ ∀ x8 . x8 ∈ {x9 ∈ x0|ap x4 x9 = ap x5 x9} ⟶ x1 x7 x8 = x6 x7 x8) ⟶ 28b0a.. {x7 ∈ x0|ap x4 x7 = ap x5 x7} x6 (proof)
Theorem c31a3.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ explicit_Group x0 x1 ⟶ ∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ explicit_Group x2 x3 ⟶ ∀ x4 x5 . MagmaHom (pack_b x0 x1) (pack_b x2 x3) x4 ⟶ MagmaHom (pack_b x0 x1) (pack_b x2 x3) x5 ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ {x8 ∈ x0|ap x4 x8 = ap x5 x8} ⟶ ∀ x8 . x8 ∈ {x9 ∈ x0|ap x4 x9 = ap x5 x9} ⟶ x1 x7 x8 = x6 x7 x8) ⟶ explicit_Group {x7 ∈ x0|ap x4 x7 = ap x5 x7} x6 (proof)
Theorem 9347c..^{MetaCat_struct_b_semigroup_equalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p Semigroup MagmaHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem e6d9e..^{MetaCat_struct_b_group_equalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p Group MagmaHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 994bf..^{MetaCat_struct_b_abelian_group_equalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p abelian_Group_alt MagmaHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param MetaCat_pullback_struct_p^{pullback_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Known ed2b0..^{product_equalizer_pullback_constr_ex} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x5 x7 x9 ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ ∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4
Known 88d6d..^{MetaCat_struct_b_semigroup} : MetaCat Semigroup MagmaHom struct_id struct_comp
Theorem 61ba2..^{MetaCat_struct_b_semigroup_pullback_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p Semigroup MagmaHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known d87b9..^{MetaCat_struct_b_group} : MetaCat Group MagmaHom struct_id struct_comp
Theorem 42863..^{MetaCat_struct_b_group_pullback_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p Group MagmaHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known da44b..^{MetaCat_struct_b_abelian_group} : MetaCat abelian_Group_alt MagmaHom struct_id struct_comp
Theorem e443a..^{MetaCat_struct_b_abelian_group_pullback_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p abelian_Group_alt MagmaHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)