Proofgold Address

Definition MetaFunctor_prop1^idT := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 . x0 x4 ⟶ x1 x4 x4 (x2 x4)
Definition MetaFunctor_prop2^compT := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 x7 x8 . x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x1 x4 x5 x7 ⟶ x1 x5 x6 x8 ⟶ x1 x4 x6 (x3 x4 x5 x6 x8 x7)
Definition MetaCat_IdR_p^idL := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 . x0 x4 ⟶ x0 x5 ⟶ x1 x4 x5 x6 ⟶ x3 x4 x4 x5 x6 (x2 x4) = x6
Definition MetaCat_IdL_p^idR := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 . x0 x4 ⟶ x0 x5 ⟶ x1 x4 x5 x6 ⟶ x3 x4 x5 x5 (x2 x5) x6 = x6
Definition MetaCat_Comp_assoc_p^compAssoc := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 x7 x8 x9 x10 . x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x1 x4 x5 x8 ⟶ x1 x5 x6 x9 ⟶ x1 x6 x7 x10 ⟶ x3 x4 x5 x7 (x3 x5 x6 x7 x10 x9) x8 = x3 x4 x6 x7 x10 (x3 x4 x5 x6 x9 x8)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition MetaCat^MetaCat := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . and (and (and (MetaFunctor_prop1 x0 x1 x2 x3) (MetaFunctor_prop2 x0 x1 x2 x3)) (and (MetaCat_IdR_p x0 x1 x2 x3) (MetaCat_IdL_p x0 x1 x2 x3))) (MetaCat_Comp_assoc_p x0 x1 x2 x3)
Known 7da4b..^MetaCat_E : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ ∀ x4 : ο . (MetaFunctor_prop1 x0 x1 x2 x3 ⟶ MetaFunctor_prop2 x0 x1 x2 x3 ⟶ (∀ x5 x6 x7 . x0 x5 ⟶ x0 x6 ⟶ x1 x5 x6 x7 ⟶ x3 x5 x5 x6 x7 (x2 x5) = x7) ⟶ (∀ x5 x6 x7 . x0 x5 ⟶ x0 x6 ⟶ x1 x5 x6 x7 ⟶ x3 x5 x6 x6 (x2 x6) x7 = x7) ⟶ (∀ x5 x6 x7 x8 x9 x10 x11 . x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x5 x6 x9 ⟶ x1 x6 x7 x10 ⟶ x1 x7 x8 x11 ⟶ x3 x5 x6 x8 (x3 x6 x7 x8 x11 x10) x9 = x3 x5 x7 x8 x11 (x3 x5 x6 x7 x10 x9)) ⟶ x4) ⟶ x4
Known 6f34f..^MetaCatOp : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ MetaCat x0 (λ x4 x5 . x1 x5 x4) x2 (λ x4 x5 x6 x7 x8 . x3 x6 x5 x4 x8 x7)
Definition MetaCat_monic_p^monic := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 . and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (∀ x7 . x0 x7 ⟶ ∀ x8 x9 . x1 x7 x4 x8 ⟶ x1 x7 x4 x9 ⟶ x3 x7 x4 x5 x6 x8 = x3 x7 x4 x5 x6 x9 ⟶ x8 = x9)
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))
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)
Definition MetaCat_coproduct_p^coproduct_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x4 x6 x7)) (x1 x5 x6 x8)) (∀ x10 . x0 x10 ⟶ ∀ x11 x12 . x1 x4 x10 x11 ⟶ x1 x5 x10 x12 ⟶ and (and (and (x1 x6 x10 (x9 x10 x11 x12)) (x3 x4 x6 x10 (x9 x10 x11 x12) x7 = x11)) (x3 x5 x6 x10 (x9 x10 x11 x12) x8 = x12)) (∀ x13 . x1 x6 x10 x13 ⟶ x3 x4 x6 x10 x13 x7 = x11 ⟶ x3 x5 x6 x10 x13 x8 = x12 ⟶ x13 = x9 x10 x11 x12))
Definition MetaCat_coproduct_constr_p^{coproduct_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 x9 . x0 x8 ⟶ x0 x9 ⟶ MetaCat_coproduct_p x0 x1 x2 x3 x8 x9 (x4 x8 x9) (x5 x8 x9) (x6 x8 x9) (x7 x8 x9)
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)
Definition MetaCat_coequalizer_p^{coequalizer_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 x5 x8 x9)) (x3 x4 x5 x8 x9 x6 = x3 x4 x5 x8 x9 x7)) (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x5 x11 x12 ⟶ x3 x4 x5 x11 x12 x6 = x3 x4 x5 x11 x12 x7 ⟶ and (and (x1 x8 x11 (x10 x11 x12)) (x3 x5 x8 x11 (x10 x11 x12) x9 = x12)) (∀ x13 . x1 x8 x11 x13 ⟶ x3 x5 x8 x11 x13 x9 = x12 ⟶ x13 = x10 x11 x12))
Definition MetaCat_coequalizer_struct_p^{coequalizer_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_coequalizer_p x0 x1 x2 x3 x7 x8 x9 x10 (x4 x7 x8 x9 x10) (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10)
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)
Definition MetaCat_pushout_p^pushout_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 x6 x4 x7)) (x1 x6 x5 x8)) (x0 x9)) (x1 x4 x9 x10)) (x1 x5 x9 x11)) (x3 x6 x4 x9 x10 x7 = x3 x6 x5 x9 x11 x8)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 x4 x13 x14 ⟶ ∀ x15 . x1 x5 x13 x15 ⟶ x3 x6 x4 x13 x14 x7 = x3 x6 x5 x13 x15 x8 ⟶ and (and (and (x1 x9 x13 (x12 x13 x14 x15)) (x3 x4 x9 x13 (x12 x13 x14 x15) x10 = x14)) (x3 x5 x9 x13 (x12 x13 x14 x15) x11 = x15)) (∀ x16 . x1 x9 x13 x16 ⟶ x3 x4 x9 x13 x16 x10 = x14 ⟶ x3 x5 x9 x13 x16 x11 = x15 ⟶ x16 = x12 x13 x14 x15))
Definition MetaCat_pushout_constr_p^{pushout_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 x4 x5 x6 : ι → ι → ι → ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x8 x9 x10 . x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ ∀ x11 x12 . x1 x10 x8 x11 ⟶ x1 x10 x9 x12 ⟶ MetaCat_pushout_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)
Definition MetaCat_subobject_classifier_p^{subobject_classifier_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . λ x6 x7 . λ x8 : ι → ι → ι → ι . λ x9 : ι → ι → ι → ι → ι → ι → ι . and (and (and (MetaCat_terminal_p x0 x1 x2 x3 x4 x5) (x0 x6)) (x1 x4 x6 x7)) (∀ x10 x11 x12 . MetaCat_monic_p x0 x1 x2 x3 x10 x11 x12 ⟶ and (x1 x11 x6 (x8 x10 x11 x12)) (MetaCat_pullback_p x0 x1 x2 x3 x4 x11 x6 x7 (x8 x10 x11 x12) x10 (x5 x10) x12 (x9 x10 x11 x12)))
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 434dd..^{equalizer_coequalizer_Op} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 x7 x8 x9 . ∀ x10 : ι → ι → ι . MetaCat_equalizer_p x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ MetaCat_coequalizer_p x0 (λ x11 x12 . x1 x12 x11) x2 (λ x11 x12 x13 x14 x15 . x3 x13 x12 x11 x15 x14) x5 x4 x6 x7 x8 x9 x10 (proof)
Theorem 71f1f..^{equalizer_coequalizer_constr_Op} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 : ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x4 x5 x6 ⟶ MetaCat_coequalizer_struct_p x0 (λ x7 x8 . x1 x8 x7) x2 (λ x7 x8 x9 x10 x11 . x3 x9 x8 x7 x11 x10) (λ x7 x8 . x4 x8 x7) (λ x7 x8 . x5 x8 x7) (λ x7 x8 . x6 x8 x7) (proof)
Theorem ed80d..^{coequalizer_equalizer_Op} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 x7 x8 x9 . ∀ x10 : ι → ι → ι . MetaCat_coequalizer_p x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ MetaCat_equalizer_p x0 (λ x11 x12 . x1 x12 x11) x2 (λ x11 x12 x13 x14 x15 . x3 x13 x12 x11 x15 x14) x5 x4 x6 x7 x8 x9 x10 (proof)
Theorem 466a7..^{coequalizer_equalizer_constr_Op} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 : ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 x1 x2 x3 x4 x5 x6 ⟶ MetaCat_equalizer_struct_p x0 (λ x7 x8 . x1 x8 x7) x2 (λ x7 x8 x9 x10 x11 . x3 x9 x8 x7 x11 x10) (λ x7 x8 . x4 x8 x7) (λ x7 x8 . x5 x8 x7) (λ x7 x8 . x6 x8 x7) (proof)
Theorem 03855..^{pullback_pushout_Op} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ι → ι → ι → ι . MetaCat_pullback_p x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ MetaCat_pushout_p x0 (λ x13 x14 . x1 x14 x13) x2 (λ x13 x14 x15 x16 x17 . x3 x15 x14 x13 x17 x16) x4 x5 x6 x7 x8 x9 x10 x11 x12 (proof)
Theorem 9b6ae..^{pullback_pushout_constr_Op} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 x4 x5 x6 : ι → ι → ι → ι → ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x4 x5 x6 x7 ⟶ MetaCat_pushout_constr_p x0 (λ x8 x9 . x1 x9 x8) x2 (λ x8 x9 x10 x11 x12 . x3 x10 x9 x8 x12 x11) x4 x5 x6 x7 (proof)
Theorem 4e78a..^{pushout_pullback_Op} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ι → ι → ι → ι . MetaCat_pushout_p x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ MetaCat_pullback_p x0 (λ x13 x14 . x1 x14 x13) x2 (λ x13 x14 x15 x16 x17 . x3 x15 x14 x13 x17 x16) x4 x5 x6 x7 x8 x9 x10 x11 x12 (proof)
Theorem d2ca5..^{pushout_pullback_constr_Op} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 x4 x5 x6 : ι → ι → ι → ι → ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p x0 x1 x2 x3 x4 x5 x6 x7 ⟶ MetaCat_pullback_struct_p x0 (λ x8 x9 . x1 x9 x8) x2 (λ x8 x9 x10 x11 x12 . x3 x10 x9 x8 x12 x11) x4 x5 x6 x7 (proof)
Known 19e22..^and10I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem 1abd1..^{product_equalizer_pullback_constr} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ ∀ x4 x5 : ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x4 x5 x6 ⟶ ∀ x7 x8 x9 : ι → ι → ι . ∀ x10 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x7 x8 x9 x10 ⟶ MetaCat_pullback_struct_p x0 x1 x2 x3 (λ x11 x12 x13 x14 x15 . x4 (x7 x11 x12) x13 (x3 (x7 x11 x12) x11 x13 x14 (x8 x11 x12)) (x3 (x7 x11 x12) x12 x13 x15 (x9 x11 x12))) (λ x11 x12 x13 x14 x15 . x3 (x4 (x7 x11 x12) x13 (x3 (x7 x11 x12) x11 x13 x14 (x8 x11 x12)) (x3 (x7 x11 x12) x12 x13 x15 (x9 x11 x12))) (x7 x11 x12) x11 (x8 x11 x12) (x5 (x7 x11 x12) x13 (x3 (x7 x11 x12) x11 x13 x14 (x8 x11 x12)) (x3 (x7 x11 x12) x12 x13 x15 (x9 x11 x12)))) (λ x11 x12 x13 x14 x15 . x3 (x4 (x7 x11 x12) x13 (x3 (x7 x11 x12) x11 x13 x14 (x8 x11 x12)) (x3 (x7 x11 x12) x12 x13 x15 (x9 x11 x12))) (x7 x11 x12) x12 (x9 x11 x12) (x5 (x7 x11 x12) x13 (x3 (x7 x11 x12) x11 x13 x14 (x8 x11 x12)) (x3 (x7 x11 x12) x12 x13 x15 (x9 x11 x12)))) (λ x11 x12 x13 x14 x15 x16 x17 x18 . x6 (x7 x11 x12) x13 (x3 (x7 x11 x12) x11 x13 x14 (x8 x11 x12)) (x3 (x7 x11 x12) x12 x13 x15 (x9 x11 x12)) x16 (x10 x11 x12 x16 x17 x18)) (proof)
Theorem 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 (proof)
Theorem b0aad..^{coproduct_coequalizer_pushout_constr_ex} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 x1 x2 x3 x5 x7 x9 ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_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_pushout_constr_p x0 x1 x2 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)