Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ 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 27155.. : ∀ 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) ⟶ and (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x2 (x2 x4 x5) x6 = x2 x4 (x2 x5 x6)) (∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (∀ x6 . x6 ∈ x0 ⟶ and (x2 x6 x5 = x6) (x2 x5 x6 = x6)) ⟶ x4) ⟶ x4) = and (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x1 (x1 x4 x5) x6 = x1 x4 (x1 x5 x6)) (∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (∀ x6 . x6 ∈ x0 ⟶ and (x1 x6 x5 = x6) (x1 x5 x6 = x6)) ⟶ x4) ⟶ x4) (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition MetaCat_initial_p^initial_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . and (x0 x4) (∀ x6 . x0 x6 ⟶ and (x1 x4 x6 (x5 x6)) (∀ x7 . x1 x4 x6 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 : ι → (ι → (ι → ι → ι) → ο) → ο
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)))
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 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 ordsucc^ordsucc : ι → ι
Param SNo^SNo : ι → ο
Param mul_SNo^mul_SNo : ι → ι → ι
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 neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known In_1_2^In_1_2 : 1 ∈ 2
Known mul_SNo_oneL^mul_SNo_oneL : ∀ x0 . SNo x0 ⟶ mul_SNo 1 x0 = x0
Known SNo_1^SNo_1 : SNo 1
Known In_0_2^In_0_2 : 0 ∈ 2
Known mul_SNo_zeroL^{mul_SNo_zeroL} : ∀ x0 . SNo x0 ⟶ mul_SNo 0 x0 = 0
Known SNo_0^SNo_0 : SNo 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 mul_SNo_assoc^{mul_SNo_assoc} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known mul_SNo_oneR^mul_SNo_oneR : ∀ x0 . SNo x0 ⟶ mul_SNo x0 1 = x0
Known cases_2^cases_2 : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Param omega^omega : ι
Known omega_SNo^omega_SNo : ∀ x0 . x0 ∈ omega ⟶ SNo x0
Param nat_p^nat_p : ι → ο
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_p_trans^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Known nat_2^nat_2 : nat_p 2
Theorem 87240.. : not (∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p Monoid MagmaHom struct_id struct_comp x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0) (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 pack_b_0_eq2^pack_b_0_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . x0 = ap (pack_b x0 x1) 0
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known In_0_1^In_0_1 : 0 ∈ 1
Known cases_1^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Theorem e6a94.. : not (∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p Monoid MagmaHom struct_id struct_comp x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0) (proof)
Definition MetaCat_pullback_p^pullback_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι . and (and (and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x4 x6 x7)) (x1 x5 x6 x8)) (x0 x9)) (x1 x9 x4 x10)) (x1 x9 x5 x11)) (x3 x9 x4 x6 x7 x10 = x3 x9 x5 x6 x8 x11)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 x13 x4 x14 ⟶ ∀ x15 . x1 x13 x5 x15 ⟶ x3 x13 x4 x6 x7 x14 = x3 x13 x5 x6 x8 x15 ⟶ and (and (and (x1 x13 x9 (x12 x13 x14 x15)) (x3 x13 x9 x4 x10 (x12 x13 x14 x15) = x14)) (x3 x13 x9 x5 x11 (x12 x13 x14 x15) = x15)) (∀ x16 . x1 x13 x9 x16 ⟶ x3 x13 x9 x4 x10 x16 = x14 ⟶ x3 x13 x9 x5 x11 x16 = x15 ⟶ x16 = x12 x13 x14 x15))
Definition MetaCat_pullback_struct_p^{pullback_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 x4 x5 x6 : ι → ι → ι → ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x8 x9 x10 . x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ ∀ x11 x12 . x1 x8 x10 x11 ⟶ x1 x9 x10 x12 ⟶ MetaCat_pullback_p x0 x1 x2 x3 x8 x9 x10 x11 x12 (x4 x8 x9 x10 x11 x12) (x5 x8 x9 x10 x11 x12) (x6 x8 x9 x10 x11 x12) (x7 x8 x9 x10 x11 x12)
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem e5932.. : not (∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p Monoid MagmaHom struct_id struct_comp x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0) (proof)
Param MetaAdjunction_strict^{MetaAdjunction_strict} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι → ι → ι) → (ι → ι) → (ι → ι) → ο
Param True^True : ο
Param HomSet^SetHom : ι → ι → ι → ο
Definition lam_id^lam_id := λ x0 . lam x0 (λ x1 . x1)
Known 80cab..^{MetaCatSet_initial} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p (λ x4 . True) HomSet (λ x4 . lam x4 (λ x5 . x5)) (λ x4 x5 x6 x7 x8 . lam x4 (λ x9 . ap x7 (ap x8 x9))) x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Known 09501.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 x13 : ι → ι . MetaAdjunction_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ ∀ x14 . ∀ x15 : ι → ι . MetaCat_initial_p x0 x1 x2 x3 x14 x15 ⟶ ∀ x16 : ο . (∀ x17 : ι → ι . MetaCat_initial_p x4 x5 x6 x7 (x8 x14) x17 ⟶ x16) ⟶ x16
Theorem 62ee6.. : not (∀ x0 : ο . (∀ x1 : ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι . MetaAdjunction_strict (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) Monoid MagmaHom struct_id struct_comp x1 x3 (λ x8 . ap x8 0) (λ x8 x9 x10 . x10) x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0) (proof)