Proofgold Address

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 MetaCat_initial_p^initial_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Param UnaryFuncHom^Hom_struct_u : ι → ι → ι → ο
Param struct_id^struct_id : ι → ι
Param struct_comp^struct_comp : ι → ι → ι → ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Known 35202.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_u x1) ⟶ x0 (pack_u 0 (λ x1 . x1)) ⟶ MetaCat_initial_p x0 UnaryFuncHom struct_id struct_comp (pack_u 0 (λ x1 . x1)) (λ x1 . lam 0 (λ x2 . x2))
Param ordsucc^ordsucc : ι → ι
Param MetaCat_terminal_p^terminal_p : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ι → (ι → ι) → ο
Param ap^ap : ι → ι → ι
Known a3e3e.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_u x1) ⟶ x0 (pack_u 1 (λ x1 . x1)) ⟶ MetaCat_terminal_p x0 UnaryFuncHom struct_id struct_comp (pack_u 1 (λ x1 . x1)) (λ x1 . lam (ap x1 0) (λ x2 . 0))
Param 5a1fb.. : ι → ι → ι
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Param If_i^If_i : ο → ι → ι → ι
Known ec613.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . ∀ x3 : ι → ι . 5a1fb.. (pack_u x0 x1) (pack_u x2 x3) = pack_u (setprod x0 x2) (λ x5 . lam 2 (λ x6 . If_i (x6 = 0) (x1 (ap x5 0)) (x3 (ap x5 1))))
Param MetaCat_product_constr_p^{product_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Known e49b4.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_u x1) ⟶ (∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (5a1fb.. x1 x2)) ⟶ MetaCat_product_constr_p x0 UnaryFuncHom struct_id struct_comp 5a1fb.. (λ x1 x2 . lam (setprod (ap x1 0) (ap x2 0)) (λ x3 . ap x3 0)) (λ x1 x2 . lam (setprod (ap x1 0) (ap x2 0)) (λ x3 . ap x3 1)) (λ x1 x2 x3 x4 x5 . lam (ap x3 0) (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (ap x4 x6) (ap x5 x6))))
Param 9fd7a.. : ι → ι → ι → ι → ι
Param Sep^Sep : ι → (ι → ο) → ι
Known 70b0f.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 x4 . 9fd7a.. (pack_u x0 x1) x2 x3 x4 = pack_u {x6 ∈ x0|ap x3 x6 = ap x4 x6} x1
Param MetaCat_equalizer_struct_p^{equalizer_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο
Known 1077c.. : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_u x1) ⟶ (∀ x1 x2 x3 x4 . x0 x1 ⟶ x0 x2 ⟶ UnaryFuncHom x1 x2 x3 ⟶ UnaryFuncHom x1 x2 x4 ⟶ x0 (9fd7a.. x1 x2 x3 x4)) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 UnaryFuncHom struct_id struct_comp x2 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param unpack_u_o^unpack_u_o : ι → (ι → (ι → ι) → ο) → ο
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition SelfInjection^struct_u_inj := λ x0 . and (struct_u x0) (unpack_u_o x0 (λ x1 . inj x1 x1))
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 prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 3af12.. : ∀ x0 . ∀ x1 : ι → ι . unpack_u_o (pack_u x0 x1) (λ x3 . inj x3 x3) = inj x0 x0 x1 (proof)
Known pack_struct_u_I^{pack_struct_u_I} : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ struct_u (pack_u x0 x1)
Theorem 894de.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ SelfInjection (pack_u x0 x1) (proof)
Theorem 83a49.. : ∀ x0 . SelfInjection x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . x4 ∈ x2 ⟶ x3 x4 ∈ x2) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5) ⟶ x1 (pack_u x2 x3)) ⟶ x1 x0 (proof)
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Theorem bdf9a..^{MetaCat_struct_u_inj_initial} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p SelfInjection UnaryFuncHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known cases_1^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Theorem 883bd..^{MetaCat_struct_u_inj_terminal} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p SelfInjection UnaryFuncHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known tuple_2_Sigma^{tuple_2_Sigma} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 x2 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ lam x0 x1
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Known ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0)
Known tuple_2_inj^tuple_2_inj : ∀ x0 x1 x2 x3 . lam 2 (λ x5 . If_i (x5 = 0) x0 x1) = lam 2 (λ x5 . If_i (x5 = 0) x2 x3) ⟶ and (x0 = x2) (x1 = 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
Theorem 501bf..^{MetaCat_struct_u_inj_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p SelfInjection UnaryFuncHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
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 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
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Theorem 0ba1a..^{MetaCat_struct_u_inj_equalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p SelfInjection UnaryFuncHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Known 6bcb5..^{MetaCat_struct_u_inj} : MetaCat SelfInjection UnaryFuncHom struct_id struct_comp
Param MetaCat_pullback_struct_p^{pullback_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
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
Theorem 40b2c..^{MetaCat_struct_u_inj_pullback_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p SelfInjection UnaryFuncHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition Permutation^struct_u_bij := λ x0 . and (struct_u x0) (unpack_u_o x0 (λ x1 . bij x1 x1))
Known bijI^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ bij x0 x1 x2
Theorem 05626.. : ∀ x0 . ∀ x1 : ι → ι . unpack_u_o (pack_u x0 x1) (λ x3 . bij x3 x3) = bij x0 x0 x1 (proof)
Theorem 22d49.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x1 x4 = x2) ⟶ x3) ⟶ x3) ⟶ Permutation (pack_u x0 x1) (proof)
Theorem a02b8.. : ∀ x0 . Permutation x0 ⟶ ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . x4 ∈ x2 ⟶ x3 x4 ∈ x2) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x2) (x3 x6 = x4) ⟶ x5) ⟶ x5) ⟶ x1 (pack_u x2 x3)) ⟶ x1 x0 (proof)
Theorem 955bd..^{MetaCat_struct_u_bij_initial} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p Permutation UnaryFuncHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 32041..^{MetaCat_struct_u_bij_terminal} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_p Permutation UnaryFuncHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Theorem 6ce53..^{MetaCat_struct_u_bij_product_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p Permutation UnaryFuncHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Theorem 24604..^{MetaCat_struct_u_bij_equalizer_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p Permutation UnaryFuncHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known 17fce..^{MetaCat_struct_u_bij} : MetaCat Permutation UnaryFuncHom struct_id struct_comp
Theorem 6f6f3..^{MetaCat_struct_u_bij_pullback_constr} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p Permutation UnaryFuncHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)