Proofgold Address

Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem 414ab.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ (∀ x4 . x4 ∈ x0 ⟶ x2 (x2 x4) = x2 x4) = ∀ x4 . x4 ∈ x0 ⟶ x1 (x1 x4) = x1 x4 (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition MetaCat_product_p^product_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x6 x4 x7)) (x1 x6 x5 x8)) (∀ x10 . x0 x10 ⟶ ∀ x11 x12 . x1 x10 x4 x11 ⟶ x1 x10 x5 x12 ⟶ and (and (and (x1 x10 x6 (x9 x10 x11 x12)) (x3 x10 x6 x4 x7 (x9 x10 x11 x12) = x11)) (x3 x10 x6 x5 x8 (x9 x10 x11 x12) = x12)) (∀ x13 . x1 x10 x6 x13 ⟶ x3 x10 x6 x4 x7 x13 = x11 ⟶ x3 x10 x6 x5 x8 x13 = x12 ⟶ x13 = x9 x10 x11 x12))
Definition MetaCat_product_constr_p^{product_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 x9 . x0 x8 ⟶ x0 x9 ⟶ MetaCat_product_p x0 x1 x2 x3 x8 x9 (x4 x8 x9) (x5 x8 x9) (x6 x8 x9) (x7 x8 x9)
Known and6I^and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ and (and (and (and (and x0 x1) x2) x3) x4) x5
Theorem 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 (proof)
Definition MetaCat_equalizer_p^equalizer_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 . λ x10 : ι → ι → ι . and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x8 x4 x9)) (x3 x8 x4 x5 x6 x9 = x3 x8 x4 x5 x7 x9)) (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x11 x4 x12 ⟶ x3 x11 x4 x5 x6 x12 = x3 x11 x4 x5 x7 x12 ⟶ and (and (x1 x11 x8 (x10 x11 x12)) (x3 x11 x8 x4 x9 (x10 x11 x12) = x12)) (∀ x13 . x1 x11 x8 x13 ⟶ x3 x11 x8 x4 x9 x13 = x12 ⟶ x13 = x10 x11 x12))
Definition MetaCat_equalizer_struct_p^{equalizer_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 : ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 x8 . x0 x7 ⟶ x0 x8 ⟶ ∀ x9 x10 . x1 x7 x8 x9 ⟶ x1 x7 x8 x10 ⟶ MetaCat_equalizer_p x0 x1 x2 x3 x7 x8 x9 x10 (x4 x7 x8 x9 x10) (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10)
Known 41253..^and8I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7
Theorem 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 (proof)
Param pack_u^pack_u : ι → (ι → ι) → ι
Definition struct_u^struct_u := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . x4 ∈ x2 ⟶ x3 x4 ∈ x2) ⟶ x1 (pack_u x2 x3)) ⟶ x1 x0
Param unpack_u_o^unpack_u_o : ι → (ι → (ι → ι) → ο) → ο
Definition 9f253..^{struct_u_idem} := λ x0 . and (struct_u x0) (unpack_u_o x0 (λ x1 . λ x2 : ι → ι . ∀ x3 . x3 ∈ x1 ⟶ x2 (x2 x3) = x2 x3))
Param UnaryFuncHom^Hom_struct_u : ι → ι → ι → ο
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)
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Param ordsucc^ordsucc : ι → ι
Param If_i^If_i : ο → ι → ι → ι
Known unpack_u_o_eq^{unpack_u_o_eq} : ∀ x0 : ι → (ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_u_o (pack_u x1 x2) x0 = x0 x1 x2
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known pack_struct_u_I^{pack_struct_u_I} : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ struct_u (pack_u x0 x1)
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known 66c4c..^{Hom_struct_u_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . UnaryFuncHom (pack_u x0 x2) (pack_u x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ ap x4 (x2 x6) = x3 (ap x4 x6))
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
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 pack_u_0_eq2^pack_u_0_eq2 : ∀ x0 . ∀ x1 : ι → ι . x0 = ap (pack_u x0 x1) 0
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
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 ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
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_u_i^unpack_u_i : ι → (ι → (ι → ι) → ι) → ι
Known unpack_u_i_eq^{unpack_u_i_eq} : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_u_i (pack_u x1 x2) x0 = x0 x1 x2
Known pack_u_ext^pack_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ pack_u x0 x1 = pack_u x0 x2
Theorem f2a7f..^{MetaCat_struct_u_idem_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 9f253.. UnaryFuncHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
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 and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Theorem 877ff..^{MetaCat_struct_u_idem_equalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p 9f253.. UnaryFuncHom 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 31a6e..^{MetaCat_struct_u_idem} : MetaCat 9f253.. UnaryFuncHom struct_id struct_comp
Theorem 5b67a..^{MetaCat_struct_u_idem_pullback_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p 9f253.. UnaryFuncHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)