Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition MetaFunctor^MetaFunctor := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . and (and (and (∀ x10 . x0 x10 ⟶ x4 (x8 x10)) (∀ x10 x11 x12 . x0 x10 ⟶ x0 x11 ⟶ x1 x10 x11 x12 ⟶ x5 (x8 x10) (x8 x11) (x9 x10 x11 x12))) (∀ x10 . x0 x10 ⟶ x9 x10 x10 (x2 x10) = x6 (x8 x10))) (∀ x10 x11 x12 x13 x14 . x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x1 x10 x11 x13 ⟶ x1 x11 x12 x14 ⟶ x9 x10 x12 (x3 x10 x11 x12 x14 x13) = x7 (x8 x10) (x8 x11) (x8 x12) (x9 x11 x12 x14) (x9 x10 x11 x13))
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem 2cb62..^MetaFunctorI : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . (∀ x10 . x0 x10 ⟶ x4 (x8 x10)) ⟶ (∀ x10 x11 x12 . x0 x10 ⟶ x0 x11 ⟶ x1 x10 x11 x12 ⟶ x5 (x8 x10) (x8 x11) (x9 x10 x11 x12)) ⟶ (∀ x10 . x0 x10 ⟶ x9 x10 x10 (x2 x10) = x6 (x8 x10)) ⟶ (∀ x10 x11 x12 x13 x14 . x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x1 x10 x11 x13 ⟶ x1 x11 x12 x14 ⟶ x9 x10 x12 (x3 x10 x11 x12 x14 x13) = x7 (x8 x10) (x8 x11) (x8 x12) (x9 x11 x12 x14) (x9 x10 x11 x13)) ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 (proof)
Known and4E^and4E : ∀ x0 x1 x2 x3 : ο . and (and (and x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4) ⟶ x4
Theorem 973e2..^MetaFunctorE : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ ∀ x10 : ο . ((∀ x11 . x0 x11 ⟶ x4 (x8 x11)) ⟶ (∀ x11 x12 x13 . x0 x11 ⟶ x0 x12 ⟶ x1 x11 x12 x13 ⟶ x5 (x8 x11) (x8 x12) (x9 x11 x12 x13)) ⟶ (∀ x11 . x0 x11 ⟶ x9 x11 x11 (x2 x11) = x6 (x8 x11)) ⟶ (∀ x11 x12 x13 x14 x15 . x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x1 x11 x12 x14 ⟶ x1 x12 x13 x15 ⟶ x9 x11 x13 (x3 x11 x12 x13 x15 x14) = x7 (x8 x11) (x8 x12) (x8 x13) (x9 x12 x13 x15) (x9 x11 x12 x14)) ⟶ x10) ⟶ x10 (proof)
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Definition MetaFunctor_strict^{MetaFunctor_strict} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . and (and (MetaCat x0 x1 x2 x3) (MetaCat x4 x5 x6 x7)) (MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 5cbb4..^{MetaFunctor_strict_I} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ MetaCat x4 x5 x6 x7 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 (proof)
Known and3E^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem 95305..^{MetaFunctor_strict_E} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ ∀ x10 : ο . (MetaCat x0 x1 x2 x3 ⟶ MetaCat x4 x5 x6 x7 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ x10) ⟶ x10 (proof)
Definition MetaNatTrans_buggy := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . λ x10 : ι → ι . λ x11 : ι → ι → ι → ι . λ x12 : ι → ι . and (∀ x13 . x0 x13 ⟶ x1 (x8 x13) (x10 x13) (x12 x13)) (∀ x13 x14 x15 . x0 x13 ⟶ x0 x14 ⟶ x1 x13 x14 x15 ⟶ x7 (x8 x13) (x10 x13) (x10 x14) (x11 x13 x14 x15) (x12 x13) = x7 (x8 x13) (x8 x14) (x10 x14) (x12 x14) (x9 x13 x14 x15))
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 10e56.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . (∀ x13 . x0 x13 ⟶ x1 (x8 x13) (x10 x13) (x12 x13)) ⟶ (∀ x13 x14 x15 . x0 x13 ⟶ x0 x14 ⟶ x1 x13 x14 x15 ⟶ x7 (x8 x13) (x10 x13) (x10 x14) (x11 x13 x14 x15) (x12 x13) = x7 (x8 x13) (x8 x14) (x10 x14) (x12 x14) (x9 x13 x14 x15)) ⟶ MetaNatTrans_buggy x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 (proof)
Theorem 1342d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . MetaNatTrans_buggy x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ ∀ x13 : ο . ((∀ x14 . x0 x14 ⟶ x1 (x8 x14) (x10 x14) (x12 x14)) ⟶ (∀ x14 x15 x16 . x0 x14 ⟶ x0 x15 ⟶ x1 x14 x15 x16 ⟶ x7 (x8 x14) (x10 x14) (x10 x15) (x11 x14 x15 x16) (x12 x14) = x7 (x8 x14) (x8 x15) (x10 x15) (x12 x15) (x9 x14 x15 x16)) ⟶ x13) ⟶ x13 (proof)
Definition MetaNatTrans_buggy_strict := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 : ι → ο . λ x5 : ι → ι → ι → ο . λ x6 : ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 : ι → ι . λ x9 : ι → ι → ι → ι . λ x10 : ι → ι . λ x11 : ι → ι → ι → ι . λ x12 : ι → ι . and (and (and (and (MetaCat x0 x1 x2 x3) (MetaCat x4 x5 x6 x7)) (MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) (MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x10 x11)) (MetaNatTrans_buggy x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
Known and5I^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Theorem 793b1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . MetaCat x0 x1 x2 x3 ⟶ MetaCat x4 x5 x6 x7 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x10 x11 ⟶ MetaNatTrans_buggy x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ MetaNatTrans_buggy_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 (proof)
Known and5E^and5E : ∀ x0 x1 x2 x3 x4 : ο . and (and (and (and x0 x1) x2) x3) x4 ⟶ ∀ x5 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5) ⟶ x5
Theorem 7f6e5.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . ∀ x4 : ι → ο . ∀ x5 : ι → ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 : ι → ι . ∀ x9 : ι → ι → ι → ι . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ι → ι . ∀ x12 : ι → ι . MetaNatTrans_buggy_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ ∀ x13 : ο . (MetaCat x0 x1 x2 x3 ⟶ MetaCat x4 x5 x6 x7 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x10 x11 ⟶ MetaNatTrans_buggy x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ x13) ⟶ x13 (proof)
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Param lam^Sigma : ι → (ι → ι) → ι
Definition lam_id^lam_id := λ x0 . lam x0 (λ x1 . x1)
Param ap^ap : ι → ι → ι
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
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)
Known 047c9..^MetaCat_I : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaFunctor_prop1 x0 x1 x2 x3 ⟶ MetaFunctor_prop2 x0 x1 x2 x3 ⟶ (∀ x4 x5 x6 . x0 x4 ⟶ x0 x5 ⟶ x1 x4 x5 x6 ⟶ x3 x4 x4 x5 x6 (x2 x4) = x6) ⟶ (∀ x4 x5 x6 . x0 x4 ⟶ x0 x5 ⟶ x1 x4 x5 x6 ⟶ x3 x4 x5 x5 (x2 x5) x6 = x6) ⟶ (∀ 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)) ⟶ MetaCat x0 x1 x2 x3
Known lam_comp_id_R^{lam_comp_id_R} : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ lam_comp x0 x2 (lam_id x0) = x2
Known lam_comp_id_L^{lam_comp_id_L} : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ lam_comp x0 (lam_id x1) x2 = x2
Known lam_comp_assoc^{lam_comp_assoc} : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ ∀ x3 x4 . lam_comp x0 x4 (lam_comp x0 x3 x2) = lam_comp x0 (lam_comp x1 x4 x3) x2
Theorem 081b4..^{MetaCatConcrete} : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ο . (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x2 x3 x4 x5 ⟶ x5 ∈ setexp (x1 x4) (x1 x3)) ⟶ (∀ x3 . x0 x3 ⟶ x2 x3 x3 (lam_id (x1 x3))) ⟶ (∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 x4 x6 ⟶ x2 x4 x5 x7 ⟶ x2 x3 x5 (lam_comp (x1 x3) x7 x6)) ⟶ MetaCat x0 x2 (λ x3 . lam_id (x1 x3)) (λ x3 x4 x5 . lam_comp (x1 x3)) (proof)
Definition True^True := ∀ x0 : ο . x0 ⟶ x0
Definition HomSet^SetHom := λ x0 x1 x2 . x2 ∈ setexp x1 x0
Known TrueI^TrueI : True
Theorem b606c..^{MetaCatConcreteForgetful} : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ο . (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x2 x3 x4 x5 ⟶ x5 ∈ setexp (x1 x4) (x1 x3)) ⟶ MetaFunctor x0 x2 (λ x3 . lam_id (x1 x3)) (λ x3 x4 x5 . lam_comp (x1 x3)) (λ x3 . True) HomSet lam_id (λ x3 x4 x5 . lam_comp x3) x1 (λ x3 x4 x5 . x5) (proof)
Known lam_id_exp_In^{lam_id_exp_In} : ∀ x0 . lam_id x0 ∈ setexp x0 x0
Known lam_comp_exp_In^{lam_comp_exp_In} : ∀ x0 x1 x2 x3 . x3 ∈ setexp x1 x0 ⟶ ∀ x4 . x4 ∈ setexp x2 x1 ⟶ lam_comp x0 x4 x3 ∈ setexp x2 x0
Theorem e4125..^MetaCatSet : MetaCat (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (proof)
Theorem 2fb6a..^MetaCatHFSet : MetaCat (λ x0 . x0 ∈ prim6 0) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (proof)
Theorem 68978..^{MetaCatSmallSet} : MetaCat (λ x0 . x0 ∈ prim6 (prim6 0)) HomSet lam_id (λ x0 x1 x2 . lam_comp x0) (proof)
Theorem ec1a3..^{MetaCatConcreteForgetful_strict} : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ο . (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x2 x3 x4 x5 ⟶ x5 ∈ setexp (x1 x4) (x1 x3)) ⟶ (∀ x3 . x0 x3 ⟶ x2 x3 x3 (lam_id (x1 x3))) ⟶ (∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 x4 x6 ⟶ x2 x4 x5 x7 ⟶ x2 x3 x5 (lam_comp (x1 x3) x7 x6)) ⟶ MetaFunctor_strict x0 x2 (λ x3 . lam_id (x1 x3)) (λ x3 x4 x5 . lam_comp (x1 x3)) (λ x3 . True) HomSet lam_id (λ x3 x4 x5 . lam_comp x3) x1 (λ x3 x4 x5 . x5) (proof)
Param unpack_e_o^unpack_e_o : ι → (ι → ι → ο) → ο
Definition PtdSetHom^Hom_struct_e := λ x0 x1 x2 . unpack_e_o x0 (λ x3 x4 . unpack_e_o x1 (λ x5 x6 . and (x2 ∈ setexp x5 x3) (ap x2 x4 = x6)))
Param unpack_u_o^unpack_u_o : ι → (ι → (ι → ι) → ο) → ο
Definition UnaryFuncHom^Hom_struct_u := λ x0 x1 x2 . unpack_u_o x0 (λ x3 . λ x4 : ι → ι . unpack_u_o x1 (λ x5 . λ x6 : ι → ι . and (x2 ∈ setexp x5 x3) (∀ x7 . x7 ∈ x3 ⟶ ap x2 (x4 x7) = x6 (ap x2 x7))))
Param unpack_b_o^unpack_b_o : ι → (ι → (ι → ι → ι) → ο) → ο
Definition MagmaHom^Hom_struct_b := λ x0 x1 x2 . unpack_b_o x0 (λ x3 . λ x4 : ι → ι → ι . unpack_b_o x1 (λ x5 . λ x6 : ι → ι → ι . and (x2 ∈ setexp x5 x3) (∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ ap x2 (x4 x7 x8) = x6 (ap x2 x7) (ap x2 x8))))
Param unpack_p_o^unpack_p_o : ι → (ι → (ι → ο) → ο) → ο
Definition UnaryPredHom^Hom_struct_p := λ x0 x1 x2 . unpack_p_o x0 (λ x3 . λ x4 : ι → ο . unpack_p_o x1 (λ x5 . λ x6 : ι → ο . and (x2 ∈ setexp x5 x3) (∀ x7 . x7 ∈ x3 ⟶ x4 x7 ⟶ x6 (ap x2 x7))))
Param unpack_r_o^unpack_r_o : ι → (ι → (ι → ι → ο) → ο) → ο
Definition BinRelnHom^Hom_struct_r := λ x0 x1 x2 . unpack_r_o x0 (λ x3 . λ x4 : ι → ι → ο . unpack_r_o x1 (λ x5 . λ x6 : ι → ι → ο . and (x2 ∈ setexp x5 x3) (∀ x7 . x7 ∈ x3 ⟶ ∀ x8 . x8 ∈ x3 ⟶ x4 x7 x8 ⟶ x6 (ap x2 x7) (ap x2 x8))))
Param unpack_c_o^unpack_c_o : ι → (ι → ((ι → ο) → ο) → ο) → ο
Definition PreContinuousHom^Hom_struct_c := λ x0 x1 x2 . unpack_c_o x0 (λ x3 . λ x4 : (ι → ο) → ο . unpack_c_o x1 (λ x5 . λ x6 : (ι → ο) → ο . and (x2 ∈ setexp x5 x3) (∀ x7 : ι → ο . (∀ x8 . x7 x8 ⟶ x8 ∈ x5) ⟶ x6 x7 ⟶ x4 (λ x8 . and (x8 ∈ x3) (x7 (ap x2 x8))))))
Param unpack_b_b_e_o^{unpack_b_b_e_o} : ι → (ι → (ι → ι → ι) → (ι → ι → ι) → ι → ο) → ο
Definition Hom_b_b_e^{Hom_struct_b_b_e} := λ x0 x1 x2 . unpack_b_b_e_o x0 (λ x3 . λ x4 x5 : ι → ι → ι . λ x6 . unpack_b_b_e_o x1 (λ x7 . λ x8 x9 : ι → ι → ι . λ x10 . and (and (and (x2 ∈ setexp x7 x3) (∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ap x2 (x4 x11 x12) = x8 (ap x2 x11) (ap x2 x12))) (∀ x11 . x11 ∈ x3 ⟶ ∀ x12 . x12 ∈ x3 ⟶ ap x2 (x5 x11 x12) = x9 (ap x2 x11) (ap x2 x12))) (ap x2 x6 = x10)))
Param unpack_b_b_e_e_o^{unpack_b_b_e_e_o} : ι → (ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ο) → ο
Definition Hom_b_b_e_e^{Hom_struct_b_b_e_e} := λ x0 x1 x2 . unpack_b_b_e_e_o x0 (λ x3 . λ x4 x5 : ι → ι → ι . λ x6 x7 . unpack_b_b_e_e_o x1 (λ x8 . λ x9 x10 : ι → ι → ι . λ x11 x12 . and (and (and (and (x2 ∈ setexp x8 x3) (∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ap x2 (x4 x13 x14) = x9 (ap x2 x13) (ap x2 x14))) (∀ x13 . x13 ∈ x3 ⟶ ∀ x14 . x14 ∈ x3 ⟶ ap x2 (x5 x13 x14) = x10 (ap x2 x13) (ap x2 x14))) (ap x2 x6 = x11)) (ap x2 x7 = x12)))
Param unpack_b_b_r_e_e_o^{unpack_b_b_r_e_e_o} : ι → (ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι → ι → ο) → ο
Definition Hom_b_b_r_e_e^{Hom_struct_b_b_r_e_e} := λ x0 x1 x2 . unpack_b_b_r_e_e_o x0 (λ x3 . λ x4 x5 : ι → ι → ι . λ x6 : ι → ι → ο . λ x7 x8 . unpack_b_b_r_e_e_o x1 (λ x9 . λ x10 x11 : ι → ι → ι . λ x12 : ι → ι → ο . λ x13 x14 . and (and (and (and (and (x2 ∈ setexp x9 x3) (∀ x15 . x15 ∈ x3 ⟶ ∀ x16 . x16 ∈ x3 ⟶ ap x2 (x4 x15 x16) = x10 (ap x2 x15) (ap x2 x16))) (∀ x15 . x15 ∈ x3 ⟶ ∀ x16 . x16 ∈ x3 ⟶ ap x2 (x5 x15 x16) = x11 (ap x2 x15) (ap x2 x16))) (∀ x15 . x15 ∈ x3 ⟶ ∀ x16 . x16 ∈ x3 ⟶ x6 x15 x16 ⟶ x12 (ap x2 x15) (ap x2 x16))) (ap x2 x7 = x13)) (ap x2 x8 = x14)))
Param pack_e^pack_e : ι → ι → ι
Known unpack_e_o_eq^{unpack_e_o_eq} : ∀ x0 : ι → ι → ο . ∀ x1 x2 . unpack_e_o (pack_e x1 x2) x0 = x0 x1 x2
Theorem f65a3..^{Hom_struct_e_pack} : ∀ x0 x1 x2 x3 x4 . PtdSetHom (pack_e x0 x2) (pack_e x1 x3) x4 = and (x4 ∈ setexp x1 x0) (ap x4 x2 = x3) (proof)
Param pack_u^pack_u : ι → (ι → ι) → ι
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 ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Theorem 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)) (proof)
Param pack_b^pack_b : ι → CT2 ι
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
Theorem 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)) (proof)
Param pack_p^pack_p : ι → (ι → ο) → ι
Param iff^iff : ο → ο → ο
Known unpack_p_o_eq^{unpack_p_o_eq} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ο . (∀ x3 : ι → ο . (∀ x4 . x4 ∈ x1 ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_p_o (pack_p x1 x2) x0 = x0 x1 x2
Known iffEL^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1
Known iffER^iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0
Theorem 55fb5..^{Hom_struct_p_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 . UnaryPredHom (pack_p x0 x2) (pack_p x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ x2 x6 ⟶ x3 (ap x4 x6)) (proof)
Param pack_r^pack_r : ι → (ι → ι → ο) → ι
Known unpack_r_o_eq^{unpack_r_o_eq} : ∀ x0 : ι → (ι → ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_r_o (pack_r x1 x2) x0 = x0 x1 x2
Theorem c84ab..^{Hom_struct_r_pack} : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . BinRelnHom (pack_r x0 x2) (pack_r x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x2 x6 x7 ⟶ x3 (ap x4 x6) (ap x4 x7)) (proof)
Param pack_c^pack_c : ι → ((ι → ο) → ο) → ι
Known unpack_c_o_eq^{unpack_c_o_eq} : ∀ x0 : ι → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ x5 ∈ x1) ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ unpack_c_o (pack_c x1 x2) x0 = x0 x1 x2
Known andEL^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Theorem 5059f..^{Hom_struct_c_pack} : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 . PreContinuousHom (pack_c x0 x2) (pack_c x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ x7 ∈ x1) ⟶ x3 x6 ⟶ x2 (λ x7 . and (x7 ∈ x0) (x6 (ap x4 x7)))) (proof)
Param pack_b_b_e^pack_b_b_e : ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι
Known unpack_b_b_e_o_eq^{unpack_b_b_e_o_eq} : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 . (∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4) ⟶ unpack_b_b_e_o (pack_b_b_e x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4
Theorem 024cd..^{Hom_struct_b_b_e_pack} : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 x8 . Hom_b_b_e (pack_b_b_e x0 x2 x3 x6) (pack_b_b_e x1 x4 x5 x7) x8 = and (and (and (x8 ∈ setexp x1 x0) (∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ap x8 (x2 x10 x11) = x4 (ap x8 x10) (ap x8 x11))) (∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ap x8 (x3 x10 x11) = x5 (ap x8 x10) (ap x8 x11))) (ap x8 x6 = x7) (proof)
Param pack_b_b_e_e^pack_b_b_e_e : ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι
Known unpack_b_b_e_e_o_eq^{unpack_b_b_e_e_o_eq} : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 . (∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ unpack_b_b_e_e_o (pack_b_b_e_e x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5
Theorem 4ba5a..^{Hom_struct_b_b_e_e_pack} : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 x8 x9 x10 . Hom_b_b_e_e (pack_b_b_e_e x0 x2 x3 x6 x7) (pack_b_b_e_e x1 x4 x5 x8 x9) x10 = and (and (and (and (x10 ∈ setexp x1 x0) (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ap x10 (x2 x12 x13) = x4 (ap x10 x12) (ap x10 x13))) (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ap x10 (x3 x12 x13) = x5 (ap x10 x12) (ap x10 x13))) (ap x10 x6 = x8)) (ap x10 x7 = x9) (proof)
Param pack_b_b_r_e_e^{pack_b_b_r_e_e} : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι → ι → ι
Known unpack_b_b_r_e_e_o_eq^{unpack_b_b_r_e_e_o_eq} : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 x6 . (∀ x7 : ι → ι → ι . (∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ x2 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ x3 x9 x10 = x8 x9 x10) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ iff (x4 x10 x11) (x9 x10 x11)) ⟶ x0 x1 x7 x8 x9 x5 x6 = x0 x1 x2 x3 x4 x5 x6) ⟶ unpack_b_b_r_e_e_o (pack_b_b_r_e_e x1 x2 x3 x4 x5 x6) x0 = x0 x1 x2 x3 x4 x5 x6
Known and6E^and6E : ∀ x0 x1 x2 x3 x4 x5 : ο . and (and (and (and (and x0 x1) x2) x3) x4) x5 ⟶ ∀ x6 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6) ⟶ x6
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 3e8fc..^{Hom_struct_b_b_r_e_e_pack} : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι → ο . ∀ x8 x9 x10 x11 x12 . Hom_b_b_r_e_e (pack_b_b_r_e_e x0 x2 x3 x6 x8 x9) (pack_b_b_r_e_e x1 x4 x5 x7 x10 x11) x12 = and (and (and (and (and (x12 ∈ setexp x1 x0) (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ap x12 (x2 x14 x15) = x4 (ap x12 x14) (ap x12 x15))) (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ap x12 (x3 x14 x15) = x5 (ap x12 x14) (ap x12 x15))) (∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ x6 x14 x15 ⟶ x7 (ap x12 x14) (ap x12 x15))) (ap x12 x8 = x10)) (ap x12 x9 = x11) (proof)
Definition struct_e^struct_e := λ x0 . ∀ x1 : ι → ο . (∀ x2 x3 . x3 ∈ x2 ⟶ x1 (pack_e x2 x3)) ⟶ x1 x0
Known pack_e_0_eq2^pack_e_0_eq2 : ∀ x0 x1 . x0 = ap (pack_e x0 x1) 0
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Theorem 1c0e1..^{MetaCat_struct_e_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_e x1) ⟶ MetaCat x0 PtdSetHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (proof)
Theorem 0f4ef..^{MetaCat_struct_e_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_e x1) ⟶ MetaFunctor x0 PtdSetHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3) (proof)
Definition struct_p^struct_p := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . x1 (pack_p x2 x3)) ⟶ x1 x0
Known pack_p_0_eq2^pack_p_0_eq2 : ∀ x0 . ∀ x1 : ι → ο . x0 = ap (pack_p x0 x1) 0
Theorem 5387a..^{MetaCat_struct_p_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_p x1) ⟶ MetaCat x0 UnaryPredHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (proof)
Theorem 57ba0..^{MetaCat_struct_p_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_p x1) ⟶ MetaFunctor x0 UnaryPredHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3) (proof)
Definition struct_r^struct_r := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . x1 (pack_r x2 x3)) ⟶ x1 x0
Known pack_r_0_eq2^pack_r_0_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ο . x2 x0 (ap (pack_r x0 x1) 0) ⟶ x2 (ap (pack_r x0 x1) 0) x0
Theorem 62658..^{MetaCat_struct_r_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_r x1) ⟶ MetaCat x0 BinRelnHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (proof)
Theorem 45945..^{MetaCat_struct_r_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_r x1) ⟶ MetaFunctor x0 BinRelnHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3) (proof)
Definition struct_u^struct_u := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . x4 ∈ x2 ⟶ x3 x4 ∈ x2) ⟶ x1 (pack_u x2 x3)) ⟶ x1 x0
Known pack_u_0_eq2^pack_u_0_eq2 : ∀ x0 . ∀ x1 : ι → ι . x0 = ap (pack_u x0 x1) 0
Theorem 7ce95..^{MetaCat_struct_u_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_u x1) ⟶ MetaCat x0 UnaryFuncHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (proof)
Theorem 6eadb..^{MetaCat_struct_u_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_u x1) ⟶ MetaFunctor x0 UnaryFuncHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3) (proof)
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
Known pack_b_0_eq2^pack_b_0_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . x0 = ap (pack_b x0 x1) 0
Theorem 125f1..^{MetaCat_struct_b_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b x1) ⟶ MetaCat x0 MagmaHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (proof)
Theorem 79957..^{MetaCat_struct_b_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b x1) ⟶ MetaFunctor x0 MagmaHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3) (proof)
Definition struct_c^struct_c := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . x1 (pack_c x2 x3)) ⟶ x1 x0
Known pack_c_0_eq2^pack_c_0_eq2 : ∀ x0 . ∀ x1 : (ι → ο) → ο . x0 = ap (pack_c x0 x1) 0
Known pred_ext_2^pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Theorem dd75c..^{MetaCat_struct_c_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_c x1) ⟶ MetaCat x0 PreContinuousHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (proof)
Theorem 58a40..^{MetaCat_struct_c_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_c x1) ⟶ MetaFunctor x0 PreContinuousHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3) (proof)
Definition struct_b_b_e^struct_b_b_e := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x4 x5 x6 ∈ x2) ⟶ ∀ x5 . x5 ∈ x2 ⟶ x1 (pack_b_b_e x2 x3 x4 x5)) ⟶ x1 x0
Known pack_b_b_e_0_eq2^{pack_b_b_e_0_eq2} : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 . x0 = ap (pack_b_b_e x0 x1 x2 x3) 0
Theorem 5f5c5..^{MetaCat_struct_b_b_e_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_e x1) ⟶ MetaCat x0 Hom_b_b_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (proof)
Theorem 9c6b9..^{MetaCat_struct_b_b_e_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_e x1) ⟶ MetaFunctor x0 Hom_b_b_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3) (proof)
Definition struct_b_b_e_e^{struct_b_b_e_e} := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x4 x5 x6 ∈ x2) ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x1 (pack_b_b_e_e x2 x3 x4 x5 x6)) ⟶ x1 x0
Known pack_b_b_e_e_0_eq2^{pack_b_b_e_e_0_eq2} : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 . x0 = ap (pack_b_b_e_e x0 x1 x2 x3 x4) 0
Theorem 936d9..^{MetaCat_struct_b_b_e_e_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_e_e x1) ⟶ MetaCat x0 Hom_b_b_e_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (proof)
Theorem 72690..^{MetaCat_struct_b_b_e_e_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_e_e x1) ⟶ MetaFunctor x0 Hom_b_b_e_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3) (proof)
Definition struct_b_b_r_e_e^{struct_b_b_r_e_e} := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x4 x5 x6 ∈ x2) ⟶ ∀ x5 : ι → ι → ο . ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x2 ⟶ x1 (pack_b_b_r_e_e x2 x3 x4 x5 x6 x7)) ⟶ x1 x0
Known pack_b_b_r_e_e_0_eq2^{pack_b_b_r_e_e_0_eq2} : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x0 = ap (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) 0
Theorem dc6cf..^{MetaCat_struct_b_b_r_e_e_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_r_e_e x1) ⟶ MetaCat x0 Hom_b_b_r_e_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (proof)
Theorem 49006..^{MetaCat_struct_b_b_r_e_e_Forgetful_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_r_e_e x1) ⟶ MetaFunctor x0 Hom_b_b_r_e_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0)) (λ x1 . True) HomSet lam_id (λ x1 x2 x3 . lam_comp x1) (λ x1 . ap x1 0) (λ x1 x2 x3 . x3) (proof)